Cool page, though the Halting Problem brings with it a lot of stuff, so using it to prove Godel's first incompleteness theorem is (imo) a bit like cheating. I've proven it before using diagonalization on my blog (but also using concepts like computability for free). At the end of the day, using these ideas, you get the Curry–Howard correspondence for free (which, again, is a bit like cheating).
> 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.
> 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.
> 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.
> 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.
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.
> 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.
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
> 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.
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.
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.
> 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:
Γ ⊨ φ → Γ ⊢ φ
Second of all, Godel's first incompleteness theorem doesn't concern itself with "truths of arithmetic" but about any sufficently-powerful logical formalism. This is why I contend that Godel numbering is actually where the trickery kind of comes in: it's what gives Godel the self-referrentiality he needs in PA. A more general definition of the theorem, and one I generally favor over ones that bring up arithmetic, is[1]: "Any adequate axiomatizable theory is incomplete. In particular the sentence 'This sentence is not provable' is true but not provable in the theory."
> 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.
> A theory Γ is said to be complete whenever for all sentences we have either Γ ⊨ φ or Γ ⊨ ¬φ.
You mean Γ ⊢ φ or Γ ⊢ ¬φ .
But note that what you said is not mutually exclusive with what /u/Tainnor said, i.e.
Γ ⊨ φ → Γ ⊢ φ
The proof of Godel's theorem is to exhibit a φ for which "Γ ⊢ φ or Γ ⊢ ¬φ" is false. From that you conclude that "Γ ⊨ φ → Γ ⊢ φ" is false on the assumption that "Γ ⊨ φ" is true. But that last part is an informal argument. We believe that "Γ ⊨ G" is true for the Godel sentence G but we (obviously) can't prove it.
Indeed, adding ¬G as an axiom to PA produces a consistent system where "Γ ⊢ G" is (trivially) true. The semantics of this system are quite interesting. The semantics of that system say that there exists a Godel number of a proof of G, but no natural number is that number. It is similar to adding axioms like "there exists a number whose successor is zero" or "there exists a number whose square root is the number whose successor is zero", which have obviously been very fruitful extensions of PA.
In principle no, though it's possible that it's defined like that in certain places, since in first-order logic, that amounts to the same thing (given the completeness theorem). But "completeness" is a notion from model theory that doesn't care about proof systems.
In a system where the completeness theorem is not true, such as second-order logic with standard semantics, we do have complete theories (such as second-order PA), where we always have Γ ⊨ φ or Γ ⊨ ¬φ, but that doesn't mean that every statement is either provable or disprovable.
> The proof of Godel's theorem is to exhibit a φ for which "Γ ⊢ φ or Γ ⊢ ¬φ" is false. From that you conclude that "Γ ⊨ φ → Γ ⊢ φ" is false on the assumption that "Γ ⊨ φ" is true. But that last part is an informal argument. We believe that "Γ ⊨ G" is true for the Godel sentence G but we (obviously) can't prove it.
I think that has it a bit backwards. It's not that we believe that PA ⊨ G - in fact, if we believed that, it would immediately imply PA ⊢ G, when that's exactly what we showed to be impossible. It's that we believe that G is true in the natural numbers, which is not the same thing as being true in PA, and that belief rests in our belief that PA is sound (which we can't prove, but seems reasonable).
(There are some different "flavours" of the incompleteness theorems, some of them rely on soundness of PA and others only on it being consistent.)
> But note that what you said is not mutually exclusive with what /u/Tainnor said, i.e.
Oh, sorry, I thought I was responding to the parent comment by /u/dvt
Let's go back to basics. To begin with, let's make sure we're on the same page with regards to notation.
"Γ ⊢ φ" means that the string φ is a theorem under Γ. This is a syntactic property of Γ. The claim that some sequence of strings P is a valid proof of φ (and that therefore Γ ⊢ φ is indeed true) can be verified mechanically.
"Γ ⊨ φ" means that the string φ is true under some model of Γ. This is a semantic property of Γ and it cannot be checked mechanically.
We want "Γ ⊨ φ → Γ ⊢ φ" to be true, that is, we would like it to be the case that for every statement φ that is true under some model of Γ, we can mechanically prove that φ is a theorem of Γ, i.e. we can show that there exists a P which is a proof of φ. If we have such a P in hand we can always check it, but if we don't have a P the question of whether or not one exists is generally an open one.
But we actually want more than that. We also want Γ to be "interesting" in some sense. There is no sport in coming up with uninteresting systems for which "Γ ⊨ φ → Γ ⊢ φ" is true. The obvious example is the empty system and a corresponding empty model where every φ is both false and not a theorem.
So we impose some minimal structure on Γ, not because the rules of formal systems demand it, but because systems where, say, P and ¬P are both false are not very interesting. So we demand that e.g. there exist at least one true statement and at least one false statement in our model, not because there is any cosmic rule that requires this, but simply because the whole enterprise becomes a pointless exercise in navel-gazing if we don't.
That raises the natural question: what is the minimal amount of structure we can impose on Γ to make it "interesting" and worthy of study. And there are many answers to this, because there are many possible things that are potentially "interesting". Propositional logic. Set theory. Yada yada yada.
The surprise is that it turns out that with only a very small amount of structure we lose "Γ ⊨ φ → Γ ⊢ φ". As with the imposition of structure in general in order to make systems interesting and worthy of study, there are many different ways in which to impose enough structure to lose this desirable property. One way, the way which historically was the first to be discovered, is to impose enough structure that the system can be modeled by the natural numbers. But this is not the only way. Another way is to impose enough structure that the system can be modeled by a simple machine consisting of a tape and a lookup table. Yet another way is to impose a structure that the system can be modeled by two urns that contain stones, and the ability to add and remove stones from the urns, and look in an urn to see if it is empty or not. There are many many variations on the theme.
All of these things turn out to be in some sense "equivalent", and because of that the details of the structure that we impose on the system are uninteresting. It doesn't matter if we use numbers or tapes or stones, there is a certain point beyond which we lose "Γ ⊨ φ → Γ ⊢ φ". And the big surprise is that the threshold is very, very low. It takes very little structure to cross the threshold. There are systems for which "Γ ⊨ φ → Γ ⊢ φ" does hold, but those are necessarily of very limited utility.
The proof of the falseness of "Γ ⊨ φ → Γ ⊢ φ" for any given system depends on the details of the system, but the general procedure is always the same: you produce a mapping from proofs to elements of the model. You then use that mapping to produce an element of the model (called G) which is true under the model if and only if there does not exist an element of the model corresponding to a proof of G under your mapping.
The key is the mapping from proofs to elements of the model, and Godel numbers were the first such map, but they are not the only such map, and there is nothing particularly special about them other than that they were the first to be discovered. They might have some advantages if you are actually writing out a detailed formal proof of Godel's theorem by hand, just as buggy whips can be useful if you are driving a horse and buggy. But there aren't many compelling reasons to do either one in today's world except as an exercise in nostalgia.
> "Γ ⊨ φ" means that the string φ is true under some model of Γ.
It means that φ is true in every model of Γ.[0]
> If we have such a P in hand we can always check it, but if we don't have a P the question of whether or not one exists is generally an open one.
> The surprise is that it turns out that with only a very small amount of structure we lose "Γ ⊨ φ → Γ ⊢ φ".
That is not true for first-order logic. In first order logic Γ ⊨ φ → Γ ⊢ φ is always true. That's the completeness theorem.[1] This really only starts to become false when you go to e.g. second-order logic, but first-order logic is really the most commonly used type of logic and plenty sufficient for almost all of mathematics (though that becomes a philosophical debate to some extent).
Gödel's theorem is really about first-order logic, and it says that even though completeness of FOL is a nice thing, it doesn't help us with the goal of finding an effective theory of the natural numbers (effective in the sense that proofs are mechanically verifiable).
That is not a definition of ⊨, that is a definition of logical implicature. Not the same thing.
The ⊨ symbol is defined in definition 1.7.4, and it is used in a different sense than we are using it here. The left-hand argument to the ⊨ operator in that book is a model (an "L-structure" using the book's terminology), not a theory. But Γ is a theory. So writing Γ ⊨ φ is fundamentally incompatible with the definition of ⊨ given in that book.
And our disagreement turns on this, at least in part, because one of the consequences of the incompleteness theorem is that there are models of PA (or RA or whatever your favorite axiomization of arithmetic happens to be) where G is true, and there are models where G is false.
> That is not true for first-order logic. In first order logic Γ ⊨ φ → Γ ⊢ φ is always true.
Only if you restrict what you mean by "first-order logic". Under some definition it is manifestly not true: any (first order) theory that includes arithmetic is incomplete.
> first-order logic is really the most commonly used type of logic and plenty sufficient for almost all of mathematics
Yes, and when you include arithmetic (or any of the other variants on that theme) it becomes incomplete.
> That is not a definition of ⊨, that is a definition of logical implicature. Not the same thing.
You should read that definition again. It's really hard to have a discussion if we can't agree on standard notation. The double turnstyle symbol has multiple uses (sad as it is), and when there is a structure on the LHS it means something different than when there is a set of formulas on the LHS. The second sense is defined in 1.9.1 and is based on the first sense.
> And our disagreement turns on this, at least in part, because one of the consequences of the incompleteness theorem is that there are models of PA (or RA or whatever your favorite axiomization of arithmetic happens to be) where G is true, and there are models where G is false.
This is true.
> any (first order) theory that includes arithmetic is incomplete.
That is basically true, assuming that the theory is also sound (because we can construct unsound complete theories of arithmetic), and if by "arithmetic" we mean "addition and multiplication" (otherwise, see Presburger Arithmetic).
Gödel's First Incompleteness theorem does give you a bit more than that though (at least in its strongest variants): it doesn't make any assumptions about the theory being sound (mainly because that's very hard to prove), it just needs the theory to be "strong enough" and to be consistent (i.e. not leading to a contradiction). So even if we were willing to accept some false statements we can't get a complete theory (technically, that's the Gödel-Rosser proof, Gödel's original proof had a slightly different condition). It also gives you a concrete example of a Gödel sentence that can be construed, which leads rather directly to the second theorem.
OK, it's good that we agree on that, but it doesn't really matter. What matters is whether or not the english statement "G cannot be proven" (or some variation on that theme) is true or false. More to the point, what matters is what it takes to persuade a human being that it is true or false. The double-turnstyle symbol may be useful, but it is not the main event.
> That is basically true, assuming that the theory is also sound
OK, so we are basically in agreement on the things that actually matter. (Ironically, AFAICT Leary & Kristiansen don't actually define the term "sound". But again, whatever. It doesn't really matter for the substance of the point I am trying to make.)
The point I am trying to make is this: the reason Godel's theorem matters is that it is a negative result on the quest to reduce all of mathematics to a mechanical process. Implicit in this goal is that the process yield results that are in some sense "reasonable", i.e. if a putative mechanical process for doing math ever yields the result that 2+2=5 then we can be pretty sure that something has gone wrong even without knowing anything about double-turnstyles or soundness or validity or consistency or any of the other myriad things that logicians concern themselves with. These are all just ways of battening down various hatches, but none of them actually matter. What matters, the reason Godel's theorem is a thing, is that it is what informs us that it is impossible to mechanize all of mathematics, and that attempting to do so is a fool's errand. Finding the weakest possible conditions under which this result holds is of secondary importance, of interest only to logicians. If you can add 1 and check for equality -- or any of a myriad other combinations of trivial operations that allow you to enumerate proofs -- you've lost. That is what matters. And that can be proven without Godel numbers.
"Soundness" is a term that AFAIK comes from philosophy. An argument is correct if it follows logically from the premises, a sound argument is one in which the premises are also "true". In the context of theories, theories are sound if they are not merely consistent but also "true", i.e. correct with respect to reality.
You quickly see that this gets us into murky territory where you have to argue, outside of logic itself, whether or not certain things are "true". That's why soundness is not necessarily talked about much in an introductory mathematical logic text such as L&K.
The reason why this matters in the context of Gödel's theorems, though, besides a purely philosophical point of view, is that "PA is sound" can not be expressed in the language of arithmetic, but "PA is consistent" can be expressed in that language, and therefore Gödel's first theorem itself can be expressed in arithmetic. That is the key that establishes the link between the first and the second incompleteness theorem, the latter of which expresses that a theory of sufficient strength can't prove itself consistent.[0]
A naïve proof via Turing Machines, to my understanding, gives you something equivalent to Godel's theorem provided PA is sound, but not just simply provided PA is consistent.
Otherwise, I agree with your conclusions about the meaning of Gödel's theorems,[1] and I even agree that knowing all the technical conditions under which they apply shouldn't be of importance to non-logicians. I don't object to teaching CS students a version of Gödel's first incompleteness theorem via Turing Machines or even to some hand-waving where necessary.
But that's not the same thing as claiming that Turing Machines make the original proof ideas obsolete.
> And that can be proven without Godel numbers.
I've said it before but Gödel numbers are a trivial technical detail. What matters is that an encoding scheme exists, not which one it is. You can take Gödel's original proof and just replace Gödel numbering with your favourite encoding scheme and nothing substantial about the proof structure will change (except that you will want to substitute the "factoring primes" routine with a corresponding decoding routine for your preferred scheme).[2]
It just so happens that mathematicians actually like Gödel numbering because primes are very simple objects and every maths major learns about unique factorisation and the infinity of primes very early on. If as a computer scientist, you disagree, no big deal: just substitute your favourite encoding scheme.
That's an entirely different discussion though as the one whether you want to prove Gödel's theorems via Turing machines or via purely logical means and the theory of primitive recursion.
[0]: That, by itself, is not terribly interesting - if the theory was inconsistent, its own consistency proof wouldn't matter (since an inconsistent theory proves everything). The reason it becomes interesting is because that also implies that a theory can't be proven consistent by a weaker theory either (since every proof in the weaker theory is a proof in the original theory). This is what essentially kills the Hilbert program: We can't, say, agree that PA is sound and consistent (which seems easy enough to believe) and use that in order to prove ZFC consistent, or some such.
[1]: Although I'm not sure they're necessarily "practically" relevant. Had it turned out that model checking of PA is "only" NP-complete, instead of uncomputable, it wouldn't practically have made it much better.
> I've said it before but Gödel numbers are a trivial technical detail.
Actually, you seemed to be saying the exact opposite before when you wrote:
> 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.
And at this point I'm still not sure if you really understand this or not because:
> you will want to substitute the "factoring primes" routine with a corresponding decoding routine for your preferred scheme
Well, yeah, obviously, but translating between strings of symbols and numbers is trivial when your alphabet is ASCII (or LATIN1 or UTF8 or whatever). You don't need to factor, all you need to do is divide/modulo by powers of 2. This is just obvious to anyone who has even the most elementary knowledge of modern computers.
> A naïve proof via Turing Machines, to my understanding, gives you something equivalent to Godel's theorem provided PA is sound, but not just simply provided PA is consistent.
No, it is vastly simpler than that. All you need is a computable mapping between programs and numbers. Once you have that, any claim about a program can be translated into a claim about a number (and vice versa). "P is a program that halts when run on input I" has a corresponding "N is a number that describes a program that halts when run on input I". From that, Godel's theorem is an elementary proof by reductio: if arithmetic were decidable, you could solve the halting problem by translating the question of whether or not a program P halts into the question of whether a number N describes a program that halts.
Note that you essentially get soundness "for free" because the halting theorem is not grounded in axioms, it is grounded in physics. We don't have to wonder if our models of Turing Machines are "true". We can simply build a TM and observe that it behaves according to the model. And so the details of your axiomatization of math don't matter at all. Whatever axiomatization you can come up with, as long as you can use it to do arithmetic, and as long as someone can write a proof-checker for it, then Godel's theorem pops out as an elementary result.
> mathematicians actually like Gödel numbering because primes are very simple objects
Yes, I get that. But Turing machines are pretty simple too. The thing that makes TMs better than primes is that we can actually build a physical artifact whose behavior corresponds to the mathematical model of a TM. You can't do the same thing for primes because primes are not models of physical systems.
> 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?
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.
That's circular logic; why would that be an interesting question to investigate absent the incompleteness theorem?
> 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.
Agreed, but that implicitly requires understanding that small theories like Presburger Arithmetic are complete (which they are in every usual meaningful sense, but you seem to be claiming otherwise).
> That's circular logic; why would that be an interesting question to investigate absent the incompleteness theorem?
Because the amount of logical infrastructure that you need is surprisingly small. All you need is to be able to do basic grade-school arithmetic: add, subtract, multiple, divide, test for equality. And you don't even need all that. You can build everything you need from much simpler primitives.
The reason this is not circular is that before Goedel's theorem mathematicians were trying to construct a formal system that would allow you to derive all true statements about not just arithmetic, but all of mathematics. It turns out that this is impossible. As soon as you can do arithmetic, Goedel's theorem applies and you have lost.
> that implicitly requires understanding that small theories like Presburger Arithmetic are complete
I don't see why. Goedel's theorem matters in the context of trying to reduce all of mathematics to a formal system. Presburger arithmetic fails not because it is syntactically incomplete but because it cannot (for example) do division, so it cannot formulate (for example) the concept of a prime number and so it cannot (for example) prove the fundamental theorem of arithmetic. So yes, PB is decidable, but it is not a plausible candidate for a complete (in the informal sense) formulation of all of mathematics. Goedel's theorem shows that if you can add, subtract, multiply and divide and test for equality, then you have lost. And if you can't do those things, then you have also lost, but you don't need a theorem to tell you that.
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).
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).
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
> 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.
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.
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.
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 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.
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.
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.
> 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.
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!
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!
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.
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.
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).
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.
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.
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.
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?
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.
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?
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?
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?
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.
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."
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.
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.
> 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.