A strikingly simple consistency statement

Suppose T is a consistent formalization of arithmetic containing PRA (Primitive Recursive Arithmetic). Use some standard arithmetical encoding of formulas. Goedel's well-known second underivability theorem says that Con(T), the standardly constructed consistency statement for T, is not derivable in T.

There are, however, formulas equivalent to Con(T), which are derivable in T (although, the derivability conditions aren't satisfied). Usually, Rosser's or Feferman's examples are quoted; these are a bit complicated and involve reference to an ordering of formulas or proofs or axioms.

Here is another, strikingly simple non-standard consistency statement which is provable in T (due to Mostowski).

Let Pr express T's provability relation (it's the standard derivability predicate, nothing kinky is going on there). Define:
Pr'(x,y) ⇔ Pr(x,y)& ¬ Pr(x, ⌈0=S0⌉)
As T contains PRA, T proves 0≠S0. Since T is also consistent, T doesn't prove 0=S0. So ¬ Pr(x, ⌈0=S0⌉) is true of all numbers x. So Pr(x,y)& ¬ Pr(x, ⌈0=S0⌉) is true of exactly the same numbers as Pr(x,y). So Pr and Pr' have the same extension.

Now, construct the consistency statement Con'(T) as follows:
Con'(T) ⇔ ∀x ¬ Pr'(x,⌈0=S0⌉)
This boils down to:
Con'(T) ∀x ¬[Pr(x,⌈0=S0⌉)& ¬ Pr(x,⌈0=S0⌉)]
which says that nothing is a number of a T-derivation that proves both 0=Sn and its negation. Clearly, proving Con'(T) in T doesn't require much effort.


Richard Zach said…
This has an unfortunate property that RCon doesn't have. If T is inconsistent, then, PA |- Con'(T). So this doesn't really have much claim to being called a consistency statement, does it?
Rafal Urbaniak said…
My response didn't fit in here. It's in the next posting.
Shawn said…
Just a bit of clarification: what is RCon?
Rafal Urbaniak said…
I think Richard meant any Rosser-style consistency statement (let me know if you need more details).