|
|
Re: Axiomization of Number Theory
Posted:
Jul 30, 2003 11:53 PM
|
|
Andrew Boucher wrote:
> David C. Ullrich wrote:
>> Supposing for the sake of argument that Keith was correct
>> when he said that there's no formal system for second-order
>> logic corresponding to the well-known formal systems for
>> first-order logic, exactly what does it mean for something
>> to go through in second-order PA?
>
> It means, can it be proved in the system PA2, second-order Peano
> Arithmetic? Briefly, PA2 is a system of second-order logic with full
> comprehension and the Peano Axioms (where the Induction Schema may be
> replaced by an axiom).
This is a spot where it's easy to get confused over terminology, and
I'm not even sure exactly what the standard terminology is. But
in any case what Andrew is describing (which I snipped) is actually
a theory of two-sorted *first*-order logic. Its models have (in one
way of describing them) two universes: One over which the
natural-number variables range, and another over which the set-of-naturals
variables range. I think these may be called "Henkin models" or
some such.
PA2, interpreted *this* way, *does* admit a formal system that mechanically
verifies or rejects putative proofs, and it does *not* fully determine
the natural numbers up to isomorphism (or even decide all first-order
sentences about them).
When you're talking about true second-order logic, you can take exactly
the same axioms as above, and now they *do* determine the natural numbers
up to isomorphism. But a "model" is a different sort of gadget: It
has only one universe. The natural-number variables range over elements
of that universe, and the set variables range over subsets of the universe.
|
|
