By my understanding, Gödel's first incompleteness theorem says that any theory with sufficient1 interpretability strength is essentially incomplete, that is, any consistent recursively enumerable extension of the theory must be incomplete.

Meanwhile, the second theorem says that any theory with sufficient2 interpretability strength can formulate, but not prove, a statement of its own consistency (and this is also true for any consistent, recursively enumerable extension of the theory).

Obviously, any theory satisfying the second theorem must also satisfy the first. But what about the converse: are there (consistent, recursively enumerable) essentially incomplete theories which can prove a statement equivalent to their own consistency, or which cannot formulate such a statement?

  • $\begingroup$ It occurs to me that, in a sufficiently weak theory, the question of whether a statement is equivalent to consistency of the theory might be ambiguous. Is there a standard way of addressing this issue? $\endgroup$ – Robin Saunders Feb 26 '16 at 17:09
  • 3
    $\begingroup$ Whether a statement is equivalent to consistency of the theory might be ambiguous: indeed. Is there a standard way of addressing this issue: not really, I’m afraid. Generally, you just hope that your readers will recognize a “reasonable” formalized expression of consistency when they see it. There are more-or-less standard ways how to construct provability predicates for sufficiently strong theories (which are then subject to the 2nd incompleteness theorem), but this is no good for your question. $\endgroup$ – Emil Jeřábek supports Monica Feb 26 '16 at 17:31
  • 3
    $\begingroup$ Anyway: fix r.e., recursively inseparable sets $A,B\subseteq\mathbb N$. Let $T$ be a theory with constants for each natural number $n$, and a unary predicate $P$, with axioms $P(n)$ for every $n\in A$, and $\neg P(n)$ for every $n\in B$. Then $T$ is essentially incomplete, but presumably not expressive enough to meaningfully formulate its own consistency (but I have no idea how to state this formally). $\endgroup$ – Emil Jeřábek supports Monica Feb 26 '16 at 17:36
  • 2
    $\begingroup$ You might want to have a look at Willard’s theories (which I’m not actually familiar with): see en.wikipedia.org/wiki/Self-verifying_theories . $\endgroup$ – Emil Jeřábek supports Monica Feb 26 '16 at 18:07
  • 3
    $\begingroup$ Are we allowed to "cheat" like this (or this)? $\endgroup$ – Burak Feb 29 '16 at 9:40

It is possible to construct first-order theories which prove their own consistency (and which are incomplete). Here is one example.

Consider a first-order theory with equality with a constant symbol 0 (zero), a unary predicate symbol N (the natural numbers), and a binary predicate symbol σ (the sequential relationship). Make the usual Peano Axiom assumptions, with the exception that one does not assume that σ is a total function, i.e. one does not assume that, for every natural number, there exists a natural number which is its successor. That is, it assumes every axiom in the following list except PA3:

(PA1) Ν0

(PA2) ∀n∀m ( Νn & σn,m ⇒ Νm )

(PA3) ∀n ( Νn ⇒ ∃m σn,m )

(PA4) ∀n∀m∀m' ( Νn & σn,m & σn,m' ⇒ m = m' )

(PA5) ∀n∀m∀n' ( Νn & Νn' & σn,m & σn',m ⇒ n = n' )

(PA6) ∀n ( Νn ⇒ ¬ σn,0 )

(PA7) Induction schema. Let φ be a well-formed formula where m does not occur and n is not a bound variable. Suppose φ[0\n] and ∀n∀m ( Νn & σn,m & φ ⇒ φ[m\n] ). Then ∀n ( Νn ⇒ φ ).

Now add a 3-ary symbol ∂. ∂f,x,n can be thought of as meaning that f is a sequence whose nth term is x. Make four assumptions about ∂:

(SEQ1) ∀x ( Nx ⇒ ∃f ∀i∀y (∂f,i,y ⇔ i = 0 & y = x) )

(SEQ2) ∀f ∀n∀m∀x ( ∂f,m,x & Nn & σn,m ⇒ ∃y ∂f,n,y )

(SEQ3) ∀f ∀n∀m∀x∀y ( ∂f,n,x & Ny & Nm & σn,m ⇒ ∃g ( ∂g,m,y & ∀i(¬ i = m ⇒ ∀z(∂f,i,z⇔∂g,i,z)) ) )

