Transforming formal proof into sound deduction (rewritten)

[PeteOlcott]

If you want to assume that Truth pertains to rattlesnakes (or anything else)
feel free yet not in the thread. The sound deductive inference model
eliminates incompleteness and inconsistency from formal systems. That
is not an assumption it is provable.

OK, but incompleteness and inconsistency are removed only IF your axioms are accepted.

The question "Should I accept those axioms?" is a decision problem.

The answer is "Yes. You should accept the axioms IF you want to eliminate incompleteness and inconsistency within your system'"

But that is a long-winded way to argue for the Coherence theory of truth

Not nearly as long winded as the 1931 Incompleteness Theorem that is refuted.

[A_Seagull]

Stipulating this definition of Axiom:
An expression of language defined to have the semantic value of Boolean True.

Stipulating this specification of True and False:
(1) True(F, x) ↔ (F ⊢ x).
(2) False(F, x) ↔ (F ⊢ ¬x).

Then formal proofs to theorem consequences specify sound deduction.

In sound deductive inference an argument is unsound unless there
is a connected chain of deductive inference steps from true premises
to a true conclusion.

Applying the law of the excluded middle (P ∨ ¬P) to the above we derive:
(3) Sound(F, x) ↔ (True(F, x) ∨ False(F, x)).

When we transform formal proof to theorem consequences into the
sound deductive inference model then truth and provability can
no longer diverge. Any closed WFF that was previously undecidable
is decided to be unsound.

I don't think you need all those references to true or truth. They are surplus to requirements.

If you have a connected chain of deductive inference from the axioms to the conclusion then your case is proven, albeit only within that axiomatic system.

What has not been proven within that system cannot be clamed to be proven within that system.

Within the above stipulations the following logic sentence:
∃F∃G (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))
(1) Asserts there exists expressions G of formal system F that are neither true nor false.
(2) Is decided to be false on the basis of Axiom(3).

Making the following paragraph false:
The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried
out, there are statements of the language of F which can neither be
proved nor disproved in F. (Raatikainen 2018)

The incompleteness theorem proves that given the assumption of completeness a logical inconsistency arises.
Conclusion: Such formal axiomatic systems are not complete.
Therefore there is no need to infer that some statements of the system can neither be proved or disproved as it cannot be established that those statements are indeed part of the system.

[PeteOlcott]

I don't think you need all those references to true or truth. They are surplus to requirements.

If you have a connected chain of deductive inference from the axioms to the conclusion then your case is proven, albeit only within that axiomatic system.

What has not been proven within that system cannot be clamed to be proven within that system.

Within the above stipulations the following logic sentence:
∃F∃G (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))
(1) Asserts there exists expressions G of formal system F that are neither true nor false.
(2) Is decided to be false on the basis of Axiom(3).

Making the following paragraph false:
The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried
out, there are statements of the language of F which can neither be
proved nor disproved in F. (Raatikainen 2018)

The incompleteness theorem proves that given the assumption of completeness a logical inconsistency arises.
Conclusion: Such formal axiomatic systems are not complete.
Therefore there is no need to infer that some statements of the system can neither be proved or disproved as it cannot be established that those statements are indeed part of the system.

I just proved otherwise but you have to actually carefully study what I rewrote.
My ideas were very messy until I finally pulled them all together yesterday.
The first post in this thread now has my latest ideas.

[PeteOlcott]

I just added the part that refutes Incompleteness.

[A_Seagull]

I just added the part that refutes Incompleteness.

How can you determine whether any statement S is within the formal system F or not within the formal system?

[PeteOlcott]

Stipulating this definition of Axiom:
An expression of language defined to have the semantic value of Boolean True.

Stipulating this specification of True and False:
Axiom(1) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) True(F, x) ↔ ((F ⊢ x)).
Axiom(2) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (False(F, x) ↔ (F ⊢ ¬x)).

Stipulating that formal systems are Boolean:
Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))

Within the above stipulations formal proofs to theorem consequences
now express the sound deductive inference model eliminating incompleteness,
undecidability and inconsistency from the notion of formal systems.

The following logic sentence is refuted on the basis of Axiom(3)
∃F∃G (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))
Because it asserts there are sentences G of formal system F that are not true or false.

