Refuting Gödel's 1931 Incompleteness Theorem in one sentence

What is the basis for reason? And mathematics?

Moderators: AMod, iMod

PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

Re: Refuting Gödel's 1931 Incompleteness Theorem in one sentence

Post by PeteOlcott »

Univalence wrote: Mon May 20, 2019 5:10 pm
PeteOlcott wrote: Mon May 20, 2019 5:07 pm Ah I see. You don't understand me simply because you don't know predicate logic well enough.
And you don't understand me because you don't understand Univalent mathematics well enough.

https://en.wikipedia.org/wiki/Univalent_foundations
Univalent foundations depart from the use of classical predicate logic as the underlying formal deduction system, replacing it, at the moment, with a version of Martin-Löf type theory.
Dodging the question regarding your knowledge of predicate logic by changing the subject
to some other logic does not really help.

To understand what I am saying you must understand this:

∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))

In English this says:
There exists a formal system F and a closed WFF G of F such that G
is materially equivalent to its own unprovability and irrefutability.
Last edited by PeteOlcott on Mon May 20, 2019 5:16 pm, edited 1 time in total.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

Re: Refuting Gödel's 1931 Incompleteness Theorem in one sentence

Post by Univalence »

PeteOlcott wrote: Mon May 20, 2019 5:15 pm Dodging the question regarding your knowledge of predicate logic by changing the subject
to some other logic does not really help.
Because Predicate Logic is dead in my universe. Some fossils in the 20th century cared about it.

You are the one who needs to catch up with the times. Proof theory is where it's at whether you like it or not.

Proofs compute.
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

Re: Refuting Gödel's 1931 Incompleteness Theorem in one sentence

Post by PeteOlcott »

Univalence wrote: Mon May 20, 2019 5:16 pm
PeteOlcott wrote: Mon May 20, 2019 5:15 pm Dodging the question regarding your knowledge of predicate logic by changing the subject
to some other logic does not really help.
Because Predicate Logic is dead in my universe.

Some fossils in the 20th century cared about it.
That slick dodge does not really work.

The language of predicate logic is merely the language that I use to say exactly what I mean.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

Re: Refuting Gödel's 1931 Incompleteness Theorem in one sentence

Post by Univalence »

PeteOlcott wrote: Mon May 20, 2019 5:17 pm That slick dodge does not really work.
Yeah. It does.

https://en.wikipedia.org/wiki/Curry%E2% ... espondence
In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relationship between computer programs and mathematical proofs.
Show me an algorithm. Or get lost.
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

Re: Refuting Gödel's 1931 Incompleteness Theorem in one sentence

Post by PeteOlcott »

Univalence wrote: Mon May 20, 2019 5:18 pm
PeteOlcott wrote: Mon May 20, 2019 5:17 pm That slick dodge does not really work.
Yeah. It does.

https://en.wikipedia.org/wiki/Curry%E2% ... espondence

Show me an algorithm. Or get lost.
I showed you the algorithm in a declarative language that you do not understand.

Because I know the crucial value of types I spent 18 month creating Minimal Type Theory
https://www.researchgate.net/publicatio ... y_YACC_BNF

and if you are paying attention you will see that the two variables below are associated with types
∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))

So your whole idea of saying the my language is no good because it does not use
types is a sham.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

Re: Refuting Gödel's 1931 Incompleteness Theorem in one sentence

Post by Univalence »

PeteOlcott wrote: Mon May 20, 2019 5:17 pm The language of predicate logic is merely the language that I use to say exactly what I mean.
I don't speak it and I have no interest in learning it.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

Re: Refuting Gödel's 1931 Incompleteness Theorem in one sentence

Post by Univalence »

PeteOlcott wrote: Mon May 20, 2019 5:24 pm I showed you the algorithm in a declarative language that you do not understand.
Correct. A language whose semantics aren't transparent to me.
Which is why I keep asking you for the meaning of your symbols.

