[FOM] Re: higher order logic, Slater

[Randall Holmes]

Dear FOM colleagues (to moderator, this could replace my previous
short note):

Slater objects that my S is a mathematical function.  It certainly
is a function symbol, and that was a slip on my part.  I should
have used a binary predicate Sxy (if S were successor, this could
be read "x is a successor of y" -- but S is not successor!)  or
I should have observed that the language of second-order logic
can be thus extended.

There's nothing explicitly "mathematical" about function symbols:
the relation of the term "the father of x" to the predicate
"y is father of x" in English has the same logical form.  Further,
there is nothing to indicate that S is a "mathematical" function:
the terms 0 and S in my example are not constants but quantified
variables, and they could be witnessed by taking 0 to be any object
and S to be the successor relation on a countably infinite sequence
of objects (which might be physical objects if the universe is large
enough).

Actually, modern treatments of second-order logic _do_ include
"nominalizing constructions": one can write terms {x | Px} for
arbitrary sentences P (or one could write something like [x:Px] if one
wanted to make it clear that one was not talking about a set)
containing x and use them as predicates (not, of course, as objects --
there is a type distinction).  Higher-order logic of order higher than
2 (up to and including omega) is well-understood and does allow
formalization of "properties of properties".  Quantification over
quantifiers can't be handled in less than third-order logic, since
quantifiers correlate with second-order properties.  Further, the
English language also includes nominalizing constructions for
predicates associated with complex open sentences (Slater seems to
value observations of this kind, and it is useful to point out that
this kind of construction is not a specifically mathematical novelty).

Sincerely, Randall Holmes