[FOM] higher order logic, Slater

[Randall Holmes]

Dear FOM colleagues,

I want to comment further (briefly I hope) on the logical moves being
used by Slater.  Probably most of us (including Slater) know this, but
I want it on record so that I'm not in danger of being mysterious to
anyone.

In standard first-order logic, we have the following constructions.

We have variables representing objects (possibly of various types,
but I won't go into this here):  x1, x2, x3... which I might use
any lower-case letter for.

We have predicates P1, Q2, R3 of various arities which can form
atomic sentences P1x, Q2xy, R3xyz.   I won't include numerals 
as parts of the names of the predicates.

We have logical connectives:  Px & Qxy is a sentence, for example.

We have quantifiers:  (Ax)(P(x)) (where P(x) is an arbitrary sentence
with x free) or (Ex)(P(x)) are sentences.

Normally, quantification is only allowed over variables (lower-case
letters), because these are the only "objects" in play.

In "higher-order logic", we allow quantification over _predicates_.

So for example we might say

(E0)(ES)((Ax)(~Sx = 0) & (Axy)(Sx = Sy -> x=y)),
capturing the idea that there is a sequence with some of the properties
of the sequence of natural numbers.

Higher order logic is very expressive but does not have the nice
proof-theoretic and model-theoretic properties of first-order logic.
A predicate variable P (of arity one, for example) is instantiable
by any complex open sentence P(x) with x free.  

The most common way to make sense of higher-order logic is to
interpret it as a kind of set theory (actually type theory): the unary
predicate P may be understood as the set {x | P(x)} and the sentence
P(x) is equivalent to x \in P.  Notice that this is _typed_ set
theory: P is not the same kind of object as the lower-case variables
x, and we cannot even consider P(P).  If we allow ourselves to
consider predicates of predicates, etc, we end up with a type theory
like that of Russell (really more like that of Ramsey).  (n-ary
predicates belong to types of n-ary relations in this system (as they
do in PM); we do not necessarily have the reduction of relations to
sets of n-tuples).  There are other issues, about extensionality for
example, which I won't go into.

Slater (or some of his intellectual predecessors, I'm not sure) have
observed that the quantifiers can be extended by definition beyond
A and E to introduce numerical quantifiers (nx)(Px) meaning
"there are exactly n x such that P".  This is unexceptionable (in
logic with identity).

Where they slip off the rails of standard predicate logic is in
proposing to quantify over these quantifiers.

How are we to make sense of (En)((nx)(P)) (which should mean "P is
finite"?).  A quantifier is a predicate of predicates: to assert
(Qx)(Px), if we are going to nominalize Q, must reduce to something
like Q({x | Px} or further to {x | Px} \in Q.  This is precisely
analogous to the standard interpretation of higher-order logic as a
type theory.  The object Q may be supposed to be of a different type
than the predicate P and the object x, just as in higher-order type
theory.

So the numerical quantifier n turns out to be interpretable
(just as I have said before) as a property of all sets of objects
of the type of the lower-case variables which have n elements.

Note that here we still have a type-theoretic rather than a
set-theoretic viewpoint.

The reasons to pass to a true set theoretic viewpoint (in which the
typed sets implementing quantifiers and predicates become general
objects) are the same as the reasons that the type discipline of
Russell's system was abandoned.  When we count things of different
types in type theory, we find that the types of our "numbers" are
different.  Of course, the temptation to proceed directly to
polymorphism in a formalism like Slater's could prove irresistable:
the formalization of something like "for all n, there are n natural
numbers less than n" in Slater's system would make no sense in type
theory (because the first n in "there are n natural numbers less than
n" counts natural numbers and the second presumably counts base type
objects).  This move exhibits (to adapt a saying of Russell (?)) all
the advantages of theft over honest toil...

In New Foundations or NFU (with suitable additional axioms), all of
this works perfectly without any (absolute) types.  The sets
corresponding to Slater's numerical quantifiers exist and are
precisely the Frege natural numbers.  For that matter, the set {V}
corresponding to the universal quantifier and the set V - {\emptyset}
corresponding to the existential quantifier also exist.  Any sentence
(Sx)(P(x)) where P is stratified and S is a set has an interpretation.
So there is an extension of Slater's language in which his numerical
quantifiers _are_ the Frege natural numbers.  

About this I have two comments:

  1.  To restrict your grammar is not to make the "ungrammatical"
sentences you avoid false -- it is simply to avoid considering them.

  2.  The reduction of Slater's system to set theory by this or some
other strategem is essential in order to establish that it makes
sense.  Reification of quantifiers is a logically dangerous move which
has to be justified by exhibiting _how_ they can be reified.

Mathematics is a religion!	|   --Sincerely, M. Randall Holmes
We are Reform Pythagoreans      |   Math. Dept., Boise State Univ.
(we eat beans).	No official BSU |   holmes at math.boisestate.edu
endorsement of above opinions!  |   http://math.boisestate.edu/~holmes