[FOM] Slater and numbers

[Randall Holmes]

Dear FOM colleagues,

Slater's latest post needs interlinear commentary.

Thus Slater:

>Randall Holmes (FOM Digest Vol 9 Issue 32) is still wanting the set 
>of those sets with n members to be the number n, i.e. {x|(ny)(y isin 
>x)}=n.

I reply:

Actually, the point I am making is subtler than that.  I do rather
like the Frege natural numbers, but I'm not convinced that they
are THE natural numbers.  But no argument Slater has made proves that
they are not.

Thus Slater:

>  He writes

>>If I read your notation this way, then your sentence (nx)(Px) expands
>>to {x | Px} \in n.  So the numeral n is a set (or class, or
>>superclass) whose elements are exactly the extensions with n elements.

>Certainly if (x)(Px iff x isin {y|Py}), then (nx)Px is equivalent to 
>(nx)(x isin {y|Py}), and so maybe to: {y|Py} isin {x|(ny)(y isin x)}, 
>i.e. the set of Ps is in the set of those sets with n members.  But 
>that is not to say that (y|Py) isin n.

>>In other words, your numerical quantifier n is exactly the same thing
>>as my Frege natural number n,

>It would be if one could say what Holmes wants to say, namely 
>{x|(ny)(y isin x)}=n, but how can one say that?   Holmes needs to 
>provide a general reformulation of 'x has n elements'  which does not 
>involve a quantifiable place 'n', and there is no such.  There is no 
>problem with '(1x)Fx', '(2x)Fx', '(3x)Fx', etc. since these can be 
>turned into standard predicate logic expressions which do not involve 
>'1', '2' ,'3'.  But not so with '(nx)Fx', since given the recursive 
>definition which includes that (nx)Fx iff 
>(Ey)(Fy.([n-1]x)(Fx.-(x=y))), one cannot get rid of the 'n'.  Hence 
>in formulating Holmes' 'set ... whose elements are exactly the 
>extensions with n elements' one must allow the 'n' place to remain, 
>and his n={x|(ny)(y isin x)} cannot be a definition of the left hand 
>side.

I reply:

There are numerous such formulations.

1.  According to standard logical usage, what Slater writes 
(nx)(Px) does _not_ contain a quantifiable place "n".

2.  Leaving the Frege numerals entirely aside, we discuss how
things are done in ZFC.  Define 0 as {} (the empty set) and
define x+ as x \cup {x} as usual.  The Axiom of Infinity combined
with Separation tells us that there is a unique set \omega = N
which is the intersection of all sets which contain 0 and are
closed under the successor operation.  Elements n of this set
N are called "natural numbers".  To say that a set A has n members
is to say that there is a bijection between A and n.  The assertion
A ~ n (A is equinumerous with n) means that A has n members
(for concrete n), and it contains a quantifiable place for n.
Numerical quantifiers have never been mentioned.

Thus Slater:

>>I would answer that _standard_ syntax does not allow quantification 
>>over quantifiers.
>>But if quantifiers are to be taken as first class objects, I insist on
>>interpreting them as classes of extensions.
>
>Here is the nub of the matter, as I see it.  It is not just that 
>Holmes is here appealing to what is 'standard' (and elsewhere to what 
>is 'generally accepted') when he is admitting to wanting to say a lot 
>of non-standard things himself, like '2 is a member of 3' etc.  For 
>the 'n' in the quantifier 'nx' is a numeral, and it is that place 
>which needs to be quantified over to get the generality required, in 
>'iota-n(nx)Fx', etc.  So Holmes simply does not want to quantify over 
>such numerical places, and allow that the second-order properties 
>which those numerals denote exist.  'To be is to be the value of a 
>variable', and Holmes does not want to recognise that numbers, as 
>opposed to sets of things with numbers of elements, exist.  But such 
>'extensionalisation' quite generally is pointless, since one does not 
>remove reference to the property F if one replaces 'x has the 
>property F' with 'x is in the set of things with the property F'.
>
>And isn't '(nx)Fx' standard syntax?  'The set of Fs has n members' is 
>standard English, and quantification over the numerical places in 
>such expressions comes out of Frege, see David Bostock's 'Logic and 
>Arithmetic' (O.U.P. Oxford 1974, Vol 1, Ch 3), and the paper by Mayo 
>in JSL 2002 previously referred to, 'Frege's Unofficial Arithmetic'. 
>Frege 'officially' preferred 'Nx:Fx = n' to '(nx)Fx', but with 
>'Nx:Fx' as 'iota-m(mx)Fx' these are interderivable as I showed before.

I reply:

This _is_ the nub of the matter, and here I'm standing on bedrock.
Read a standard mathematical logic text.  Quantification over
numerical (or any) quantifiers is not allowed as a move in first-order
logic.  Frege might have quantified over them, and he also quantified
over predicates, but standard predicate logic as now understood does
not allow either of these moves.  This is not to say that they cannot
be fruitfully studied.

