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

[Roger Bishop Jones]

In response to : <JoeShipman at aol.com>Wednesday, August 30, 2000 5:01 AM


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

This is indeed obvious.
Except for your reference to "underlying set theory".

There will be no "underlying set theory" unless you attempt to define the
semantics of SOL in set theory.
If you do, and you chose first order set theory for that purpose, then you
have made a mistake.
It's not up to the job.
This is down to pretty much the same causes as the previously alleged
irreducibility of SOL to FOL by meaning preserving reductions.
That the semantics of second order logic cannot properly be defined in first
order set theory is a problem with set theory not with SOL.
(a second order axiomatisation of set theory would do of course, or third
order logic)

> If you want to talk about deductive calculi and actual proofs, standard
> semantics won't get you anywhere useful.

Unless you think that using a language in which your concepts mean what they
are intended to mean is helpful.
Standard semantics is essential even if you only want to talk specifically
about natural numbers, and of course, formulae and proofs.

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

I consider it a considerable loss of deductive power to derive theorems
which may happen to be syntactically identical but in fact mean something
else altogether.

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

Personally I think it a red herring to worry about how "logical" your axioms
are.
It suffices that the deductive system is sound relative to the semantics of
the language.
This makes all the theorems "analytic" in one important sense of that word
(essentially that of A.J.Ayer, who made pretty much this point in "Language
Truth and Logic").

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

If you substituted "PROOF THEORETIC" for "TECHNICAL" here, I might let it
pass.
But as one who uses formal notations for communication rather than as an
object of study, I consider semantics to be a technical matter of prime
importance.

I hope we are not still talking "at cross purposes", but in my experience
this is the norm rather than the exception.

Roger Jones