FOM: second-order logic is a myth

[Randall Holmes]

It seems clear to me that second-order logic is topic neutral.
Second-order quantifiers do not need to be understood as ranging over
sets; it is sufficient to understand them as ranging over properties.

For example, to be a natural number is to be an object which has all
the properties which belong to 0 and belong to the successor of any
object having them (once we decide what "0" and "successor" mean).
The specifically mathematical content of this definition is all in the
definitions of "0" and "successor".

Talk of properties does not belong to any particular subject; in any
subject whatever, we will use language about properties.  If we adopt
the position that there "aren't any properties" (whatever this means),
the problem of explaining away talk about properties is a general
philosophical problem -- it belongs to philosophy, not to mathematics;
it may even be taken to belong to logic (see below)!  If we adopt the
position that there "are" properties and that we can quantify over
them, this is again a philosophical position which admits application
in every area of knowledge.

Historically, it is my understanding that Frege originally presented
his logic (the ancestor of modern first-order logic) in a way which
admitted quantification over predicates.  Moreover, I believe that the
first-order theories of arithmetic and analysis are adaptations of
theories originally stated in second-order form before set theory was
ever formally proposed (or at about the same time).

Second-order logic is not set theory in disguise.  It may be the
theory of universals, but this is not a mathematical issue -- the
issue of existence or nonexistence of universals is of universal
interest (topic-neutral).

I agree that second-order logic is not a formal system of deduction.
If formal systems of deduction exhaust logic, then "second-order
logic" is not "logic".

I think that second-order logic is _obviously_ logic, and so (by
reductio) formal systems don't exhaust logic.  Logic includes the
study of the form of sentences; the maneuver involved in second-order
logic (quantifying over predicates) is certainly of logical interest
and calls for logical analysis.

I'm looking at a dictionary definition of the word "logic".  The 2nd
definition of the word given is "a system of formal principles of
deduction or inference".  I have already granted (as I must) that
second-order logic is not that.  (second-order logic is not a logic(2)).

The first definition given is "a science that deals with the canons
and criteria of validity in thought and demonstration and that
traditionally comprises the principles of definition and
classification and correct use of terms and {\em the principles of
correct predication\/} (my italics) and the principles of reasoning
and demonstration".  It appears obvious that the question of the
meaningfulness of second-order quantifiers falls under this
definition; second-order logic is part of the subject matter of logic
(though one might belong to a school of logic which regards
second-order logic as inadmissible: "thou shalt not quantify over
predicates").  Second-order logic falls within the scope of logic(1);
the question of the admissibility of second-order logic as a
fundamental system of reasoning is part of the analysis of
predication, which is a logical(1) issue.

If one's "principles of correct predication" allow one to quantify
over predicates (part of one's logic(1)) then a logic(2) (formal
system of inference) which one would accept would be the system in
which the rules of first-order logic are extended to cover
second-order quantifiers and comprehension axioms are provided to
assert the existence of particular properties.  This is of course
formally also a first-order two-sorted system.  (Further logical(1)
reasoning would lead one to accept stronger and stronger logics(2) in
a way which no meta-logic(2) can capture formally, e.g. by considering
G\"odel sentences of successive theories).

The "principles of definition" clause of the definition of logic(1) is
also of interest.  The natural numbers and the reals are definable up
to isomorphism in second-order logic; this is not the case in any
first-order theory.  Techniques which allow effective definitions are
of logical interest!  This is important re the claim that second-order
logic is set theory in disguise: the use of mathematical induction and
least upper bound principles (defining characteristics of the natural
numbers and the real line) is older than set theory; it is more
straightforward to understand these as applications of 
topic-neutral logic(1) to mathematics than as covert applications of a
branch of mathematics which at that time was not recognized!

Beyond second-order logic I partially agree with Steve and others.
Third order logic adds nothing to the logical(1) effectiveness of
second-order logic; it is best understood as a second-order theory
with two sorts of first-order object: sort 0 of third order logic
translates to a first-order sort; sort 1 of second-order logic
translates to a first-order sort; sort 2 of first-order logic
translates to the second-order sort of properties of objects of the
first-order sort interpreting sort 1.  But second-order logic does
things of logical(1) interest for us which first-order logic does not
do.  (Of course first-order logic has advantages of its own: it is a
logic(2) of fundamental importance, though we can use second-order
considerations to build stronger logics(2)).

In particular, much as I like the theory of types, NF or NFU, I don't
normally view them as higher-order logics.  But I should add that I
don't regard it as illegitimate to view the theory of types as a
higher order logic: it is a logical(1) issue whether it is sensible to
have predicates of predicates, etc, and whether one can quantify over
such things.  Higher order logic can be viewed as logic(1) as well,
but it is important to be aware that it is eliminable in favor of
second-order logic -- but not in favor of first-order logic, in which
one loses advantages re definition and analysis of predication (and
gains advantages re formalization as a logic(2)).  Similarly, NF or
NFU could, I suppose, be viewed as logics(1) (and I think have been by
some).  Associated with any of these higher-order logics there is a
logic(2) which is the corresponding many-sorted first-order theory;
but those who accept these theories as logics(1) would also subscribe
to stronger logics(2) in ways which cannot be determined from the
simplest logic(2) associated with each theory.  Subscribing to the
theory of types as a first order theory is not at all the same thing
as subscribing to omega-order logic as a logic(1).

Any positions expressed here are tentative; I enjoyed the way that the
dictionary definition almost automatically made the points I wanted to
make, and Simpson, at least, (qua Aristotelean) ought to take
arguments from the proper definitions of terms seriously...

And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes
the gates of Cantor's paradise, that the       | Boise State U. (disavows all) 
slow-witted and the deliberately obtuse might | holmes at math.idbsu.edu
not glimpse the wonders therein. | http://math.idbsu.edu/~holmes