Gödel’s first incompleteness theorem – an interactive tutorial(tigyog.app)
tigyog.app
Gödel’s first incompleteness theorem – an interactive tutorial
https://tigyog.app/d/H7XOvXvC_x/r/goedel-s-first-incompleteness-theorem
22 comments
> the Halting Problem brings with it a lot of stuff
Not really. The idea of a Turing Machine brings with it a lot of stuff, but nowadays Turing Machines are a dime a dozen, and the idea of a "program" is common place. So proving the non-computability of the halting problem is pretty easy [1]:
Assume that there exists a program H that solves the halting problem, that is, H takes two input parameters, a program P and an input I and returns true if P halts when run on input I, false otherwise.
Construct a program B that does the following: B accepts as input a program P and computes H(P,P), that is, it calls H as a subroutine to determine if program P halts when run on a copy of itself as the input. If the result from H is true then B enters an infinite loop, otherwise B halts (that is, B does the opposite of what P would do when run on a copy of itself).
Now consider what happens if we run B on a copy of itself. B will halt iff H(B,B) is false. But H(B,B) is false iff B doesn't halt, which is a contradiction. Therefore, our assumption is false, and H is impossible. QED.
---
[1] Taken from https://flownet.com/ron/chaitin.html
Not really. The idea of a Turing Machine brings with it a lot of stuff, but nowadays Turing Machines are a dime a dozen, and the idea of a "program" is common place. So proving the non-computability of the halting problem is pretty easy [1]:
Assume that there exists a program H that solves the halting problem, that is, H takes two input parameters, a program P and an input I and returns true if P halts when run on input I, false otherwise.
Construct a program B that does the following: B accepts as input a program P and computes H(P,P), that is, it calls H as a subroutine to determine if program P halts when run on a copy of itself as the input. If the result from H is true then B enters an infinite loop, otherwise B halts (that is, B does the opposite of what P would do when run on a copy of itself).
Now consider what happens if we run B on a copy of itself. B will halt iff H(B,B) is false. But H(B,B) is false iff B doesn't halt, which is a contradiction. Therefore, our assumption is false, and H is impossible. QED.
---
[1] Taken from https://flownet.com/ron/chaitin.html
> nowadays Turing Machines are a dime a dozen, and the idea of a "program" is common place
I think you may have misconstrued what I meant. From a metamathematical standpoint, leveraging the Halting Problem gives you a lot of stuff for free. Just the fact that we're assuming that a formal logic system and a programming language are isomorphic is actually a pretty huge deal and those developments span several generations of logicians.
Specifically, Godel numbering really originally made this entire thing work. And that sausage was not very intuitively-made.
I think you may have misconstrued what I meant. From a metamathematical standpoint, leveraging the Halting Problem gives you a lot of stuff for free. Just the fact that we're assuming that a formal logic system and a programming language are isomorphic is actually a pretty huge deal and those developments span several generations of logicians.
Specifically, Godel numbering really originally made this entire thing work. And that sausage was not very intuitively-made.
> leveraging the Halting Problem gives you a lot of stuff for free.
Not exactly for free. You still have to prove the non-computability of the halting problem. But I get your meaning.
> Just the fact that we're assuming that a formal logic system and a programming language are isomorphic is actually a pretty huge deal and those developments span several generations of logicians.
Sure, but that is no different from any technological advance. Arabic numerals were a major breakthrough when they were first invented. Nowadays it is pretty safe to take them for granted in most cases.
> Godel numbering really originally made this entire thing work.
Sure, but that was only necessary because Godel didn't know about ASCII. Proving Godel's theorem using Godel numbers is kind of like writing a C compiler as a state table for a Turing Machine. You could do it, but no one in their right mind would except perhaps as an intellectual exercise.
The history of how technological innovations came about is very different, and usually much more difficult, than the way one can re-invent those innovations with the benefit of hindsight.
Not exactly for free. You still have to prove the non-computability of the halting problem. But I get your meaning.
> Just the fact that we're assuming that a formal logic system and a programming language are isomorphic is actually a pretty huge deal and those developments span several generations of logicians.
Sure, but that is no different from any technological advance. Arabic numerals were a major breakthrough when they were first invented. Nowadays it is pretty safe to take them for granted in most cases.
> Godel numbering really originally made this entire thing work.
Sure, but that was only necessary because Godel didn't know about ASCII. Proving Godel's theorem using Godel numbers is kind of like writing a C compiler as a state table for a Turing Machine. You could do it, but no one in their right mind would except perhaps as an intellectual exercise.
The history of how technological innovations came about is very different, and usually much more difficult, than the way one can re-invent those innovations with the benefit of hindsight.
Gödel numbering is chosen because numbers are very easy to reason about and mathematicians like that things are provable from simple principles like arithmetic, and because for Gödel's theorem to actually work on theories of arithmetic the encodings of formulas have to be numbers.
Of course, you can choose some other encoding scheme - one that is easier for humans to read, such as the binary encoding of a nicely formatted string - but that's not as directly amenable to a rigorous mathematical proof. In particular, you technically have to prove that that encoding scheme doesn't lead to ambiguities, i.e. every string has (at most) a unique parsing. That may seem (and is) obvious, but technically does require a proof, something you can avoid when you just use Gödel numbering via the fundamental theorem of arithmetic instead
But Gödel numbering is not really the bread and butter of the proof. The more technically relevant part about Gödel's proofs that doesn't just readily follow from the halting problem is the fact that incompleteness of first-order theories has only very weak conditions - Robinson arithmetic is already sufficient.
You have to prove that Robinson arithmetic is strong enough to express every primitive recursive function and that requires some mathematical tricks.
Of course, you can choose some other encoding scheme - one that is easier for humans to read, such as the binary encoding of a nicely formatted string - but that's not as directly amenable to a rigorous mathematical proof. In particular, you technically have to prove that that encoding scheme doesn't lead to ambiguities, i.e. every string has (at most) a unique parsing. That may seem (and is) obvious, but technically does require a proof, something you can avoid when you just use Gödel numbering via the fundamental theorem of arithmetic instead
But Gödel numbering is not really the bread and butter of the proof. The more technically relevant part about Gödel's proofs that doesn't just readily follow from the halting problem is the fact that incompleteness of first-order theories has only very weak conditions - Robinson arithmetic is already sufficient.
You have to prove that Robinson arithmetic is strong enough to express every primitive recursive function and that requires some mathematical tricks.
> because for Gödel's theorem to actually work on theories of arithmetic the encodings of formulas have to be numbers
ASCII codes are numbers.
> but that's not as directly amenable to a rigorous mathematical proof
Why not?
> you technically have to prove that that encoding scheme doesn't lead to ambiguities,
ASCII is unambiguous. In fact, the only difference between ASCII and Godel numbers is that ASCII encodes strings as powers of 256 whereas Godel numbers encode strings as powers of prime numbers.
> i.e. every string has (at most) a unique parsing
Huh? That makes no sense. Did you mean that every number has a unique mapping to a string? Because ASCII certainly meets that requirement.
> The more technically relevant part about Gödel's proofs that doesn't just readily follow from the halting problem is the fact that incompleteness of first-order theories has only very weak conditions - Robinson arithmetic is already sufficient.
Why does that matter? This seems to me like an interesting bit of trivia about Robinson arithmetic, but I don't see why this matters to the main point. Any system less powerful than PA is trivially incomplete.
ASCII codes are numbers.
> but that's not as directly amenable to a rigorous mathematical proof
Why not?
> you technically have to prove that that encoding scheme doesn't lead to ambiguities,
ASCII is unambiguous. In fact, the only difference between ASCII and Godel numbers is that ASCII encodes strings as powers of 256 whereas Godel numbers encode strings as powers of prime numbers.
> i.e. every string has (at most) a unique parsing
Huh? That makes no sense. Did you mean that every number has a unique mapping to a string? Because ASCII certainly meets that requirement.
> The more technically relevant part about Gödel's proofs that doesn't just readily follow from the halting problem is the fact that incompleteness of first-order theories has only very weak conditions - Robinson arithmetic is already sufficient.
Why does that matter? This seems to me like an interesting bit of trivia about Robinson arithmetic, but I don't see why this matters to the main point. Any system less powerful than PA is trivially incomplete.
Your point about ASCII codes ignores that we don't just want individual symbols to be numbers, we want entire formulas to be numbers too.
Of course, you can encode any sequence of ASCII codes as a number (just concatenate the binary digits), I didn't doubt that. But to formally prove that this leads to unique parsing requires unnecessary technical work that mathematicians prefer to avoid because the exact coding scheme doesn't matter.
> Any system less powerful than PA is trivially incomplete.
That is false. See here for examples of complete theories, for which Gödel's incompleteness theorems don't apply because they are not strong enough: https://en.m.wikipedia.org/wiki/Complete_theory
(Moreover, there are theories that are neither stronger nor weaker than PA. One such theory can give rise to an interesting proof of consistency of PA: https://en.m.wikipedia.org/wiki/Gentzen%27s_consistency_proo...)
Of course, you can encode any sequence of ASCII codes as a number (just concatenate the binary digits), I didn't doubt that. But to formally prove that this leads to unique parsing requires unnecessary technical work that mathematicians prefer to avoid because the exact coding scheme doesn't matter.
> Any system less powerful than PA is trivially incomplete.
That is false. See here for examples of complete theories, for which Gödel's incompleteness theorems don't apply because they are not strong enough: https://en.m.wikipedia.org/wiki/Complete_theory
(Moreover, there are theories that are neither stronger nor weaker than PA. One such theory can give rise to an interesting proof of consistency of PA: https://en.m.wikipedia.org/wiki/Gentzen%27s_consistency_proo...)
> Why does that matter? This seems to me like an interesting bit of trivia about Robinson arithmetic, but I don't see why this matters to the main point. Any system less powerful than PA is trivially incomplete.
Isn't this backwards? Systems that are simple enough (e.g. Presburger arithmetic) are complete, which is what we'd expect.
Isn't this backwards? Systems that are simple enough (e.g. Presburger arithmetic) are complete, which is what we'd expect.
I guess I should have been more precise: trivially incomplete with respect to truths about numbers, which is the thing we actually care about.
It is trivial to construct a complete system that is completely (!) uninteresting. The empty system is complete with respect to its own theorems, of which there are none, but that is about as uninteresting as it gets.
The interesting thing is that as soon as you get a system that is sufficiently expressive to capture even an elementary subset of what we would consider "truths about numbers" that system is necessarily incomplete, and it cannot be made complete by making it more powerful. That is the interesting thing, and proving it does not depend (AFAICT) on the details of any particular encoding of truths about numbers as long as it is well defined.
It is trivial to construct a complete system that is completely (!) uninteresting. The empty system is complete with respect to its own theorems, of which there are none, but that is about as uninteresting as it gets.
The interesting thing is that as soon as you get a system that is sufficiently expressive to capture even an elementary subset of what we would consider "truths about numbers" that system is necessarily incomplete, and it cannot be made complete by making it more powerful. That is the interesting thing, and proving it does not depend (AFAICT) on the details of any particular encoding of truths about numbers as long as it is well defined.
> It is trivial to construct a complete system that is completely (!) uninteresting.
It's also easy enough to construct complete theories that are rather interesting.
> That is the interesting thing, and proving it does not depend (AFAICT) on the details of any particular encoding of truths about numbers as long as it is well defined.
No, the encoding scheme doesn't matter, that's correct.
What does matter is that the theory doesn't need to be as powerful as a full-blown Turing machine. That's why all the machinery about Gödel's proof is necessary.
You seem to be mistaken about the fact that Gödel numbering is the complicated part about that proof, when that is in fact the easy part (and, if you really want, can be entirely replaced by some other encoding scheme), and the complicated part is about proving that a relatively weak theory like Robinson arithmetic, which doesn't even have induction axioms, can nevertheless completely express all primitive recursive functions, and that predicates such as "x is a proof of y" can be expressed as primitive recursive functions.
It's also easy enough to construct complete theories that are rather interesting.
> That is the interesting thing, and proving it does not depend (AFAICT) on the details of any particular encoding of truths about numbers as long as it is well defined.
No, the encoding scheme doesn't matter, that's correct.
What does matter is that the theory doesn't need to be as powerful as a full-blown Turing machine. That's why all the machinery about Gödel's proof is necessary.
You seem to be mistaken about the fact that Gödel numbering is the complicated part about that proof, when that is in fact the easy part (and, if you really want, can be entirely replaced by some other encoding scheme), and the complicated part is about proving that a relatively weak theory like Robinson arithmetic, which doesn't even have induction axioms, can nevertheless completely express all primitive recursive functions, and that predicates such as "x is a proof of y" can be expressed as primitive recursive functions.
How exactly did you think "Any system less powerful than PA is trivially incomplete." conveyed any of this? You seem to be claiming two almost opposite things about PA.
> How exactly did you think "Any system less powerful than PA is trivially incomplete." conveyed any of this?
I thought it was understood that the word "incomplete" in the context of a discussion of Godel's Incompleteness Theorem meant incomplete with respect to the truths of arithmetic, because that is what Godel's Incompleteness Theorem is about. It didn't seem like a huge leap at the time.
> You seem to be claiming two almost opposite things about PA.
And those two things would be...?
I thought it was understood that the word "incomplete" in the context of a discussion of Godel's Incompleteness Theorem meant incomplete with respect to the truths of arithmetic, because that is what Godel's Incompleteness Theorem is about. It didn't seem like a huge leap at the time.
> You seem to be claiming two almost opposite things about PA.
And those two things would be...?
> incomplete with respect to the truths of arithmetic
This is not at all what it's about. First of all, "incompleteness" has a very specific meaning in logic, namely that the following conditional (what we call "completeness") does not hold hold for some formal system S:
[1] https://math.hawaii.edu/~dale/godel/godel.html
This is not at all what it's about. First of all, "incompleteness" has a very specific meaning in logic, namely that the following conditional (what we call "completeness") does not hold hold for some formal system S:
Γ ⊨ φ → Γ ⊢ φ
[1] https://math.hawaii.edu/~dale/godel/godel.html
> This is not at all what it's about. First of all, "incompleteness" has a very specific meaning in logic, namely that the following conditional (what we call "completeness") does not hold hold for some formal system S:
> Γ ⊨ φ → Γ ⊢ φ
That is, unfortunately, a misunderstanding because the words "(in)completeness" have two very distinct meanings that are both used in logic.
One is the completeness of some system of logic, namely what you mentioned: "Γ ⊨ φ → Γ ⊢ φ". That's provably true for fist-order logic (though not for second-order logic), giving rise to Gödel's completeness proof. It remains true when Γ = PA (more specifically, first-order PA). In other words, any truth about numbers that follows from PA has a proof.
When we talk about the incompleteness theorems, however, we're talking about the completeness of theories. A theory Γ is said to be complete whenever for all sentences we have either Γ ⊨ φ or Γ ⊨ ¬φ. While there are examples of complete theories (I linked the Wiki article in a comment more up-thread, but it includes simple examples like the theory of dense linear orders sets with endpoints), it is also easy enough to construct a theory that is not complete. In particular (and this follows from the first incompleteness theorem), first-order PA is not complete. What this also implies is that not every true statement about the natural numbers follows from PA, or equivalently, that there are models of PA, i.e. structures in which all axioms of (again, first-order) PA are true, that are nevertheless distinct from the natural numbers because some sentences that are true in the one structure are false in the other.
More precisely, the first incompleteness theorem states something like "any effectively axiomatisable theory that is sufficiently strong is incomplete", where "effectively axiomatisable" means that we can determine in finite time whether something is an axiom of that theory, and "sufficiently strong" means something like "can encode every primitive recursive function" (the exact formulation depends a bit, because there are several different "flavours" of the first incompleteness theorem). In particular, it also states that any theory that includes Robinson arithmetic (e.g. PA) is incomplete.
> Γ ⊨ φ → Γ ⊢ φ
That is, unfortunately, a misunderstanding because the words "(in)completeness" have two very distinct meanings that are both used in logic.
One is the completeness of some system of logic, namely what you mentioned: "Γ ⊨ φ → Γ ⊢ φ". That's provably true for fist-order logic (though not for second-order logic), giving rise to Gödel's completeness proof. It remains true when Γ = PA (more specifically, first-order PA). In other words, any truth about numbers that follows from PA has a proof.
When we talk about the incompleteness theorems, however, we're talking about the completeness of theories. A theory Γ is said to be complete whenever for all sentences we have either Γ ⊨ φ or Γ ⊨ ¬φ. While there are examples of complete theories (I linked the Wiki article in a comment more up-thread, but it includes simple examples like the theory of dense linear orders sets with endpoints), it is also easy enough to construct a theory that is not complete. In particular (and this follows from the first incompleteness theorem), first-order PA is not complete. What this also implies is that not every true statement about the natural numbers follows from PA, or equivalently, that there are models of PA, i.e. structures in which all axioms of (again, first-order) PA are true, that are nevertheless distinct from the natural numbers because some sentences that are true in the one structure are false in the other.
More precisely, the first incompleteness theorem states something like "any effectively axiomatisable theory that is sufficiently strong is incomplete", where "effectively axiomatisable" means that we can determine in finite time whether something is an axiom of that theory, and "sufficiently strong" means something like "can encode every primitive recursive function" (the exact formulation depends a bit, because there are several different "flavours" of the first incompleteness theorem). In particular, it also states that any theory that includes Robinson arithmetic (e.g. PA) is incomplete.
> I thought it was understood that the word "incomplete" in the context of a discussion of Godel's Incompleteness Theorem meant incomplete with respect to the truths of arithmetic, because that is what Godel's Incompleteness Theorem is about.
What does "with respect to the truths of arithmetic" even mean? How is Presburger Arithmetic "incomplete" in this sense?
> And those two things would be...?
That it's so complex as to be obviously incomplete, but also so simple that anything smaller than it is obviously trivial. There are interesting systems smaller than PA, and none of this is obvious.
What does "with respect to the truths of arithmetic" even mean? How is Presburger Arithmetic "incomplete" in this sense?
> And those two things would be...?
That it's so complex as to be obviously incomplete, but also so simple that anything smaller than it is obviously trivial. There are interesting systems smaller than PA, and none of this is obvious.
> What does "with respect to the truths of arithmetic" even mean?
It means: with respect to some axiomatization of arithmetic that allows Godel numbers to be constructed. Peano arithmetic, for example.
> obviously incomplete
I guess that depends on what you consider "obvious". It was far from obvious before Godel proved it. But nowadays it's not hard to understand. One generation's "obvious" is a prior generation's major breakthrough.
The big surprise in Godel's theorem is that the amount of complexity you need to introduce into a theory to render it incomplete is quite small. Peano arithmetic is sufficient, but not necessary.
It means: with respect to some axiomatization of arithmetic that allows Godel numbers to be constructed. Peano arithmetic, for example.
> obviously incomplete
I guess that depends on what you consider "obvious". It was far from obvious before Godel proved it. But nowadays it's not hard to understand. One generation's "obvious" is a prior generation's major breakthrough.
The big surprise in Godel's theorem is that the amount of complexity you need to introduce into a theory to render it incomplete is quite small. Peano arithmetic is sufficient, but not necessary.
ASCII has 7 bits
ASCII encodes strings as powers of 128.
:-D
Otherwise seems legit
ASCII encodes strings as powers of 128.
:-D
Otherwise seems legit
Isn't it circular logic? B=H(B) - if circular logic doesn't work, why would it mean that some unrelated function H doesn't exist?
Simplified proof: assume H exists, then consider equation 1=0, it's a contradiction, therefore the assumption is false and H doesn't exist.
Simplified proof: assume H exists, then consider equation 1=0, it's a contradiction, therefore the assumption is false and H doesn't exist.
But 1=0 is not a contradiction, it is simply false. All contradictions are false, but not all false statements are contradictions.
But that is neither here nor there. What matters is that a provably false statement (in this case a contradiction, but that doesn't really matter) follows from some assumption, and therefore the assumption must be false. This is not circular reasoning, it is proof by reductio ad absurdum (https://en.wikipedia.org/wiki/Reductio_ad_absurdum).
But that is neither here nor there. What matters is that a provably false statement (in this case a contradiction, but that doesn't really matter) follows from some assumption, and therefore the assumption must be false. This is not circular reasoning, it is proof by reductio ad absurdum (https://en.wikipedia.org/wiki/Reductio_ad_absurdum).
That's a standard proof by contradiction. Make an assumption, derive a contradiction, the conclusion is that the assumption must be wrong.
There's indeed an extra assumption in here, namely that we can write a program such as B that runs on "itself". That's not difficult to see though, if we think in terms of Turing Machines (or an actual computer with memory, for that matter).
I think the given proof is essentially correct.
There's indeed an extra assumption in here, namely that we can write a program such as B that runs on "itself". That's not difficult to see though, if we think in terms of Turing Machines (or an actual computer with memory, for that matter).
I think the given proof is essentially correct.
Circular logic is a known source of paradoxes, it's difficult to assume it to be a priori correct.
I don't think you know how circular logic, or proof by contradictions work.
If you could indeed derive 1=0 from H, then that would indeed by reason to dismiss H, but you can't just "consider" 1=0, you have to prove it from H.
If you could indeed derive 1=0 from H, then that would indeed by reason to dismiss H, but you can't just "consider" 1=0, you have to prove it from H.
That's the point, B=H(B) doesn't follow from H, it's a new independent construct, so you need an independent proof of its validity.
If you've managed to prove the halting problem, then I don't think it is cheating to use it on an easier result.
This is how it was taught when I learned CS theory in uni [0]
[0]: https://introtcs.org/public/lec_09_godel.html
This is how it was taught when I learned CS theory in uni [0]
[0]: https://introtcs.org/public/lec_09_godel.html
Further, there just isn’t “cheating” in a proof. Being able to do a demonstration yet another way just illuminates the phenomena all the better.
You might know something if you know one way to do it. You have a much better understanding if you have two ways. Three and your understanding is probably pretty solid. Etc
Edit of to if, damn autocorrect
You might know something if you know one way to do it. You have a much better understanding if you have two ways. Three and your understanding is probably pretty solid. Etc
Edit of to if, damn autocorrect
> Proving Godel's first incompleteness theorem (don't even get me started on the second) from first principles is actually much more involved; and certainly more difficult to make it intelligible for non-logicians.
I remember having to do it for my logic class final exam. I wouldn't remember exactly how to do it today though.
The little click sounds on the linked page are unfortunate. I had to stop after like 20 seconds.
I remember having to do it for my logic class final exam. I wouldn't remember exactly how to do it today though.
The little click sounds on the linked page are unfortunate. I had to stop after like 20 seconds.
IMO It's cool to invoke the lean halting theorem, since the author proves the informal version of the halting theorem in the previous lesson.
See: https://tigyog.app/d/fr9uub3hqgab/r/the-halting-problem
See: https://tigyog.app/d/fr9uub3hqgab/r/the-halting-problem
[deleted]
A math prof had a brilliant blog and one of the subjects he covered was Gödel's incomepleteness theorems. I really loved his style (and his wife's illustrations). Too bad he stopped posting.
https://infinityplusonemath.wordpress.com/2017/07/22/kurt-go...
https://infinityplusonemath.wordpress.com/2017/08/04/godels-...
https://infinityplusonemath.wordpress.com/2017/09/04/how-god...
https://infinityplusonemath.wordpress.com/2017/07/22/kurt-go...
https://infinityplusonemath.wordpress.com/2017/08/04/godels-...
https://infinityplusonemath.wordpress.com/2017/09/04/how-god...
Using the halting problem here shows the consequences of the incompleteness theorem pretty well, but I don't think it explains it. This is basically hiding the self-references behind the halting problem black box.
I really like this video for explaining it, I find it very funny and approachable: https://www.youtube.com/watch?v=WylL1m4K6Bk
I really like this video for explaining it, I find it very funny and approachable: https://www.youtube.com/watch?v=WylL1m4K6Bk
> Will the string "(n : nat) : 0 + n = n" appear in this list?
No, because the given alphabet does not contain the space character ...
No, because the given alphabet does not contain the space character ...
Thank you for your precise eyes! Fixed!
Similar nit, when you ask "Will theorems() discover `theorem halting_problem (n) :
¬ computable_pred (λ c, ..."
I don't believe it will since `const alphabet` does not contain λ or ¬. Apart from my very slight indignance after answering that one incorrectly, loved the article! :)
I don't believe it will since `const alphabet` does not contain λ or ¬. Apart from my very slight indignance after answering that one incorrectly, loved the article! :)
Great tutorial, by the way!
There is another typo in one of the javascript functions, where you should write "return t;" instead of "return thm;"
There is another typo in one of the javascript functions, where you should write "return t;" instead of "return thm;"
Yes, this is in the definition of theorems().
I think there's either a mistake or a very very large omission here. It starts here:
>This is looking better! We have an amazing function, is_statement_true, that can tell us whether anything is true or false, given enough time!
>Read it through, and try to prove to yourself that is_collatz_true really does eventually return the truth of the Collatz conjecture.
Namely, I think the author confuses Lean theorems and metatheory theorems, where when I say metatheory, I mean the language and the system we use to talk about lean, about Godel's incompleteness theorem, and everything else - basically, the English-math language in which the chapter is written. Hence, it's wrong to say that is_statement_true can tell us whether any statement is true - it can merely tell us which of the two options it is: the statement is a theorem of Lean or its negation is a theorem of Lean. Same for is_collatz_true - sure, it must tell us what Lean thinks about the Collatz conjecture but doesn't tell us anything about the truth or falsity of the Collatz conjecture.
And finally, in the very end of Chapter 2, this problem arises as well. The chapter says that if Lean is sound and complete, then we can define a function which, for any Turing machine, returns one of two options: Lean thinks it halts, or Lean thinks it doesn't halt. But we haven't proved that what Lean thinks about that had anything to do with whether it actually halts or not.
>This is looking better! We have an amazing function, is_statement_true, that can tell us whether anything is true or false, given enough time!
>Read it through, and try to prove to yourself that is_collatz_true really does eventually return the truth of the Collatz conjecture.
Namely, I think the author confuses Lean theorems and metatheory theorems, where when I say metatheory, I mean the language and the system we use to talk about lean, about Godel's incompleteness theorem, and everything else - basically, the English-math language in which the chapter is written. Hence, it's wrong to say that is_statement_true can tell us whether any statement is true - it can merely tell us which of the two options it is: the statement is a theorem of Lean or its negation is a theorem of Lean. Same for is_collatz_true - sure, it must tell us what Lean thinks about the Collatz conjecture but doesn't tell us anything about the truth or falsity of the Collatz conjecture.
And finally, in the very end of Chapter 2, this problem arises as well. The chapter says that if Lean is sound and complete, then we can define a function which, for any Turing machine, returns one of two options: Lean thinks it halts, or Lean thinks it doesn't halt. But we haven't proved that what Lean thinks about that had anything to do with whether it actually halts or not.
He skips connecting it with model theory by choosing statements where it is clear what they mean (collatz conjecture, halting problem). I think that's OK.
It's not clear to me that model theory has much to say about Lean; do you have any resources on this? plato.stanford.edu does hedge that while modern model theory focuses on first-order logic, there's a broader sense of model theory which can be used to study even natural languages. But if you try to study type theory as natural language statements you aren't going to get much out of it. Going about it that way, the models you'll come up with are going to be of the form "doing some formal symbol manipulation X has certain formal symbol results Y" which will be neither illuminating nor useful. I did find an abstract[0] which claims that model theory has historical roots in type theory but I'm doubtful I have any way to access it.
[0] https://www.cambridge.org/core/journals/bulletin-of-symbolic...
[0] https://www.cambridge.org/core/journals/bulletin-of-symbolic...
First you have to see that the tutorial uses Lean basically as a blackbox. All that is needed is that you can express proofs in it, that applying lean to proofs yields lean theorems, that proofs are enumerable, and that Lean is powerful enough to express the collatz conjecture and the halting problem. So you can replace Lean by any other such blackbox B, for example B = (first-order logic + ZFC), and the argument in the tutorial goes the same way. Therefore type theory or not is not an issue here.
What IS an issue is that to fully explain what "express the collatz conjecture in B" means, you need model theory. You are right, type theory often doesn't come with model theoretic semantics, but it can be done in a natural way even for type theories.
The paper you are referencing is on sci-hub, by the way: http://sci-hub.wf/10.1017/S1079898600010568
What IS an issue is that to fully explain what "express the collatz conjecture in B" means, you need model theory. You are right, type theory often doesn't come with model theoretic semantics, but it can be done in a natural way even for type theories.
The paper you are referencing is on sci-hub, by the way: http://sci-hub.wf/10.1017/S1079898600010568
> But we haven't proved that what Lean thinks about that had anything to do with whether it actually halts or not.
Well I can tell you if it actually halts: it does. By the time of the heat-death of the universe, all computers will have stopped running, so the halting problem is quite solvable.
But the halting problem, and the Collatz conjecture, and all mathematical truth, is fundamentally embedded inside of systems of formal logic. Gödel's Incompleteness Theorem doesn't say anything about systems of truth outside of formal mathematical logic. So this result isn't relevant to Physics, for example.
However, Gödel's Theorem, and this proof, don't rely on any particular qualities of the formal system, other than the ability to enumerate proofs (and other things that we think of as inherit to logic). So this proof applies not just to Lean, but also to every method of proving things in math.
Well I can tell you if it actually halts: it does. By the time of the heat-death of the universe, all computers will have stopped running, so the halting problem is quite solvable.
But the halting problem, and the Collatz conjecture, and all mathematical truth, is fundamentally embedded inside of systems of formal logic. Gödel's Incompleteness Theorem doesn't say anything about systems of truth outside of formal mathematical logic. So this result isn't relevant to Physics, for example.
However, Gödel's Theorem, and this proof, don't rely on any particular qualities of the formal system, other than the ability to enumerate proofs (and other things that we think of as inherit to logic). So this proof applies not just to Lean, but also to every method of proving things in math.
> Well I can tell you if it actually halts: it does. By the time of the heat-death of the universe, all computers will have stopped running, so the halting problem is quite solvable.
This is wrong - see Dyson's eternal intelligence.
This is wrong - see Dyson's eternal intelligence.
I know this proof is not as rigorous as some mathematicians would like, but it helped me a lot to understand a concept that I've failed to understand all my life, at least at an intuitive level. So thank you very much for sharing!
Never come across TigYog. Seems pretty cool: https://tigyog.app/
Yes. There must be a Javascript framework for creating this type of interactive training. Does anyone know of one?
Hi! TigYog.app actually started out as an attempt at building something like a JS framework for this. But it's evolved into a platform. Here are some reasons why ...
- The "gradually revealed content" flow tends to require full control over the page. See by contrast https://quantum.country/ which uses https://withorbit.com/, which is more like a framework. For that reason, it's quite restricted in what it can do in terms of flow control.
- Tracking progress - you can just save answers client-side, but I wanted something that would allow users to sign on their mobile and continue from wherever they were on the desktop, etc. This also enables flashcard-style spaced repetition emails (future feature)
- Saving answers while being able to edit the page requires that you have stable identifiers for all questions and buttons. The WYSIWYG does that for you.
- I wanted it to feel like blogging, or traditional writing, rather than coding.
All that said - I'm thinking about ways to open up TigYog for more like framework-style creation. Email me if you're interested!
- The "gradually revealed content" flow tends to require full control over the page. See by contrast https://quantum.country/ which uses https://withorbit.com/, which is more like a framework. For that reason, it's quite restricted in what it can do in terms of flow control.
- Tracking progress - you can just save answers client-side, but I wanted something that would allow users to sign on their mobile and continue from wherever they were on the desktop, etc. This also enables flashcard-style spaced repetition emails (future feature)
- Saving answers while being able to edit the page requires that you have stable identifiers for all questions and buttons. The WYSIWYG does that for you.
- I wanted it to feel like blogging, or traditional writing, rather than coding.
All that said - I'm thinking about ways to open up TigYog for more like framework-style creation. Email me if you're interested!
One way to think of incompleteness/halting is that the future is not computable. Meaning that to see the result of some symbolic/computational process you have to actually run the program and there is no shortcut to making a prediction one way or the other if we want to know for certain what the result would actually be.
There is something called abstract interpretation that can tell you what the result of some computation will be but by necessity it can only be an approximation because it must halt in some finite amount of time. Type systems are a good example of abstract interpretation because type systems assign a logical/mathematical semantics to code and allow one to determine in a finite amount of time whether some code is logically coherent according to the rules of the type system.
The larger philosophical implication of all this is that symbolic/computational models of reality are always approximations. Whatever one can know for certain has either already happened and is in the past or there is some symbolic model/approximation which must necessarily have some degree of uncertainty and error.
The tutorial itself is pretty cool. Props to the author for putting it together.
There is something called abstract interpretation that can tell you what the result of some computation will be but by necessity it can only be an approximation because it must halt in some finite amount of time. Type systems are a good example of abstract interpretation because type systems assign a logical/mathematical semantics to code and allow one to determine in a finite amount of time whether some code is logically coherent according to the rules of the type system.
The larger philosophical implication of all this is that symbolic/computational models of reality are always approximations. Whatever one can know for certain has either already happened and is in the past or there is some symbolic model/approximation which must necessarily have some degree of uncertainty and error.
The tutorial itself is pretty cool. Props to the author for putting it together.
Well the correct statement would be "to know the result of ANY computational process, in some cases you would have to run it".
For instance, there are many "simple programs" for which you can give the results by way of formal methods without running them. The incompleteness theorem says that there will exist one program for which you can't.
For instance, there are many "simple programs" for which you can give the results by way of formal methods without running them. The incompleteness theorem says that there will exist one program for which you can't.
It says something more than that. There are necessarily infinitely many programs like that.
Even if you can predict halting (which for the large class of decidable problems you can) you still have to run the computation to see the results.
To me it's more about the expressiveness of languages.
To me it's more about the expressiveness of languages.
> But the same reasoning can be applied to any formal system F, with fairly minimal assumptions:
Strictly speaking, F has to be satisfiable/consistent as well. {P, ~P} is a trivially recursively enumerable, complete theory which contains Q.
Strictly speaking, F has to be satisfiable/consistent as well. {P, ~P} is a trivially recursively enumerable, complete theory which contains Q.
You get this for free in (2). You couldn't "reason about programs" if F were inconsistent, nor would the halting problem make any sense in an inconsistent system.
I would argue "reasoning about programs" formally means "can prove P Q R ..." (with appropriate choices for P Q R) and doesn't implicitly carry an assumption of consistency. But, fair enough.
You make a good point, and on the other hand you're right that "reasoning about programs" is not a term of art, so who knows what it means. Given how Lean is used in the article, I took it as basically being some kind of Turing-complete language (lambda-calculus or some variant or what-not).
I think you can explain incompleteness without forcing readers to learn a prooflang
The section header "Theorem mining — better than crypto?" makes me wonder: instead of POW based cryptocurrencies, could we use POT(Proof of Theorem)? Machines could grind away looking for theorems. It's still a POW method, but it provides some potentially useful output.
This wouldn't work because all theorems are trivially extensible. Either by adding extra theorems via conjunction, e.g. my new theorem C = previously-mined theorems {A} ∪ {B}; or by adding garbage to the end, e.g my new theorem C = {A} ∪ {...arbitrary nonsense that cancels out}, e.g. (+ 0 + 0 + 0), or (- 1 + 1 - 1 + 1), or vastly more complex formulations.
Logic isn't the study of merely finding out what's true, but what's true and interesting.
Logic isn't the study of merely finding out what's true, but what's true and interesting.
It's only useful if the theorems proven are interesting. Maybe there could be a cryptocurrency for mathematicians where you post theorem statements and put money in them. First one to find a proof gets whatever money was in the theorem.
The way blockchain works is that you generate a problem based on the contents of the block. If the proof you find is in no way related to a block it cannot be a cryptocurrency.
You could make a system to reward people for finding proofs, but it would be more of a Bounty system or a Leaderboard than a cryptocurrency. Indeed people do put up prizes for those kind of things today.
You could make a system to reward people for finding proofs, but it would be more of a Bounty system or a Leaderboard than a cryptocurrency. Indeed people do put up prizes for those kind of things today.
Most useful proof-of-work yet...
However, it is somewhat hard to mathematically define all criteria used to recognize *useful* theorem.
There may be many propositions that are true, but cause no excitement among mathematicians.
However, it is somewhat hard to mathematically define all criteria used to recognize *useful* theorem.
There may be many propositions that are true, but cause no excitement among mathematicians.
You have to know in advance about how long it will take to mine the next block. Is it possible to do it here? Probably not.
Proof of... proof?
Is the essential similarity of the key trick in Godel's incompleteness theorem and the Y combinator well known? I finally "got" the incompleteness theorem when that relationship dawned on me. As a cute entry point, consider the standard lambda term with no normal form, "(lambda x. (x x)) (lambda x. (x x))". Now consider the Godel formula "Substitute(F, n)", which takes a number F, the Godel number of a formula with a single free variable, and another number n. It simplifies to a number M which is the Godel number of the formula F with n replacing all instances of its free variable. One might interpret F as function-like, in the sense that for any number n, F [free_var := n] simplifies to some other number m. So now consider "Substitute(F, F)", which is suggestive of "(x x)" in lambda notation. Let M be the Godel number of this formula, which has one free variable. Finally, use an analogy to the above self-referential lambda term to create the formula G, defined as "Substitute(M, M)". To what number does this arithmetic formula with no free variables simplify? The delightful answer is that it simplifies to its own Godel number! Just as it is a short step from the above simple self-referential lambda term to the Y combinator, so it is a short step from the above fact to the standard Godel formula for which neither it nor its negation has a proof.
I’ve always thought that the completeness theorem was more interesting.
Also I really like approaching this from Lawvere’s fixed point theorem. https://ncatlab.org/nlab/show/Lawvere's+fixed+point+theorem
I have been thinking about some of this stuff
https://github.com/adamnemecek/adjoint
Join the discord https://discord.gg/mr9TAhpyBW
Also I really like approaching this from Lawvere’s fixed point theorem. https://ncatlab.org/nlab/show/Lawvere's+fixed+point+theorem
I have been thinking about some of this stuff
https://github.com/adamnemecek/adjoint
Join the discord https://discord.gg/mr9TAhpyBW
I love the fact that it's interactive. Wish more articles were written that way. It was also relatively easy for me to follow up till "Consistency":
> But what if theorems() contains both coll_conj and ¬coll_conj? Is that possible?
> ...
> But in general, a formal system can have both S and ¬S as theorems.
Is there an intuitive explanation for this?
> But what if theorems() contains both coll_conj and ¬coll_conj? Is that possible?
> ...
> But in general, a formal system can have both S and ¬S as theorems.
Is there an intuitive explanation for this?
Formal systems need not be consistent; if a formal system assumes both P and ~P as axioms, you can derive S and ~S (for any S) by explosion.
Is the problem that you can't proof consistency? Because if it's consistent then shouldn't either P or ~P be true or the axiom doesn't exist?
It is possible to prove consistency but to do so requires using a more powerful system of axioms which in turn might be inconsistent. What Goedel showed is that in any system that can encode arithmetic (and consequently some notion of computation, e.g. lambda calculus) can not be complete if it is consistent.
Ah, thank you, that makes more sense. Maybe a weird follow-up question: Is it possible (or does it make sense) to find a proof in an inconsistent system and to try to "transform" it into a consistent one?
Yes, paraconsistent logic could be considered an instance of such a system: https://en.wikipedia.org/wiki/Paraconsistent_logic.
[deleted]
By Gödel incompleteness, the fundamental axioms of mathematics actually don't quite pin down the world of mathematics the way we would perhaps like them to do. As a consequence (also a result by Gödel), there are actually many worlds of mathematics, each spelling out the basic notions of mathematics in slightly different ways.
I tried to survey this multiverse philosophy here: https://iblech.gitlab.io/bb/multiverse.html
I tried to survey this multiverse philosophy here: https://iblech.gitlab.io/bb/multiverse.html
What are “the fundamental axioms of mathematics”?
I am sorry, I was being sloppy there.
There are several systems of axioms we can use to base mathematics on.
A common such is ZFC, Zermaelo–Fraenkel set theory with the axiom of choice. Among its axioms are assertions like "there is a set which is empty", "there is an infinite set" and "if A and B, then in particular A".
Another is Martin-Löf type theory in one of its flavors, perhaps homotopy type theory.
There are several systems of axioms we can use to base mathematics on.
A common such is ZFC, Zermaelo–Fraenkel set theory with the axiom of choice. Among its axioms are assertions like "there is a set which is empty", "there is an infinite set" and "if A and B, then in particular A".
Another is Martin-Löf type theory in one of its flavors, perhaps homotopy type theory.
The assumption of this theorem is that we may encode any problem that is unbounded and infinite. What if we limit ourselves to *bounded* and *computable* functions only?
See draft presented at many top logic conferences yet: https://arxiv.org/abs/2106.13309
Since the observable universe is bounded, and we are most interested in computable, why not to focus on maths that is most relevant to our universe instead of infinitary alternate?
See draft presented at many top logic conferences yet: https://arxiv.org/abs/2106.13309
Since the observable universe is bounded, and we are most interested in computable, why not to focus on maths that is most relevant to our universe instead of infinitary alternate?
> So, even though 1+1=3 is surely false, we could prove it in Lean like so: “Let’s assume that ¬(1+1=3). But this leads to a contradiction: coll_conj and ¬coll_conj. We can therefore deduce that our assumption must be false, so 1+1=3.”
I was following along with the logic, but got completely lost here. Can anyone explain how does the assumption "1 plus 1 is equal to three is false" lead to a contradiction? What is the contradiction here exactly?
I was following along with the logic, but got completely lost here. Can anyone explain how does the assumption "1 plus 1 is equal to three is false" lead to a contradiction? What is the contradiction here exactly?
It doesn't lead to a contradiction, the contradiction was already there. If you have a contradiction on your system you can prove everything:
1- Assume ¬X
2- Point out the contradiction
3- Therefore X is true
1- Assume ¬X
2- Point out the contradiction
3- Therefore X is true
How and why does a specific contradiction "coll_conj and ¬coll_conj" apply to all possible conjectures?
If your system of logic contains a contradiction, then it can be said that any statement in that system "leads to" a contradiction. Thus "proof by contradiction" can prove any statement in that system.
Trying to find a formal system that encodes unbounded infinitary mathematical objects including most of maths, but yet to require that all statements are decidable within a finite number of steps...
Is it contradiction in the proof, or rather a contradiction in assumptions?
More on logic that permits all that *Bounded* Turing Machine does: https://arxiv.org/abs/2106.13309
Is it contradiction in the proof, or rather a contradiction in assumptions?
More on logic that permits all that *Bounded* Turing Machine does: https://arxiv.org/abs/2106.13309
> then it can be said that any statement in that system "leads to" a contradiction
Why exactly it "leads to"? I don't get it.
Why system can't have a contradiciton for one set of inputs, and not have it for others?
Why exactly it "leads to"? I don't get it.
Why system can't have a contradiciton for one set of inputs, and not have it for others?
One is the only number. Zero isn't one. n cannot equal anything other than n; adding anything else is what's creating the inconsistency and incompleteness. n must equal n. But, if that's true - which it is - the game is over and math is just a game of never ending bifurcations.
Rather Borgesian I think.
returning null for false and the string itself for true, lol,
"mike-drop" should be "mic-drop"
I don't object grammar fascism, and I see the visual beauty of "mic-drop", but mike as a shortened form of microphone is well-established. "The talk show guest was miked up and ready to go on stage."
kind of like bicycle and bike
kind of like bicycle and bike
mike as a shortened form of microphone is well-established.
mike is, sometimes, but 'mike drop' for 'mic drop', not so much. But for even more pedantry, that would be spelling rather than grammar pedantry.
mike is, sometimes, but 'mike drop' for 'mic drop', not so much. But for even more pedantry, that would be spelling rather than grammar pedantry.
well if we are delving into pedantry, natural language is spoken; we learn our native language as pre-literate children and we already have our vocabulary stored in our brains with phonetic features way before we learn to read and write. Orthography is thus but a facsimile of our language.
We exchange and learn new words primarily by hearing them, and I'll bet "drop the mike" was first uttered out loud by a comedian/entertainer type, and to say that it even had a spelling is an unjustified leap.
We exchange and learn new words primarily by hearing them, and I'll bet "drop the mike" was first uttered out loud by a comedian/entertainer type, and to say that it even had a spelling is an unjustified leap.
I don't think any of these are true (that this particular argument constitutes or delves into pedantry, what 'natural language' is, etc) but we've probably extracted what pedantifun was to be had already.
[deleted]
[deleted]
> Gödel’s original proof was slightly stronger
Technically speaking, a lot stronger. Proving Godel's first incompleteness theorem (don't even get me started on the second) from first principles is actually much more involved; and certainly more difficult to make it intelligible for non-logicians.