2.1 Various hierarchies of formulas

In this subsection, we define various types of hierarchy on the formula of set theory. Most set theorists work with the usual Levy hierarchy, with the following definition.

For a given theory T and a formula $\phi $ , $\phi $ is $\Sigma _n$ or $\Pi _n$ over T, or T-provably $\Sigma _n$ or $\Pi _n$ if T proves $\phi $ is equivalent to some $\Sigma _n$ or $\Pi _n$ formula respectively. If T proves $\phi $ is equivalent to both of a $\Sigma _n$ and a $\Pi _n$ formula, then we say T is $\Delta _n$ over T. We omit T and simply say a formula is $\Sigma _n$ , $\Pi _n$ , or $\Delta _n$ if the context is clear. Also, we call $\Sigma _0$ -formulas as $\Delta _0$ -formulas for convenience.

It is well-known folklore that repeating the same type of quantifiers does not affect being $\Sigma _n$ or $\Pi _n$ ; For example, for a bounded formula $\phi (x,y)$ , $\exists x\exists y\phi (x,y)$ is equivalent to a $\Sigma _1$ -formula although it is not literally $\Sigma _1$ . Let us formulate this folklore into a solid language for future use. The point of the subsequent lemmas is that they are provable over very weak subsystem of $\mathsf {ZFC}$ , namely, bounded Zermelo set theory without powerset $\mathsf {Z}_0^-$ , comprising Extensionality, Foundation, Pairing, Union, Infinity, and Separation for bounded formulas. The following results are presented in [Reference Friedman, Li and Wong4], and similar proofs for them appear in [Reference Jeon and Walsh8], but we reproduce the results and their proofs for future use.

Proof. We can see that the following equivalences hold:

1. (1) $z = \{x,y\} \iff (x\in z \land y\in z) \land \forall w\in z(w=x\lor w=y)$ .

2. (2) $\{x,y\}\in z \iff \exists w\in z (w = \{x,y\})$ .

3. (3) $z = \langle x,y\rangle \iff (\{x\}\in z\land \{x,y\}\in z)\land \forall w\in z (w = \{x\} \lor w = \{x,y\})$ .

4. (4) $z=\bigcup x \iff [\forall w\in z\exists y\in x (w\in y)] \land [\forall y\in x\forall w\in y (w\in z)]$ .

5. (5) $z=x\cup y \iff [\forall w\in x(w\in z)\land \forall w\in y(w\in z)] \land [\forall w\in z(z\in x \lor z\in y)]$ .

6. (6) $z=\varnothing \iff \forall w\in z (w\neq w)$ .

Now let us turn our view to the correctness of Kuratowski ordered pair. Suppose that $\langle x_0,x_1\rangle = \langle y_0,y_1\rangle $ , that is,

$$ \begin{align*} \{\{x_0\},\{x_0,x_1\}\} = \{\{y_0\},\{y_0,y_1\}\}. \end{align*} $$

Then we have $\{x_0\}=\{y_0\}\lor \{x_0\}=\{y_0,y_1\}$ . Similarly, we have $\{x_0,x_1\}=\{y_0\}\lor \{x_0,x_1\}=\{y_0,y_1\}$ . Based on this, let us divide the cases:

• • If $\{x_0\} = \{y_0,y_1\}$ , then $x_0=y_0=y_1$ . Thus we get $\{x_0,x_1\}=\{y_0\}$ , so $x_1=y_0$ . In sum, $x_0=x_1=y_0=y_1$ .

• • If $\{x_0,x_1\}=\{y_0\}$ , then by an argument similar to the previous one, we have $x_0=x_1=y_0=y_1$ .

• • Now consider the case $\{x_0\}=\{y_0\}$ and $\{x_0,x_1\}=\{y_0,y_1\}$ . Then we have $x_0=y_0$ , so $\{x_0,x_1\}=\{x_0,y_1\}$ . Hence $x_1\in \{x_0,y_1\}$ , so either $x_1=x_0$ or $x_1=y_1$ . But if $x_1=x_0$ , then from $y_1\in \{x_0,x_1\}$ we get $x_1=y_1$ .

Proof. Consider the following functions:

• • $\pi _0(x)=\bigcup \{ u\in \bigcup x\mid \forall v\in x (u\in v)\}$ .

• • $\pi _1(x) = \bigcup \{u\in \bigcup x \mid \exists v\in \bigcup x \forall p\in x [p=\{v\}\lor p=\{u,v\}]\}$ .

Clearly, $\mathsf {Z}_0^-$ proves the above functions are well-defined. Moreover, we can see that the formulas $\pi _0(x)=y$ and $\pi _1(x)=y$ are equivalent to $\Delta _0$ -formulas: First, we can see

$$ \begin{align*} z\in \pi_0(x) &\iff \exists w [y\in w_0 \land w_0\in \mathop{\textstyle \bigcup} x \land \forall v\in x(y\in v)] \\ &\iff \exists w [y\in w_0 \land (\exists w_1\in w_0 (w_0\in w_1)) \land \forall v\in x(y\in v)] \\ &\iff \exists w_1 \in x\exists w_0\in w_1 (y\in w\land\forall v\in x (y\in v)), \end{align*} $$

which is $\Delta _0$ , and we can see

$$ \begin{align*} \pi_0(x)\subseteq y &\iff \forall z (z\in \pi_0(x)\to z\in y) \\ &\iff \forall z \left[ [\exists w_1 \in x\exists w_0\in w_1 (y\in w\land\forall v\in x (y\in v))]\to z\in y\right]\\ &\iff \forall z\forall w_1\in x\forall w_0\in w_1 [(z\in w_0\land \forall v\in x(z\in v))\to z\in y] \\ &\iff \forall w_1\in x\forall w_0\in w_1\forall z\in w_0 [\forall v\in x(z\in v))\to z\in y] \end{align*} $$

