Re: Fw: Something for Platonists]

From: Bruno Marchal <marchal.domain.name.hidden>
Date: Tue, 17 Jun 2003 12:11:53 +0200

At 10:46 16/06/03 -0700, Hal Finney wrote:
>Jesse Mazer writes:
> > Yes, a Platonist can feel as certain of the statement "the axioms of Peano
> > arithmetic will never lead to a contradiction" as he is of 1+1=2, based on
> > the model he has of what the axioms mean in terms of arithmetic. It's hard
> > to see how non-Platonist could justify the same conviction, though, given
> > Godel's results. Since many mathematicians probably would be willing to
> bet
> > anything that the statement was true, this suggests a lot of them are at
> > least closet Platonists.
>
>What is the status of the possibility that a given formal system such as
>the one for arithmetic is inconsistent? Godel's theorem only shows that
>if consistent, it is incomplete, right? Are there any proofs that formal
>systems specifying arithmetic are consistent (and hence incomplete)?

As Jesse Mazer said we all have an intuitive model of Peano Arithmetic (PA),
and this should convince us of PA consistency. (We learned that model in
secondary school).
We can "formalize" such an argument in a set theory like ZF, that is, a model
of PA can be constructed in ZF, as a first order citizen. Now this should not
really convince us that PA is consistent because the ZF axioms are more
demanding, and we would be entitled to ask for a proof of the consistency
of ZF.
By Godel second incompleteness theorem PA cannot prove the consistency of
PA, ZF cannot prove the consistency of ZF. But ZF can prove the consistency
of PA. Note that this latter fact *can* be proved in PA, that is: PA can
prove that
ZF can prove the consistency of PA, of course PA cannot prove the consistency
of ZF, so this is not very useful here.
A perhaps more relevant question is: does it exist a *finitary* proof of PA
consistency?
It all depends of course of what is meant by "finitary". If by finitary
you mean
"arithmetically representable", then by Godel, the answer is no. But many
logicians
consider that "transfinite induction" toward some reasonable ordinal can be
considered as finitary. Actually Gentzen succeeds in presenting a proof of the
consistency of PA through a transfinite induction up to \epsilon_0 (which
is omega
up to omega up to omega up to omega ...). This shows (by Godel again) that
"transfinite induction up to \epsilon_0" cannot be done in PA, although it
can be
shown that all transfinite induction up to any \alpha little than
\epsilon_0 can be
done in PA. This has lend to "ordinal analysis" of formal theories where the
strongness of provability of a theory is measured in term of ordinal. Remember
that computability is an absolute notion (Church thesis), and formal
provability is a
necessary relative notion.
I conjecture that the consistency of COMP should need at least a
transfinite induction
up to the Church-Kleene least non constructive ordinal (omega_1^CK).
This should reflect the fact that the consistency of COMP is not provable by
any consistent machines ... (although machines could bet on it, at their
own risk
and peril).

Bruno
Received on Tue Jun 17 2003 - 06:11:26 PDT