Something I wouldn't have to do if the source code was available to me.
PeteOlcott wrote: Mon May 20, 2019 5:24 pm Because I know the crucial value of types I spent 18 month creating Minimal Type Theory
https://www.researchgate.net/publicatio ... y_YACC_BNF
So you re-invented the wheel?
These tools already exist: https://en.wikipedia.org/wiki/Proof_assistant
PeteOlcott wrote: Mon May 20, 2019 5:24 pm So your whole idea of saying the my language is no good because it does not use
types is a sham.
And yet the moment you put your idea in C++ I immediately pointed out your type error.

I am telling you that I am not going to learn your ancient and practically useless language.
If you want me to review your proof - you are going to have to learn mine.

Choices. Choices.
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

Re: Refuting Gödel's 1931 Incompleteness Theorem in one sentence

Post by PeteOlcott »

Univalence wrote: Mon May 20, 2019 5:25 pm
PeteOlcott wrote: Mon May 20, 2019 5:24 pm I showed you the algorithm in a declarative language that you do not understand.
Correct. A language whose semantics aren't transparent to me.
Which is why I keep asking you for the meaning of your symbols.

Something I wouldn't have to do if the source code was available to me.
PeteOlcott wrote: Mon May 20, 2019 5:24 pm Because I know the crucial value of types I spent 18 month creating Minimal Type Theory
https://www.researchgate.net/publicatio ... y_YACC_BNF
So you re-invented the wheel?
These tools already exist: https://en.wikipedia.org/wiki/Proof_assistant
PeteOlcott wrote: Mon May 20, 2019 5:24 pm So your whole idea of saying the my language is no good because it does not use
types is a sham.
I am telling you that I am not going to learn your ancient and practically useless language.
If you want me to review your proof - you are going to have to learn mine.

Choices. Choices.
So it boils down to this:
You cannot evaluate whether or not [Deductively sound formal proofs of mathematical logic]
refutes the 1931 Incompleteness theorem only because you refuse to understand exactly what
the 1931 Incompleteness theorem is asserting because the formalization of the enormously simplified
conclusion of the 1931 Incompleteness theorem was written in a language that you just don't like.
Univalence
Posts: 492
Joined: Sun May 12, 2019 6:28 pm

Re: Refuting Gödel's 1931 Incompleteness Theorem in one sentence

Post by Univalence »

PeteOlcott wrote: Mon May 20, 2019 6:10 pm
Univalence wrote: Mon May 20, 2019 5:25 pm
PeteOlcott wrote: Mon May 20, 2019 5:24 pm I showed you the algorithm in a declarative language that you do not understand.
Correct. A language whose semantics aren't transparent to me.
Which is why I keep asking you for the meaning of your symbols.

Something I wouldn't have to do if the source code was available to me.
PeteOlcott wrote: Mon May 20, 2019 5:24 pm Because I know the crucial value of types I spent 18 month creating Minimal Type Theory
https://www.researchgate.net/publicatio ... y_YACC_BNF
So you re-invented the wheel?
These tools already exist: https://en.wikipedia.org/wiki/Proof_assistant
PeteOlcott wrote: Mon May 20, 2019 5:24 pm So your whole idea of saying the my language is no good because it does not use
types is a sham.
I am telling you that I am not going to learn your ancient and practically useless language.
If you want me to review your proof - you are going to have to learn mine.

Choices. Choices.
So it boils down to this:
You cannot evaluate whether or not [Deductively sound formal proofs of mathematical logic]
refutes the 1931 Incompleteness theorem only because you refuse to understand exactly what
the 1931 Incompleteness theorem is asserting because the formalization of the enormously simplified
conclusion of the 1931 Incompleteness theorem was written in a language that you just don't like.
Yes.

The same conclusions can be arrived via Turing’s halting problem. Which may be historically latter but it is conceptually prior to Godel’s work.

So I see no reason to learn your dead and useless language.

Bonus points. I don’t have to learn Gödel numbers and I can explain it to a 15 year old.

Keep it simple, stupid!
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

Re: Refuting Gödel's 1931 Incompleteness Theorem in one sentence

Post by PeteOlcott »

