Refuting Incompleteness and Undefinability

[Speakpigeon]

So the question is whether any one of these methods is the one and only one which is correct. Up until such a day as we can decide which method is correct, if even there is one, grandiose claims about formal logic can be dismissed out of hand.

Observe that you have simply moved the problem elsewhere.

No, this has been the same problem from day one and it ain't gonna move.

In what formal system would you arbitrate the "correctness" or "incorrectness" of your methodology? What is the objective standard for "correctness" ?

This has been the problem from day one, 2,500 years ago. Still there.

Science uses predictive utility as arbiter.

Well, as I already explained, it's not a few hundred years of science that will likely equate the 525-million-years logic of the human brain.
Still, when you don't know what to do, you still do something and then you may just as well do something that seems useful to you. I'm not going to try and stop you.
EB

[Logik]

So the question is whether any one of these methods is the one and only one which is correct. Up until such a day as we can decide which method is correct, if even there is one, grandiose claims about formal logic can be dismissed out of hand.

Observe that you have simply moved the problem elsewhere.

No, this has been the same problem from day one and it ain't gonna move.

In what formal system would you arbitrate the "correctness" or "incorrectness" of your methodology? What is the objective standard for "correctness" ?

This has been the problem from day one, 2,500 years ago. Still there.

Science uses predictive utility as arbiter.

Well, as I already explained, it's not a few hundred years of science that will likely equate the 525-million-years logic of the human brain.
Still, when you don't know what to do, you still do something and then you may just as well do something that seems useful to you. I'm not going to try and stop you.
EB

I know that. You are saying dumb shit like "So the question is whether any one of these methods is the one and only one which is correct" it appears that you don't. Because that's not THE question. THE question is: "What is THE objective framework which decides correct/incorrect?"

As epistemologists call them: the problems of criterion AND justification.

The point is - but are unsolved. Hence Munchhausen trillema.

Foundationalists pretend to have solved it.

Religions bunch - the lot of them...

[PeteOlcott]

As I see it, we can make any number of formal methods and, obviously, true formulas will depend on the kind of proof method used.
So the question is whether any one of these methods is the one and only one which is correct. Up until such a day as we can decide which method is correct, if even there is one, grandiose claims about formal logic can be dismissed out of hand.
EB

When-so-ever a formal proof is specified to a theorem consequence this means that this
proof has an empty set of premises. When a formal proof has an empty set of premises
this is the same thing as saying that its axioms are its premises. When these axioms are
defined to be true, then the formal proof has the same basis as sound deduction.

If a formal prove uses the same rules-of-inference as valid deduction then this proof
specifies the same thing as deduction, as (R. B. Braithwaite 1962) agrees:

The chain of symbolic manipulations in the calculus corresponds to and represents the chain
of deductions in the deductive system. (R. B. Braithwaite 1962: 2)

Axioms are defined to be true
The elementary statements which belong to T are called the elementary theorems of T
and said to be true. In this way, a theory is a way of designating a subset of E which consists
entirely of true statements. (Haskell Curry 2010).

Then formal proofs (having an empty set of premises) to consequences can be construed
as directly representing sound deductive inference because the truth value of the axioms
is propagated to the theorem consequences.

This allows us to interpret this symbolic logic expression: ∀x True(x) ↔ ⊢ x as specifying
sound deductive inference as formal proofs to theorem consequences.

[Speakpigeon]

When-so-ever a formal proof is specified to a theorem consequence this means that this proof has an empty set of premises. When a formal proof has an empty set of premises this is the same thing as saying that its axioms are its premises. When these axioms are defined to be true, then the formal proof has the same basis as sound deduction.
If a formal prove uses the same rules-of-inference as valid deduction then this proof specifies the same thing as deduction, as (R. B. Braithwaite 1962) agrees: The chain of symbolic manipulations in the calculus corresponds to and represents the chain of deductions in the deductive system. (R. B. Braithwaite 1962: 2)
Axioms are defined to be true
The elementary statements which belong to T are called the elementary theorems of T and said to be true. In this way, a theory is a way of designating a subset of E which consists entirely of true statements. (Haskell Curry 2010).
Then formal proofs (having an empty set of premises) to consequences can be construed as directly representing sound deductive inference because the truth value of the axioms is propagated to the theorem consequences.
This allows us to interpret this symbolic logic expression: ∀x True(x) ↔ ⊢ x as specifying sound deductive inference as formal proofs to theorem consequences.

