Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
Opportunities arising from the refutation of Godel's incompleteness theorem
7 views
Skip to first unread message
xilog
May 10, 2019, 4:50:36 AM5/10/19
to
Anyone who is able to prove that Godel's incompleteness theorem is false will have a difficult time in persuading others of this, since Godel's proof of this theorem is accepted universally by professional logician's.
There is a way to overcome this difficulty, as follows.
Godel's result has been fully formalised and machine checked, more than once.
Someone in possession of a proof of its negation is therefore in a position to obtain a fully formal machine checked proof of a contradiction in an established logical system (e.g. in HOL, which is certainly capable of proving Godel's result).
This would not be ignored.
No-one who develops software for doing formalised mathematics can tolerate the derivation of contradictions using their software.
If a contradiction is derived they will devote considerable effort to locating the infelicity in the proof checker, and if the problem lies not in the proof checker but in the consistency of the logical system which it implements, then they will certainly want that to be known and understood by the community at large.
By this means someone able to refute Godel's proof would be able to persuade many others of the merits of his arguments.
Of course, this is not easy to do.
You need to have or acquire a competence in using an interactive theorem prover to obtain and check formal proofs, and you probably have to do an amount of work similar to what would ordinarily be involved in obtaining a PhD.
But the reward would be substantial kudos.
On the other hand, arguing informally that Godel was wrong, is probably not going to work.
There is a way to overcome this difficulty, as follows.
Godel's result has been fully formalised and machine checked, more than once.
Someone in possession of a proof of its negation is therefore in a position to obtain a fully formal machine checked proof of a contradiction in an established logical system (e.g. in HOL, which is certainly capable of proving Godel's result).
This would not be ignored.
No-one who develops software for doing formalised mathematics can tolerate the derivation of contradictions using their software.
If a contradiction is derived they will devote considerable effort to locating the infelicity in the proof checker, and if the problem lies not in the proof checker but in the consistency of the logical system which it implements, then they will certainly want that to be known and understood by the community at large.
By this means someone able to refute Godel's proof would be able to persuade many others of the merits of his arguments.
Of course, this is not easy to do.
You need to have or acquire a competence in using an interactive theorem prover to obtain and check formal proofs, and you probably have to do an amount of work similar to what would ordinarily be involved in obtaining a PhD.
But the reward would be substantial kudos.
On the other hand, arguing informally that Godel was wrong, is probably not going to work.
xilog
May 10, 2019, 5:10:50 AM5/10/19
to
To be specific, a description of a relatively recent proof in a modern proof tool may be found here:
https://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-logic.pdf
Someone in possession of a refutation would be able to extend this work to obtain a derivation of a contradiction in isabelle/HOL, which would be taken seriously by many people.
https://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-logic.pdf
Someone in possession of a refutation would be able to extend this work to obtain a derivation of a contradiction in isabelle/HOL, which would be taken seriously by many people.
peteolcott
May 10, 2019, 11:30:34 AM5/10/19
to
On 5/10/2019 3:50 AM, xilog wrote:
> Anyone who is able to prove that Godel's incompleteness theorem is false will have a difficult time in persuading others of this, since Godel's proof of this theorem is accepted universally by professional logician's.
>
> There is a way to overcome this difficulty, as follows.
>
> Godel's result has been fully formalised and machine checked, more than once.
None-the-less when construed within the sound deductive inference model:
> Anyone who is able to prove that Godel's incompleteness theorem is false will have a difficult time in persuading others of this, since Godel's proof of this theorem is accepted universally by professional logician's.
>
> There is a way to overcome this difficulty, as follows.
>
> Godel's result has been fully formalised and machine checked, more than once.
Introduction to Mathematical logic Sixth edition Elliott Mendelson (2015)
1.4 An Axiom System for the Propositional Calculus page 28
A wf C is said to be a consequence in S of a set Γ of wfs if and only if there is a
sequence B1, …, Bk of wfs such that C is Bk and, for each i, either Bi is an axiom
or Bi is in Γ, or Bi is a direct consequence by some rule of inference of some of
the preceding wfs in the sequence. Such a sequence is called a proof (or deduction)
of C from Γ. The members of Γ are called the hypotheses or premisses of the proof.
We use Γ ⊢ C as an abbreviation for “C is a consequence of Γ”...
Simply the subset of the above conventional formal proofs of mathematical logic having
true premises: True(Γ) ⊢ C
Then this sentence becomes simply false:
∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))
Because this part is deductively unsound: (F ⊬ G) ∧ (F ⊬ ¬G)
That valid deduction applied to True premises necessitates a true consequence
is a tautology.
> Someone in possession of a proof of its negation is therefore in a position to obtain a fully formal machine checked proof of a contradiction in an established logical system (e.g. in HOL, which is certainly capable of proving Godel's result).
system is insufficiently expressive to detect and reject semantic error.
The issue is comparable to this:
When a man that has never been married is asked:
Have you stopped beating your wife yet?
This question does not prove that human reasoning is
incomplete on the basis of questions lacking correct answers.
It simply proves that incorrect polar questions exist.
In this exact same way we decide that there is no closed
WFF of formal logic that lacks a specific Boolean value.
Any closed WFF that cannot be resolved to True or False
is semantically unsound.
>
> This would not be ignored.
> No-one who develops software for doing formalised mathematics can tolerate the derivation of contradictions using their software.
> If a contradiction is derived they will devote considerable effort to locating the infelicity in the proof checker, and if the problem lies not in the proof checker but in the consistency of the logical system which it implements, then they will certainly want that to be known and understood by the community at large.
expression: Γ ⊢ C can be transformed into a complete and consistent
formal system by making this one change: True(Γ) ⊢ C
True(x) is defined as: (⊢x)
False(x) is defined as: (¬⊢x)
Deductively_Sound_Consequent(x) is defined as (True(x) ∨ False(x))
Thus correctly classifying every conventionally undecidable logic sentence
(closed WFF) as simply deductively unsound.
>
> By this means someone able to refute Godel's proof would be able to persuade many others of the merits of his arguments.
>
True premises combined with valid inference necessitates true consequences.
How hard is it to understand ¬Sound_Deduction as either not true premises
or not valid deduction?
It really should not take any wild stretch of the imagination to realize
that any logic sentences X that cannot possibly be resolved to X or ¬X
are deductively unsound.
All of the undecidable sentences of conventional mathematical logic then
simply become deductively unsound.
And the man that has never been married when asked:
Have you stopped beating your wife yet?
correctly answers:
Incorrect_Question("Have you stopped beating your wife yet?")
> Of course, this is not easy to do.
> You need to have or acquire a competence in using an interactive theorem prover to obtain and check formal proofs, and you probably have to do an amount of work similar to what would ordinarily be involved in obtaining a PhD.
> But the reward would be substantial kudos.
>
> On the other hand, arguing informally that Godel was wrong, is probably not going to work.
>
Copyright 2019 Pete Olcott
All rights reserved
peteolcott
May 10, 2019, 11:34:47 AM5/10/19
to
How hard is it to understand the basic model of Sound_Deduction?
True premises combined with valid inference necessitates true consequences.
How hard is it to understand ¬Sound_Deduction as either not true premises
or not valid deduction?
It really should not take any wild stretch of the imagination to realize
that any logic sentences X that cannot possibly be resolved to X or ¬X
are deductively unsound.
All of the undecidable sentences of conventional mathematical logic then
simply become deductively unsound.
True premises combined with valid inference necessitates true consequences.
How hard is it to understand ¬Sound_Deduction as either not true premises
or not valid deduction?
It really should not take any wild stretch of the imagination to realize
that any logic sentences X that cannot possibly be resolved to X or ¬X
are deductively unsound.
All of the undecidable sentences of conventional mathematical logic then
simply become deductively unsound.
xilog
May 10, 2019, 12:04:16 PM5/10/19
to
I am unclear what part of my post you are disagreeing with and on what grounds.
Are you disagreeing that Godel's theorem has been formally proven?
Are you disagreeing that if it were formally proven a formal proof of its negation would permit a formal derivation of a contradiction to be constructed?
Are you disagreeing that a formal derivation of a contradiction would be convincing to those who trust the relevant proof checking software?
Enlighten me.
Are you disagreeing that Godel's theorem has been formally proven?
Are you disagreeing that if it were formally proven a formal proof of its negation would permit a formal derivation of a contradiction to be constructed?
Are you disagreeing that a formal derivation of a contradiction would be convincing to those who trust the relevant proof checking software?
Enlighten me.
peteolcott
May 10, 2019, 12:45:51 PM5/10/19
to
expressive to detect and reject semantically unsound logic sentences.
It should have decided Semantically_Incorrect(G). Instead it concluded Incomplete(F).
peteolcott
May 10, 2019, 1:28:07 PM5/10/19
to
When a man that has never been married is asked:
Have you stopped beating your wife yet?
The lack of a correct answer does not indicate that all of human
Have you stopped beating your wife yet?
reasoning is fundamentally incomplete.
When-so-ever a yes or no question lacks a correct yes or no answer the
question itself is incorrect.
When-so-ever a logic sentence lacks a correct true or false Boolean
value the logic sentence itself is incorrect.
There is no set of true premises combined with valid inference
that satisfies the following predicate:
Sound_Deduction("G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G))") thus
"G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G))" is rejected as semantically unsound in
the same way that the unmarried guy is asked about beating his wife.
peteolcott
May 10, 2019, 1:56:16 PM5/10/19
to
On 5/10/2019 11:04 AM, xilog wrote:
Deductively Sound Formal Proofs
https://www.researchgate.net/publication/332864362_Deductively_Sound_Formal_Proofs
xilog
May 10, 2019, 2:26:24 PM5/10/19
to
As far as I can see, you did not answer any of the questions I asked.
peteolcott
May 10, 2019, 2:35:19 PM5/10/19
to
On 5/10/2019 11:04 AM, xilog wrote:
http://liarparadox.org/Provable_Mendelson.pdf
¬((Γ ⊢ C) ∨ (Γ ⊢ ¬C)) defines ¬Deductively_Sound(Γ, C)
This excludes every undecidable logic sentence of conventional formal proofs
as deductively unsound thus semantically incorrect.
Deductively Sound Formal Proofs
https://www.researchgate.net/publication/332864362_Deductively_Sound_Formal_Proofs
peteolcott
May 10, 2019, 2:36:45 PM5/10/19
to
On 5/10/2019 1:26 PM, xilog wrote:
> As far as I can see, you did not answer any of the questions I asked.
>
You must be looking at my answer from thw wrong frame-of-reference.
> As far as I can see, you did not answer any of the questions I asked.
>
If the question is what math error did Godel make?
The answer is that math itself was in error.
peteolcott
May 10, 2019, 2:40:43 PM5/10/19
to
On 5/10/2019 1:36 PM, peteolcott wrote:
> On 5/10/2019 1:26 PM, xilog wrote:
>> As far as I can see, you did not answer any of the questions I asked.
>>
>
> You must be looking at my answer from thw wrong frame-of-reference.
>
> If the question is what math error did Godel make?
> The answer is that math itself was in error.
>
Math itself was in error because math itself was insufficiently expressive
> On 5/10/2019 1:26 PM, xilog wrote:
>> As far as I can see, you did not answer any of the questions I asked.
>>
>
> You must be looking at my answer from thw wrong frame-of-reference.
>
> If the question is what math error did Godel make?
> The answer is that math itself was in error.
>
to detect and reject semantically malformed expressions.
xilog
May 10, 2019, 2:44:04 PM5/10/19
to
I asked three questions, each of which should have a yes/no answer, and I still don't know your answer to any of those questions.
peteolcott
May 10, 2019, 2:45:34 PM5/10/19
to
On 5/10/2019 1:26 PM, xilog wrote:
> As far as I can see, you did not answer any of the questions I asked.
>
When you ask me what math error did Godel make,
>
it is just like asking the guy that has never been married:
Have you stopped beating your wife yet?
He answers no because he has no wife and you take this to mean
that he is still beating his wife.
What math error did Godel make?
Within the math system, none.
So then he was correct.
Not at all. The math system itself was incorrect, there was a mistake,
it was just not his mistake, the mistake belonged to someone else.
peteolcott
May 10, 2019, 2:53:22 PM5/10/19
to
On 5/10/2019 12:56 PM, peteolcott wrote:
> On 5/10/2019 11:04 AM, xilog wrote:
>> I am unclear what part of my post you are disagreeing with and on what grounds.
>>
These question are like asking a guy that has never been married:
> On 5/10/2019 11:04 AM, xilog wrote:
>> I am unclear what part of my post you are disagreeing with and on what grounds.
>>
Did you stop beating your wife yet.
>> Are you disagreeing that Godel's theorem has been formally proven?
that this incorrect formal system woujld support his conclusions.
>>
>> Are you disagreeing that if it were formally proven a formal proof of its negation would permit a formal derivation of a contradiction to be constructed?
>>
in the same way that one would conclude that when a guy that has never been married is asked:
Have you stopped beating your wife yet?
and he answers "no" because he has no wife,
the incorrect inference that he still beats his wife would be made.
There is no contradiction, merely a gap in reasoning that causes incorrect inference.
Filling in this gap rejects the question is incorrect.
>> Are you disagreeing that a formal derivation of a contradiction would be convincing to those who trust the relevant proof checking software?
xilog
May 10, 2019, 3:27:35 PM5/10/19
to
OK, so:
1. you accept that Godel's proof is syntactically correct
2. you don't accept that his formal system is sound (you think it proves falsehoods)
3. you don't claim that you could derive the denial of Godel's result in that same system
So far that doesn't actually refute Godel's theorem.
To refute it, you have to prove its negation.
Do you have a proof of its negation?
1. you accept that Godel's proof is syntactically correct
2. you don't accept that his formal system is sound (you think it proves falsehoods)
3. you don't claim that you could derive the denial of Godel's result in that same system
So far that doesn't actually refute Godel's theorem.
To refute it, you have to prove its negation.
Do you have a proof of its negation?
peteolcott
May 10, 2019, 3:52:53 PM5/10/19
to
I can only do this by correcting the error that is built-in to the conventional
notion of a formal system.
When asking a guy that has never been married:
Have you stopped beating your wife yet?
The answer of "no" would be incorrectly construed as meaning that he still beats his wife.
The formal system is unable to detect its semantic gap.
There is no detectable contradiction, merely an undetectable gap.
Someone comes along an augments this formal system:
Do you have a wife?
Have you ever beat your wife?
Have you stopped beating your wife?
else skip
else skip
Is G a closed WFF?
Is G true?
is ~G true?
else skip
else skip
peteolcott
May 11, 2019, 1:37:00 AM5/11/19
to
On 5/10/2019 2:27 PM, xilog wrote:
that lets semantically incorrect expressions of language go undetected.
http://liarparadox.org/Provable_Mendelson.pdf
Within this conventional notion of formal proof:
Γ ⊢ C means “C is a consequence of the set of premises Γ”
[Deductively sound formal proofs of mathematical logic]
are defined by adding this single axiom schema to these proofs:
Deductively_Sound(Γ, C) := (True(Γ) ∧ ((Γ ⊢ C) ∨ (Γ ⊢ ¬C)))
Where LHS := RHS means that the LHS is defined as an alias for the RHS
In English this axiom schema means:
If the premises are true and either the consequent or its negation
are provable from these premises then the premises and the consequent
form a sound deductive argument.
Every undecidable logic sentence in the conventional formal proofs of
mathematical logic is shown to be deductively unsound thus semantically
incorrect in [Deductively sound formal proofs].
As you can see the above axiom schema decides that the Gödel sentence of
the 1931 Incompleteness Theorem is deductively unsound thus semantically
incorrect: G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G))
xilog
May 11, 2019, 6:41:22 AM5/11/19
to
The material you refer to from Mendelson is standard and uncontroversial.
Your definitions of "Deductively sound", "deductively sound formal proof" and "semantically incorrect" are not, and so its not surprising that they are not found in your citation from Mendelson.
According to your own definitions, Godel's incompleteness theorem is obtained by a deductively sound formal proof, even though what it proves, if we adopt your usage, is that there are "semantically incorrect" sentences in arithmetic (which most mathematicians would still consider to have a definite truth value).
If this is considered to be a defect in Godel's theorem, then it is one which affects the whole of classical mathematics, since there are no classical formal systems capable of doing non-trivial mathematics which do not share the same defect.
Of course, you are not the first person to indict mathematics in this way, card carrying intuitionists do so, but even intuitionists regard Godel's theorem as true because provable by their preferred methods.
Your definitions of "Deductively sound", "deductively sound formal proof" and "semantically incorrect" are not, and so its not surprising that they are not found in your citation from Mendelson.
According to your own definitions, Godel's incompleteness theorem is obtained by a deductively sound formal proof, even though what it proves, if we adopt your usage, is that there are "semantically incorrect" sentences in arithmetic (which most mathematicians would still consider to have a definite truth value).
If this is considered to be a defect in Godel's theorem, then it is one which affects the whole of classical mathematics, since there are no classical formal systems capable of doing non-trivial mathematics which do not share the same defect.
Of course, you are not the first person to indict mathematics in this way, card carrying intuitionists do so, but even intuitionists regard Godel's theorem as true because provable by their preferred methods.
peteolcott
May 11, 2019, 6:25:44 PM5/11/19
to
On 5/11/2019 5:41 AM, xilog wrote:
> The material you refer to from Mendelson is standard and uncontroversial.
>
> Your definitions of "Deductively sound", "deductively sound formal proof"
This utterly refutes your first two.
> The material you refer to from Mendelson is standard and uncontroversial.
>
> Your definitions of "Deductively sound", "deductively sound formal proof"
To make the conventional formal proofs of mathematical logic
conform to the sound deductive inference model we only have
to select the subset of conventional formal proofs having
true premises: thus Γ ⊢ C becomes this True(Γ) ⊢ C.
> and "semantically incorrect" are not, and so its not surprising that they are not found in your citation from Mendelson.
>
https://www.researchgate.net/publication/332864362_Deductively_Sound_Formal_Proofs
> According to your own definitions, Godel's incompleteness theorem is obtained by a deductively sound formal proof,
All of mathematical logic totally ignores sound and only pays attention to valid,
that is their BIG MISTAKE !!!
> even though what it proves, if we adopt your usage, is that there are "semantically incorrect" sentences in arithmetic (which most mathematicians would still consider to have a definite truth value).
>
(see my paper).
> If this is considered to be a defect in Godel's theorem, then it is one which affects the whole of classical mathematics, since there are no classical formal systems capable of doing non-trivial mathematics which do not share the same defect.
>
> Of course, you are not the first person to indict mathematics in this way, card carrying intuitionists do so, but even intuitionists regard Godel's theorem as true because provable by their preferred methods.
>
How hard is it to understand the basic model of Sound_Deduction?
True premises combined with valid inference necessitates true consequences.
Please read my updated one page paper.
True premises combined with valid inference necessitates true consequences.
peteolcott
May 11, 2019, 7:36:53 PM5/11/19
to
On 5/11/2019 5:41 AM, xilog wrote:
understand sound deduction then you already understand that the
intersection of these two by itself specifies a necessarily
complete and consistent formal system.
From true premises and valid inference a true consequence necessarily
follows. There are no loopholes or possible exceptions.
Once we have such formal system it rejects Tarski and Godel as unsound.
peteolcott
May 13, 2019, 2:58:27 PM5/13/19
to
On 5/11/2019 5:41 AM, xilog wrote:
> The material you refer to from Mendelson is standard and uncontroversial.
>
> Your definitions of "Deductively sound", "deductively sound formal proof" and "semantically incorrect" are not, and so its not surprising that they are not found in your citation from Mendelson.
>
https://www.researchgate.net/publication/332864362_Deductively_Sound_Formal_Proofs
>
> Your definitions of "Deductively sound", "deductively sound formal proof" and "semantically incorrect" are not, and so its not surprising that they are not found in your citation from Mendelson.
>
My definition of deductively valid within the sound deductive inference model
as specifying exactly the same thing as provability in formal proofs is now
clear enough that it has been agreed to as correct. (Page 1 of the above paper).
Page 2 of the above paper shows exactly how the deductively sound of aspect
of the sound deductive inference model could be specified within formal proofs
of symbolic logic: All formal proofs to theorem consequences where Axioms are
stipulated as having the semantic value of Boolean true (as Haskell Curry stipulates)
necessarily specify sound deduction.
Since sound deduction derives consequences that are necessarily true
[deductively sound formal proofs of mathematical logic] specify a universal
Truth predicate: True(C) := (⊢ C).
> According to your own definitions, Godel's incompleteness theorem is obtained by a deductively sound formal proof,
As sound deductive inference itself has defined it and as I have translated sound
deductive inference into [deductively sound formal proofs of mathematical logic]
∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))
and every logic sentence must be true or false.
> even though what it proves, if we adopt your usage, is that there are "semantically incorrect" sentences in arithmetic (which most mathematicians would still consider to have a definite truth value).
>
> If this is considered to be a defect in Godel's theorem, then it is one which affects the whole of classical mathematics, since there are no classical formal systems capable of doing non-trivial mathematics which do not share the same defect.
>
0 new messages