Re: A question on GIT.
From: Herman Jurjus (h.jurjus_at_hetnet.nl)
Date: 09/09/04
- Next message: Andrew Boucher: "Re: A question on GIT."
- Previous message: Jose Juan Mendoza Rodriguez: "Re: theorems/problems with lots of quantifiers"
- In reply to: Andrew Boucher: "Re: A question on GIT."
- Next in thread: Andrew Boucher: "Re: A question on GIT."
- Reply: Andrew Boucher: "Re: A question on GIT."
- Messages sorted by: [ date ] [ thread ]
Date: Thu, 09 Sep 2004 21:45:10 +0200
Andrew Boucher wrote:
> 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.
Thank you very much! A very interesting post. You wrote about this some
time ago, didn't you. Any newest references?
> 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.
Ah! Do you have a reference for this?
-- Cheers, Herman Jurjus
- Next message: Andrew Boucher: "Re: A question on GIT."
- Previous message: Jose Juan Mendoza Rodriguez: "Re: theorems/problems with lots of quantifiers"
- In reply to: Andrew Boucher: "Re: A question on GIT."
- Next in thread: Andrew Boucher: "Re: A question on GIT."
- Reply: Andrew Boucher: "Re: A question on GIT."
- Messages sorted by: [ date ] [ thread ]