2

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?
13
  • 1. Consistency is still an open question. It can be proved within the metatheory (see Gentzen's consistency proof). Jun 29 at 19:35
  • 1
    2. The fact that the theory in question is not able to prove its own consistency does not mean that it is inconsistent. No one have found inconsistencies in arithmetic up to now... Jun 29 at 19:36
  • One can also point to strong intuitions that the basic axioms and function definitions in Peano arithmetic will not be inconsistent because they can be understood semantically as describing true facts about counting, adding, and multiplying finite elements...for example, an argument for AB=BA always holding is that you can think of "A*B" as a rectangular array with A rows & B dots per row (so each column has A dots, each row has B dots), and then if you just rotate it 90 degrees you have a rectangular array with B rows & A dots per row (each column has B dots, each row has A dots).
    – Hypnosifl
    Jun 29 at 20:29
  • 1
    "Can we then deduce that it is impossible to prove consistency of mind..." NO; Godel's Th applies to formal system with some specific features. Human mind is not a formal system. In addition, if we try to consider human language as a "system", it is clearly inconsistent. Jun 30 at 6:07
  • 1
    @Ajax - a system means: fixed language, fixed rules for forming expressions, fixed rules for deriving new formulas from axioms and a recursive set of axioms. If so, where are the axiom? Remember that from an intuitive point of view naive comprehension principle can be assumed as a good example of "common sense" axiom. Using it, we derive the well-known Paradox. Conclusion: human mind is inconsistent. Jun 30 at 9:26
2

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

3
  • thank you for your answer. I am not very familiar with C-H correspondence. Can you elucidate what's the point of C-H? Does it hold in general? Is my intuition that because algorithm A "decides" theorem T, it must be the case that A encodes proof of T in some way... -correct?
    – Ajax
    Jun 30 at 17:32
  • @Ajax: No, the correspondence is a lot more subtle and general than that. It has more to do with type theory than with computation theory. Algorithms that "decide" things, or indeed algorithms in general, are not really the point of C-H correspondence.
    – Kevin
    Jun 30 at 19:36
  • Excellent answer. You may wish to note that ω-consistency can be weakened to Σ1-soundness. C is not Σ1-sound. That is why if we believe that A is meaningful we must believe that B is meaningful and that C is meaningless.
    – user21820
    Oct 25 at 6:53
0

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.

1
  • It depends exactly what you mean by "complete" here. For example, T:=ZFC+"ZFC is inconsistent" is a consistent theory assuming ZFC itself is, but of course T proves "For each sentence p, either T proves p or T disproves p" (since in fact T proves its own inconsistency). ZFC + "ZFC is consistent and complete" is inconsistent, though. Sep 26 at 3:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.