Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?

From: Jeffrey Ketland (ketland_at_ketland.fsnet.co.uk)
Date: 01/12/05 

Date: Wed, 12 Jan 2005 02:11:35 -0000

Tim Chow:

>PRA isn't strong enough
>to prove Goedel's theorems, for example.

Happy new year.
PRA is strong enough, which is what lies behind the Goedel-von Neumann
second incompleteness theorem (i.e., the first incompleteness theorem can be
formalized in a weak subsystem of arithmetic).

Easier to think in terms of ISigma_1 which conservatively extends PRA.
ISigma_1 is the subsystem of PA with induction restricted to Sigma_1
formulas phi(x, y1, ..., yn) (allowing parameters y1, ..., yn).
ISigma_1 is enough because you only need to prove things about provability,
and provability is r.e. (and thus Sigma_1 definable).
That ISigma_1 is a conservative extension of PRA is due to Parsons 1970 (who
says philosophers never prove interesting mathematical results!), but I've
never worked through the details.

Suppose T is an axiomatizable theory extending Q and G is a Goedel-Rosser
sentence for T.
Then ISigma_1 proves the first incompleteness result. I.e., it proves "if T
is consistent then G is undecidable in T".

Sketch of details (for more, see Hajek/Pudlak 1991, _Metamathematics of
First-Order Arithmetic_):

1. Let T be an axiomatizable theory in some countable first-order L, which
is goedel-coded into N. For expression E, let #E be its code, and [E] be its
canonical numeral.
2. Let Proof_T(x, y) be some definition of "x is the code of a proof of a
formula whose code is y in T" satisfying Hilbert-Bernays derivability
conditions (to block funny provability predicates).
3. Let Prov_T(x) be Ey Proof_T(y, x).
4. Let G be a Goedel-Rosser fixed-point sentence relative to this
provability predicate.
5. Let Con(T) be "there is no proof in T of 0=1".

Then, the 1st incompleteness theorem says "If T is consistent, then G is
undecidable in T". This can be proved in ISigma_1. I.e.,

   (*) ISigma_1 |- Con(T) -> (~Prov_T([G]) & ~Prov_T([~G]))

Thus,

   (**) ISigma_1 |- Con(T) -> G

Second Incompleteness Theorem: If T is consistent, then T does not prove
Con(T).
Proof: If T extends ISigma_1 and T proves Con(T), then (by (**)), T proves
G. But, by the First incompleteness theorem, if T is consistent, then T does
not prove G. Hence, if T is consistent, then T does not prove Con(T).

This finitary reasoning can itself be formalized within ISigma_1. Thus,

  ISigma_1 |- Con(T) -> ~Prov_T([Con(T])

(i.e., we have a finitary proof of "if T is consistent, then Con(T) is not
provable in T.")

--- Jeff

Quantcast