and

$$ \begin{align*} \pi_0(x)=y \iff \pi_0(x)\subseteq y \land \forall z\in y(z\in \pi_0(x)), \end{align*} $$

so $\pi _0(x)=y$ is equivalent to a $\Delta _0$ -formula. In a similar way, but with a longer proof, we can see that $\pi _1(x)=y$ is equivalent to a $\Delta _0$ -formula.

The second part follows from induction on a bounded formula $\phi $ . We may also prove it by using the fact that ordered pair functions and projections $\pi _0$ , $\pi _1$ are rudimentary, hence simple. (See [Reference Jensen6]).

Lemma 2.4 ( $\mathsf {Z}_0^-$ ).

Let $\phi _0(x_0,x_1,v_0,\ldots , v_{n-1})$ be a $\Delta _0$ -formula. Then $\phi _0(\pi _0(x),\pi _1(x), v_0,\ldots , v_{n-1})$ is also $\Delta _0$ and

$$ \begin{align*} \forall x_0\forall x_1\exists v_0\cdots\mathsf{Q} v_{n-1} \phi_0(x_0,x_1,v_0,\ldots, v_{n-1}) \leftrightarrow \forall x \exists v_0\cdots\mathsf{Q} v_{n-1} \phi_0(\pi_0(x),\pi_1(x),v_0,\ldots, v_{n-1}) \end{align*} $$

From the previous lemma, we get the following.

Proof. Let us only consider the case when $\phi $ and $\psi $ are $\Pi _n$ . The case for $\Sigma _n$ is symmetric.

We first claim that if $\phi (x)$ is $\Pi _n$ , then $\forall x\phi (x)$ is equivalent to a $\Pi _n$ -formula. Suppose that $\phi (x)$ is of the form

$$ \begin{align*} \forall v_0\exists v_1\cdots\mathsf{Q} v_{n-1} \phi_0(x,v_0,\ldots,v_{n-1}) \end{align*} $$

for some $\Delta _0$ -formula $\phi _0$ . By Lemma 2.4, we have

$$ \begin{align*} \forall x\forall v_0\exists v_1\cdots\mathsf{Q} v_{n-1} \phi_0(x,v_0,v_1,\ldots, v_{n-1}) \leftrightarrow \forall x \exists v_1\cdots\mathsf{Q} v_{n-1} \phi_0(\pi_0(x),\pi_1(x),v_1,\ldots, v_{n-1}). \end{align*} $$

Next, let us prove that $\phi \land \psi $ is equivalent to a $\Pi _n$ -formula. The case for $\phi \lor \psi $ is analogous. Since $\phi $ and $\psi $ are $\Pi _n$ , we have $\Delta _0$ -formulas $\phi _0$ and $\psi _0$ such that

(1) $$ \begin{align} \phi(\vec{x}) \equiv \forall u_0 \exists u_1 \cdots \mathsf{Q} u_{n-1} \phi_0(\vec{x}, u_0,u_1,\ldots, u_{n-1}) \end{align} $$

and

(2) $$ \begin{align} \psi(\vec{x}) \equiv \forall v_0 \exists v_1 \cdots \mathsf{Q} v_{n-1} \psi_0(\vec{x}, v_0,v_1,\ldots, v_{n-1}). \end{align} $$

We may assume that all of $u_i$ and $v_i$ are different variables by substitution, so by predicate-logic level computation, we have

$$ \begin{align*} \phi(\vec{x})\land\psi(\vec{x}) \iff \\ \forall u_0\forall v_0 \exists u_1\exists v_1\cdots \mathsf{Q}u_{n-1}\mathsf{Q}v_{n-1}[\phi_0(\vec{x}, u_0,u_1,\ldots, u_{n-1})\land \psi_0(\vec{x},, v_0,v_1,\ldots, v_{n-1})]. \end{align*} $$

Now inductively reduce duplicated quantifiers from the inside to the outside by applying Lemma 2.4. As a result, we can see that $\phi \land \psi $ is equivalent to

$$ \begin{align*} &\forall w_0\exists w_1\cdots \mathsf{Q} w_{n-1} [\phi_0(\vec{x}, \pi_0(w_0), \pi_0(w_1),\ldots, \pi_0(w_{n-1}))\\&\quad\land \psi_0(\vec{x}, \pi_1(w_0), \pi_1(w_1),\ldots, \pi_1(w_{n-1}))].\\[-34pt] \end{align*} $$

Observe that the above proof works uniformly on formulas, so we can see the following meta-corollary holds:

Its proof follows from observing the proof of Lemma 2.5. Let us provide the corresponding D-formulas when $\phi $ and $\psi $ are $\Pi _n$ for future use: Let $\phi (\vec {x})=\phi (x_0,\ldots ,x_m)$ and $\psi (\vec {x}) = \psi (x_0,\ldots , x_m)$ be $\Pi _n$ -formulas as stated in the proof of Lemma 2.5, (1) and (2). Then

• • $D_{\forall x_0 \phi }$ is $\forall w \exists u_1\cdots \mathsf {Q} u_{n-1}\phi _0(\pi _0(w),x_1,\ldots ,x_m,\pi _1(w),u_1,\ldots , u_{n-1}).$

