FOM: Re: SOL confusion
JoeShipman@aol.com
JoeShipman at aol.com
Fri Sep 8 20:06:20 EDT 2000
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
More information about the FOM
mailing list