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:
Now, construct the consistency statement Con'(T) as follows:
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.
Comments