• • $D_{\phi \land \psi }(\vec {x})$ is $\forall w_0\exists w_1\ldots \mathsf {Q} w_{n-1} [\phi _0(\pi _0(w_0), \ldots , \pi _0(w_{n-1}))\land \psi _0(\pi _1(w_0), \pi _1(w_{n-1}))].$

• • $D_{\phi \lor \psi }(\vec {x})$ is $\forall w_0\exists w_1\ldots \mathsf {Q} w_{n-1} [\phi _0(\pi _0(w_0), \ldots , \pi _0(w_{n-1}))\lor \psi _0(\pi _1(w_0), \pi _1(w_{n-1}))].$

2.2 Hierarchies of formulas with j

Due to the subtle nature of the Wholeness axiom, we should distinguish formulas with the elementary embedding symbol $j\colon V\to V$ and without the elementary embedding symbol. Following the notation introduced in [Reference Matthews9] and [Reference Jeon and Matthews7], we distinguish formulas with j and those without j.

Lastly, for a given class of formulas $\Gamma $ , we define $\Sigma _n(\Gamma )$ , $\Pi _n(\Gamma )$ as the Levy hierarchy starting from $\Gamma $ . That is, $\Delta _0(\Gamma )=\Sigma _0(\Gamma )=\Pi _0(\Gamma )$ is the least class of formulas containing $\Gamma $ and closed under logical connectives and bounded quantifiers, and we define $\Sigma _n(\Gamma )$ and $\Pi _n(\Gamma )$ similarly. We also use notation like $\Sigma _n^j(\Gamma )$ to distinguish formulas with j. Especially, $\Delta ^j_0(\Sigma _\infty )$ is the least class of formulas containing $\Sigma _\infty $ -formulas, that is, formulas without j, which is closed under logical connectives and quantifiers bounded by terms.

Let us remark that we can reduce the repeating quantifiers in $\Sigma ^j_n$ - and $\Pi ^j_n$ -formulas similar to what Lemma 2.4 state and the reduction procedure is uniform. Their proof is similar to that of Lemma 2.4, Lemma 2.5, and Corollary 2.6 so we only provide their statements. Furthermore, the proof of the following lemmas does not use any properties of j, so they are provable over $\mathsf {Z}_0^-$ .

2.3 $\mathsf {BTEE}$ and $\mathsf {WA}$

In this subsection, we review the Basic Theory of Elementary Embeddings $\mathsf {BTEE}$ , the Wholeness Axiom $\mathsf {WA}$ and their consequences. Most of the definitions and results in this subsection are due to [Reference Corazza3]. We start from a ‘minimal’ theory for an elementary embedding $j\colon V\to V$ , named the Basic Theory of Elementary Embeddings $\mathsf {BTEE}$ .

$\mathsf {BTEE}$ is so weak that it even does not allow applying induction on $\omega $ to formulas with j. Thus we postulate induction over $\omega $ for j-formulas as a separate claim. Also, we consider Separation restricted to formulas in $\Gamma $ to gauge the strength of restricted Separation:

It is easy to see that $\Gamma $ -Separation shows not only $\Gamma $ -Induction but also induction for the negation of formulas in $\Gamma $ .

We sometimes consider $\Delta _n$ properties, which is both $\Sigma _n$ and $\Pi _n$ . Unlike the latter two, there is no single entity of $\Delta _n$ -formulas that is independent of the background theory. Thus defining axioms restricted to $\Delta _n$ -properties requires a different formulation.

With an appropriate induction scheme, we can show we can recursively define a function over the set of natural numbers.

For the later analysis, let us provide the proof for the above theorem.

Proof. Let $\phi (x,y,p)$ be a $\Sigma ^j_n$ -formula defining $F(x)=y$ . Now let $\gamma (g,m,p)$ be the following formula:

$$ \begin{align*} \gamma(g,m,p)\equiv \text{"}g \text{ is a function"} \land \operatorname{dom} g = m \land \forall i\in m \phi(g\upharpoonright i, g(i),p). \end{align*} $$

If $\phi (x,y,p)$ is $\Sigma ^j_n$ , then $\gamma (g,m,p)$ is $\Pi ^j_{n+1}$ due to the universal quantifier over i. Now we will claim the following statements: For every natural number m,

• • If $\gamma (f,m,p)$ and $\gamma (g,m,p)$ , then $f=g$ .

• • There is g such that $\gamma (g,m,p)$ .

The first claim follows from applying induction to the formula $i<m \to f(i)=g(i)$ , which is $\Delta _0$ . The second claim follows from applying induction on m to the formula $\exists g \gamma (g,m,p)$ , which is $\Sigma ^j_{n+2}$ . Now define $G(m)$ as follows:

$$ \begin{align*} G(m)=y \iff \exists g [\gamma(g,m+1,p)\land g(m)=y]. \end{align*} $$

If $\phi (x,y,p)$ is $\Delta ^j_0$ , then $\gamma (g,m,p)$ is also $\Delta ^j_0$ . Hence the formula $\exists g \gamma (g,m,p)$ is $\Sigma ^j_1$ , so $\Sigma ^j_1$ -Induction suffices to prove $\forall m<\omega \exists g \gamma (g,m,p)$ . Finally, the defining formula for G is $\Sigma ^j_1$ with parameter p. It is clear that the defining formula of G is uniform in p.

The reader might be curious why the definitional complexity of G is $\Sigma ^j_{n+2}$ and not $\Sigma ^j_n$ . We will show a trick on how to reduce the complexity of G. However, let us point out that our naive $\mathsf {ZFC}$ -minded argument does not work: It is unclear whether bounded quantifiers do not affect the complexity of formulas. If we work over $\mathsf {ZFC}$ , then the axiom of Collection

