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.