Some doubts on Incompleteness Theorems

Question

An important point to note about first incompleteness theorem is that while a certain formula is "true" but unprovable, it is "true" on the basis of my understanding (intended interpretation) of the "formal system" in question. That is what I think one means when it is said that one can see that it is true. Wikipedia provides explanation:

The Gödel sentence is designed to refer, indirectly, to itself. The sentence states that, when a particular sequence of steps is used to construct another sentence, that constructed sentence will not be provable in F. However, the sequence of steps is such that the constructed sentence turns out to be GF itself. In this way, the Gödel sentence GF indirectly states its own unprovability within F (Smith 2007, p. 135).

... The first incompleteness theorem shows that the Gödel sentence GF of an appropriate formal theory F is unprovable in F. Because, when interpreted as a statement about arithmetic, this unprovability is exactly what the sentence (indirectly) asserts, the Gödel sentence is, in fact, true (Smoryński 1977 p. 825; also see Franzén 2005 pp. 28–33). For this reason, the sentence GF is often said to be "true but unprovable." (Raatikainen 2015).

So far I am good. Next comes consistency.

System cannot demonstrate its own consistency. Proving consistency means "It is not possible to derive a contradiction i.e. 1=0". If this statement is proven, consistency is established. Second Theorem: Consistency cannot be proven within the system. So, I can add an axiom that my system S is consistent, and arrive at a new system S' where S' = S + (S is consistent). My question is:

1. This still doesn't make S consistent! Or does it? If I understand the rules of system S, can I again see but not prove consistency of S, or is consistency of S still an open question?
2. How is consistency of a system S related to Universal Turing Machine for first order logic? I mean what is the technical analog of consistency in Turing machines? Is my computer really not provably consistent? And does that mean someday it may give a recognisable contradiction?

Answer 1

So, I can add an axiom that my system S is consistent, and arrive at a new system S' where S' = S + (S is consistent)

Yes, that is fine. If you will allow me to switch to variables that are easier to distinguish from one another, you can have:

B = A + (A is consistent)

Or even

C = A + (A is not consistent)

Neither(!) of those will entail a contradiction (but C will fail to be omega-consistent, which is a stronger form of consistency that arises when you try to reconcile theory and metatheory with one another). Neither B nor C can prove that B/C is itself consistent, although B obviously proves that A is consistent.

The full explanation of C is out of scope here, but in brief, it asserts that a proof of some contradiction, such as 0=1, exists and can be encoded with some Gödel numeral, but it turns out that this numeral does not actually exist in the standard model of arithmetic (it is not any of 0, 1, 2, etc.). Peano arithmetic is not strong enough to disprove the existence of such nonstandard numbers, so no contradiction arises within the system C. Nevertheless, it's intuitively obvious that C is "wrong" in some sense, and that's what omega-consistency is all about.

But there's a big exception: If A is already inconsistent, then it proves everything, including its own consistency and its own inconsistency, and that inconsistency is inherited by B and C. Whenever we talk about any of the incompleteness theorems, we always take the consistency of the theory as a baseline assumption, because there's very little you can usefully say about an inconsistent theory of arithmetic.

On the other hand, we can't get away with something like this:

D = A + (D is consistent)

Because it turns out that, assuming you can find a way to express the self-reference (with clever use of Gödel numbering), the resulting system would run afoul of the second incompleteness theorem and therefore be inconsistent.

Now, returning to your questions:

This still doesn't make S consistent! Or does it? If I understand the rules of system S, can I again see but not prove consistency of S, or is consistency of S still an open question?

If you believe that S' does not prove any contradictions (or equivalently, that S' is consistent), then you necessarily believe that S is consistent, and so a proof is not required. If S were inconsistent, then S' would also be inconsistent, and any "proofs" it provided would be worthless. Therefore, you can't use S' to prove that S is consistent, because either you already believe that S is consistent, or you already doubt that S' is consistent, and so S' accomplishes nothing for you.

How is consistency of a system S related to Universal Turing Machine for first order logic? I mean what is the technical analog of consistency in Turing machines? Is my computer really not provably consistent? And does that mean someday it may give a recognisable contradiction?

The fact that you are unable to prove consistency does not mean that a system is necessarily inconsistent. Mathematicians have carefully considered the consistency of Peano arithmetic and Zermelo-Fraenkel set theory for a very long time, and nobody has ever demonstrated that either system is inconsistent. We might imagine that some incredibly subtle and elaborate contradiction might one day be constructed, but it would not be a simple restatement of e.g. Russell's paradox, because all of the "simple" problems such as Russell's paradox have already been explored and "fixed." If we ever did find such a contradiction, it could likely be constrained by a slight modification of the axioms in order to rule out whatever line of argument leads to a contradiction, so we could likely recover most existing mathematical theorems with little disruption.

Frankly, I would be much more concerned about the possibility that your computer's software is buggy or incorrectly designed, rather than that the entire Curry-Howard correspondence is going to come crashing down at some point in the near future. Software bugs happen all the time; mathematics bugs are (in recent years) much rarer.

But in any event, under the aforementioned C-H correspondence, the fixed-point combinators can already be used to recover Curry's paradox (or rather, they would be able to, if the C-H correspondence had not explicitly excluded the untyped lambda calculus in which fixed-point combinators arise, precisely in order to fix this problem). Effectively, modern (Turing-complete) programming languages have already "opted out" of consistency altogether (and this becomes even more obvious when you consider the possibility of arbitrary type casting in most statically-typed languages).

Answer 2

Take an inconsistent system S and create another system S’ by adding the axiom “S’ is consistent”. Now you have a very simple proof that S’ is consistent. But you still have some statement X with s proof for both X and not X, so S’ is just as inconsistent as S, plus you have a direct contradiction to the added axiom!

Instead add an axiom “S’ is complete”. But just as in S, you can express a statement X that says in layman’s terms “there is no proof for the statement X”. We don’t need to prove or disprove X, just the fact that we can express it causes Gödels law to strike. The existence of X shows that S’ is either incomplete or inconsistent. Of course the added axiom shows that S’ is not incomplete, therefore it is inconsistent.

What if we add “S’ is incomplete”? Every inconsistent system is complete, so we have an immediate proof again that S’ is consistent. But a proof that S’ is consistent doesn’t stop it from being inconsistent so nothing gained.