1 Introduction
1.1 Tangled type theory
The language
${\mathcal {L}_{\mathrm {TST}}}$
of Simple Type Theory is the many-sorted language of set theory with one binary relation symbol
$\varepsilon $
and countably many types (or sorts) indexed by
$\mathbb {N}$
. Each variable of
${\mathcal {L}_{\mathrm {TST}}}$
is assigned a unique type, which we indicate by a superscript. The
${\mathcal {L}_{\mathrm {TST}}}$
-formulas are built inductively from the atomic formulas
$x^i \varepsilon y^{i+1}$
and
$x^i = y^i$
in the usual way.
Simple Type Theory (
$\mathrm {TST}$
) is axiomatized by two sets of axioms. The Axiom of Extensionality (
$\mathrm {Ext}$
) is the set of all the following sentences for each type
$i \in \mathbb {N}$
:
$$\begin{align} \forall x^{i+1}, y^{i+1} (x^{i+1} = y^{i+1} \leftrightarrow \forall z^i (z^i \varepsilon x^{i+1} \leftrightarrow z^i \varepsilon y^{i+1})). \end{align} $$
The Axiom of Comprehension (
$\mathrm {Co}$
) is the set of all the following sentences for each type
$i \in \mathbb {N}$
and formula
$\phi $
of
${\mathcal {L}_{\mathrm {TST}}}$
:
$$\begin{align} \forall \bar{u} \exists y^{i+1} \forall x^i (x^i \varepsilon y^{i+1} \leftrightarrow \phi(x^i, \bar{u})), \end{align} $$
where
$y^{i+1}$
is not free in
$\phi $
. We define
$\mathrm {TST} = \mathrm {Ext} + \mathrm {Co}$
. For each
$i \in \mathbb {N}$
, we let
$\mathrm {CoP}^{i+1}$
be the axiom we get from
$\mathrm {Co}^{i+1}$
if we restrict the types of the bound variables in
$\phi $
to not exceed i and the types of the free variables in
$\phi $
to not exceed
$i+1$
. The Axiom of predicative Comprehension (
$\mathrm {CoP}$
) is the set of all
$\mathrm {CoP}^{i+1}$
for
$i \in \mathbb {N}$
. We define predicative Simple Type Theory (
$\mathrm {TSTP}$
) as
$\mathrm {TSTP} = \mathrm {Ext} + \mathrm {CoP}$
.
Now, the language
${\mathcal {L}_{\mathrm {TTT}}}$
of Tangled Type Theory is the same as
${\mathcal {L}_{\mathrm {TST}}}$
, but its formulas are built inductively from the atomic formulas
$x^i = y^i$
and
$x^i \varepsilon y^j$
for
$i < j$
. For each function
$s \colon \mathbb {N} \to \mathbb {N}$
and each
${\mathcal {L}_{\mathrm {TST}}}$
-formula
$\phi $
, we denote by
$\phi ^s$
the
${\mathcal {L}_{\mathrm {TTT}}}$
-formula that we get if we replace each type index i of a variable in
$\phi $
with
$s(i)$
. For each set of
${\mathcal {L}_{\mathrm {TST}}}$
-sentences T, we let
$$\begin{align*}T^\circ = \{ \sigma^s : \sigma \in T \text{ and } s \colon \mathbb{N} \to \mathbb{N} \text{ strictly increasing} \}. \end{align*}$$
Tangled Type Theory (
$\mathrm {TTT}$
) is defined as
$\mathrm {TTT} = \mathrm {TST}^\circ $
, whereas predicative Tangled Type Theory (
$\mathrm {TTTP}$
) as
$\mathrm {TTTP} = \mathrm {TSTP}^\circ $
.
A structure
$\mathscr {A}$
for the language
${\mathcal {L}_{\mathrm {TST}}}$
is a sequence
$(A_0, A_1, \ldots , \{\varepsilon ^{\mathscr {A}}_{i,i+1}\}_{i \in \mathbb {N}})$
, where
$A_0, A_1, \ldots $
are non-empty sets interpreting the countably many types of
${\mathcal {L}_{\mathrm {TST}}}$
, and each
$\varepsilon ^{\mathscr {A}}_{i,i+1} \subseteq A_i \times A_{i+1}$
is a binary relation interpreting
$\varepsilon $
for type
$i \in \mathbb {N}$
. Similarly, a structure
$\mathscr {A}$
for the language
${\mathcal {L}_{\mathrm {TTT}}}$
is a sequence
$(A_0, A_1, \ldots , \{\varepsilon ^{\mathscr {A}}_{i,j})\}_{i < j}$
, where
$A_0, A_1, \ldots $
are non-empty sets, and
$\varepsilon ^{\mathscr {A}}_{i,j} \subseteq A_i \times A_j$
, for all
$i, j \in \mathbb {N}$
such that
$i < j$
.
Let us now introduce the notion of standard transitive
${\mathcal {L}_{\mathrm {TTT}}}$
-structure. First, we fix some notation about tuples in our metatheory. For all n-tuples
$u = (u_1, \ldots , u_n)$
and
$0 \leq i \leq n$
, where
$n> 0$
, we let
$$\begin{align*}(u)_i = \begin{cases} u, & \text{if } i = 0, \\ u_i, & \text{o.w.} \\ \end{cases} \end{align*}$$
Definition 1.1. An
${\mathcal {L}_{\mathrm {TTT}}}$
-structure
$\mathscr {A} = (A_0, A_1, \ldots , \{\varepsilon ^{\mathscr {A}}_{i,j}\}_{i < j})$
is standard transitive if:
-
(i) for all
$n \in \mathbb {N}$
,
$$\begin{align*}A_{n+1} \subseteq \prod^n_{i = 0} {\mathscr{P}}(\{ (u)_i : u \in A_i \}), \end{align*}$$
-
(ii) for all
$i < j$
,
$u \in A_i$
, and
$v \in A_j$
,
$$\begin{align*}u \varepsilon^{\mathscr{A}}_{i,j} v \Leftrightarrow (u)_i \in (v)_{i+1}. \end{align*}$$
To simplify notation, we will denote
$\mathscr {A}$
as
$(A_0, A_1, \ldots , \in )$
.
Note. Let us make the definition above a bit less confusing. First of all, notice that in Tangled Type Theory, every set of type n has n extensions (one for each type below n). The elements of
$A_n$
are basically n-tuples that code this fact. More precisely, it follows by the definition of
$\varepsilon ^{\mathscr {A}}_{i,n}$
that the extension of a set
$v \in A_n$
over type i is its (
$i+1$
)-th projection
$(v)_{i+1}$
. It is important to note that the extension of v over type i is a set of i-th projections of elements of
$A_i$
and not a set of elements of
$A_i$
. So, in the sense we just described, an element of
$A_n$
is a tuple of its n extensions over types
$0, \ldots , n-1$
. Keep in mind that there is nothing mysterious about the tuples
$v = ((v)_1, \ldots , (v)_n)$
in
$A_n$
; each
$(v)_i$
is simply an element of
${\mathscr {P}}^i(A_0)$
. It is also worth noting that we imposed no restrictions on
$A_0$
, which means that
$A_0$
can be any set.
It is always easier to work with standard transitive structures, and as we show below we may always assume that extensional
${\mathcal {L}_{\mathrm {TTT}}}$
-structures (i.e., structures that satisfy
$\mathrm {Ext}^\circ $
) are standard transitive.
Definition 1.2. Let
$\mathscr {A}$
,
$\mathscr {B}$
be two
${\mathcal {L}_{\mathrm {TTT}}}$
-structures. We say that f is an
${\mathcal {L}_{\mathrm {TTT}}}$
-isomorphism from
$\mathscr {A}$
to
$\mathscr {B}$
, if f is a sequence
$(f_0, f_1, \ldots )$
of functions such that:
-
(i) for all
$i \in \mathbb {N}$
,
$f_i \colon A_i \to B_i$
is a bijection, -
(ii) for all
$i, j \in \mathbb {N}$
such that
$i < j$
, and for all
$u \in A_i$
and
$v \in A_j$
,
$$\begin{align*}u \varepsilon^{\mathscr{A}}_{i,j} v \Leftrightarrow f_i(u) \varepsilon^{\mathscr{B}}_{i,j} f_j(v). \end{align*}$$
When such an
${\mathcal {L}_{\mathrm {TTT}}}$
-isomorphism exists, we say that
$\mathscr {A}$
and
$\mathscr {B}$
are
${\mathcal {L}_{\mathrm {TTT}}}$
-isomorphic (or just isomorphic).
The next proposition follows easily by induction on the complexity of
$\phi $
.
Proposition 1.3. Let
$\mathscr {A}$
and
$\mathscr {B}$
be two
${\mathcal {L}_{\mathrm {TTT}}}$
-structures. If
$f \colon \mathscr {A} \to \mathscr {B}$
is an
${\mathcal {L}_{\mathrm {TTT}}}$
-isomorphism, then for every formula
$\phi (x^{i_1}_1, \ldots , x^{i_n}_n)$
of
${\mathcal {L}_{\mathrm {TTT}}}$
and
$a_1 \in A_{i_1}, \ldots , a_n \in A_{i_n}$
, we have that
$$\begin{align*}\mathscr{A} \models \phi(a_1, \ldots, a_n) \Leftrightarrow \mathscr{B} \models \phi(f_{i_1}(a_1), \ldots, f_{i_n}(a_n)). \end{align*}$$
Lemma 1.4. Every extensional
${\mathcal {L}_{\mathrm {TTT}}}$
-structure is isomorphic to a standard transitive
${\mathcal {L}_{\mathrm {TTT}}}$
-structure.
Proof Let
$\mathscr {A} = (A_0, A_1, \ldots , \{\varepsilon ^{\mathscr {A}}_{i,j}\}_{i < j})$
be an extensional
${\mathcal {L}_{\mathrm {TTT}}}$
-structure. We define a standard transitive
${\mathcal {L}_{\mathrm {TTT}}}$
-structure
$\mathscr {B} = (B_0, B_1, \ldots , \in )$
. Let
$B_0 = A_0$
and
$f_0$
be the identity function on
$A_0$
. For
$n \in \mathbb {N}$
, we define
$B_{n+1} = \operatorname {\mathrm {ran}}(f_{n+1})$
, where
$f_{n+1}$
is defined such that for all
$u \in A_{n+1}$
,
$$\begin{align*}f_{n+1}(u) = (\{(f_0(v))_0 : v \varepsilon^{\mathscr{A}}_{0,n+1} u\}, \ldots, \{(f_n(v))_n : v \varepsilon^{\mathscr{A}}_{n,n+1} u\}). \end{align*}$$
It is easy to verify that
$\mathscr {B}$
is standard transitive and that f is an
${\mathcal {L}_{\mathrm {TTT}}}$
-isomorphism from
$\mathscr {A}$
to
$\mathscr {B}$
.
The following lemma establishes a practical criterion for extensionality.
Lemma 1.5. A standard transitive
${\mathcal {L}_{\mathrm {TTT}}}$
-structure
$\mathscr {A} = (A_0, A_1, \ldots , \in )$
is extensional iff for all
$0 \leq i < n$
, and
$u, v \in A_n$
,
$$\begin{align*}(u)_{i+1} = (v)_{i+1} \Rightarrow u = v. \end{align*}$$
Proof Just notice that
$\mathscr {A}$
is extensional iff for all
$0 \leq i < n$
,
$$ \begin{align*} &\mathscr{A} \models \forall u^n, v^n (u^n = v^n \leftrightarrow \forall w^i (w^i \varepsilon u^n \leftrightarrow w^i \varepsilon v^n)) \\ &\Leftrightarrow \forall u, v \in A_n (u = v \leftrightarrow \forall w \in A_i ((w)_i \in (u)_{i+1} \leftrightarrow (w)_i \in (v)_{i+1})) \\ &\Leftrightarrow \forall u, v \in A_n (u = v \leftrightarrow (u)_{i+1} = (v)_{i+1}), \end{align*} $$
where the second equivalence holds because
$(u)_{i+1}, (v)_{i+1} \in {\mathscr {P}}(\{ (w)_i : w \in A_i \})$
.
Note. Notice that by the previous lemma, if
$\mathscr {A} = (A_0, A_1, \ldots , \in )$
is extensional, then for all
$0 \leq i \leq n$
, and
$u, v \in A_n$
,
$$\begin{align*}(u)_{i+1} = (v)_{i+1} \Leftrightarrow u = v. \end{align*}$$
1.2 New foundations
The language
${\mathcal {L}_{\mathrm {NF}}}$
of New Foundations is the usual one-sorted language of set theory,
$\{\epsilon \}$
, where
$\epsilon $
is a binary relation symbol. New Foundations (
$\mathrm {NF}$
) is axiomatized by the axioms of
$\mathrm {TST}$
if we erase all type superscripts. Similarly, by erasing all type superscripts from the axioms of
$\mathrm {TSTP}$
, we get the axioms of predicative
$\mathrm {NF}$
(
$\mathrm {NFP}$
).
What do we know about
$\mathrm {NFP}$
? First of all, we know that it is a rather weak subtheory of
$\mathrm {NF}$
since for example its consistency can be proved in
$\mathrm {PA}$
(see [Reference Crabbé1]). We also know that it is finitely axiomatizable (see [Reference Randall Holmes4]), and that if the Union axiom
$$ \begin{align} \forall z \exists y \forall x (x \epsilon y \leftrightarrow \exists v (v \epsilon z \wedge x \epsilon v)) \end{align} $$
is added to it, we get full
$\mathrm {NF}$
, i.e.,
$\mathrm {NFP} + \mathrm {Union} = \mathrm {NF}$
(see [Reference Crabbé1]). The most interesting fact about
$\mathrm {NFP}$
though is that it is consistent with properties (like choice principles; see [Reference Crabbé1, Reference Randall Holmes3]) that fail in
$\mathrm {NF}$
(see [Reference Specker6] or [Reference Forster2]). Below, we describe a way of constructing such models of
$\mathrm {NFP}$
.
2 Models of predicative
$\mathrm {NF}$
We work in
$\mathrm {ZF} + (V = L)$
. We are going to construct a standard transitive model
$\mathscr {A}$
of
$\mathrm {TTTP}$
. Let
$\kappa $
be an infinite cardinal. For all
$n \in \mathbb {N}$
, we define recursively a set
$X_n$
, an ordinal
$\kappa \leq \alpha _n < \kappa ^+$
, and a bijection
$f_n \colon \kappa \to X_n$
such that
$f_n \in L_{\alpha _{n+1}}$
. Let
$\alpha _0 = \kappa $
,
$X_0 = L_{\alpha _0}$
, and let
$f_0 \colon \kappa \to X_0$
be a bijection. For
$n> 0$
, let
$$\begin{align*}X_n = L_{\alpha_n} \cap {\mathscr{P}}(X_{n-1}), \end{align*}$$
where
$\alpha _n$
is the least limit ordinal that is greater than
$\alpha _{n-1}$
and for which
$f_{n-1} \in L_{\alpha _n}$
. We know that
$\alpha _n < \kappa ^+$
and
$|X_n| = \kappa $
, so there exists some bijection
$f_n \colon \kappa \to X_n$
.
Let
$A_0 = X_0 $
and for all
$n> 0$
, let
$$\begin{align*}A_n = \{ (f_1(\alpha), \ldots, f_n(\alpha)) : \alpha < \kappa\}. \end{align*}$$
We define
$\mathscr {A} = (A_0, A_1, \ldots , \{\varepsilon ^{\mathscr {A}}_{i,j}\}_{i < j})$
, where for all
$i < j$
,
$u \in A_i$
, and
$v \in A_j$
,
$$\begin{align*}u \varepsilon^{\mathscr{A}}_{i,j} v \Leftrightarrow (u)_i \in (v)_{i+1}. \end{align*}$$
Notice that for all
$n \in \mathbb {N}$
, since
$f_0, \ldots , f_n \in L_{\alpha _{n+1}}$
and
$\alpha _{n+1}$
is a limit ordinal, we have
$$\begin{align*}X_0, \ldots, X_n, A_0, \ldots, A_n \in L_{\alpha_{n+1}}. \end{align*}$$
Lemma 2.1.
$\mathscr {A}$
is a standard transitive model of
$\mathrm {TTTP}$
.
Proof We have that for all
$i \in \mathbb {N}$
,
$$\begin{align*}\{ (u)_i : u \in A_i \} = \operatorname{\mathrm{ran}}(f_i) = X_i. \end{align*}$$
Therefore, for all
$n \in \mathbb {N}$
,
$$\begin{align*}A_{n+1} \subseteq \prod^n_{i = 0} \operatorname{\mathrm{ran}}(f_{i+1}) = \prod^n_{i = 0} X_{i+1} \subseteq \prod^n_{i = 0} {\mathscr{P}}(X_i) = \prod^n_{i = 0} {\mathscr{P}}(\{ (u)_i : u \in A_i \}), \end{align*}$$
i.e.,
$\mathscr {A}$
is standard transitive.
We show that
$\mathscr {A}$
is an extensional structure. Let
$0 \leq i < n$
, and
$u, v \in A_n$
. We know that
$u = (f_1(\alpha ), \ldots , f_n(\alpha ))$
and
$v = (f_1(\beta ), \ldots , f_n(\beta ))$
for some
$\alpha , \beta < \kappa $
. If
$(u)_{i+1} = (v)_{i+1}$
, then
$f_{i+1}(\alpha ) = f_{i+1}(\beta )$
, so since
$f_{i+1}$
is 1–1, we have that
$\alpha = \beta $
, i.e.,
$u = v$
. Therefore, by Lemma 1.5,
$\mathscr {A}$
is extensional.
It remains to show that
$\mathscr {A} \models \mathrm {CoP}^\circ $
. Let
$s \colon \mathbb {N} \to \mathbb {N}$
be strictly increasing, and let
$\phi (x^i, u^{i_1}_1, \ldots , u^{i_n}_n)$
be some
${\mathcal {L}_{\mathrm {TST}}}$
-formula
$$\begin{align*}\operatorname{\mathrm{Q}}_1 x^{j_1}_1 \ldots \operatorname{\mathrm{Q}}_m x^{j_m}_m \psi(x^{j_1}_1, \ldots, x^{j_m}_m, x^i, u^{i_1}_1, \ldots, u^{i_n}_n), \end{align*}$$
where
$\operatorname {\mathrm {Q}}_1, \ldots , \operatorname {\mathrm {Q}}_n$
are quantifiers,
$\psi $
is quantifier-free,
$\max \{j_1, \ldots , j_m\} \leq i$
, and
$\max \{i_1, \ldots , i_n\} \leq i+1$
. We show that
$\mathscr {A} \models (\forall u^{i_1}_1, \ldots , u^{i_n}_n \exists y^{i+1} \forall x^{i} (x^{i} \varepsilon y^{i+1} \leftrightarrow \phi (x^{i}, u^{i_1}_1, \ldots , u^{i_n}_n)))^s$
, i.e., that
$$\begin{align*}\mathscr{A} \models \forall u^{s(i_1)}_1, \ldots, u^{s(i_n)}_n \exists y^{s(i+1)} \forall x^{s(i)} (x^{s(i)} \varepsilon y^{s(i+1)} \leftrightarrow \phi(x^{s(i)}, u^{s(i_1)}_1, \ldots, u^{s(i_n)}_n)). \end{align*}$$
Let
$u_1 \in A_{s(i_1)}, \ldots , u_n \in A_{s(i_n)}$
. Let
$$ \begin{align*} &y' = \{ (x)_{s(i)} : x \in A_{s(i)} \wedge \operatorname{\mathrm{Q}}_1 x_1 \in A_{s(j_1)} \ldots \operatorname{\mathrm{Q}}_m x_m \in A_{s(j_m)} \\ &\mathscr{A} \models \psi(x_1, \ldots, x_m, x, u_1, \ldots, u_n) \}. \end{align*} $$
Now, by Remark 1.1 and the way
$\varepsilon $
is interpreted in standard transitive structures, it follows that the statement
$\mathscr {A} \models \psi (x_1, \ldots , x_m, x, u_1, \ldots , u_n)$
is equivalent to a quantifier-free
${\mathcal {L}_{\mathrm {ZF}}}$
-formula that (apart from
$x_1, \ldots , x_m, x$
) has as parameters only the
$s(i)+1$
first coordinates of
$u_1, \ldots , u_n$
, where each such coordinate is in
$L_{\alpha _{s(i)+1}}$
. Moreover, we know that
$A_{s(i)}, A_{s(j_1)}, \ldots , A_{s(j_n)} \in L_{\alpha _{s(i)+1}}$
because
$s(j_1), \ldots , s(j_n) \leq s(i)$
. Therefore, since
$\alpha _{s(i)+1}$
is a limit ordinal, we have that
$$\begin{align*}y' \in L_{\alpha_{s(i)+1}} \cap {\mathscr{P}}(X_{s(i)}) = X_{s(i)+1}. \end{align*}$$
Let
$y \in A_{s(i+1)}$
such that
$(y)_{s(i)+1} = y'$
. Clearly, y witnesses that
$$\begin{align*}\mathscr{A} \models \exists y^{s(i+1)} \forall x^{s(i)} (x^{s(i)} \varepsilon y^{s(i+1)} \leftrightarrow \phi(x^{s(i)}, u_1, \ldots, u_n)).\\[-34pt] \end{align*}$$
We now show that
$\mathscr {A}$
inherits some interesting properties from L. Below, we present two such properties. We begin by proving that in
$\mathscr {A}$
every universe is well-orderable. Before we proceed though, let us examine what it means for an element to be a Wiener–Kuratowski pair in
$\mathscr {A}$
. For each
$i \in \mathbb {N}$
, let
$\mathrm {Pair}_i(u^i, v^i, z^{i+2})$
be the following
${\mathcal {L}_{\mathrm {TST}}}$
-formula:
$$ \begin{align*} &\exists x^{i+1}_1, x^{i+1}_2 (\forall w^i (w^i \varepsilon x^{i+1}_1 \leftrightarrow w^i = u^i) \wedge \forall w^i (w^i \varepsilon x^{i+1}_2 \leftrightarrow w^i = u^i \vee w^i = v^i) \\ & \quad \wedge \forall x^{i+1} (x^{i+1} \varepsilon z^{i+2} \leftrightarrow x^{i+1} = x^{i+1}_1 \vee x^{i+1} = x^{i+1}_2)), \end{align*} $$
expressing that
$z^{i+2}$
is the Wiener–Kuratowski pair of
$u^i, v^i$
. Notice that for
$s \colon \mathbb {N} \to \mathbb {N}$
strictly increasing,
$i \in \mathbb {N}$
,
$u, v \in A_{s(i)}$
, and
$z \in A_{s(i+2)}$
, we have that
$\mathscr {A} \models \mathrm {Pair}^s_i(u, v, z)$
is equivalent to
$$ \begin{align*} &\exists x_1, x_2 \in A_{s(i+1)} (\forall w \in A_{s(i)} ((w)_{s(i)} \in (x_1)_{s(i)+1} \leftrightarrow (w)_{s(i)} = (u)_{s(i)}) \\ &\quad\wedge (\forall w \in A_{s(i)} ((w)_{s(i)} \in (x_2)_{s(i)+1} \leftrightarrow (w)_{s(i)} = (u)_{s(i)} \vee (w)_{s(i)} = (v)_{s(i)}) \\ &\quad\wedge \forall x \in A_{s(i+1)} ((x)_{s(i+1)} \in (z)_{s(i+1)+1} \\ &\quad\leftrightarrow (x)_{s(i+1)} = (x_1)_{s(i+1)} \vee (x)_{s(i+1)} = (x_2)_{s(i+1)})), \end{align*} $$
or in more compact notation iff
$$ \begin{align*} &\exists x_1, x_2 \in A_{s(i+1)} ( (z)_{s(i+1)+1} = \{ (x_1)_{s(i+1)}, (x_2)_{s(i+1)} \} \\ &\quad\wedge (x_1)_{s(i)+1} = \{(u)_{s(i)}\} \wedge (x_2)_{s(i)+1} = \{(u)_{s(i)}, (v)_{s(i)}\}). \end{align*} $$
To simplify notation, let us denote by
$\mathrm {Pair}^{\mathscr {A},s}_i(u, v, z)$
the above
${\mathcal {L}_{\mathrm {ZF}}}$
-formula which is equivalent to
$\mathscr {A} \models (\mathrm {Pair}_i(u, v, z))^s$
.
Lemma 2.2.
$\mathscr {A} \models (\{\text {"}V^{i+1} \text { is well-orderable"}\}_{i \in \mathbb {N}})^\circ $
.
Proof Let
$s \colon \mathbb {N} \to \mathbb {N}$
be strictly increasing,
$i \in \mathbb {N}$
, and let
$\phi (u^i, v^i, W^{i+2})$
be the following
${\mathcal {L}_{\mathrm {TST}}}$
-formula:
Let
$\chi (W^{i+2})$
be the following
${\mathcal {L}_{\mathrm {TST}}}$
-formula:
$$ \begin{align*} &\forall u^i, v^i (\phi(u^i, v^i, W^{i+2}) \vee \phi(v^i, u^i, W^{i+2}) \vee u^i = v^i) \\ & \quad\wedge \forall u^i, v^i, w^i (\phi(u^i, v^i, W^{i+2}) \wedge \phi(v^i, w^i, W^{i+1}) \to \phi(u^i, w^i, W^{i+2})) \\ &\quad\wedge \forall x^{i+1} \exists u^i (u^i \varepsilon x^{i+1} \wedge \forall v^i (v^i \varepsilon x^{i+1} \wedge u^i \neq v^i \to \phi(u^i, v^i, W^{i+2}))). \end{align*} $$
For all
$W \in A_{s(i+2)}$
, we have
$\mathscr {A} \models \chi ^s(W)$
iff
$$ \begin{align*} &\forall u, v \in A_{s(i)} (\phi^{\mathscr{A},s}(u, v, W) \vee \phi^{\mathscr{A},s}(v, u, W) \vee (u)_{s(i)} = (v)_{s(i)}) \\ &\quad\wedge \forall u, v, w \in A_{s(i)} (\phi^{\mathscr{A},s}(u, v, W) \wedge \phi^{\mathscr{A},s}(v, w, W) \to \phi^{\mathscr{A},s}(u, w, W)) \\ &\quad\wedge \forall x \in A_{s(i+1)} \exists u \in A_{s(i)} ((u)_{s(i)} \in (x)_{s(i)+1} \\ &\quad\wedge \forall v \in A_{s(i)} ((v)_{s(i)} \in (x)_{s(i)+1} \wedge (u)_{s(i)} \neq (v)_{s(i)} \to \phi^{\mathscr{A},s}(u, v, W))), \end{align*} $$
where
$\phi ^{\mathscr {A},s}(u, v, W)$
is the following
${\mathcal {L}_{\mathrm {ZF}}}$
-formula:
$$\begin{align*}\exists x \in A_{s(i+1)} ((x)_{s(i+1)} \in (W)_{s(i+1)+1} \wedge (u)_{s(i)} \in (x)_{s(i)+1} \wedge (v)_{s(i)} \notin (x)_{s(i)+1}). \end{align*}$$
Let
$\psi (u,v)$
be an
${\mathcal {L}_{\mathrm {ZF}}}$
-formula that defines some well-ordering of L. Let
$$ \begin{align*} &W' = \{ (x)_{s(i+1)} : x \in A_{s(i+1)} \\ &\quad\wedge \exists u \in A_{s(i)} \forall v \in A_{s(i)} ((v)_{s(i)} \in (x)_{s(i)+1} \leftrightarrow \psi((u)_{s(i)}, (v)_{s(i)}))\}. \end{align*} $$
We know that
$W' \in L_{\alpha _{s(i+1)+1}} \cap {\mathscr {P}}(X_{s(i+1)}) = X_{s(i+1)+1}$
, so there exists some
$W \in A_{s(i+2)}$
such that
$(W)_{s(i+1)+1} = W'$
. Notice that
$W'$
is the set of all
$(x)_{s(i+1)}$
for which
$x \in A_{s(i+1)}$
and
$(x)_{s(i)+1}$
is an initial segment of the well-ordering defined by
$\psi $
restricted to
$X_{s(i)}$
. Therefore, W witnesses that
$\mathscr {A} \models \chi ^s(W)$
. Now, let
$$\begin{align*}R' = \{ (z)_{s(i+2)} : z \in A_{s(i+2)} \wedge \exists u,v \in A_{s(i)} (\mathrm{Pair}^{\mathscr{A},s}_i(u,v,z) \wedge \phi^{\mathscr{A},s}(u,v,W)) \}. \end{align*}$$
We have that
$R' \in L_{\alpha _{s(i+2)+1}} \cap {\mathscr {P}}(X_{s(i+2)}) = X_{s(i+2)+1}$
, so there exists an
$R \in A_{s(i+3)}$
such that
$(R)_{s(i+2)+1} = R'$
. It is easy to see that
$\mathscr {A} \models \chi ^s(W)$
implies
$\mathscr {A} \models (\text {"}R$
is a well-ordering of
$V^{i+1}\text {"})^s$
. Hence,
$\mathscr {A} \models (\text {"}V^{i+1} \text { is well-orderable"})^s$
.
Next, we show that in
$\mathscr {A}$
every universe is cantorian (i.e., it is equinumerous to the set of singletons). This essentially follows from the fact that for all
$i, j \in \mathbb {N}$
, there are functions in
$\mathscr {A}$
witnessing that
$|X_i| = \kappa = |\iota "X_j|$
.
Lemma 2.3.
$\mathscr {A} \models (\{\text {"}V^{i+2} \text { is cantorian"}\}_{i \in \mathbb {N}})^\circ $
.
Proof Let
$s \colon \mathbb {N} \to \mathbb {N}$
be strictly increasing, and let
$i \in \mathbb {N}$
. We show that
$\mathscr {A} \models (\text {"}V^{i+2} \text { is cantorian"})^s$
, i.e., that
$$ \begin{align*} \mathscr{A} \models (\exists g^{i+4}(\text{"}g\text{ is a bijection from }V^{i+2}\text{ to }\iota"V^{i+1}\text{"}))^s. \end{align*} $$
An
${\mathcal {L}_{\mathrm {TST}}}$
-sentence that expresses the statement
$$\begin{align*}\exists g^{i+4}(\text{"}g\text{ is a bijection from }V^{i+2}\text{ to }\iota"V^{i+1}\text{"}) \end{align*}$$
is the following:
$$ \begin{align*} &\exists g^{i+4} ( \forall z^{i+3} (z^{i+3} \varepsilon g^{i+4} \to \exists u^{i+1}, v^{i+1} (\mathrm{Pair}_{i+1}(u^{i+1}, v^{i+1}, z^{i+3}))) \\ &\wedge \forall u^{i+1}, v^{i+1}, w^{i+1}, x^{i+3}, y^{i+3} (\mathrm{Pair}_{i+1}(u^{i+1}, v^{i+1}, x^{i+3}) \wedge \mathrm{Pair}_{i+1}(u^{i+1}, w^{i+1}, y^{i+3}) \\ &\wedge x^{i+3} \varepsilon g^{i+4} \wedge y^{i+3} \varepsilon g^{i+4} \to v^{i+1} = w^{i+1}) \\ &\wedge \forall u^{i+1}, v^{i+1}, w^{i+1}, x^{i+3}, y^{i+3} (\mathrm{Pair}_{i+1}(u^{i+1}, w^{i+1}, x^{i+3}) \wedge \mathrm{Pair}_{i+1}(v^{i+1}, w^{i+1}, y^{i+3}) \\ &\wedge x^{i+3} \varepsilon g^{i+4} \wedge y^{i+3} \varepsilon g^{i+4} \to u^{i+1} = v^{i+1}) \\ &\wedge \forall u^{i+1} \exists v^{i+1}, z^{i+3} (\mathrm{Pair}_{i+1}(u^{i+1}, v^{i+1}, z^{i+3}) \wedge z^{i+3} \varepsilon g^{i+4} \\ &\wedge \exists a^i \forall b^i (b^i \varepsilon v^{i+1} \leftrightarrow b^i = a^i)) \\ &\wedge \forall v^{i+1} (\exists a^i \forall b^i (b^i \varepsilon v^{i+1} \leftrightarrow b^i = a^i) \\ &\to \exists u^{i+1}, z^{i+3} (\mathrm{Pair}_{i+1}(u^{i+1}, v^{i+1}, z^{i+3}) \wedge z^{i+3} \varepsilon g^{i+4}))). \end{align*} $$
We therefore have that
$\mathscr {A} \models (\text {"}V^{i+2} \text { is cantorian"})^s$
iff
$$ \begin{align*} &\exists g \in A_{s(i+4)} ( \forall z \in A_{s(i+3)} ((z)_{s(i+3)} \in (g)_{s(i+3)+1} \\ &\to \exists u, v \in A_{s(i+1)} (\mathrm{Pair}^{\mathscr{A},s}_{i+1}(u, v, z))) \\ &\wedge \forall u, v, w \in A_{s(i+1)} \forall x, y \in A_{s(i+3)} (\mathrm{Pair}^{\mathscr{A},s}_{i+1}(u, v, x) \wedge \mathrm{Pair}^{\mathscr{A},s}_{i+1}(u, w, y) \\ &\wedge (x)_{s(i+3)} \in (g)_{s(i+3)+1} \wedge (y)_{s(i+3)} \in (g)_{s(i+3)+1} \to (v)_{s(i+1)} = (w)_{s(i+1)}) \\ &\wedge \forall u, v, w \in A_{s(i+1)} \forall x, y \in A_{s(i+3)} (\mathrm{Pair}^{\mathscr{A},s}_{i+1}(u, w, x) \wedge \mathrm{Pair}^{\mathscr{A},s}_{i+1}(v, w, y) \\ &\wedge (x)_{s(i+3)} \in (g)_{s(i+3)+1} \wedge (y)_{s(i+3)} \in (g)_{s(i+3)+1} \to (u)_{s(i+1)} = (v)_{s(i+1)}) \\ &\wedge \forall u \in A_{s(i+1)} \exists v \in A_{s(i+1)} \exists z \in A_{s(i+3)} (\mathrm{Pair}^{\mathscr{A},s}_{i+1}(u, v, z) \wedge (z)_{s(i+3)} \in (g)_{s(i+3)+1} \\ &\wedge \exists a \in A_{s(i)} \forall b \in A_{s(i)} ((b)_{s(i)} \in (v)_{s(i)+1} \leftrightarrow (b)_{s(i)} = (a)_{s(i)})) \\ &\wedge \forall v \in A_{s(i+1)} (\exists a \in A_{s(i)} \forall b \in A_{s(i)} ((b)_{s(i)} \in (v)_{s(i)+1} \leftrightarrow (b)_{s(i)} = (a)_{s(i)}) \\ &\to \exists u \in A_{s(i+1)} \exists z \in A_{s(i+3)} (\mathrm{Pair}^{\mathscr{A},s}_{i+1}(u, v, z) \wedge (z)_{s(i+3)} \in (g)_{s(i+3)+1}))). \end{align*} $$
Let
$$ \begin{align*} &g' = \{ (z)_{s(i+3)} : z \in A_{s(i+3)} \wedge \exists u, v \in A_{s(i+1)} ( \mathrm{Pair}^{\mathscr{A},s}_{i+1}(u, v, z) \\ &\wedge \exists \alpha < \kappa ( (u)_{s(i+1)} = f_{s(i+1)}(\alpha) \wedge (v)_{s(i)+1} = \{f_{s(i)}(\alpha)\})) \}. \end{align*} $$
We have that
$g' \in L_{s(i+3)+1} \cap {\mathscr {P}}(X_{s(i+3)}) = X_{s(i+3)+1}$
, so there is a
$g \in A_{s(i+4)}$
such that
$(g)_{s(i+3)+1} = g'$
. Clearly, g witnesses that
$$\begin{align*}\mathscr{A} \models (\exists g^{i+4} (\text{"}g \text{ is a bijection from }V^{i+2}\text{ to }\iota"V^{i+1}\text{"}))^s.\\[-36pt] \end{align*}$$
We have shown that
$$\begin{align*}\mathrm{TTTP} + (\{\text{"}V^{i+1} \text{ is well-orderable"}\}_{i \in \mathbb{N}})^\circ + (\{\text{"}V^{i+2} \text{ is cantorian"}\}_{i \in \mathbb{N}})^\circ \end{align*}$$
is consistent. By slightly modifying Holmes’ proof for the equiconsistency of
$\mathrm {TTT}$
and
$\mathrm {NF}$
(see [Reference Randall Holmes3]), we can now prove the following proposition.
Proposition 2.4.
$\mathrm {NFP} + \text {"}V\text { is well-orderable"} + \text {"}V\text { is cantorian"}$
is consistent.
Proof Let
$\Delta = \{\sigma _1, \ldots , \sigma _n\}$
be a finite subset of
$$\begin{align*}\mathrm{TTTP} + (\{\text{"}V^{i+1} \text{ is well-orderable"}\}_{i \in \mathbb{N}})^\circ + (\{\text{"}V^{i+2} \text{ is cantorian"}\}_{i \in \mathbb{N}})^\circ. \end{align*}$$
Let
$m \in \mathbb {N}$
be such that all variables appearing in
$\sigma _1, \ldots , \sigma _n$
have types that are less or equal to m. For each
$X \subseteq \mathbb {N}$
such that
$|X| = m+1$
, let
$s_X$
be the unique strictly increasing function from
$\{0, \ldots , m\}$
to X. Let
$F \colon [\mathbb {N}]^{m+1} \to 2^n$
such that for all
$X \in [\mathbb {N}]^{m+1}$
,
$F(X) = (\delta _1, \ldots , \delta _n)$
, where for each
$1 \leq i \leq n$
,
$\delta _i {\kern-1.2pt}={\kern-1.2pt} 1$
iff
$\mathscr {A} {\kern-1.2pt}\models{\kern-1.2pt} (\sigma _i)^{s_X}$
. By Ramsey’s theorem, there exists some infinite
$H {\kern-1.2pt}\subseteq{\kern-1.2pt} \mathbb {N}$
such that H is homogeneous for F. Let
$H {\kern-1.5pt}={\kern-1.2pt} \{h_0, h_1, \ldots \}$
, where
$h_0 {\kern-1.2pt}<{\kern-1.2pt} h_1 {\kern-1.2pt}<{\kern-1.2pt} \cdots $
, and let
$\mathscr {B} = (A_{h_0}, A_{h_1}, \ldots , \{\varepsilon ^{\mathscr {A}}_{h_i,h_{i+1}}\}_{i \in \mathbb {N})})$
. It is easy to see that
$\mathscr {B}$
is a model of
$\mathrm {TSTP} {\kern-1.2pt}+{\kern-1.2pt} \{\text {"}V^{i+1}\text { is well-orderable"}\}_{i \in \mathbb {N}} {\kern-1.2pt}+{\kern-1.2pt} \{\text {"}V\text { is cantorian"}\}_{i \in \mathbb {N}} {\kern-1.2pt}+{\kern-1.2pt} \{ \sigma {\kern-1.2pt}\leftrightarrow{\kern-1.2pt} \sigma ^+ {\kern-1.5pt}: \sigma {\kern-1.2pt}\in{\kern-1.2pt} \Delta \}$
, where
$\sigma ^+$
is the sentence we get if we raise the type of every variable of
$\sigma $
by one. By Compactness, it follows that
$\mathrm {TSTP} + \{\text {"}V^{i+1}\text { is well-orderable"}\}_{i \in \mathbb {N}} + \{\text {"}V^{i+2}\text { is cantorian"}\}_{i \in \mathbb {N}} + \{ \sigma \leftrightarrow \sigma ^+ : \sigma \text { is a sentence } \}$
is consistent. Therefore, by Specker’s results on ambiguity (see [Reference Forster2] or [Reference Specker7]), it follows that there is a model of
$\mathrm {TSTP} + \{\text {"}V^{i+1}\text { is well-orderable"}\}_{i \in \mathbb {N}} + \{\text {"}V^{i+2}\text { is cantorian"}\}_{i \in \mathbb {N}}$
with a type shifting automorphism, which means that there is a model of
$\mathrm {NFP} + \text {"}V\text { is well-orderable"} + \text {"}V\text { is cantorian."}$
Although
$\mathrm {NFP}$
is consistent with a very strong choice principle like the one above, it is inconsistent with some other forms of choice. For example, let
$\mathrm {AC}$
be the statement “for any set x of non-empty pairwise disjoint sets, there exists a choice set z, i.e., a set that has exactly one element in common with each element of x,” which can be can be expressed formally as the following
${\mathcal {L}_{\mathrm {NF}}}$
-sentence:
Theorem 2.5.
$\mathrm {NFP} \vdash \neg \mathrm {AC}$
.
Proof As Crabbé observed in [Reference Crabbé1],
$\mathrm {NFP} + \forall x (x \subseteq \iota "V \to \exists y (x = \iota "y)) = \mathrm {NF}$
. But, in
$\mathrm {NFP}$
,
$\mathrm {AC}$
implies
$\forall x (x \subseteq \iota "V \to \exists y (x = \iota "y))$
because if x is a set of singletons and y is a choice set for x, then
$x = \iota "y$
. So,
$\mathrm {NFP} + \mathrm {AC} = \mathrm {NF}$
, which means that
$\mathrm {NFP} \vdash \neg \mathrm {AC}$
.
Note. Notice of course that the above form of choice is impredicative, and therefore not really suitable for a predicative theory. A more sensible and unproblematic statement in this setting would be the following: “for any set x of non-empty pairwise disjoint sets, there exists a set of singletons z, where every element of a singleton in z belongs to exactly one element of x” (notice that in this version, z has the same relative type as x).
3 Conclusion
We described a simple way of constructing a model of
$\mathrm {NFP}$
using L. We also showed that there are properties of L that can be transferred naturally to this model. We have chosen to present just two such properties that are inconsistent with
$\mathrm {NF}$
, but there are others. It would be nice to have a more general result on what kind of properties can be transferred though.
Question 1. What properties of L can be transferred to our model of
$\mathrm {NFP}$
?
The construction of our model seems to be quite flexible. For example, we could modify the definition of
$\alpha _n$
so that more sets are included in
$X_{\alpha _n}$
. This could lead us to stronger consistent extensions of
$\mathrm {NFP}$
. For example, the following question seems promising.
Question 2. Can this construction be modified so that we get a model of
$\mathrm {NFP}$
satisfying some weak version of Union?
Finding consistency proofs for subtheories of Tangled Type Theory is really important for understanding the problem of the consistency of
$\mathrm {NF}$
. On the other hand, the opposite direction is equally interesting: if we assume the consistency of
$\mathrm {NF}$
(see [Reference Randall Holmes5]), and therefore of Tangled Type Theory, we may get new results in other areas of set theory. For example, as we have shown, there seems to be a connection between models of Tangled Type Theory and L.
Question 3. Does the consistency of Tangled Type Theory have any implications for L?
Acknowledgments
This research was co-financed by Greece and the European Union (European Social Fund) through the Operational Program “Human Resources Development, Education and Lifelong Learning” in the context of the project “Reinforcement of Postdoctoral Researchers—2nd Cycle” (No. MIS-5033021), implemented by the State Scholarships Foundation (IKY).