(SEQ4) ∀f∀i∀x∀y ( ∂f,i,x & ∂f,i,y ⇒ x = y )

Call this theory fpa. The most important thing to take away from fpa is that its ontological assumptions about the naturals are downward. That is, if a natural number n exists, then one can prove that all natural numbers less than n exist and have all the normal properties, but not that any number greater than n exists. As to sequences, if a natural number n exists, one can prove that there is a sequence from 0 to n but not any longer, and all properties of sequences and subsequences up to length n hold.

It is easy to define addition and multiplication formulas which have all the usual properties, with the exception of totality. E.g. one can prove commutativity of addition

+(x,y,z) ⇒ +(y,x,z)

even though one can't prove, given x and y, that there exists such a z.

Continue in this way. Define a predicate one(x) to abbreviate Nx & σ0,x. Again, one can prove all the usual properties of 1 except that it exists. Define two(x) and so forth.

Prove simple facts about sequences, in particular what it means for h to be the concatenation of f and g. Again, remark that given f and g, one cannot prove that h exists.

Now provide some Godel numbering for your system. Say use one(x) to represent left-parenthesis and two(x) to represent right-parenthesis and so forth. variable(x) can be defined by ∃y (ten(y) & x > y). (I haven't said how to define > but it's defined in the obvious way.)

A string, a formula, and a proof are just sequences of symbols. You can define what it means to be a term, an atomic wff (it's a particular kind of sequence), and then a wff (another particular kind of sequence). Eventually you can define the particular sequences which are proofs. That is, Proof(s) will state that sequence s represents a proof (as usual one will not be able to prove that there exists a sequence which is a proof). Finally, define the consistency of fpa as the wff Cons asserting the non-existence of a proof of the wff ¬ 0 = 0.

One proves Cons as follows. Suppose there exists a sequence-proof of the contradiction ¬ 0 = 0. But fpa can be modeled by a model of a single element, 0. For atomic wffs Nt, ∂f,t,u, and t = u assign the value of true. For atomic wffs St,u assign the value false. Continue in the obvious way. For instance a wff equivalent to ∀x(W) gets assigned the value that W has. Then one can prove that every wff gets assigned one and only one value (true or false), all the axioms will be assigned true, and that Modus Ponens and Generalization preserve truth. Hence, one can prove that every step in any proof in fpa must be true. But ¬ 0 = 0 is assigned the value false. This is a contradiction. Hence there does not exist a sequence-proof of a contradiction, i.e. fpa is consistent. But one has proved this in fpa, i.e. fpa has proved its own consistency.

  • 1
    $\begingroup$ Thanks for this answer. I have a (maybe dumb) question: By my understanding, (PA3) says that every natural number has a successor, (PA2) says that the successor is also a natural number, and (PA4) says that it is unique. But you said the whole point of fpa was that you couldn't say this. Am I missing something here, or should (PA3) be omitted from the axioms? $\endgroup$ – Robin Saunders Mar 1 '16 at 15:40
  • $\begingroup$ Sorry, bad editing. I meant the list was the usual list, but fpa was not assuming PA3. I'll edit to make this clear. $\endgroup$ – abo Mar 1 '16 at 16:55
  • $\begingroup$ @abo OT, but sad to see your website go, with all its interesting papers. $\endgroup$ – David Roberts Mar 1 '16 at 22:29
  • $\begingroup$ Alright, thanks for clearing that up. What I particularly like about this answer is that it should be easy to generalize the construction to other axiom systems. And I think Emil's construction, in the comments above, is in some sense the flip side of this: it essentially gives a forgetful functor on theories, since the (Gödel numbers of) provable and unprovable statements of any strong enough theory are recursively inseparable. That would give a semi-canonical construction for both halves of the question, which is about as nice a result as one could hope for. Does that sound about right? $\endgroup$ – Robin Saunders Mar 1 '16 at 23:08
  • $\begingroup$ @Robin. I do think you should be able to generalize my part, but am not sure how it meshes with Emil's construction. $\endgroup$ – abo Mar 2 '16 at 7:42

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.