$$ \begin{align*} \forall x\in a\exists y\phi(x,y)\to \exists b\forall x\in a\exists y\in b \phi(x,y) \end{align*} $$

provides a way to reduce bounded quantifiers. However, we do not have Collection for j-formulas.

But in this case, we can reduce bounded quantifiers in a different way. Let us observe that the bounded quantifier that increases the complexity of the formula $G(m)=y$ is $\forall i\in m$ , which is bounded by a natural number. We can see that under $\Sigma ^j_n$ -Induction, adding a quantifier bounded by a natural number to a $\Sigma ^j_n$ -formula does not increase the complexity of a $\Sigma ^j_n$ -formula.

Lemma 2.15 ( $\mathsf {Z}^-_0+\Sigma ^j_n$ -Induction).

Let $\phi (i,y)$ be a $\Pi ^j_{n-1}$ -formula Then we can prove the following: For a natural number $m<\omega $ ,

$$ \begin{align*} \forall i<m \exists y\phi(i,y)\to \exists f[(f \text{ is a function}) \land \operatorname{dom} f=m\land \forall i<m \phi(i,f(i))]. \end{align*} $$

Proof. Suppose that $\forall i<m\exists y\phi (i,y)$ holds. We apply induction to the following formula:

$$ \begin{align*} k\le m\to \exists f (f \text{ is a function}) \land \operatorname{dom} f=k\land \forall i<k \phi(i,f(i)). \end{align*} $$

We can see that the above formula is equivalent to a $\Sigma ^j_n$ -formula, so we can apply $\Sigma ^j_n$ -Induction. The case $k=0$ is easy, and now assume that the above statement holds for a given k. If $k+1\le m$ , then $k<m$ , so we can find y such that $\phi (k,y)$ . By the inductive hypothesis, we have a function $f\colon k\to V$ such that $\phi (i,f(i))$ holds for all $i<k$ . If we take $f'=f\cup \{(k,y)\}$ , then $f'$ is the desired function we find.

By Lemma 2.9, a conjunction of $\Pi ^j_{n-1}$ formulas is equivalent to a $\Pi ^j_{n-1}$ formula. Hence we get

Going back to the proof of Theorem 2.14, we can see that if F is defined by a $\Sigma ^j_n$ -formula and we have $\Sigma ^j_n$ -Induction, then the resulting G is $\Sigma ^j_n$ -definable. Furthermore, if F is $\Delta ^j_n$ -definable, then $\gamma (g,m)$ becomes a $\Delta ^j_n$ -formula. We still need a $\Sigma ^j_n$ -Induction to ensure $\exists g \gamma (g,m)$ holds for all m, but by uniqueness of g satisfying $\gamma (g,m)$ , the following formula also defines G, which is $\Pi ^j_n$ :

$$ \begin{align*} \forall g [\gamma(g,m+1)\to g(m)=y]. \end{align*} $$

Hence if F is $\Delta ^j_n$ -definable, then G is also $\Delta ^j_n$ -definable. In sum, we have the following.

Now let us define an abbreviation for some formulas, which is related to iterating j.

Corazza [Reference Corazza3, (2.7)–(2.9)] called each of the above formulas $\Theta $ , $\Phi $ , $\Psi $ respectively with a different formulation of $\Phi $ : Corazza did not include $f(n)=y$ as a part of $\Phi $ (or $j\mathsf {iter}$ under our notation.)

We can show the following results.

Also, if we have $\Sigma ^j_0$ -Induction, then we can prove the following.

If we further assume $\Sigma ^j_1$ -Induction, we can see that iterating j defines a total function.

We can see that $\Sigma ^j_n$ -Induction is equivalent to $\Pi ^j_n$ -Induction. The author included a proof for the implication by modifying a proof of [Reference Corazza3, Corollary 5.4] based on Don Hatch’s unpublished result. However, the reviewer pointed out that the following argument is folklore known in the 1970s at the latest. [Reference Parsons10, Section 1(D)]