Univalence wrote: Mon May 20, 2019 6:11 pm
PeteOlcott wrote: Mon May 20, 2019 6:10 pm
Univalence wrote: Mon May 20, 2019 5:25 pm
Correct. A language whose semantics aren't transparent to me.
Which is why I keep asking you for the meaning of your symbols.

Something I wouldn't have to do if the source code was available to me.


So you re-invented the wheel?
These tools already exist: https://en.wikipedia.org/wiki/Proof_assistant


I am telling you that I am not going to learn your ancient and practically useless language.
If you want me to review your proof - you are going to have to learn mine.

Choices. Choices.
So it boils down to this:
You cannot evaluate whether or not [Deductively sound formal proofs of mathematical logic]
refutes the 1931 Incompleteness theorem only because you refuse to understand exactly what
the 1931 Incompleteness theorem is asserting because the formalization of the enormously simplified
conclusion of the 1931 Incompleteness theorem was written in a language that you just don't like.
Yes.

The same conclusions can be arrived via Turing’s halting problem. Which may be historically latter but it is conceptually prior to Godel’s work.

So I see no reason to learn your dead and useless language.

Bonus points. I don’t have to learn Gödel numbers and I can explain it to a 15 year old.

Keep it simple, stupid!
Do you see any Gödel numbers here?
∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))

The above is the simplest possible way to formalize the conclusion of the 1931 Incompleteness Theorem.
37 pages boiled down to a single logic sentence.
philosopher
Posts: 416
Joined: Fri Jun 08, 2018 3:37 pm

Re: Refuting Gödel's 1931 Incompleteness Theorem in one sentence

Post by philosopher »

When the notion of true is defined as provable from axioms and axioms
are defined to be finite strings having the semantic property of
Boolean true then any expression of language that is not provable
is not true.
Sorry, but this has already been attempted by Paul Finsler, Ernst Zermelo and Ludwig Wittgenstein in the early and mid-20th century, without success.

I have faith in that they - all of them great mathematicians - have constructed better systems than any 21st century internet discussion members.

I'm also sure if there is ever found anything that even hints at refuting Gödel's Incompleteness Theorem, then it will be all over the media and the foundation of modern mathematics (which relies heavily on Gödels Incompleteness Theorem) will be shaken and teared apart.

You can't prove a solid theorem false in just one sentence. It is ridiculous to think you can do so.
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

Re: Refuting Gödel's 1931 Incompleteness Theorem in one sentence

Post by PeteOlcott »

philosopher wrote: Mon May 20, 2019 8:40 pm
When the notion of true is defined as provable from axioms and axioms
are defined to be finite strings having the semantic property of
Boolean true then any expression of language that is not provable
is not true.
Sorry, but this has already been attempted by Paul Finsler, Ernst Zermelo and Ludwig Wittgenstein in the early and mid-20th century, without success.

I have faith in that they - all of them great mathematicians - have constructed better systems than any 21st century internet discussion members.

I'm also sure if there is ever found anything that even hints at refuting Gödel's Incompleteness Theorem, then it will be all over the media and the foundation of modern mathematics (which relies heavily on Gödels Incompleteness Theorem) will be shaken and teared apart.

You can't prove a solid theorem false in just one sentence. It is ridiculous to think you can do so.
Since I have proven two theorems false with this one sentence:
If the notion of true is defined a provable from axioms and axioms
are defined to be finite strings having the semantic property of
Boolean true then any expression of language that is not provable
is not true.

Your mere disbelief to the contrary provides no rebuttal at all.
philosopher
Posts: 416
Joined: Fri Jun 08, 2018 3:37 pm

Re: Refuting Gödel's 1931 Incompleteness Theorem in one sentence

Post by philosopher »

PeteOlcott wrote: Mon May 20, 2019 8:46 pm
philosopher wrote: Mon May 20, 2019 8:40 pm
When the notion of true is defined as provable from axioms and axioms
are defined to be finite strings having the semantic property of
Boolean true then any expression of language that is not provable
is not true.
Sorry, but this has already been attempted by Paul Finsler, Ernst Zermelo and Ludwig Wittgenstein in the early and mid-20th century, without success.

