FOM: SOL confusion

[Harvey Friedman]

Reply to Shipman 10:48AM 9/6/00:

>I find this situation a little confusing.  By working in SOL with standard
>semantics one can develop much of ordinary mathematics in a more natural way
>than via the usual foundation in first-order ZFC (or ZC, since the
>Replacement Axiom is not needed in the standard developments).  But
>apparently within set theory one needs more information than which sentences
>are second-order validities, there have to be axioms specifically about sets,
>such as the powerset axiom.

You cannot formalize any mathematics at all by working in SOL with standard
semantics. That's because SOL with standard semantics, which is the same as
simply SOL, does not have any axioms or rules of inference.

If you add axioms and rules of inference to SOL for the purposes of
formalizing mathematics, then you get a version of set theory. Its
convenience for the purposes of formalizing mathematics will then directly
correspond to the extent that it resembles or imitates standard systems of
set theory.