[SleekEagle]

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 ...

[qsort]

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.

[ginnungagap]

> 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.