A recent thread on sci.math reminded me of something I've
wondered about for some time. Consider the following two
"facts":

(i) Every once in a while on usenet I hear someone say
"[someone] proved ZF|-Con(PA), using induction up to
epsilon_0".

(ii) The fact that ZF|-Con(PA) is obvious: it's clear that the
finite ordinals form a model of PA.

While (i) and (ii) are not mathematically inconsistent,
they're "real-world inconsistent" - if ZF|-Con(PA) is
really as simple as suggested in (ii) then nobody would
talk about who proved it (also I don't see what the reasoning
in (ii) has to do with "induction up to epsilon_0".)

David C. Ullrich says...

A recent thread on sci.math reminded me of something I've
wondered about for some time. Consider the following two
"facts":

(i) Every once in a while on usenet I hear someone say
"[someone] proved ZF|-Con(PA), using induction up to
epsilon_0".

(ii) The fact that ZF|-Con(PA) is obvious: it's clear that the
finite ordinals form a model of PA.

While (i) and (ii) are not mathematically inconsistent,
they're "real-world inconsistent" - if ZF|-Con(PA) is
really as simple as suggested in (ii) then nobody would
talk about who proved it (also I don't see what the reasoning
in (ii) has to do with "induction up to epsilon_0".)

The interesting thing about (ii) is that it doesn't really use
much ZFC at all. You can prove Con(PA) in *PA*, if you add the
principle of epsilon_0 induction. That is, you come up with a
coding #alpha of the ordinals less than epsilon_0 as naturals
(not hard) and define a recursive binary relation lt(x,y) which
holds if and only if for some ordinals alpha and beta,
x = #alpha and y = #beta and alpha < beta. That isn't hard, either.
Then you add the following induction schema to PA:

all y (all x ( lt(x,y) -> Phi(x) ) -> Phi(y))
-> all y Phi(y)

Then this new theory, PA + epsilon_0 induction, is able to prove con(PA).

The proof is *proof-theoretic* rather than *model-theoretic*. Basically,
you assign an ordinal less than epsilon_0 to each proof in PA. Then you
prove (by induction) that there is no proof of a contradiction.

I think this was due to Gentzen.

(i) Every once in a while on usenet I hear someone say
"[someone] proved ZF|-Con(PA), using induction up to
epsilon_0".

(ii) The fact that ZF|-Con(PA) is obvious: it's clear that the
finite ordinals form a model of PA.

...The interesting thing about (ii) is that it doesn't really use
much ZFC at all.

...Thanks. If your first sentence was a typo for "The interesting thing
about (i) is that it doesn't really use much ZFC at all" then this
makes sense to me. ???

Then this new theory, PA + epsilon_0 induction, is able to prove con(PA).

daryl@atc-nycorp.com (Daryl McCullough) wrote in message news:<btucm401bua@drn.newsguy.com>...
Then this new theory, PA + epsilon_0 induction, is able to prove con(PA).

Actually it is an esential feature of Gentzen's proof that it is formalizable
in PRA+epsilon_0 induction. That is, only quantifier-free induction is used.

So the proof is perfectly finitary except for the use of epsilon_0 induction.

On 12 Jan 2004 09:35:26 -0800, torkel@sm.luth.se (Torkel Franzen)
wrote:

daryl@atc-nycorp.com (Daryl McCullough) wrote in message
news:<btucm401bua@drn.newsguy.com>...
Then this new theory, PA + epsilon_0 induction, is able to prove con(PA).

Actually it is an esential feature of Gentzen's proof that it is formalizable
in PRA+epsilon_0 induction. That is, only quantifier-free induction is used.

I can't figure out what you mean by "quantifier-free induction".
(No doubt it should be clear and I'm just being slow...)

I can't figure out what you mean by "quantifier-free induction".
(No doubt it should be clear and I'm just being slow...)

Daryl and Torkel have exhibited Gentzen's result, but perhaps it's worth
adding that not only PA+e_0 induction |- Con(PA), but e_0 is the least
ordinal a such that well-orderings of type a can't be proved to be well
orderings in PA.

Aatu Koskensilta <aatu.koskensilta@xortec.fi> writes:


Daryl and Torkel have exhibited Gentzen's result, but perhaps it's worth
adding that not only PA+e_0 induction |- Con(PA), but e_0 is the least
ordinal a such that well-orderings of type a can't be proved to be well
orderings in PA.


But there are also well-orderings of type omega that can't be proved
to be well-orderings in PA.

David C. Ullrich <ullrich@math.okstate.edu> wrote in message news:<im3600tfe6fpml3h04c0jt81s928votf1b@4ax.com>...
I can't figure out what you mean by "quantifier-free induction".
(No doubt it should be clear and I'm just being slow...)

It's a technical term, hence necessarily opaque if you're not familiar
with it.

PRA, primitive recursive arithmetic, has symbols for *all*
primitive recursive functions, not just multiplication and
addition, with corresponding defining axioms. The induction
axioms, however, are restricted to quantifier-free A(x). An inductive
proof of (x)A(x) in PRA is thus quantifier-free, and indeed is often
called "logic-free": it consists in a series of rewrites, as typified
by the inductive proof of x+y=y+x or x*(y*z)=(x*y)*z. It has been argued
by Tait, and is widely accepted, that PRA embodies finitistic mathematics
in Hilbert's sense. Thus even if we completely set aside the idea that
the consistency of PA is somehow problematic, Gentzen's proof remains
significant: it shows that every proof in PA of a statement of the
form (x)A(x) with A(x) a primitive recursive predicate can be proved using
finitistic reasoning extended with epsilon_0-induction.