FOM: Re: SOL confusion

[JoeShipman@aol.com]

Harvey and Martin,

I am enjoying your exchange, which seems to be gradually converging but is 
not there yet.  Permit me to pose some questions, which seem to me to be the 
most important issues in the discussion that are not merely reducible to 
differing uses of terminology.

Because of SOL's incompleteness, there is no obvious choice for a deductive 
calculus (deductive calculus=algorithm for generating validities, or, 
alternatively, satisfiabilities).  However, there are some standard deductive 
calculi for SOL, for example the ones given in chapter II of Manzano's book, 
which are sound for standard semantics.  Furthermore, these calculi allow for 
the development of "ordinary mathematics" without the standard 
set-theoretical apparatus, using an interpretation where the first-order 
variables are integers, the unary relations are sets of integers, etc.  (The 
development can proceed further either by coding, as in Simpson's "Subsystems 
of Second-Order Arithmetic", or by introducing higher types, since we know 
the validities of HOL are recursively equivalent to the validities of SOL.)

Questions: Is there a canonical "most complete" deductive calculus for SOL 
other than the "ZFC-calculus": "generate proofs in ZFC that sentences of SOL 
are second-order-validities in the standard semantics"?  If so, how does its 
set of validities compare under inclusion with the ones generated by the 
ZFC-calculus? 

The point here is that the ZFC axioms are "set-theoretic" rather than 
"logical" in nature.  I want to compare, not "FOL vs. SOL", but rather 
"FOL+ZFC vs. SOL", in order to evaluate the philosophy of mathematics known 
as "logicism".  

I expect that none of the standard calculi for SOL generate any validities 
not generated by the ZFC-calculus.  (For any reasonable deductive calculus 
CALC for SOL that ZFC proves is sound, the arithmetic statement "CALC is 
consistent" is equivalent to the validity of a particular second-order 
sentence that belongs to the ZFC-calculus but not to CALC; the interest would 
be in finding a plausible calculus whose soundness was not provable in ZFC.)

So it appears that FOL+ZFC is "stronger" than SOL with respect to any of its 
usual calculi.  But is this greater strength too high up to matter in 
ordinary mathematics?  Another way of asking this is "for what subsystems X 
of ZFC is FOL+X still stronger than SOL with respect to any of its usual 
calculi? "  The last question can be made precise by specifying a particular 
SOL-calculus; for definiteness I will take the calculus C2 from Chapter II of 
Manzano.

-- Joe Shipman