From Trotsky to Gödel: The Life of Jean van Heijenoort
prospectmagazine.co.uk
prospectmagazine.co.uk
Gödel’s work is characterized like this all the time, like if he proved that there is something magical about mathematics, as if it’s above and beyond logic. But that’s not what Gödel proved, right?
My understanding is: All of mathematics can in principle be derived from ZFC. Gödel proved that there are mathematical statements (conjectures) that are true but cannot be proven (in ZFC). They are however, by definition, not theorems (in ZFC) and not part of mathematics in any reasonable sense.
Even this isn't true; many useful (as in often-used) statements are independent of ZFC, and not even in the semantically funny way a Gödel sentence is.
Or maybe ZFC is inconsistent, in which case all of mathematics surely can be derived from it - but so can all mathematical lies. Gödel also proves we can't know if it is or isn't (at least by the standards mathematical formalists seek).
> not part of mathematics in any reasonable sense.
This is an aesthetic claim about what theorems get to count as "real mathematics", and one both Gödel (who believed in the literal existence of mathematical objects and therefore actual truth of his sentences) and contemporary hardcore formalists (whose goal was to find some extension of PA both complete and consistent) would disagree with.
Gödel quite literally proved mathematics is "beyond" (as in its truths cannot be wholly captured by) and "above" (as in mathematical rules seem to be able to characterize the whole of) mathematical logic. Whether that makes it "magical" or not is something we will probably debate for another century.
I struggle to make any sense of this claim though... What is a proof if not an explanation of how a statement can be deduced from other statements (which in turn... all the way back to axioms)? And are you saying formal proof assistants like coq and isabelle are fools errands, in the sense that mathematics is in principal beyond formalization? If not, then why not?
There are also very easy to understand number-theoretic and combinatorial results, like the Paris-Harrington Theorem [1] and Goodstein's Theorem [2] which are provably independent of Peano Arithmetic.
The latter has an interpretation as a "hydra" game: there is a rooted tree (hydra), and you can cut off a number of heads in one shot. The hydra grows back a finite number of heads according to a specified rule. The question is, is there a strategy to slay the hydra?
The surprising answer is that any strategy will work(!), but you cannot prove this fact inside Peano arithmetic.
[1] https://en.wikipedia.org/wiki/Paris%E2%80%93Harrington_theor...
Perhaps less useful than one might think. Given that an inconsistent system can prove anything, if you weren't convinced of ZFC's consistency to begin with I hardly think you'd be convinced by a proof of its consistency in itself.
Godel's Second Incompleteness Theorem is important "in the other direction," that is its consequence for systems bigger than ZFC (or indeed PA)/larger statements that imply the consistency of your formal system in question.
(A previous comment I made on this in greater detail https://news.ycombinator.com/item?id=25118038)
No Godel's incompleteness theorems prove nothing about truth by themselves. They are only statements about proofs and can be independently paired with other statements (as well as their negation), both philosophical and mathematical, about truth. That is the incompleteness theorems are silent on the matter of truth as a direct consequence, but require other theorems or philosophies to further mold statements on truth (the incompleteness theorems do have important indirect impact on those statements).
For example there is Godel's Completeness Theorem , which in a vague sense proves that "all true things are provable" (I can explain in greater detail if so desired). Godel's Completeness Theorem holds independently of Godel's Incompleteness Theorems (that is all four possible pairings of holding/not holding can apply to different formal systems). Notably Godel's Completeness Theorem holds for first order logic, the most common formalization of mathematical foundations (which includes ZFC and Peano Arithmetic).
> Can you give an example of a statement that is independent of ZFC yet useful/often-used?
Very briefly, the proof of Fermat's Last Theorem used an axiom that is independent of ZFC (it used a large cardinal axiom). It was later found that the proof did not require this axiom and could be fully formalized within ZFC.
There are separately simple-sounding and useful-sounding, but not actually used, statements which are independent of ZFC (such as if the set X is smaller than the set Y by cardinality then X has fewer subsets than Y).
But almost all of mainstream mathematics is perfectly happy to remain in ZFC.
There is separately an interesting empirical/philosophical question of whether there might still be a "practically complete" set of axioms to do mathematics which is not definitively settled by Godel's Incompleteness Theorems.
> And are you saying formal proof assistants like coq and isabelle are fools errands, in the sense that mathematics is in principal beyond formalization? If not, then why not?
Ugh this is why associating Godel's Incompleteness Theorems with truth can be so misleading. Godel's Incompleteness Theorems, in contexts where Godel's Completeness Theorem holds, has little overall consequence for formal proof assistants. Whether the conception of abstraction in a human mind in principle is beyond formalization is a deep philosophical question (but this is not specific to mathematics, this is really just the age old philosophical question of whether qualia and the human consciousness are reducible). However mathematics as practiced by working mathematicians and laid out in theorems and proofs is formalizable essentially by definition.
About futility of theorem proving: I think a useful perspective on this is that the context of formal logic with respect to "all mathematics" used to really mean "all of mathematics in one system" a hundred years ago.
This is the logicist program started by Frege and Russell - make everything formal - and this was shattered.
Now nothing stops us from formalizing some part of mathematics. Today, when people say "you can formalize all mathematics" post Gödel, it means you pick your area and formalize away, knowing that effectively proving consistency of your formal system (within the same system) is out of reach.
So nobody tries to claim "all in one system" but many logics and sets of axioms coexist without there being any distinguished one that is better (in the sense of effectively proved consistent and strong enough to be "useful").
So I think we’re back were we started: All of mathematics can in principle be deduced from ZFC. There are a few border cases that can be useful, and can be included by extending ZFC.
But you perhaps may find it interesting to consider what could be meant when someone says "there are true statements that are not provable" in a way that doesn't exaggerate the results of the Incompleteness Theorems. I don't actually support this line of thinking, but I find it interesting to engage with.
So here goes:
Whatever you might say about more abstract mathematical structures, there seems to be something indelibly real about the natural numbers. I can verify simple facts about them by physically counting things. While definitionally perhaps it might make sense to create a formal system that says 5 + 6 = 8, I can go and count apples and realize that nope actually 5 + 6 = 11.
Now luckily statements of this form, that don't use any quantification (i.e. the words "for all," "there exists," or their equivalents such as "always," or "eventually"), are entirely decided by our usual axioms about the natural numbers.
But it seems like, while perhaps a tad less concrete than statements such as 1 + 1 = 2, there are other statements involving quantification that still have some "one-sided" concrete aspect to them. For example if I claim there exists a natural number with some arithmetical property and there indeed is such a number, simply by physically counting up I will eventually come across such a number. However, if I'm wrong, then I will never know (this is what is meant by one-sided). Likewise if I claim a property is true of every natural number, I will eventually have experimental proof if I'm wrong, but I will never know for certain if I'm right (at least by physically counting things).
Godel's Incompleteness Theorem says there will always be such quantified statements that any given formal system cannot decide. Yet they seem to have definite truth values in our physical universe! Either my physical act of counting will come to an end or it won't. This seems like a very real consequence.
So sure you can claim that these statements are different than theorems because either themselves or their negation can be added to our pre-existing axioms about the natural numbers without any conflict and that might be true in theory, but we would like to preserve the property that our axioms about the natural numbers correctly reflect how natural numbers act in our universe, and it seems, at least at a first glance, that Godel's Incompleteness Theorem disallows that, or at the very least that the act of trying to find these axioms requires extra-mathematical justification.
This isn't what I mean when I say "formalize all mathematics" at least. For example the diversity among the current crop of proof assistants has nothing to do with incompleteness and everything instead to do with with proof writing ergonomics. Assuming we perfectly solved the problem of the ergonomics of writing formal proofs, ZFC would be enough to do the overwhelming majority of modern mathematics.
> effectively proving consistency of your formal system (within the same system)
This isn't the significance of the Second Incompleteness Theorem though. Since an inconsistent formal system can prove anything, why would you ever trust a proof of consistency within the same system? To avoid repetition, I'll just link to a previous comment I made: https://news.ycombinator.com/item?id=25118038
> many logics and sets of axioms coexist without there being any distinguished one that is better
(Syntactic) completeness has never really been a criteria for creating an end-all-be-all formal system in and of itself. We happily use many different mutually incompatible geometric systems (Euclidean, hyperbolic, etc.), in spite of the fact that many are complete.
That being said, it is true a pre-Godel desirable property of a foundational system of mathematics would be completeness, but foundations has never really been all that important for the working mathematician.
bjornsing: All of mathematics can in principle be derived from ZFC. morelisp: not all, there are independent statements. Mathematics is beyond formalization. bjornsing: like what? are you saying that formalization is futile? or not? me: CH is an example. formalizing is not futile, but affected by incompleteness theorems in the sense that all those proof assistants, when used for developing some theory, will require something else to prove the consistency of that theory.
dwohnitmok: the point of incompleteness is not that it requires a stronger system, but that a weaker system cannot prove a stronger system, killing the idea of trusted computing base.
See, I was not trying to expound the significance of the Second Incompleteness Theorem; I do not really care what mathematicians consider as in or out of "all mathematics," but I noticed that "being able to formalize all mathematics" has become a somewhat technical expression in logic.
I like very much what you're writing in that comment. I have also seen Gentzen's consistency argument for PA and think the qualification that you include at the end about weaker systems sometimes being able to show the consistency of stronger ones is needed.
I did not imply that proving consistency of X within X is desirable.
However, I am intrigued by Artemov using a provability operator to prove consistency of PA in PA: https://arxiv.org/abs/1902.07404 Provability logic is interesting, a modal logic that adds Loeb's theorem as axiom (maybe Carl Hewitt would consider it a foundation of computer science? but I digress.)
Now, the reason I feel compelled to comment back: I do not understand why you bring up completeness. What are you reacting to? Are you trying to imply that using incomplete foundations is the key to ignore the challenge of proving consistency?
Saying "ZFC is enough for all mathematics" is a commitment to ZFC axioms and to first-order logic. First order logic is compact and complete. As such, it is very much affected by the First Incompleteness Theorem and also the Second, and there will also be non-standard models and the Skolem paradox.
I don't have a horse in the foundation and formalization race, just curious what you mean. As far as I can tell (and I may well be off, not a mathematician), it seems quite desirable that foundations worthy of the name would let us prove all theorems of arithmetic and natural numbers.
I think the crucial part of bjornsing's original question is "Can you give an example of a statement that is independent of ZFC yet useful/often-used?"
As such CH is not, in and of itself, an obvious answer to bjornsing's original question since there hasn't been a case to be made that CH is useful/often-used. Now there can be a case to be made that CH (or its consequences) are indeed useful/often-used, but that is not obvious and probably would need further exploration to convince bjornsing (certainly I personally find it arguable, potentially convincingly so, but nonetheless far from settled).
That is, the way I interpret bjornsing's original intent is, "okay so [syntactic] incompleteness is theoretically a thing, practically what impact does it have on current attempts at formalizing mathematics?"
And that impetus to explore the practical impact of the incompleteness theorems is what I'm jumping off of.
My central thesis is this:
The actual practical process of the formalization of mathematics in the last few decades, as exemplified by proof assistants, is minimally affected by syntactic incompleteness (i.e. Godel's incompleteness theorems).
Your comment
> Today, when people say "you can formalize all mathematics" post Gödel, it means you pick your area and formalize away, knowing that effectively proving consistency of your formal system (within the same system) is out of reach. So nobody tries to claim "all in one system" but many logics and sets of axioms coexist without there being any distinguished one that is better (in the sense of effectively proved consistent and strong enough to be "useful").
makes me think that you think the diversity of proof assistants and different logics underlying them is due to syntactic incompleteness, when this is not the case. These logics are for the most part bi-interpretable, they are not distinguished by what fragment of mathematics they are capable of formalizing, but rather the different ergonomics of different approaches. In expressiveness they are all basically ZFC (potentially plus some "smallish" large cardinal axiom).
And perhaps the big thing is that mathematicians, maybe surprisingly, don't really care about consistency proofs. This is both because mathematicians don't really care about foundations as a whole, but also (and potentially a direct result of) because the vast majority of mathematics proofs are, logically speaking, extraordinarily simple. Even something like Peano Arithmetic is way overkill for most proofs out there, so Godel's incompleteness results, even in theory, have much less impact than might be assumed.
> I do not understand why you bring up completeness. What are you reacting to? Are you trying to imply that using incomplete foundations is the key to ignore the challenge of proving consistency?
I didn't really mean to bring up completeness when I linked to my previous comment, I meant more to talk about the "reverse" direction of consistency that is important for the second incompleteness theorem (rather than proving the consistency of the theory in question itself).
However, now that the cat is out of the bag, I will secondarily state that I think semantic completeness (Godel's completeness theorem) is in fact a more influential factor behind different philosophies of formalization than syntactic incompleteness (I will go as far as to say that any human system for the foundations of mathematics implicitly assumes semantic completeness to hold, which I won't elaborate in this already long comment, but can in a reply if you would like).
> First order logic is compact and complete. As such, it is very much affected by the First Incompleteness Theorem and also the Second, and there will also be non-standard models and the Skolem paradox.
Semantic compactness and completeness are entirely independent of Godel's incompleteness theorems. There are theories which are semantically complete and syntactically incomplete and vice versa (as well as theories that are both semantically and syntactically incomplete or both semantically and syntactically complete). As an aside it is also weird to talk about first order logic being affected by the incompleteness theorems because the incompleteness theorems refer to specific theories within a logic rather than the logic itself.
Godel's incompleteness theorems are instead closely tied to arithmetic, in particular arithmetic's peculiar property that any natural number in the metatheory can be translated to a natural number in the object theory, while preserving the usual arithmetic operators, by finite application of the successor function.
Moreover non-standard models and the Lowenheim-Skolem theorem both affect first-order theories "from the outside" so to speak, but don't really affect them "from the inside." That is if you're using a proof assistant, you can never observe consequences of those non-standard models while you're formalizing things.
> Saying "ZFC is enough for all mathematics" is a commitment to ZFC axioms and to first-order logic.
Perhaps I should qualify my previous statement. When I said "ZFC would be enough to do the overwhelming majority of modern mathematics" I really do mean "modern" here. It's possible that future mathematics will require a different axiom system. My point was simply that basically none of the problems people in the field of formal proof assistants have right now can be chalked up to anything outside of ZFC or syntactic completeness. If those researchers could magically wave a wand and say "here's a perfectly ergonomic formal proof assistant understandable and usable by any mathematician but oh it's limited to things provable in ZFC" I think they would absolutely elated.
Personally, far from being committed to ZFC, I don't actually like ZFC as a foundation of mathematics. However, I dislike ZFC for reasons completely unrelated to syntactic completeness. It's a clunky encoding of mathematics that doesn't reflect mathematicians' intuitions about various different structures.
Now I do separately think that first-order logic (or something that obeys Godel's completeness theorem) is essentially a requirement for any system purporting to be a foundation of mathematics, but as I mentioned in an earlier parenthetical, I don't want to delve into that in this particular reply.
> As far as I can tell (and I may well be off, not a mathematician), it seems quite desirable that foundations worthy of the name would let us prove all theorems of arithmetic and natural numbers.
I agree. I think any mathematician pre-Godel would've wanted this. That being said, my point is that even though this state of affairs is undesirable, it has little practical effect on anything related to ongoing efforts to formalize mathematics.
I now realized that I confused "syntactic" and "semantic" completeness.
I agree on your points; my first up there was ignoring a bit of the context (it was late...) and not meant to "motivate" the multitude of proof assistants by incompleteness theorem.
As a programming language person, I am quite convinced there will never, ever be an agreement on a common formal language (even if there was or is agreement on foundations it should be based upon) - it is the same as for programming languages.
This is more due to human nature rather than technical factors, and if we conceive logic as a linguistic activity, then we can see how foundations and the corresponding ergonomic language logic are related, maybe two sides of the same coin. "Foundations" in the context of mathematics appear (to me at least) as something technical and interchangeable.
Is there a venue for discussions on logics like these outside of the occasional logic-related HN threads? : )
I strongly agree. The formalization of mathematics bears strong resemblances to programming (and is in deep theoretical senses the same endeavor) so it would be hardly surprising for the same social phenomena to show up. As an aside I think the relationship between the halting problem and real-world programming languages is a good heuristic for the effect that Godel's incompleteness theorems have on formalization of mathematics (e.g. very little in programming language development is directly attributable to the halting problem and its existence doesn't spell the doom of programming, but it's always there in the background).
> Is there a venue for discussions on logics like these outside of the occasional logic-related HN threads? : )
There's the Foundations of Mathematics (FOM) mailing list: https://cs.nyu.edu/mailman/listinfo/fom, but it's geared towards cutting edge and very technical research rather than more layman discussions of the sort found on HN.
Otherwise I don't know of one unfortunately.
No, and I have no clue how you could get that from what I wrote. To move back into a more familiar domain, Rice's theorem puts a frustrating limit on what we can accomplish via static analysis of programs, and yet the static analysis we can do remains extremely helpful in programming.
Godel's Incompletness Theorems do not by themselves address truth, but instead require additional theorems and/or philosophical commitments to decide either way.
This is itself a sort of philosophical commitment - and again, not one shared by Gödel or the logicist program.
In very real ways Godel's Incompleteness Theorems do not address truth. Their proofs are purely syntactic rather than semantic.
> and again, not one shared by Gödel or the logicist program.
The logicist program is a bit tricky to pin down; the major figures associated with it either were no longer active in mathematical logic by the time of Godel's result (e.g. Russell) or were but never made any response to them (e.g. Hilbert).
However, we know Godel's take on the matter. In particular I don't think this is an accurate account of Godel's own viewpoint. It is clear Godel clearly believed that there were mathematical truths that could not be expressed by formal systems.
However, it is also clear that Godel acknowledges this to be an additional philosophical commitment. Godel himself cleanly states this in his 1951 Gibbs Lecture.
> Does it [his incompleteness theorems, in particular his second one] mean that no well-defined system of mathematics can contain all of mathematics proper? It does, if by mathematics proper is understood the system of all true mathematical propositions; it does not, however, if one understands by it the system of all demonstrable mathematical propositions. I shall distinguish between these two meanings of mathematics as mathematics in the objective and in the subjective sense.
Godel is pointing out that his incompleteness theorems require an additional philosophical commitment to "objective" or "subjective" mathematics in order to make a statement on truth (what he refers to as "true" in his comment already demonstrates his own predilection towards "objective" mathematics being the correct philosophical commitment, but the important point here is that he is making the distinction).
As a footnote, Godel's notion of mathematical truth is an extremely strong Platonist position that I don't think most HN commentators would agree with (at least at the beginning; they may be swayed to come around to it). Godel believed there were no truly independent mathematical statements, only ones temporarily independent of our limited set of axioms. Every mathematical statement is either true or false. For example, the continuum hypothesis will be definitively decided one way or the other (if I recall Godel ultimately estimated the continuum hypothesis to be false).
https://www.newyorker.com/news/letter-from-silicon-valley/th...