Proof. We only consider the implication from $\Sigma ^j_n$ -Induction to $\Pi ^j_n$ -Induction since the remaining case is analogous. The case $n=0$ is trivial, so let us consider the case $n>0$ . Assume the contrary, suppose that $\phi (n,p)$ is a $\Pi ^j_n$ -formula that satisfy $\phi (0,p)$ and $\forall n<\omega [(\phi (n,p)\to \phi (n+1,p)]$ , but $\forall n<\omega \phi (n,p)$ fails. Thus there is $N\in \omega $ such that $\lnot \phi (N,p)$ .

Now consider the formula $\psi (n,p,N)$ given by

$$ \begin{align*} \psi(n,p,N)\equiv n\le N \to \lnot\phi(N-n,p). \end{align*} $$

$\psi (n,p,N)$ is equivalent to a $\Sigma ^j_n$ -formula. We claim that induction on n for $\psi $ fails. Assume the contrary that the induction for $\psi $ holds. Clearly $\psi (0,p,N)$ holds. If $\psi (n,p,N)$ holds and $n+1\le N$ , then we have $\psi (n+1,p,N)$ from $\phi (N-n-1,p)\to \phi (N-n,p)$ . Hence $\psi (n,p,N)$ holds for all n, and especially, $\psi (N,p,N)$ holds, which is equivalent to $\lnot \phi (0,p)$ , a contradiction.

Finally, let us define the Wholeness axiom as the combination of $\mathsf {BTEE}$ and $\Sigma ^j_n$ -Separation. We know that $\Sigma ^j_n$ -Separation implies $\Sigma ^j_n$ -Induction, so we can use consequences of $\Sigma ^j_n$ -Induction when we assume $\mathsf {WA}_n$ . Also, we have the following results.

We should be careful when we talk about $V_{j^n(\kappa )}\prec V$ . This statement is actually a schema on a formula, and what it says is for each formula $\phi (x)$ and $a\in V_{j^n(\kappa )}$ , we have $\phi (a)\leftrightarrow V_{j^n(\kappa )}\vDash \phi (a)$ . Finally, we define $\mathsf {WA}$ as the combination of $\mathsf {BTEE}$ and $\Sigma ^j_\infty $ -Separation, that is, Separation for arbitrary j-formulas.

2.4 Reducing axioms

Before finishing this section, let us introduce a form of $\Sigma _n^j$ -Separation that uses a minimal number of quantifiers.

Definition 2.25. Reduced $\Gamma $ -Separation scheme is the statement of the form $\forall a\exists b \mathsf {Sep}^{\prime }_\phi (a,b)$ for a $\Gamma $ -formula $\phi (u)$ with a only single free variable u, where $\mathsf {Sep}^{\prime }_\phi (a,b)$ is the following formula:

$$ \begin{align*} \forall x\in a(\phi(x)\to x\in b) \land \forall x\in b (x\in a\land \phi(x)). \end{align*} $$

Proof. Let a be a non-empty set and $\phi (x,y)$ be a $\Gamma $ -formula. We want to show that for a parameter set p, there is a set b such that

$$ \begin{align*} \forall x[x\in b \leftrightarrow x\in a\land \phi(x,p)]. \end{align*} $$

Let $a'=\{\langle x,p\rangle \mid x\in a\}$ . $a'$ exists since the map $x\mapsto \langle x,p\rangle $ is a $\Delta _0$ -definable class function, so we can apply the $\Delta _0$ -replacement to get $a'$ . By the reduced $\Gamma $ -Separation, the following set exists:

$$ \begin{align*} b' = \{x\in a' \mid \phi(\pi_0(x),\pi_1(x)) \}, \end{align*} $$

