FOM: FoM: Neo-Fregean reverse mathematics

[A.P. Hazen]

(This may not lead to anything interesting AT ALL; it's just something that
caught my attention.)
   As Charles Parsons points out, the two systems PA2 (Second-Order Peano
Arithmetic) and "FA" ("Frege Arithmetic"=Second-order logic plus "Hume's
Principle") are PROOF-THEORETICALLY equivalent.  Each can be interpreted in
the other.
   Looked at SEMANTICALLY (with the "standard" semantics, not the "Henkin"
one) they are startlingly different: PA2 is categorical, and its only (up
to isomorphism) model has a denumerable domain of individuals.  FA has
models with individual domains of every infinite cardinality.  This has
recursion-theoretic consequences.  The sets of (semantically) valid
sentences of the two systems are both non-recursive (and non-r.e.), but the
degree of the set of validities of FA is much higher than that of the set
of validities of PA2.   ... Relating this to the proof-theoretic point: I
guess the point is that the interpretation of PA2 in FA is FAITHFUL, but
that of FA in PA2 is not,  since it translates non-theorems of FA (for
instance: any two concepts that don't have natural numbers as cardinalities
have the same cardinality) into theorems of PA2.
   I don't know what follows from this, but it seems as if it's the sort of
thing that OUGHT to be interesting!  (O.k., I'll shut up.)
--
   Allen Hazen
   Philosophy Department
   University of Melbourne