Comment by qsort | Hacker News Reader

Comment by qsort | Hacker News Reader

Parent Full thread

This is probably the editorialization.

He's alluding to the fact that unlike what one might naively intuit, it's impossible to formulate a set of axioms that can formally express all mathematics.

Because of Godel's incompleteness theorems, any formal system that's sufficiently powerful to formulate basic arithmetic (see for instance Robinson arithmetic) and consistent (that is, it cannot prove false statements) is both incomplete (meaning that it's possible to formulate a wff within that system that the system itself can neither prove nor disprove) and can't prove it's own consistency.

This fact is often portrayed in popular media as being a "bug" or a "missing foundation" of mathematics. That is inaccurate -- it's just a property of how logical systems work -- but it does prove that the search for the holy grail of a grand unified system of axioms for all of mathematics is destined to remain fruitless.

Modern mathematics is most often implicitly assumed to be formulated in a formal system called ZFC, but there are alternatives.

I think the second theorem is the "worse" result for mathematics. It shows that it's completely impossible to use a weaker system, which is hopefully self-evident, to prove the consistency of a stronger, but weirder system like ZFC.

Hilbert wanted to show that, even if you don't "believe" in ZFC, we could at least try to convince you that it doesn't lead to contradictions, but that fundamentally didn't work.

Oh this is interesting, I didn't know about this historical detail.

It makes sense, Godel's first could be mostly seen as a version of the halting problem, while the second is "game over" for a Hilbert-like foundation program.

p.s. Just wanted to point out that it's funny how we wrote two mostly identical sets of comments. Great minds think alike? :)

> Oh this is interesting, I didn't know about this historical detail.

That's the characterisation I got from Peter Smith's book about Gödel's theorems. I didn't verify original sources or anything, but it sounds very plausible to me.

And it also kind of answers the question about why we should care: if a system can't prove its own consistency, well that's not terribly interesting (even if it could, we would have to believe the system a priori to trust its own consistency proof). But if it also can't prove a stronger system consistent, then that's much more interesting.

> Great minds think alike?

That would be a bit too self-aggrandizing for me. :D I'm very curious about logic (and maths in general), that's why I know some stuff about it, but I'm no maths genius.

It's not a "bug" but it is disappointing.

To mathematicians and non-mathematicians.

Being unable to prove or disprove certain statements is a rainy cloud. Like maybe the Riemann hypothesis is just impossible to prove.

It doesn't mean math is "broken" but it is disappointing, no?

Is the fact that these systems cannot prove their own consistency actually a feature of the incompleteness theorem? I thought it effectively boiled down to "you can keep either consistency or completeness, not both". It's been a while since my metamathematics course ...

It depends on exactly what you mean with those terms.

When you say "you can keep consistency or completeness but not both" you are essentially stating Godel's first.

Morally speaking, Godel's first is "no system is complete", but there are two exceptions: if the system isn't powerful enough to formulate the Godel sentence then the proof doesn't work, and any inconsistent system is trivially complete because ex falso quodlibet sequitur, i.e. any wff is true.

The part about a system not being able to prove its own consistency is Godel's second theorem.

But the theorem only does what it says on the tin: the system not being able to prove its own consistency doesn't mean that it being inconsistent! [1] This is the case for ZFC, for example. We can't prove ZFC's consistency within ZFC: that would violate Godel's second, and we know that either ZFC is inconsistent (that is, you can derive an absurd from the axioms) or ZFC is incomplete (that is, there exists a well-formed formula of ZFC that cannot be proved or disproved within ZFC).

We don't know which one it is.

[1] This implication and similar ones are often made in pop-culture presentations of the foundation problem. I generally vigorously object to them because they're not only imprecise -- that's understandable -- but they leave a layman with a completely wrong impression.

> the system not being able to prove its own consistency doesn't mean that it being inconsistent!

Another funny thing that can happen is that a system proves its own inconsistency, despite being consistent. The short summary is to never trust a system talking about its own consistency.

Reply on news.ycombinator.com