Very few logicians would identify the natural number n with the
quantifier in (nx)(Px), though we do understand that it is possible to
define such quantifiers for each concrete n.  The "n" in this context
does NOT represent a natural number (or any object) on a standard
understanding of logic -- it is just an abbreviation, and an entirely
independent one for each concrete n.  (nx)(Px) is itself standard
syntax (or rather a definitional extension of standard syntax, not
uniform in the parameter n), but the n cannot be bound.  To try to
quantify over it can be said to involve a confusion between theory and
meta-theory.

Although Frege may have done this and a few workers may have
investigated this subject, this is not a standard approach.  I'm
familiar with Bostock's work, and it is interesting but the logic in
it is not mainstream.

I'm entirely willing to admit the existence of second-order properties
represented by quantifiers.  In fact, one must suppose that
quantifiers represent second-order properties in order to allow
quantification over quantifiers.  But to read quantifiers in this way
is not part of standard predicate logic: one is now doing higher-order
logic.

Extensionalization (the identification of properties with their
extensions) is not pointless: it represents one of the answers to the
question of what identity conditions are for properties considered as
objects.  Further, if a quantifier Q represents a property, it will
respect extension in the following sense: (Ax)(Fx iff Gx) can
reasonably be supposed to imply (Qx)(Fx) iff (Qx)(Gx) no matter what Q
may be.  So Q is a property of _extensions_, not a property of
properties.  So it is entirely reasonable to regard a natural number n
(in Slater's sense) as a property of _sets_.  Since I hold that whatever
is so is necessarily so, I regard extensional identity as the correct
criterion of identity between properties, and identify properties and
sets completely.  But this is not prerequisite to understanding my
comments here.  [It is worth noting that completely nonextensional type
theory of properties and extensional type theory with urelements are
mutually interpretable theories (and the latter is mutually
interpretable with NFU); in my article "Foundations of mathematical
logic in polymorphic type theory" in a recent issue of Topoi, I
explain how to motivate NFU starting with type theory without any form
of extensionality.  Basically, the idea is to translate "x is an
element of y" as "x has the property y and y is a property depending
only on extension".]

Most fundamentally, and crucially for Slater to understand why his
arguments are unconvincing, the standard definitions of the natural
numbers have nothing to do with numerical quantifiers.  One cannot
argue from the grammar of numerical quantifiers to any position about
what numbers can or cannot be unless the point is granted that the
numbers must be defined in terms of numerical quantifiers, and it
isn't -- not by me, and in fact not by anyone to speak of in
mathematics or logic.

The Frege definition comes closest, since the sets which are used as
numerals in this definition actually do have a certain connection with
the numerical quantifiers (the extension of the Frege natural number n
is the same as the collection of _extensions_ which have the
second-order property represented by the numerical quantifier n).  But
the ability to quantify over the Frege natural numbers is derived from
the fact that the Frege natural numbers are individually sets
(objects) and that we can define the property of being a Frege natural
number in set-theoretical language and restrict quantifiers to that
domain.  At no point do we quantify over quantifiers in this
development; the logic is standard first-order logic all the way.  It
is interesting to observe at the end of the process that all the sets
which would represent the numerical quantifiers actually exist; it is
possible to _interpret_ the nonstandard logic with quantification over
quantifiers in NFU (as long as the quantifiers are only applied to
stratified formulas).

There is a further very serious logical problem with the
interpretation of numerical quantifiers as second-order properties.
The difficulty is that numerical quantifiers can be applied to
variables of different types.  If one regards numerical quantifiers as
second-order properties one seems to have to differentiate between
occurrences of numerical quantifiers over base type objects, or over,
for example, numbers (of base type objects) themselves.  Second-order
properties of extensions whose members are of different sorts must on
the face of it be of different sorts themselves.  So a sentence like
"the number of natural numbers less than 9 is the same as the number
of planets circling the sun" would be ill-typed.  In the
interpretation in NFU (with an additional strong axiom) there are no
type distinctions and so the identification of numerical quantifiers
over all domains succeeds.  The sentence "For all n, the number of
natural numbers less than n is equal to n" provides a further logical
caution: the interpretation of this sentence in NFU is what is called
Rosser's Axiom of Counting, and it isn't a theorem of NFU: NFU with
the Axiom of Counting is consistent but significantly stronger than
NFU with Infinity (which is equivalent in strength to the theory of
types with infinity).  [obviously this is true for every concrete n,
but the simplest models of NFU contain nonstandard natural numbers] It
is possible to justify polymorphic treatment of the numerical
quantifiers over different domains, but it is not trivially easy.

I actually quite like higher-order logic, and I even like considering
the possibility of quantifying over quantifiers, but these are not
logically primitive moves (and thus probably should not be components
of the foundational exercise of defining the natural numbers).  It is
generally (although not universally) believed that to do higher order
logic is at bottom to do set theory (mod quibbles (and they are
demonstrably just quibbles from a _mathematical_ standpoint) about
extensionality).

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.boisestate.edu
not glimpse the wonders therein. | http://math.boisestate.edu/~holmes