FOM: SOL confusion

[JoeShipman@aol.com]

In a message dated 9/6/00 12:44:20 PM Eastern Daylight Time, 
friedman at math.ohio-state.edu writes:

<< 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. >>

Harvey --

Of course I am referring here to formalizing mathematics in SOL using a 
deductive calculus such as one of the calculi given in Manzano's book.  I 
just left the deductive calculus unspecified because my point was that ANY 
deductive calculus which produces second-order validities will fail to be 
strong enough to reproduce some theorems of ZFC without adding axioms of a 
set-theoretic rather than a logical character.  This is the point of my fifth 
question which was answered by Solovay.

The point of my fourth question was to establish that furthermore, any 
reasonable deductive calculus for SOL won't do more in the way of generating 
second-order validities than ZFC can.

I think I agree with you that the effectiveness of a deductive calculus for 
SOL will "directly correspond to the extent that it resembles or imitates 
standard systems of
 set theory" -- by asking these technical questions I was trying to clarify 
this very point.

-- JS