I agree with you that Tarski got it wrong, but logic doesn't care about truth or about what's true. Logic would work the same for any two-valued syntax, say black and white, hot and cold, empty and full. Logic is not about truth, it is about inference (or consequence, validity, etc.). There's been a shift in this respect and most philosophers and mathematicians seems now to have understood this point.
So logic is essentially the business of correctly inferring the truth of a proposition from another proposition assumed true. So truth is whatever goes through the pipeline. Could be truth, could be whiteness, could be heat, could fullness, as long as it is preserved in the process.
A formal method of logic has therefore to specify a method of inference that is somehow correct. Aristotle provided a first example of inference. The scholastic specified a method of proof. Leibniz conceived of the mathematisation of logic. Russell offered a calculus. Gentzen reinvented natural deduction. Now there are I don't know how many methods of logic. But we still don't know how to specify a method of inference that would be correct.
EB

[PeteOlcott]

I agree with you that Tarski got it wrong, but logic doesn't care about truth or about what's true. Logic would work the same for any two-valued syntax, say black and white, hot and cold, empty and full. Logic is not about truth, it is about inference (or consequence, validity, etc.). There's been a shift in this respect and most philosophers and mathematicians seems now to have understood this point.
So logic is essentially the business of correctly inferring the truth of a proposition from another proposition assumed true. So truth is whatever goes through the pipeline. Could be truth, could be whiteness, could be heat, could fullness, as long as it is preserved in the process.
A formal method of logic has therefore to specify a method of inference that is somehow correct. Aristotle provided a first example of inference. The scholastic specified a method of proof. Leibniz conceived of the mathematisation of logic. Russell offered a calculus. Gentzen reinvented natural deduction. Now there are I don't know how many methods of logic. But we still don't know how to specify a method of inference that would be correct.
EB

And when Tarski and Goedel concluded that there are some expressions of language
that are true but not provable they did so incorrectly because their model of truth was broken.

[Arising_uk]

... the 525-million-years logic of the human brain. ...

Eh!?

[PeteOlcott]

Can this: ∃F∃G(G ↔ ~(F ⊢ G)) be shown to be satisfiable without Gödel numbers ?

[Logik]

Can this: ∃F∃G(G ↔ ~(F ⊢ G)) be shown to be satisfiable without Gödel numbers ?

If you are talking about Godel numbers then you are necessarily looking for a symbolic, not numeric satisfiability.

Godel is isomorphic to Turing. Let Godel sleep. Further - Curry-Howard isomorphism tells us that a "proof" is a working computer program. An algorithm so...

Strategy 1:
LHS ↔ RHS ↔ True
G ↔ True
F ⊢ G ↔ False

Strategy 2:
LHS ↔ RHS ↔ False
G ↔ False
F ⊢ G ↔ True