I have faith in that they - all of them great mathematicians - have constructed better systems than any 21st century internet discussion members.

I'm also sure if there is ever found anything that even hints at refuting Gödel's Incompleteness Theorem, then it will be all over the media and the foundation of modern mathematics (which relies heavily on Gödels Incompleteness Theorem) will be shaken and teared apart.

You can't prove a solid theorem false in just one sentence. It is ridiculous to think you can do so.
Since I have proven two theorems false with this one sentence:
If the notion of true is defined a provable from axioms and axioms
are defined to be finite strings having the semantic property of
Boolean true then any expression of language that is not provable
is not true.

Your mere disbelief to the contrary provides no rebuttal at all.
In short plain English your sentence says:

"You can prove any axiom to be true or false."

But this is what Kurt Gödel's papers are all about refuting.
Gödel thought so himself, and concluded - back and forth that the incompleteness theorem is false, true, false, true etc.
This indicates very strongly that Gödel was very much aware of that sentence anyway.
PeteOlcott
Posts: 1514
Joined: Mon Jul 25, 2016 6:55 pm

Re: Refuting Gödel's 1931 Incompleteness Theorem in one sentence

Post by PeteOlcott »

philosopher wrote: Mon May 20, 2019 8:53 pm
PeteOlcott wrote: Mon May 20, 2019 8:46 pm
philosopher wrote: Mon May 20, 2019 8:40 pm

Sorry, but this has already been attempted by Paul Finsler, Ernst Zermelo and Ludwig Wittgenstein in the early and mid-20th century, without success.

I have faith in that they - all of them great mathematicians - have constructed better systems than any 21st century internet discussion members.

I'm also sure if there is ever found anything that even hints at refuting Gödel's Incompleteness Theorem, then it will be all over the media and the foundation of modern mathematics (which relies heavily on Gödels Incompleteness Theorem) will be shaken and teared apart.

You can't prove a solid theorem false in just one sentence. It is ridiculous to think you can do so.
Since I have proven two theorems false with this one sentence:
If the notion of true is defined a provable from axioms and axioms
are defined to be finite strings having the semantic property of
Boolean true then any expression of language that is not provable
is not true.

Your mere disbelief to the contrary provides no rebuttal at all.
In short plain English your sentence says:

"You can prove any axiom to be true or false."
Not really not at all.

Introduction to Mathematical logic Sixth edition Elliott Mendelson (2015):28
1.4 An Axiom System for the Propositional Calculus page 27-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 Γ”...

If Γ is the empty set ∅, then ∅ ⊢ C if and only if C is a theorem. It is customary
to omit the sign “∅” and simply write ⊢ C. Thus, ⊢ C is another way of asserting that
C is a theorem.

It is exactly: ⊢ C with the additional stipulation that Axioms are actually true,
not this conventional true-ish: http://mathworld.wolfram.com/Axiom.html
philosopher
Posts: 416
Joined: Fri Jun 08, 2018 3:37 pm

Re: Refuting Gödel's 1931 Incompleteness Theorem in one sentence

Post by philosopher »

PeteOlcott wrote: Mon May 20, 2019 9:03 pm Not really not at all.

Introduction to Mathematical logic Sixth edition Elliott Mendelson (2015):28
1.4 An Axiom System for the Propositional Calculus page 27-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 Γ”...

If Γ is the empty set ∅, then ∅ ⊢ C if and only if C is a theorem. It is customary
to omit the sign “∅” and simply write ⊢ C. Thus, ⊢ C is another way of asserting that
C is a theorem.

It is exactly: ⊢ C with the additional stipulation that Axioms are actually true,
not this conventional true-ish: http://mathworld.wolfram.com/Axiom.html
Thanks for clarifying this, however I do not understand the meanings of those symbols (⊢, Γ, wfs, Bk etc.) so I can't really discuss the matter in-depth as much as I'd like to.

I admit I'm not educated enough to actually refuting or verifying either theory.

But I'd like to learn the language of logic, is there a youtube tutorial series you would recommend? Alternatively, if possible - could you explain those symbols?
Post Reply