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

JoeShipman@aol.com JoeShipman at aol.com
Wed Aug 30 00:01:12 EDT 2000

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

```