
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 secondorder >> logic corresponding to the wellknown formal systems for >> firstorder logic, exactly what does it mean for something >> to go through in secondorder PA? > > It means, can it be proved in the system PA2, secondorder Peano > Arithmetic? Briefly, PA2 is a system of secondorder 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 twosorted *first*order logic. Its models have (in one way of describing them) two universes: One over which the naturalnumber variables range, and another over which the setofnaturals 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 firstorder sentences about them).
When you're talking about true secondorder 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 naturalnumber variables range over elements of that universe, and the set variables range over subsets of the universe.