If you define "⊢" in a regular language for us ( https://en.wikipedia.org/wiki/Regular_language )
Then we can simply resort to any SAT algorithm:

https://en.wikipedia.org/wiki/Boolean_s ... ty_problem

[Speakpigeon]

And when Tarski and Goedel concluded that there are some expressions of language that are true but not provable they did so incorrectly because their model of truth was broken.

Yes, but there's a distinction between different kinds of proofs. A logical proof isn't an empirical proof. I won't use logic to decide that it is true that I am in pain. I just bloody know it's true I am in pain whenever I am in pain. Science does use logical proofs to ascertain the truth of theoretical results. However, broadly, a scientific theory will claim that a result is true just because the theory proves this result as conclusion of a logically valid inference "if observation is true, then result is true". A valid inference merely preserves the truth of the observation in the truth of the conclusion.
So, an expression is provable in logic if it can be deduced from another expression already assumed true, irrespective of whether it is actually true. Anything else is pie in the sky and so we have to decide for ourselves whether to accept particular expressions as true premises and that's not a logical problem.
Still, as I see it, mathematical logic isn't logic proper. Rather, it's an extension or an application of logic to mathematics. It is the discipline where mathematicians try to develop theoretical tools to more conveniently prove theorems. I suspect that Tarski and Gödel say something true nonetheless. As I understand it, mathematicians have thought they should be able to infer the whole of mathematics from logic alone. They came to believe that because they didn't understand what is logic. They don't understand it because most people don't and first among them, Aristotle. He started the confusion. He definitely single-handedly created formal logic nearly from scratch but he also focused on a narrow restriction of logic to particular syllogistic forms. And this is precisely what is 1st order logic, a mathematical restriction of logic (it's also approximative but that's another question). Hence the confusion. 1st order logic relies on quantification and the subject/predicate distinction. But that in itself is already beyond logic. You can make it logical of course but it's not logic proper, it's already mathematics. So, basically, mathematicians have deluded themselves that logic could justify mathematics when the logic they used was already mathematics. So, Tarski and Gödel merely put an end to that confused delusion. Logic cannot prove anything true unless it follows from something you've already accepted as true and goes for mathematics as well.
I'm not sure you're idea is not that your solution could ultimately revive the mathematician's dream?
EB

[PeteOlcott]

Can this: ∃F∃G(G ↔ ~(F ⊢ G)) be shown to be satisfiable without Gödel numbers ?

If you are talking about Godel numbers then you are necessarily looking for a symbolic, not numeric satisfiability.

No I am definitely not talking about Gödel numbers, they are off topic. I am restricting the
analysis of this expression: ∃F∃G(G ↔ ~(F ⊢ G)) to some order of predicate logic.

[Eodnhoj7]

https://www.researchgate.net/publicatio ... finability

Philosophy of Logic – Reexamining the Formalized Notion of Truth
I update this linked paper all the time: I just added an explanation for laymen:
https://philpapers.org/archive/OLCPOL.pdf

All completeness and incompleteness are axioms.

As axioms they are assumed.

Hence completeness and incompleteness are states of definition which in themselves are assumed.

Completeness and incompleteness reflect the dichotomy of unity/multiplicity, order/chaos, form/formlessness, etc.

[Logik]

No I am definitely not talking about Gödel numbers, they are off topic. I am restricting the
analysis of this expression: ∃F∃G(G ↔ ~(F ⊢ G)) to some order of predicate logic.

Sorry. No go - I don't like arbitrary constraints.

Lets start with Highest order logic (order N). Turing completeness.

[PeteOlcott]

No I am definitely not talking about Gödel numbers, they are off topic. I am restricting the
analysis of this expression: ∃F∃G(G ↔ ~(F ⊢ G)) to some order of predicate logic.

Sorry. No go - I don't like arbitrary constraints.

Lets start with Highest order logic (order N). Turing completeness.

The problem with Gödel numbers and diagonalization is that it only shows
{that} an expression is unprovable, thus totally masking over {why} it is
unprovable.

When an expression is shown to be unprovable by diagonalization this masks
over the key detail that it is only unprovable because it is ill-formed.

∀F ∈ Formal_Systems ∀x ∈ WFF(F) (True(F, x) ↔ (F ⊢ x))

[Logik]

When an expression is shown to be unprovable by diagonalization this masks
over the key detail that it is only unprovable because it is ill-formed.

∀F ∈ Formal_Systems ∀x ∈ WFF(F) (True(F, x) ↔ (F ⊢ x))

You keep bumping your head against the epistemic problem of criterion.

Clearly that is an algorithm in your head which can determine which expression is "well formed" and which expression is "badly formed".
What is your classification rule?

https://en.wikipedia.org/wiki/Classification_rule

[Eodnhoj7]

When an expression is shown to be unprovable by diagonalization this masks
over the key detail that it is only unprovable because it is ill-formed.

∀F ∈ Formal_Systems ∀x ∈ WFF(F) (True(F, x) ↔ (F ⊢ x))

You keep bumping your head against the epistemic problem of criterion.

Clearly that is an algorithm in your head which can determine which expression is "well formed" and which expression is "badly formed".
What is your classification rule?

https://en.wikipedia.org/wiki/Classification_rule

Criterion is assumed, as it is determined by its coherency which effectively acts as a foundation.