Making the following paragraph false:
The first incompleteness theorem states that in any consistent formal system F
within which a certain amount of arithmetic can be carried out, there are statements
of the language of F which can neither be proved nor disproved in F. (Raatikainen 2018)

[PeteOlcott]

I just added the part that refutes Incompleteness.

How can you determine whether any statement S is within the formal system F or not within the formal system?

Stipulating this specification of True and False:
Axiom(1) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) True(F, x) ↔ ((F ⊢ x)).
Axiom(2) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (False(F, x) ↔ (F ⊢ ¬x)).

Stipulating that formal systems are Boolean:
Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))

That was great feedback, I didn't realize that my short-hand was confusing.
S is either defined to be a part of F or it is not a part of F.

[wtf]

Stipulating that formal systems are Boolean:
Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))

How can a wff have a truth value without a model?

In fact Wikipedia is in on THIS conspiracy as well. Here's what they have to say about WFFs:

A formula is a syntactic object that can be given a semantic meaning by means of an interpretation.


https://en.wikipedia.org/wiki/Well-formed_formula

Is this what you deny? You say that given a WFF we can look at it and know if it's true or false just by looking at it? How can that be?

Can you explain this in English? Just give me the overview of your thinking. Is that Wiki quote wrong?

[PeteOlcott]

Stipulating that formal systems are Boolean:
Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))

How can a wff have a truth value without a model?

https://en.wikipedia.org/wiki/Stipulative_definition
A stipulative definition is a type of definition in which a new or currently-existing
term is given a new specific meaning for the purposes of argument or discussion
in a given context.

I reformulate the notion of formal system such that it can directly express
the semantic value of true by making this stipulation:

Stipulating this definition of Axiom:
An expression of language defined to have the semantic value of Boolean True.

This is a mandatory requirement of converting formal systems to conform
to the sound deductive inference model.

[Logik]

https://en.wikipedia.org/wiki/Stipulative_definition
A stipulative definition is a type of definition in which a new or currently-existing
term is given a new specific meaning for the purposes of argument or discussion
in a given context.

You left out some very important details from the very page you quoted.

1. a stipulative definition cannot be "correct" or "incorrect". it can only differ from other definitions,
2. it can be useful for its intended purpose.

What is your intended purpose for defining an "axiom", Pete?
Why are you trying to make formal systems to "conform to the sound deductive inference model"?

[PeteOlcott]

https://en.wikipedia.org/wiki/Stipulative_definition
A stipulative definition is a type of definition in which a new or currently-existing
term is given a new specific meaning for the purposes of argument or discussion
in a given context.

You left out some very important details from the very page you quoted.

1. a stipulative definition cannot be "correct" or "incorrect". it can only differ from other definitions,
2. it can be useful for its intended purpose.

What is your intended purpose for defining an "axiom", Pete?
Why are you trying to make formal systems to "conform to the sound deductive inference model"?

This eliminates incompleteness, undecidability and inconsistency from formal systems.

[Logik]

This eliminates incompleteness, undecidability and inconsistency from formal systems.

It also eliminates their expressive power and removes meaning.

[PeteOlcott]

This eliminates incompleteness, undecidability and inconsistency from formal systems.

It also eliminates their expressive power and removes meaning.

Maybe to someone that fails to understand this is semantically impossible: True ↔ False

Conventional Sound Deductive Inference: A conclusion is only true when it is provable**
on the basis of true premises. Symbolic logic diverged from this correct model of truth,
thus symbolic logic erred.

**a connected sequence of valid deductions from premises to conclusion

[Logik]

Maybe to someone that fails to understand this is semantically impossible: True ↔ False

Perhaps you fail to understand? There are no semantic impossibilities.

It's called imagination.

The expression: True ↔ False is meaningless without interpretation.

[PeteOlcott]

Maybe to someone that fails to understand this is semantically impossible: True ↔ False

Perhaps you fail to understand? There are no semantic impossibilities.

It's called imagination.

The expression: True ↔ False is meaningless without interpretation.

That is one way of looking at it.

Alternatively an algorithm could specify its semantic meaning in terms of a set
of connected relations.