Re: A question on GIT.

From: Andrew Boucher (Helene.Boucher_at_toto.fr)
Date: 09/09/04 

Date: Thu, 09 Sep 2004 21:33:35 +0200

In article <2qan75Ftaq0lU1@uni-berlin.de>,
 Herman Jurjus <h.jurjus@hetnet.nl> wrote:

> Now imagine what that would do to the _meaning_ of notions like
> 'fol-proof', 'consistent', 'recursively decidable'. All of these
> notions refer crucially to natural numbers, and especially to our
> realistic picture of the 'intended model of PA'.
> (Only finite proofs are allowed, only calculations with finitely
> many steps are allowed. In all these cases, unfeasibly large numbers
> are included, but infinite numbers (non-standard numbers), are
> excluded.)
>
> The difficulty, of course, is that it is very hard to imagine any
> mathematics in which the natural number sequence does not exist,
> or is not unique.
> It's like assuming a contradiction and discussing the consequences.
>
> --
> Cheers,
> Herman Jurjus

I was meaning to reply to a previous post of yours but I'll use this one.

Consider second-order Peano Arithmetic without the successor axiom (i.e.
excluding the assumption that every number has a successor). I could
go into the details, but just accept that there exists an axiomatization
of arithmetic which has as models the intended model as well as all
initial segments, {0}, {0,1}, {0,1,2}, etc. Such a system is
"downward" - once a natural number exists, all numbers less than it can
also be proven to exist. However, given any natural number, one cannot
prove that numbers greater than it exist.

Now you are right that usually "first-order logic" is usually defined in
a way which assumes PA and specifically the successor axiom, e.g. one
reads in beginning textbooks: If A is a wff and B is a wff, then (A&B)
is a wff. That is, there is the supposition that wffs can be
constructed ad infinitum: A, (A&A), ((A&A)&A), etc.

But this is not essential to the spirit of first-order logic. One could
define what a wff is in a downward fashion, e.g. A is a wff if there
exist B and C such that A is (B & C).

Similarly, one could define what an axiom is, and what a proof is, all
without supposing the successor axiom. E.g. something is a proof if it
can be broken down into smaller things satisfying particular conditions.
Intuitively, I hope, you see the process can be done in a "downward"
fashion, without supposing the existence of any larger numbers.

And finally one can define what it means for a system to be consistent,
still without the successor axiom. Icing on the cake: such a system
can prove its own consistency! (Godel doesn't apply - even Robinson's
Arithmetic Q uses the successor axiom.)

Now I'd assert that such a system is true and that the successor axiom
might not be true. So PA may not be true.

I would, though, expect PA still to be consistent, even if it is not
true. On the other hand, the completeness theorem's proof requires the
successor axiom, so even if PA is consistent, one cannot infer that PA
has a model.