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

Relevant Pages

  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... second incompleteness theorem (i.e., the first incompleteness theorem can be ... ISigma_1 is enough because you only need to prove things about provability, ... Suppose T is an axiomatizable theory extending Q and G is a Goedel-Rosser ... Then, the 1st incompleteness theorem says "If T is consistent, then G is ...
    (sci.logic)
  • Re: THIS STATEMENT HAS NO PROOF IN ANY SYSTEM = true or false?
    ... second incompleteness theorem (i.e., the first incompleteness theorem can be ... ISigma_1 is enough because you only need to prove things about provability, ... Suppose T is an axiomatizable theory extending Q and G is a Goedel-Rosser ... Then, the 1st incompleteness theorem says "If T is consistent, then G is ...
    (sci.math)
  • Re: Goedel - interesting problem?
    ... Gödel's 1st incompleteness theorem says that for any consistent formal ... formal theory containing elementary arithmetic and certain simple facts ... about formal provability are provable in T, ...
    (sci.logic)
  • Re: Kresss Probability Trilogy Qs
    ... be a proof that first-order arithmetic is consistent, ... Incompleteness Theorem only prohibits using a logical system to prove *its ... If a theorem prover is complete (in some domain, ... you can't guarantee it. ...
    (rec.arts.sf.science)
  • Re: Godels Incompleteness theorem
    ... incompleteness theorem in a simple way. ... consistent G is true but not formally derivable in the theory. ... Here a formal theory consists of a mathematically specified language ... with certain formulas specified as axioms. ...
    (sci.math)