where $\pi _0$ and $\pi _1$ are projection functions for the Kuratowski ordered pair, which are $\Delta _0$ -definable. We can check by induction on a complexity of $\phi $ that $\phi (\pi _0(x),\pi _1(x))$ is a $\Gamma $ -formula if $\phi (x,y)$ is a $\Gamma $ -formula, so we can apply the reduced $\Gamma $ -Separation to get $b'$ . Then $b=\pi _0^"[b'] = \{x \mid \langle x,p\rangle \in b'\}$ , and we can see that b satisfies ${b=\{x\in a\mid \phi (x,p)\}}$ .

The following theorem says we can replace Critical Point of $\mathsf {BTEE}$ to a simpler axiom under the Elementarity of j and $\Delta ^j_0$ -Separation.

4.1 A proof of $\mathsf {Con}(\mathsf {ZFC}+\mathsf {WA}_0)$

In this subsection, we prove the consistency of $\mathsf {ZFC}+\mathsf {WA}_0$ from $\mathsf {ZFC}+\mathsf {WA}_0$ + $\Pi ^j_1$ -Induction, which also implies $\mathsf {ZFC}+\mathsf {WA}_1\vdash \mathsf {Con}(\mathsf {ZFC}+\mathsf {WA}_0)$ . Before starting the proof for the main result, let us review the proof-theoretic tools we will use. First, let us fix the language for the theories we will formulate.

There are different ways to formulate first-order logic in proof theory, and we will use Tait-styled one-sided sequent calculus. Hence there is no negation connective, but we include literals (atomic formulas and its negations) as a basic notion. Then we define the negation as follows:

• • $\lnot (s=t) \equiv (s\neq t)$ and $\lnot (s\neq t) \equiv (s=t)$ , and similarly for $\in $ and $\notin $ .

• • $\lnot (\phi \land \psi ) \equiv \lnot \phi \lor \lnot \psi $ and $\lnot (\phi \lor \psi ) \equiv \lnot \phi \land \lnot \psi $ .

• • $\lnot (\forall x \phi (x))\equiv \exists x \lnot \phi (x)$ and $\lnot (\exists x \phi (x))\equiv \forall x \lnot \phi (x)$ , and similarly for bounded quantifiers.

Then let us formulate sequent calculus for first-order logic as follows. We follow terminologies and facts in [Reference Arai1], but the reader may also refer to [Reference Pohlers11, Chapter 4]. We use $A,B,C,\ldots $ to denote formulas, $\Gamma ,\Delta ,\ldots $ to denote sequents (i.e., a finite set of formulas), $s, t$ for terms, and $x,y,z,\ldots $ for free variables. For sequents $\Gamma _0,\ldots ,\Gamma _{m-1}$ and formulas $A_0,\ldots , A_{n-1}$ , the sequence $\Gamma _0,\ldots ,\Gamma _{m-1},A_0,\ldots ,A_{n-1}$ denotes the sequent $\bigcup _{i<m}\Gamma _i\cup \{A_0,\ldots ,A_{n-1}\}$ .

Definition 4.2. Sequent calculus $\mathbf {G}_1$ comprises the following inference rules:

Here Ax applies only when L is a literal, and $\forall $ applies only when y does not occur in the lower sequent $\Gamma ,\forall x A(x)$ freely. We call y in the $\forall $ rule an eigenvariable of the inference rule $\forall $ .

Note that the cut rule

is not part of $\mathbf {G}_1$ . It is known that $\mathbf {G}_1$ with the Cut rule is sound [Reference Arai1, Proposition 1.1], and $\mathbf {G}_1$ (even without the Cut rule) is complete.

The completeness theorem holds for not only $\mathbf {G}_1$ but also a modification of $\mathbf {G}_1$ augmented with new inference rules associated with a given theory T. The easiest way to add a new inference associated with $A\in T$ is by adding the rule

When A takes the form $\forall \vec {y} \left [ \left [\bigwedge _{i<n} \forall \vec {x}_i \bigvee \Phi _i(\vec {x}_i,\vec {y}) \right ]\to \bigwedge \Phi (\vec {y})\right ]$ , we may add the following rule instead:

where $\vec {z}_i$ do not occur free in $\Gamma ,\Phi (\vec {t})$ . Let us say $\mathbf {G}_T \supseteq \mathbf {G}_1$ is an admissible expansion for T if $\mathbf {G}_T$ comprises rules of $\mathbf {G}_1$ and one of $\mathrm {Ax}_A$ or $\mathrm {Ax}^{\prime }_A$ for each $A\in T$ . The following theorem follows from a proof of [Reference Arai1, Theorem 2.2].

Now let us consider the case $T=\mathsf {ZFC}+\mathsf {WA}_0$ . We consider the following admissible expansion $\mathbf {G}_{\mathsf {WA}_0}$ : It comprises axioms of $\mathbf {G}_1$ and

In $b\forall $ and $\Delta ^j_0$ -Sep, y does not occur free in the lower sequent, $s\subseteq t$ is an abbreviation of $\forall x\in s(x\in t)$ , and in $\Delta ^j_0$ -Sep, $A(x)$ is a $\Delta ^j_0(\Sigma _\infty )$ -formula. We call the free variable y the eigenvariable of the corresponding inference rule. By Theorem 4.4, every $\mathsf {ZFC}+\mathsf {WA}_0$ -theorem is a theorem of $\mathbf {G}_{\mathsf {WA}_0}$ .

Example 4.5. The following proof tree is a proof of the symmetry of equality, where A is the formula $(t_0=t_1 \lor t_1\neq t_0)$ :

Also, observe that for every $\mathbf {G}_{\mathsf {WA}_0}$ -proof $\pi $ with the end sequent $\Gamma $ , every formula occurring in $\pi $ is either $\Delta ^j_0(\Sigma _\infty )$ -formula or a subformula of a formula in $\Gamma $ .

The presence of a partial truth predicate shows the soundness of $\mathsf {ZFC}+\mathsf {WA}_0$ . More precisely,

Hence we have the following.

4.2 Wholeness by numbers, one, two, three…

In this subsection, we prove that $\mathsf {ZFC}+\mathsf {WA}_{n+1}$ proves the consistency of $\mathsf {ZFC}+\mathsf {WA}_n$ . Let us consider the sequent calculus $\mathbf {G}_{\mathsf {WA}_n}$ obtained from $\mathbf {G}_{\mathsf {WA}_0}$ by replacing $\Delta ^j_0$ -Sep rule to $\Sigma ^j_n$ -Sep rule stated in (7), which is obtained by modifying $\Delta ^j_0$ -Sep rule by allowing $A(x)$ to be $\Sigma ^j_n(\Sigma _\infty )$ and replacing bounded quantification in

$$ \begin{align*} \exists x\in t_i (A(x)\land x\notin y_i) \end{align*} $$

to an equivalent unbounded quantification $\exists x (x\in t_i\land A(x)\land x\notin y_i)$ . Observe that $\mathsf {ZFC} + \mathsf {WA}_0$ + $\Pi ^j_1$ -Induction proves $\vDash _{\Sigma ^j_n(\Sigma _\infty )}$ is $\Sigma ^j_n$ -definable, so so we may replace the $\Sigma ^j_n$ -Sep rules to its single instance given by $\vDash _{\Sigma ^j_n(\Sigma _\infty )}$ . Moreover, a proof of Lemma 2.26 tells us we may assume that $A(x)$ has a unique single variable x. Again, it follows that if $\mathsf {ZFC}+\mathsf {WA}_n\vDash \bigvee \Gamma $ , then $\mathbf {G}_{\mathsf {WA}_n}\vdash \Gamma $ .

Now we claim that $\mathsf {ZFC}+\mathsf {WA}_n + \Pi ^j_{n+1}$ -Induction proves the consistency of $\mathsf {ZFC}+\mathsf {WA}_n$ . More precisely, we have the following.

Theorem 4.8 ( $\mathsf {ZFC}+\mathsf {WA}_n + \Pi ^j_{n+1}$ -Induction).

Let $\Gamma $ be a sequent in which every formula is in $\Sigma ^j_n(\Sigma _\infty )\cup \Pi ^j_n(\Sigma _\infty )$ . We define $\Gamma _{\Sigma ^j_n(\Sigma _\infty )} \subseteq \Gamma $ is the subsequent comprising every $\Sigma ^j_n(\Sigma _\infty )$ -formula of $\Gamma $ , and define $\Gamma _{\Pi ^j_n(\Sigma _\infty )} \subseteq \Gamma $ similarly. Suppose that $\mathbf {G}_{\mathsf {WA}_n}\vdash \Gamma $ . Then we have

$$ \begin{align*} \textstyle \forall \vec{a}\in V^{<\omega}\left[ \vDash_{\underline{\Sigma}^j_n(\Sigma_\infty)} \left( \bigvee \Gamma_{\Sigma^j_n(\Sigma_\infty)} \right)(\vec{a}) \lor \vDash_{\underline{\Pi}^j_n(\Sigma_\infty)} \left( \bigvee \Gamma_{\Pi^j_n(\Sigma_\infty)} \right)(\vec{a}) \right] \end{align*} $$

if we interpret $\mathsf {j}$ by j and $\dot {\kappa }$ by $\kappa $ .

Proof. The proof is more convoluted than that of Theorem 4.6 due to $\Sigma ^j_n$ -Sep rule: The upper sequent of $\Sigma ^j_n$ -Sep rule has $\exists x\in y \lnot A(x)$ , which is not in $\Sigma ^j_n(\Sigma _\infty )\cup \Pi ^j_n(\Sigma _\infty )$ when A is $\Sigma ^j_n(\Sigma _\infty )$ . We handle this issue by manually substituting an appropriate instance.

Let us fix a $\mathbf {G}_{\mathsf {WA}_n}$ -proof $\pi $ of $\Gamma $ . From the previous discussion, we may assume that $\pi $ uses a single instance of $\Sigma ^j_n$ -Sep for the formula $A(x)$ whose only free variable is x. Let $\{x_i\mid i<N\}$ be the enumeration of eigenvariables of $\forall $ or $b\forall $ , or free variables occurring in $\pi $ , and $\{y_i\mid i<m\}$ and $\{t_i\mid i<m\}$ be enumerations of eigenvariables and terms of $\Sigma ^j_n$ -Sep rule

(7)

By indexing the eigenvariables from the bottommost sequent of $\pi $ , we may assume that if $y_{i'}$ occurs in $\Gamma $ of the $\Sigma ^j_n$ -Sep rule, then $i'<i$ . We can also find a finite sequence of natural numbers $\{k_i\mid i<m\}$ such that if $x_k$ occurs in $\Gamma ^{\prime }_i$ of the instance of $\Sigma ^j_n$ -Sep, then $k<k_i$ . We may also assume $\langle k_i\mid i<m\rangle $ is increasing. Then we have that every $t_i$ is of the form $\mathsf {j}^{p_i}(v)$ for some $p_i<\omega $ and $v\in \{\dot {\kappa }\}\cup \{x_k\mid k<k_i\}\cup \{y_{i'}\mid i'<i\}$ .

Then let us define subsidiary parameters $c_i(\vec {a})$ , $b_i(\vec {a})$ , and $d_i(\vec {a})$ by induction on $i<m$ as follows: First, define

• • $c_i(\vec {a}) := j^{p_i}(\kappa )$ when $t_i \equiv \mathsf {j}^{p_i}(\dot {\kappa })$ .

• • $c_i(\vec {a}) := j^{p_i}(\vec {a}_{x_k})$ when $t_i \equiv \mathsf {j}^{p_i}(x_k)$ .

• • $c_i(\vec {a}) := j^{p_i}(c_{i'}(\vec {a}))$ when $t_i \equiv \mathsf {j}^{p_i}(y_{i'})$ .

We set $c(\vec {a}) = \bigcup _{i<m} c_i(\vec {a})$ and $b(\vec {a}) = \{x\in c(\vec {a}) \mid \vDash _{\Sigma ^j_n(\Sigma _\infty )} A(x)\}$ . Then define

$$ \begin{align*} d_i(\vec{a}) = \begin{cases} j^{p_i}(b_{i'}(\vec{a})), & t_i\equiv \mathsf{j}^{p_i}(y_{i'}), \\ c_i(\vec{a}), & \text{otherwise,} \end{cases} \end{align*} $$

and $b_i(\vec {a}) = b(\vec {a}) \cap d_i(\vec {a})$ . Finally, define $\vec {a}' = \vec {a}[b_0(\vec {a})/y_0,\ldots , b_{m-1}(\vec {a})/y_{m-1}]$ .

Lemma 4.9. We have the following:

1. (1) $\vDash _{\Delta ^j_0(\Sigma _\infty )} d_i(\vec {a}) = t_i[\vec {a}']$ .

2. (2) $b_i(\vec {a}) \subseteq d_i(\vec {a}) \subseteq c_i(\vec {a})$ .

3. (3) $b_i(\vec {a}) = \{x\in d_i(\vec {a}) \mid \vDash _{\Sigma ^j_n(\Sigma _\infty )} A(x)\}$ .

Proof.

1. (1) If $t_i \equiv \mathsf {j}^{p_i}(y_{i'})$ , then $d_i(\vec {a}) = j^{p_i}(b_{i'}(\vec {a}))$ and $\vDash _{\Delta ^j_0(\Sigma _\infty )} t_i[\vec {a}'] = j^{p_i}(b_{i'}(\vec {a}))$ . The equality is clear otherwise.

2. (2) We prove it by induction on $i<m$ : The first inclusion follows from the definition. For the second inclusion, if $t_i\not \equiv \mathsf {j}^{p_i}(y_{i'})$ for every $i'<i$ , then $d_i(\vec {a})=c_i(\vec {a})$ . If $t_i\equiv \mathsf {j}^{p_i}(y_{i'})$ for some $i'<i$ , then

   $$ \begin{align*} d_i(\vec{a}) = j^{p_i}(b_{i'}(\vec{a})) \subseteq j^{p_i}(c_{i'}(\vec{a})) = c_i(\vec{a}) \end{align*} $$

   by the induction hypothesis on $i'<i$ .

3. (3) Follows from the previous inclusion and the definition of $b(\vec {a})$ .

Before applying the induction, we further assume we fixed an enumeration of sequents occurring in $\pi $ in a way that upper sequents occur earlier than lower sequents in the enumeration. There is no guarantee that every formula occurring in $\pi $ is in $\Sigma ^j_n(\Sigma _\infty )\cup \Pi ^j_n(\Sigma _\infty )$ . However, we can still see that the only formula occurring in $\pi $ that is not in $\Sigma ^j_n(\Sigma _\infty )\cup \Pi ^j_n(\Sigma _\infty )$ is $\exists x\in y_i \lnot A(x)$ for some eigenvariable $y_i$ . Then we claim the following by $\Pi ^j_{n+1}$ -Induction on a sequent $\Gamma $ of $\pi $ :

(8) $$ \begin{align} \textstyle \vDash_{\underline{\Sigma}^j_n(\Sigma_\infty)} \left( \bigvee \Gamma_{\Sigma^j_n(\Sigma_\infty)} \right)(\vec{a}') \lor \vDash_{\underline{\Pi}^j_n(\Sigma_\infty)} \left( \bigvee \Gamma_{\Pi^j_n(\Sigma_\infty)} \right)(\vec{a}'). \end{align} $$

( $\Gamma $ may contain formulas not in $\Sigma ^j_n(\Sigma _\infty )\cup \Pi ^j_n(\Sigma _\infty )$ , but it will turn out that we can ignore such formulas.) Let us only consider the following non-trivial cases:

1. (1) When $\Gamma $ is the lower sequent of $\Sigma ^j_n$ -Sep rule: By the induction hypothesis, we have either (8), or $\exists x [\vDash _{\Sigma ^j_n(\Sigma _\infty )} x\in d_i(\vec {a})\land A(x) \land x\notin b_i(\vec {a})]$ , or $b_i(\vec {a})\nsubseteq d_i(\vec {a})$ . The latter two cases fail, so we get (8).

2. (2) When $\Gamma $ is the lower sequent of $b\exists $ rule introducing $\exists x\in y_i \lnot A(x)$ :

   

   Let $e=t(\vec {a}')$ . From the induction hypothesis, we have ((8) or $e\in b_i(\vec {a})$ ) and ((8) or $\vDash _{\Pi ^j_n(\Sigma _\infty )}\lnot A(e)$ ). But we have $\lnot ( e\in b_i(\vec {a})\land \vDash _{\Pi ^j_n(\Sigma _\infty )} \lnot A(e))$ , so (8) holds.

Hence we have

We also note that the consistency separation result also shows $\mathsf {ZFC}+\mathsf {WA}$ is not finitely axiomatizable.

4.3 Separating $\Pi ^j_n$ -Induction

$\Pi ^j_{n+1}$ -Induction has a critical role in the previous subsections, and we may ask if we can separate $\Pi ^j_n$ -Induction by their strength. To answer the question, we prove that for $m\ge n$ , $\mathsf {ZFC}+\mathsf {WA}_n + \Pi ^j_{m+1}$ -Induction proves the consistency of $\mathsf {ZFC}+\mathsf {WA}_n + \Pi ^j_{m}$ -Induction. We fix $m\ge n$ throughout this section, and we may assume $m>n$ since we have considered the case $m=n$ .

We need an appropriate sequent calculus for $\mathsf {ZFC}+\mathsf {WA}_n + \Pi ^j_{m}$ -Induction to prove the theorem. Let us recall that the statement $x\in \omega $ is $\Delta _0$ -expressible in set theory and so we identify $x\in \omega $ with the corresponding $\Delta _0$ -expression. Then let us consider the following rule:

Here $A(x)$ is $\Pi ^j_m(\Sigma _\infty )$ , and y does not occur free in $\Gamma $ . In principle, $0$ and $y+1$ are not part of the language of set theory we consider. However, both $0$ and the successor function are $\Delta _0$ -definable, and for each $\Sigma ^j_m(\Sigma _\infty )$ -formula $A(x)$ , we can uniformly find a $\Sigma ^j_m(\Sigma _\infty )$ -formula equivalent to $A(0)$ and $A(y+1)$ respectively. We fix such $\Sigma ^j_m(\Sigma _\infty )$ -formulas, and apply them to formulate $\Sigma ^j_m$ -Ind rule.

We can see that if $\mathsf {ZFC}{\kern-1pt}+{\kern-1pt}\mathsf {WA}_n {\kern-1pt}+{\kern-1pt} \Pi ^j_m$ -Induction proves $\phi $ , then ${\mathbf {G}_{\mathsf {WA}_n}{\kern-1pt}+{\kern-1pt} \Pi ^j_m\text {-Ind}\vdash \phi }$ . Then let us prove the following.

Proposition 4.12 ( $\mathsf {ZFC}+\mathsf {WA}_n+\Pi ^j_{m+1}$ -Induction).

Let $\Gamma $ be a sequent in which every formula is $\Sigma ^j_m(\Sigma _\infty )\cup \Pi ^j_m(\Sigma _\infty )$ . If , then the following holds:

$$ \begin{align*} \textstyle \forall \vec{a}\in V^{<\omega}\left[ \vDash_{\underline{\Sigma}^j_m(\Sigma_\infty)} \left( \bigvee \Gamma_{\Sigma^j_n(\Sigma_\infty)} \right)(\vec{a}) \lor \vDash_{\underline{\Pi}^j_m(\Sigma_\infty)} \left( \bigvee \Gamma_{\Pi^j_n(\Sigma_\infty)} \right)(\vec{a}) \right]. \end{align*} $$