\documentclass{article}
\usepackage{amssymb}
\title{Identity of indiscernibles in Quine's ``New Foundations'' and related theories}
\author{M. Randall Holmes}
\begin{document}
\maketitle
We demonstrate that equality is dispensable as a logical primitive in
set theory with stratified comprehension for open sentences and
without any extensionality axiom, and so in all nontrivial fragments
of Quine's system ``New Foundations'' of \cite{nf}.
We work in a first order language in which the only predicate is
$\in$. The results apply to languages with additional predicates (and
in fact to languages with function symbols) if the notion of
stratification is extended appropriately.
\begin{description}
\item[Definition:] A function $\sigma$ from variables to integers is called a {\em
stratification of $\phi$\/} iff for each atomic subformula `$x \in y$'
of $\phi$ we have $\sigma($`$x$'$)+1 = \sigma($`$y$'$)$. (If equality
were present as a primitive, we would also require for each atomic
subformula `$x = y$' that $\sigma($`$x$'$) = \sigma($`$y$'$)$.) A
formula $\phi$ is said to be {\em stratified\/} iff there is a
stratification of $\phi$.
\end{description}
The point of this definition is that a formula is stratified iff there
is a way to assign types to the variables in the formula which makes
sense in the simple theory of types of Russell (as simplified by
Ramsey). The following axiom scheme (introduced by Quine in his paper
\cite{nf}) is known to be consistent; it has the same paradox-averting
powers as the simple theory of types while avoiding the syntactical
encumbrances of type theory:
\begin{description}
\item[Axiom Scheme of Stratified Comprehension:]
If $\phi$ is a stratified formula in which the variable $A$ is not
free, $(\exists A.(\forall x.x \in A \leftrightarrow \phi))$.
Informally, $\{x \mid \phi\}$ exists when $\phi$ is stratified (in the
absence of extensionality assumptions, there may be more than one such
``set''; any use of the notation $\{x \mid \phi\}$ in this paper
refers to some witness to the appropriate instance of the
comprehension axiom, and does not implicitly assume the existence of a
unique or even a canonical witness).
\item[Definition:] A stratification of the abstract $\{x \mid \phi\}$ is defined as a stratification of the formula $(\forall x.x \in A \leftrightarrow \phi)$.
\end{description}
Quine proposed this axiom as part of the theory {\em NF\/} (``New
Foundations'') introduced in \cite{nf}. The only other axiom of {\em
NF\/} is the axiom of extensionality. He suggested the same
definition of equality which we will give below, but he did not
address the question as to whether the defined notion could be shown
to have the correct logical properties; in his later \cite{ml} he
gives a different definition of equality (from which the logical
properties of equality could not be derived) then postulates an axiom
from which substitutivity of identity can be derived.
The consistency of {\em NF\/} remains an open question. The axiom
scheme of stratified comprehension is known to be consistent, because
Jensen showed in \cite{nfu} that {\em NFU\/}, the theory in which
extensionality is restricted to nonempty sets (or, equivalently, in
which extensionality is restricted to sets and non-sets with no
elements are permitted) is consistent. Marcel Crabb\'e showed in
\cite{sf} that {\em SF\/}, the theory whose axioms consist entirely of
the axiom scheme of stratified comprehension, interprets {\em NFU\/}.
The axiom scheme of stratified comprehension can be liberalized.
There is no need for variables free in an instance of the stratified
comprehension scheme to satisfy stratification restrictions, since any
instance of naive comprehension which fails to be stratified for this
reason is actually a substitution instance of an instance of
stratified comprehension. This motivates the following:
\begin{description}
\item[Definition:] A function $\sigma$ from variables to integers is called a {\em
weak stratification of $\phi$\/} iff for each atomic subformula `$x
\in y$' of $\phi$ in which `$x$' and `$y$' are both bound we have
$\sigma($`$x$'$)+1 = \sigma($`$y$'$)$. (If equality were present as a
primitive, we would also require for each atomic subformula `$x = y$'
in which `$x$' and `$y$' were bound that $\sigma($`$x$'$) =
\sigma($`$y$'$)$.) A formula $\phi$ is said to be {\em weakly stratified\/}
iff there is a weak stratification of $\phi$.
\item[Observation:]
It is a consequence of the Axiom Scheme of Stratified Comprehension
that $(\exists A.(\forall x.x \in A \leftrightarrow \phi))$ holds
whenever $\phi$ is a formula in which $A$ is not free and $(\forall
x.x \in A \leftrightarrow \phi)$ is weakly stratified (notice that it
is not sufficient for $\phi$ to be weakly stratified; free occurrences
of `$x$' in $\phi$ must be subject to stratification restrictions as
well as the bound variables of $\phi$).
\item[Definition:] We say that a set abstract $\{x \mid \phi\}$ is weakly stratified
exactly when the formula $(\forall x.x \in A \leftrightarrow \phi)$ is
weakly stratified.
\end{description}
As we stated above, we will not work in the full theory {\em NF\/} or
even in {\em SF\/}. We adopt the version of the axiom scheme of
stratified comprehension restricted to quantifier-free formulas
$\phi$. This axiom scheme has been considered by Forster in
\cite{nfo}; the theory with extensionality and this scheme
(and with equality as a logical primitive) is there called {\em
NF0\/}, so our working theory may be called {\em NF0U\/}. We remind
the reader that we do not adopt equality as a logical primitive.
We define equality as follows:
\begin{description}
\item[Definition:] We define $x=y$ as an abbreviation for the formula $(\forall z.x \in z \leftrightarrow y \in z)$.
\item[Definition:]
For any formula $\phi$ and variables $x$ and $y$, we define
$\phi[y/x]$ as the result of substituting $y$ for all free occurrences
of $x$ in $\phi$. We define $\phi[u,v/x,y]$ as the result of
simultaneous substitution of $u$ and $v$ for free occurrences of $x$
and $y$, respectively.
\end{description}
The definition can be seen as motivated by Leibniz's principle of the
identity of indiscernibles. The essential property of equality is
that $x = y$ should imply $\phi[x/a]
\leftrightarrow
\phi[y/a]$. Our definition guarantees this when there is a set $\{a
\mid \phi\}$, but we are only provided with such a set when the abstract $\{a
\mid \phi\}$ is weakly stratified.
It is not immediately obvious that objects which are distinguishable
by their unstratified properties must be separated by sets. It may
not be obvious -- but it does turn out to be true!
\begin{description}
\item[Lemma:] If $\phi$ is a quantifier-free formula, then
$x = y \rightarrow \phi[x/a] \leftrightarrow \phi[y/a]$.
\item[Proof of Lemma:]
If $\{a \mid \phi\}$ is weakly stratified, this is obvious. The only
way in which this formula can fail to be weakly stratified is if
$\phi$ contains occurrences of $a \in a$. We define a modified
formula $\phi'$, obtained by replacing each occurrence of $a$ with one
of the new variables (not occurring in $\phi$) $a_0$ or $a_1$, in such
a way that each subformula $a \in a$ becomes $a_0 \in a_1$. It is
clear that the abstracts $\{a_0 \mid \phi'\}$ and $\{a_1 \mid \phi'\}$
are weakly stratified. Now $\phi[x/a] = \phi'[x,x/a_0,a_1]
\leftrightarrow x \in \{a_1 \mid \phi'[x/a_0]\} \leftrightarrow y \in \{a_1 \mid \phi'[x/a_0]\} \leftrightarrow \phi[x,y/a_0,a_1] \leftrightarrow x \in \{a_0 \mid \phi'[y/a_1]\} \leftrightarrow y \in \{a_0 \mid \phi'[y/a_1]\} \leftrightarrow \phi'[y,y/a_0,a_1] = \phi[y/a]$ follows by repeated applications of the hypothesis $x = y$ (as defined above) and the axiom scheme of stratified comprehension for open formulas. The proof of the Lemma is complete.
\item[Theorem:] For any formula $\phi$, $x = y \rightarrow \phi[x/a] \leftrightarrow \phi[y/a]$.
Suppose without loss of generality that $\phi$ is given in prenex
normal form, and proceed by induction on the number of leading
quantifiers. The basis case of the induction is handled by the Lemma.
We now present the induction step. Suppose that $\phi$ = $(\exists
z.\psi)$. We prove $\phi[x/a] \rightarrow \phi[y/a]$. Suppose that
$\phi[x/a] = (\exists z.\psi[x/a])$ is true. Select a witness $w$
which makes this existential statement true. Apply the inductive
hypothesis to $\psi[x,w/a,z]$ to conclude that $\psi[y,w/a,z]$ holds,
and so that $\phi[y/a]$ holds. The same argument with the roles of
$x$ and $y$ interchanged establishes the converse implication. Since
universal sentences are negations of existential sentences, this is
all that is needed. The proof of the Theorem is complete.
\end{description}
It should be clear that our claim of the logical adequacy of the
defined notion of equality has been established.
This result applies to almost all of the known consistent fragments of
{\em NF\/}. It is clear that the result applies to {\em NF\/} itself
and to {\em NFU\/}. We claim that it also applies to the theory {\em
NF$_3$\/} of Grishin (extensionality plus stratified comprehension for
formulas $\phi$ with stratifications with range having only three
elements) and the theory {\em NFP\/} of Crabb\'e (predicative {\em
NF\/}: extensionality plus stratified comprehension for those
abstracts $\{x \mid \phi\}$ with stratifications $\sigma$ whose range
includes nothing larger than $\sigma($`$x$'$)+1$ and which map only
free variables to $\sigma($`$x$'$)+1$). Both of these theories are
known to be consistent and admit interesting known-to-be-consistent
extensions. This claim can be established by a careful consideration
of weakly stratified abstracts $\{x \mid
\phi\}$ with $\phi$ quantifier-free. Any such abstract is a
substitution instance of an abstract $\{x \mid \phi'\}$ in which no
free variable appears more than once. Such an abstract admits a
stratification with range $\{0,1,2\}$ obtained by assigning $x$ type
1, then assigning each free variable which occurs in an atomic
subformula with $x$ type 0 or 2 as the syntax requires, and assigning
all remaining free variables type 0. The resulting stratification
satisfies the conditions placed on stratifications by both {\em
NF$_3$\/} and {\em NFP\/}.
The result appears to apply as well to the intuitionistic version of
{\em NF\/} (studied recently by Dzierzgowski; not known to be
consistent nor known to be as strong as classical {\em NF\/}). Prenex
normal form is not available, so a more complex structural induction on
formulas is needed, with clauses for propositional connectives as
well as quantifiers, which appears to succeed.
\begin{thebibliography}{99}
\bibitem{sf} Marcel Crabb\'e, ``On {\em NFU\/}'', {\em Notre Dame Journal of Formal Logic\/}, vol. 33 (1992), pp. 112-19.
\bibitem{nfo} T. E. Forster, ``Term Models for Weak Set Theories with
a Universal Set'', {\em Journal of Symbolic Logic\/}, vol. 52 (1987),
pp. 374-87.
\bibitem{nfu} Ronald Bjorn Jensen, ``On the consistency of a slight
(?) modification of Quine's `New Foundations'\,,'' {\em Synthese}, 19
(1969), pp. 250--63.
\bibitem{nf} W. V. O. Quine, ``New Foundations for Mathematical
Logic,'' {\em American Mathematical Monthly}, 44 (1937), pp. 70--80.
\bibitem{ml} W. V. O. Quine, {\em Mathematical Logic\/}, second
edition, Harvard, 1951.
\end{thebibliography}
\end{document}