FOM: ``Reduction'' of Second-Order Logic to First-Order Logic

[JoeShipman@aol.com]

Much of the discussion about second-order logic seems to be at cross-purposes.

It is obvious that the standard semantics for second(and higher)-order logic 
is more natural but that this logic doesn't have the nice proof-theoretic 
properties that second-order logic with Henkin semantics or first-order logic 
do, and the set of validities depends crucially on your underlying set 
theory. 

If you want to talk about deductive calculi and actual proofs, standard 
semantics won't get you anywhere useful.  You might as well just interpret 
type theory in V(omega+omega) and make the theorems of your deductive 
calculus be the sentences which when so interpreted are theorems of ZFC.  Or, 
as Manzano shows in "Extensions of First Order Logic", you can change your 
semantics with no loss of real deductive power but a big gain in 
proof-theoretical convenience. (There's also a lot of other good stuff in her 
book unrelated to the FOL-SOL issue.)

On the other hand, if you care most about the philosophy of mathematics, and 
have no problem with the notion of arbitrary subset or arbitrary relation, 
you may prefer to frame things in terms of SOL (or Type Theory) with standard 
semantics, on the grounds that this comes very close to achieving the 
logicist goal of reducing mathematics to logic.  The Godel incompleteness 
phenomenon is really no worse here; the only real problem I have with this 
approach is that I'm not clear on how "logical" the axioms of Choice and 
Replacement can be made (because I'll want a deductive calculus whose axioms 
are logical but which can still obtain theorems we need these axioms for in 
ZFC).

I think Manzano makes a persuasive case that SOL doesn't have any important 
TECHNICAL advantages over (many-sorted) FOL, and I am sure that when people 
like Steve emphasize this point they are also aware of the PHILOSOPHICAL 
advantage that it unquestionably does have.

-- Joe Shipman