Proof. 1. Let $\varphi (x, y)$ be the formula $x = y \to \Box x = y$ . Firstly, we prove $\mathbf {PA}_{\Box } \vdash \forall y \varphi (0, y)$ . Since $\mathbf {PA} \vdash 0 = 0$ , we have $\mathbf {PA}_{\Box } \vdash \Box 0 = 0$ , and hence $\mathbf {PA}_{\Box } \vdash \varphi (0, 0)$ . Since $\mathbf {PA} \vdash 0 \neq S(y)$ , we also have $\mathbf {PA}_{\Box } \vdash \varphi (0, S(y))$ , and thus $\mathbf {PA}_{\Box } \vdash \forall y(\varphi (0, y) \to \varphi (0, S(y)))$ . By the induction axiom for $\varphi (0, y)$ , we obtain $\mathbf {PA}_{\Box } \vdash \forall y \varphi (0, y)$ .

Secondly, we prove $\mathbf {PA}(\mathbf {K}) \vdash \forall y \varphi (x, y) \to \forall y \varphi (S(x), y)$ . Since $\mathbf {PA} \vdash S(x) \neq 0$ , we have $\mathbf {PA}_{\Box } \vdash \varphi (S(x), 0)$ . It follows from $\mathbf {PA} \vdash S(x) = S(y) \to x = y$ that $\mathbf {PA}_{\Box } \vdash \varphi (x, y) \land S(x) = S(y) \to \Box x = y$ . Since $\mathbf {PA} \vdash x = y \to S(x) = S(y)$ , we have $\mathbf {PA}(\mathbf {K}) \vdash \Box x = y \to \Box S(x) = S(y)$ . Thus, we get

$$\begin{align*}\mathbf{PA}(\mathbf{K}) \vdash \varphi(x, y) \land S(x) = S(y) \to \Box S(x) = S(y). \end{align*}$$

This means $\mathbf {PA}(\mathbf {K}) \vdash \varphi (x, y) \to \varphi (S(x), S(y))$ . By the universal instantiation, we have $\mathbf {PA}(\mathbf {K}) \vdash \forall y \varphi (x, y) \to \varphi (S(x), S(y))$ , and hence

$$\begin{align*}\mathbf{PA}(\mathbf{K}) \vdash \forall y\varphi(x, y) \to \forall y(\varphi(S(x), y) \to \varphi(S(x), S(y))). \end{align*}$$

From this with $\mathbf {PA}_{\Box } \vdash \varphi (S(x), 0)$ , we obtain $\mathbf {PA}(\mathbf {K}) \vdash \forall y \varphi (x, y) \to \forall y \varphi (S(x), y)$ by the induction axiom for $\varphi (S(x), y)$ .

Finally, by the induction axiom for $\forall y \varphi (x, y)$ , we conclude $\mathbf {PA}(\mathbf {K}) \vdash \forall x \forall y \varphi (x, y)$ .

2. This is proved by induction on the construction of $\varphi (x)$ . We only prove the case that $\varphi (x)$ is of the form $\Box \psi (x)$ and the statement holds for $\psi (x)$ . By the induction hypothesis, $\mathbf {PA}(\mathbf {K}) \vdash x = y \to (\psi (x) \to \psi (y))$ . Then, $\mathbf {PA}(\mathbf {K})$ proves $\Box x = y \to (\Box \psi (x) \to \Box \psi (y))$ . By combining this with Clause 1, we conclude $\mathbf {PA}(\mathbf {K}) \vdash x = y \to (\Box \psi (x) \to \Box \psi (y))$ .

Proof. We prove the proposition by induction on the length of proofs of $\varphi $ in $\mathbf {PA}(\mathbf {Triv})$ .

• • If $\varphi $ is an axiom of $\mathbf {PA}$ , then $\alpha (\varphi ) \equiv \varphi $ and $\mathbf {PA} \vdash \alpha (\varphi )$ .

• • If $\varphi $ is a logical axiom, then so is $\alpha (\varphi )$ , and it is $\mathbf {PA}$ -provable.

• • If $\varphi $ is an induction axiom in the language $\mathcal {L}_A(\Box )$ , then $\alpha (\varphi )$ is also an induction axiom in $\mathcal {L}_A$ , and so $\mathbf {PA} \vdash \alpha (\varphi )$ .

• • If $\varphi $ is $\forall \vec {x}(\Box (\psi \to \sigma ) \to (\Box \psi \to \Box \sigma ))$ , then $\alpha (\varphi )$ is the $\mathbf {PA}$ -provable sentence $\forall \vec {x} \bigl ((\alpha (\psi ) \to \alpha (\sigma )) \to (\alpha (\psi ) \to \alpha (\sigma )) \bigr )$ .

• • If $\varphi $ is $\forall \vec {x} (\psi \leftrightarrow \Box \psi )$ , then $\alpha (\varphi )$ is $\forall \vec {x}(\alpha (\psi ) \leftrightarrow \alpha (\psi ))$ . This is provable in $\mathbf {PA}$ .

• • If $\varphi $ is derived from $\psi $ and $\psi \to \varphi $ by MP, then by the induction hypothesis, $\mathbf {PA} \vdash \alpha (\psi )$ and $\mathbf {PA} \vdash \alpha (\psi ) \to \alpha (\varphi )$ , and hence $\mathbf {PA} \vdash \alpha (\varphi )$ .

• • If $\varphi $ is derived from $\psi (x)$ by Gen, then $\varphi \equiv \forall x \psi (x)$ . By the induction hypothesis, $\mathbf {PA} \vdash \alpha (\psi (x))$ and hence $\mathbf {PA} \vdash \forall x \alpha (\psi (x))$ . Therefore, $\mathbf {PA} \vdash \alpha (\varphi )$ .

• • If $\varphi $ is derived from $\psi $ by Nec, then $\varphi \equiv \Box \psi $ . By the induction hypothesis, $\mathbf {PA} \vdash \alpha (\psi )$ . Since $\alpha (\varphi ) \equiv \alpha (\psi )$ , we have $\mathbf {PA} \vdash \alpha (\varphi )$ .

Proof. Let $\varphi $ be any $\mathcal {L}_A$ -sentence such that $\mathbf {PA}(\mathbf {Triv}) \vdash \varphi $ . By Proposition 2.3, $\mathbf {PA} \vdash \alpha (\varphi )$ . Since $\alpha (\varphi ) \equiv \varphi $ , $\mathbf {PA} \vdash \varphi $ . Furthermore, by the $\mathcal {L}_A$ -soundness of $\mathbf {PA}$ , $\mathbf {PA}(\mathbf {Triv})$ is also $\mathcal {L}_A$ -sound.

Proof. As in the proof of Proposition 2.3, this proposition is proved by induction on the length of proofs of $\varphi $ in $\mathbf {PA}(\mathbf {Verum})$ . We only give proofs of the following three cases:

• • If $\varphi $ is $\forall \vec {x}(\Box (\psi \to \sigma ) \to (\Box \psi \to \Box \sigma ))$ , then $\beta (\varphi )$ is the $\mathbf {PA}$ -provable sentence $\forall \vec {x} (0=0 \to (0=0 \to 0=0))$ .

• • If $\varphi $ is $\Box \bot $ , then $\beta (\varphi )$ is the $\mathbf {PA}$ -provable sentence $0=0$ .

• • If $\varphi $ is derived from $\psi $ by Nec, then $\varphi \equiv \Box \psi $ . Since $\beta (\varphi ) \equiv 0=0$ , this is $\mathbf {PA}$ -provable.

Proof. Before proving the theorem, we show that for any $\Sigma _1$ formula $\psi $ , there exists a $\Sigma _1$ formula $\psi '$ such that $\mathbf {PA} \vdash \psi \leftrightarrow \psi '$ , $\psi '$ does not contain the connectives $\neg $ and $\to $ , and every atomic formula contained in $\psi '$ is of the form $t_1 = t_2$ for some $\mathcal {L}_A$ -terms $t_1$ and $t_2$ . First, we easily find a $\Sigma _1$ formula $\psi _0$ without the connective $\to $ such that $\psi _0$ is logically equivalent to $\psi $ and every negation symbol $\neg $ in $\psi _0$ is applied to an atomic formula. Then, by replacing every negated atomic formula $\neg (t_1 = t_2)$ or $\neg (t_1 < t_2)$ of $\psi_0$ by $t_1 < t_2 \lor t_2 < t_1$ or $t_1 = t_2 \lor t_2 < t_1$ respectively, we obtain a $\mathbf {PA}$ -equivalent $\Sigma _1$ formula $\psi _1$ without having $\neg $ . Finally, by replacing every atomic formula $t_1 < t_2$ of $\psi _1$ by $\exists y(t_1 + S(y) = t_2)$ , we obtain a required equivalent $\Sigma _1$ formula $\psi '$ . Since $\mathbf {PA}(\mathbf {K}) \vdash \Box \psi \leftrightarrow \Box \psi '$ , to prove the theorem, it suffices to show that $\mathbf {PA}(\mathbf {K}) \vdash \varphi \to \Box \varphi $ for any $\Sigma _1$ formula $\varphi $ such that it does not contain the connectives $\neg $ and $\to $ , and that every atomic formula contained in $\varphi $ is of the form $t_1 = t_2$ for some $\mathcal {L}_A$ -terms $t_1$ and $t_2$ .

This theorem is proved by induction on the construction of $\varphi $ . If $\varphi $ is $t_1 = t_2$ , then $\mathbf {PA}(\mathbf {K}) \vdash t_1 = t_2 \to \Box t_1 = t_2$ follows from $\mathbf {PA}(\mathbf {K}) \vdash x = y \to \Box x = y$ (Proposition 2.1) by substituting $t_1$ and $t_2$ into $x$ and y, respectively. The cases for $\land $ , $\lor $ , $\forall x < t$ and $\exists $ are proved as in the proof of Theorem 3.13.

Proof. We prove the proposition by induction on the construction of $\varphi $ .

• • If $\varphi $ is $\Sigma _1$ , then there exists a $\Delta _0$ formula $\psi $ such that $\mathbf {PA} \vdash \varphi \leftrightarrow \exists v \psi $ .

• • If $\varphi $ is of the form $\Box \varphi _0$ , then $\varphi \in \Delta (\mathrm {B})$ and $\mathbf {PA}_{\Box } \vdash \varphi \leftrightarrow \exists v \varphi $ for a variable $v $ not contained in $\varphi $ .

• • Let $\circ \in \{\land , \lor \}$ . If $\varphi $ is of the form $\varphi _0 \circ \varphi _1$ , then by the induction hypothesis, there exist distinct variables $v_0$ and $v_1$ and $\Delta (\mathrm {B})$ formulas $\psi _0$ and $\psi _1$ such that $\mathbf {PA}_{\Box }$ proves $\varphi _0 \leftrightarrow \exists v_0 \psi _0$ and $\varphi _1 \leftrightarrow \exists v_1 \psi _1$ . Let $v $ be any variable that does not occur in $\psi _0$ or $\psi _1$ , and is not $v_0$ or $v_1$ . Then, $\mathbf {PA}_{\Box }$ proves the equivalence $\varphi \leftrightarrow \exists v \, \exists v_0 < v \, \exists v_1 < v \, (\psi _0 \circ \psi _1)$ .

• • If $\varphi $ is of the form $\exists x \varphi _0$ , then by the induction hypothesis, there exist a variable $v_0$ and a $\Delta (\mathrm {B})$ formula $\psi _0$ such that $\mathbf {PA} \vdash \varphi _0 \leftrightarrow \exists v_0 \psi _0$ . Let $v $ be any variable not contained in $\psi _0$ and is not $v_0$ or $x$ . Then, $\mathbf {PA}_{\Box }$ proves the equivalence $\varphi \leftrightarrow \exists v \, \exists x < v \, \exists v_0 < v \, \psi _0$ .

• • The case that $\varphi $ is of the form $\exists x < t\, \varphi _0$ , where $t$ is an $\mathcal {L}_A$ -term in which $x$ does not occur is proved as in the proof of the case of $\exists $ .

• • Suppose $\varphi $ is of the form $\forall x < t\, \varphi _0$ , where $t$ is an $\mathcal {L}_A$ -term in which $x$ does not occur. By the induction hypothesis, there exists a variable $v_0$ and a $\Delta (\mathrm {B})$ formula $\psi _0$ such that $\mathbf {PA}_{\Box } \vdash \varphi _0 \leftrightarrow \exists v_0 \psi _0$ . Then, $\mathbf {PA}_{\Box } \vdash \varphi \leftrightarrow \forall x < t\, \exists v_0 \psi _0$ . By the collection principle for $\mathcal {L}_A(\Box )$ -formulas derived from the induction axioms for $\mathcal {L}_A(\Box )$ -formulas, we obtain

  $$\begin{align*}\mathbf{PA}_{\Box} \vdash \varphi \leftrightarrow \exists v\, \forall x < t\, \exists v_0 < v\, \psi_0 \end{align*}$$
  for some appropriate variable $v $ .

Proof. We prove the proposition by induction on the construction of $\varphi $ .

• • If $\varphi $ is a $\Delta _0$ sentence, then either $\mathbf {PA} \vdash \varphi $ or $\mathbf {PA} \vdash \neg \varphi $ . Thus, $\mathbf {PA}(\mathbf {K}) \vdash \varphi \leftrightarrow \Box 0=0$ or $\mathbf {PA}(\mathbf {K}) \vdash \varphi \leftrightarrow \bot $ .

• • If $\varphi $ is of the form $\Box \psi $ , then the statement is trivial.

• • If $\varphi $ is of the form $\psi \land \sigma $ , then there exist sentences $\xi _0, \ldots , \xi _{k-1}, \eta _0, \ldots , \eta _{l-1}$ such that $\mathbf {PA}(\mathbf {K}) \vdash \psi \leftrightarrow \bigvee _{i < k} \Box \xi _i$ and $\mathbf {PA}(\mathbf {K}) \vdash \sigma \leftrightarrow \bigvee _{j < l} \Box \eta _j$ . Then, $\mathbf {PA}(\mathbf {K}) \vdash \varphi \leftrightarrow \bigvee _{i < k} \bigvee _{j < l} \Box (\xi _i \land \eta _j)$ .

• • If $\varphi $ is of the form $\psi \lor \sigma $ , then the statement is obvious by the induction hypothesis.

• • If $\varphi $ is of the form $\exists y < t\, \psi (y)$ for some $\mathcal {L}_A$ -term $t$ , then $t$ is a closed term because $\varphi $ is a sentence. Let m be the value of $t$ , then $\mathbf {PA}(\mathbf {K}) \vdash \varphi \leftrightarrow \bigvee _{i < m} \psi (\overline {i})$ . Then, the statement holds by the induction hypothesis.

• • If $\varphi $ is of the form $\forall y < t\, \psi (y)$ for some closed $\mathcal {L}_A$ -term $t$ , then for the value m of the term $t$ , $\mathbf {PA}(\mathbf {K}) \vdash \varphi \leftrightarrow \bigwedge _{i < m} \psi (\overline {i})$ . We can prove the statement by the induction hypothesis as in the proof of the case $\land $ .

Proof. Suppose, towards a contradiction, that $\varphi $ is a $\Delta (\mathrm {B})$ sentence such that $T \vdash \neg \Box \bot \leftrightarrow \varphi $ . By Proposition 3.11, there exist $k$ and $\psi _0, \ldots , \psi _{k-1}$ such that $\mathbf {PA}(\mathbf {K}) \vdash \varphi \leftrightarrow \bigvee _{i < k} \Box \psi _i$ . Then, $T \vdash \neg \Box \bot \leftrightarrow \bigvee _{i < k} \Box \psi _i$ . Since $T \nvdash \Box \bot $ , we get $k> 0$ . Then, $T \vdash \Box \psi _0 \to \neg \Box \bot $ . On the other hand, $T \vdash \neg \Box \psi _0 \to \neg \Box \bot $ because T is an extension of $\mathbf {PA}(\mathbf {K})$ . Therefore, we obtain $T \vdash \neg \Box \bot $ . This is a contradiction.

Proof. We prove the theorem by induction on the construction of $\varphi $ .

• • If $\varphi $ is a $\Sigma _1$ formula, then $\mathbf {PA}(\mathbf {K}) \vdash \varphi \to \Box \varphi $ by Theorem 2.8.

• • If $\varphi $ is of the form $\Box \psi $ , then $\mathbf {PA}(\mathbf {K4}) \vdash \varphi \to \Box \varphi $ .

• • If $\varphi $ is $\psi \land \sigma $ , then by the induction hypothesis, $\mathbf {PA}(\mathbf {K4}) \vdash \varphi \to \Box \psi \land \Box \sigma $ . We have $\mathbf {PA}(\mathbf {K4}) \vdash \varphi \to \Box \varphi $ .

• • If $\varphi $ is $\psi \lor \sigma $ , then by the induction hypothesis, $\mathbf {PA}(\mathbf {K4})$ proves $\psi \to \Box (\psi \lor \sigma )$ and $\sigma \to \Box (\psi \lor \sigma )$ . Hence, $\mathbf {PA}(\mathbf {K4}) \vdash \varphi \to \Box \varphi $ .

• • Suppose that $\varphi $ is $\exists x \psi $ . Since $\mathbf {PA}(\mathbf {K}) \vdash \psi \to \exists x \psi $ , we have $\mathbf {PA}(\mathbf {K}) \vdash \Box \psi \to \Box \exists x \psi $ . By the induction hypothesis, $\mathbf {PA}(\mathbf{K4}) \vdash \psi \to \Box \psi $ . Thus, $\mathbf {PA}(\mathbf{K4}) \vdash \psi \to \Box \exists x \psi $ . Then, we obtain $\mathbf {PA}(\mathbf {K4}) \vdash \varphi \to \Box \varphi $ .

• • Before proving the case that $\varphi $ is of the form $\forall x < t\, \psi (x)$ generally, we prove the restricted case that $t$ is some variable y not occurring in $\psi $ . Suppose that $\varphi (y)$ is of the form $\forall x < y\, \psi (x)$ for some variable y not occurring in $\psi (x)$ . Let $\xi (y)$ be the formula $\varphi (y) \to \Box \varphi (y)$ , and then we prove $\mathbf {PA}(\mathbf {K}) \vdash \forall y \xi (y)$ by using the induction axiom.

  For the base step, since trivially $\mathbf {PA}(\mathbf {K}) \vdash \forall x < 0\, \psi (x)$ , we have $\mathbf {PA}(\mathbf {K}) \vdash \Box \varphi (0)$ and hence $\mathbf {PA}(\mathbf {K}) \vdash \xi (0)$ .

  For the induction step, since

  $$\begin{align*}\mathbf{PA}(\mathbf{K}) \vdash [\forall x < S(y)\, \psi(x)] \leftrightarrow [(\forall x < y\, \psi(x)) \land \psi(y)], \end{align*}$$
  we have
  (1) $$ \begin{align} \mathbf{PA}(\mathbf{K}) \vdash \varphi(S(y)) \leftrightarrow [\varphi(y) \land \psi(y)]. \end{align} $$
  By the induction hypothesis, $\mathbf {PA}(\mathbf {K4}) \vdash \psi (y) \to \Box \psi (y)$ . By combining this with (1) and the definition of $\xi (y)$ ,
  $$\begin{align*}\mathbf{PA}(\mathbf{K4}) \vdash \xi(y) \land \varphi(S(y)) \to \Box \varphi(y) \land \Box \psi(y). \end{align*}$$
  Then, by (1) again,
  $$\begin{align*}\mathbf{PA}(\mathbf{K4}) \vdash \xi(y) \land \varphi(S(y)) \to \Box \varphi(S(y)). \end{align*}$$
  Equivalently, $\mathbf {PA}(\mathbf {K4}) \vdash \xi (y) \to \xi (S(y))$ .

  Therefore, by the induction axiom, we conclude $\mathbf {PA}(\mathbf {K4}) \vdash \forall y \xi (y)$ .

  Finally, suppose that $\varphi $ is of the form $\forall x < t\, \psi $ for some $\mathcal {L}_A$ -term $t$ . We have already proved that $\mathbf {PA}(\mathbf {K4})$ proves $\forall x < y\, \psi \to \Box \forall x < y\, \psi $ for some variable y not occurring in $\psi $ . By substituting $t$ for y in this formula, we obtain $\mathbf {PA}(\mathbf {K4}) \vdash \varphi \to \Box \varphi $ .

Proof. This is proved by induction on the length of a proof of $\varphi $ in $T + X$ . We only give a proof of the case that $\varphi $ is derived from $\psi $ by the rule Nec. Then, $\varphi $ is of the form $\Box \psi $ . By the induction hypothesis, $T \vdash \sigma _0 \land \cdots \land \sigma _{k-1} \to \psi $ for some $\sigma _0, \ldots , \sigma _{k-1} \in X$ . Then, $T \vdash \Box \sigma _0 \land \cdots \land \Box \sigma _{k-1} \to \Box \psi $ . By Theorem 3.13, $T \vdash \sigma _0 \land \cdots \land \sigma _{k-1} \to \Box \psi $ .

Proof. 1. Let $\varphi _1, \ldots , \varphi _n$ be any sentences such that $T \vdash \Box \varphi _1 \lor \cdots \lor \Box \varphi _n$ . Then, $T \vdash \Box \varphi _1 \lor \cdots \lor \Box \varphi _n \lor \Box \varphi _n$ . By $\mathrm {B}^{n+1}$ - $\mathrm {DP}$ , for some i ( $1 \leq i \leq n$ ), we have $T \vdash \Box \varphi _i$ .

2. $(\Rightarrow )$ : Let $\varphi $ and $\psi $ be any $\Delta (\mathrm {B})$ sentences such that $T \vdash \varphi \lor \psi $ . By Proposition 3.11, there exist sentences $\varphi _0, \ldots , \varphi _{k-1}$ and $\psi _0, \ldots , \psi _{l-1}$ such that $T \vdash \varphi \leftrightarrow \bigvee _{i < k} \Box \varphi _i$ and ${T \vdash \psi \leftrightarrow \bigvee _{j < l} \Box \psi _j}$ . Then, $T \vdash \bigvee _{i < k} \Box \varphi _i \lor \bigvee _{j < l} \Box \psi _j$ . If $k = 0$ or $l = 0$ , then we easily obtain $T \vdash \varphi $ or ${T \vdash \psi} $ . Thus, we may assume both $k$ and l are larger than  $0$ . Then, $k+l \geq 2$ . By $\mathrm {B}^{k+l}$ - $\mathrm {DP}$ , there exists $i < k$ or $j < l$ such that $T \vdash \Box \varphi _i$ or ${T \vdash \Box \psi _j}$ . Then, we obtain that $T \vdash \varphi $ or $T \vdash \psi $ .

$(\Leftarrow )$ : We prove this implication by induction on $n \geq 2$ . Since $\mathrm {B} \subseteq \Delta (\mathrm {B})$ , T has $\mathrm {B}^2$ - $\mathrm {DP}$ . Suppose that T has $\mathrm {B}^n$ - $\mathrm {DP}$ and we would like to prove that T also has $\mathrm {B}^{n+1}$ - $\mathrm {DP}$ . Let $\varphi _1, \ldots , \varphi _n, \varphi _{n+1}$ be any sentences such that $T \vdash \Box \varphi _1 \lor \cdots \lor \Box \varphi _n \lor \Box \varphi _{n+1}$ . Since both $\Box \varphi _1 \lor \cdots \lor \Box \varphi _n$ and $\Box \varphi _{n+1}$ are $\Delta (\mathrm {B})$ sentences, we have $T \vdash \Box \varphi _1 \lor \cdots \lor \Box \varphi _n$ or $T \vdash \Box \varphi _{n+1}$ by $\Delta (\mathrm {B})$ - $\mathrm {DP}$ . In the former case, we obtain $T \vdash \Box \varphi _i$ for some i ( $1 \leq i \leq n$ ) by the induction hypothesis. We have proved that T has $\mathrm {B}^{n+1}$ - $\mathrm {DP}$ .

Proof. We only give a proof of Clause 1 for $\mathrm {MEP}$ and $\mathrm {MDP}$ . Let $\varphi $ and $\psi $ be any sentences such that $T \vdash \Box \varphi \lor \Box \psi $ . Then, $T \vdash \exists x \Box \bigl ((x = 0 \land \varphi ) \lor (x \neq 0 \land \psi ) \bigr )$ . By $\mathrm {MEP}$ , there exists a natural number $n$ such that $T \vdash (\overline {n} = 0 \land \varphi ) \lor (\overline {n} \neq 0 \land \psi )$ . If $n=0$ , $T \vdash \varphi $ ; if $n \neq 0$ , $T \vdash \psi $ . Therefore, T has $\mathrm {MDP}$ .

Proof. Suppose $T \vdash \Box \varphi _1 \lor \cdots \lor \Box \varphi _n \lor \sigma $ and $T \nvdash \sigma $ , and we would like to show $T \vdash \Box \varphi _i$ for some i. We may assume that $\sigma $ is of the form $\exists x \delta (x)$ for some $\Delta _0$ formula $\delta (x)$ . Then, $\mathbb {N} \models \forall x \neg \delta (x)$ because $T \nvdash \sigma $ . By the Fixed Point Lemma, for each i with $1 \leq i \leq n$ , let $\psi _i^0$ and $\psi _i^1$ be $\Sigma _1$ sentences satisfying the following equivalences:

• • $\mathbf {PA} \vdash \psi _i^0 \leftrightarrow \exists x \Bigl ( \bigl (\delta (x) \lor \mathrm {Prf}_T(\ulcorner \Box \psi _i^1\urcorner , x) \bigr ) \land \forall y < x \, \neg \mathrm {Prf}_T(\ulcorner \Box (\varphi _i \lor \psi _i^0)\urcorner , y) \Bigr )$ ,

• • $\mathbf {PA} \vdash \psi _i^1 \phantom{\quad}\leftrightarrow \exists y \Bigl (\mathrm {Prf}_T(\ulcorner \Box (\varphi _i \lor \psi _i^0)\urcorner , y) \land \forall x \leq y \, \bigl (\neg \delta (x) \land \neg \mathrm {Prf}_T (\ulcorner \Box \psi _i^1\urcorner , x) \bigr ) \Bigr )$ .

Then, for each i, we get $\mathbf {PA} \vdash \sigma \to \psi _i^0 \lor \psi _i^1$ . Hence, we have

$$\begin{align*}\mathbf{PA} \vdash \sigma \to \psi_1^0 \lor \cdots \lor \psi_n^0 \lor (\psi_1^1 \land \cdots \land \psi_n^1). \end{align*}$$

By Theorem 2.8,

$$\begin{align*}\mathbf{PA}(\mathbf{K}) \vdash \sigma \to \Box \psi_1^0 \lor \cdots \lor \Box \psi_n^0 \lor \Box (\psi_1^1 \land \cdots \land \psi_n^1). \end{align*}$$

Hence,

(2) $$ \begin{align} \mathbf{PA}(\mathbf{K}) \vdash \sigma \to \Box (\varphi_1 \lor \psi_1^0) \lor \cdots \lor \Box (\varphi_n \lor \psi_n^0) \lor \Box (\psi_1^1 \land \cdots \land \psi_n^1). \end{align} $$

On the other hand, for each i, we have $\mathbf {PA}(\mathbf {K}) \vdash \Box \varphi _i \to \Box (\varphi _i \lor \psi _i^0)$ . From our supposition, we obtain

$$\begin{align*}T \vdash \Box (\varphi_1 \lor \psi_1^0) \lor \cdots \lor \Box (\varphi_n \lor \psi_n^0) \lor \sigma. \end{align*}$$

By combining this with (2),

$$\begin{align*}T \vdash \Box (\varphi_1 \lor \psi_1^0) \lor \cdots \lor \Box (\varphi_n \lor \psi_n^0) \lor \Box (\psi_1^1 \land \cdots \land \psi_n^1). \end{align*}$$

By $\mathrm {B}^{n+1}$ - $\mathrm {DP}$ , we have $T \vdash \Box (\varphi _i \lor \psi _i^0)$ for some i or $T \vdash \Box (\psi _1^1 \land \cdots \land \psi _n^1)$ . If $T \vdash \Box (\psi _1^1 \land \cdots \land \psi _n^1)$ , then $T \vdash \Box \psi _i^1$ for each i.

• • If $T \vdash \Box (\varphi _i \lor \psi _i^0)$ and $T \nvdash \Box \psi _i^1$ , then $\mathbb {N} \models \psi _i^1$ by the choice of $\psi _i^1$ because $\mathbb {N} \models \forall x \neg \delta (x)$ . Thus, $T \vdash \psi _i^1$ by $\Sigma _1$ -completeness, and hence $T \vdash \Box \psi _i^1$ . This is a contradiction.

• • If $T \vdash \Box \psi _i^1$ and $T \nvdash \Box (\varphi _i \lor \psi _i^0)$ , then $\mathbb {N} \models \psi _i^0$ , and hence $T \vdash \psi _i^0$ . Thus, $T \vdash \varphi _i \lor \psi _i^0$ and hence $T \vdash \Box (\varphi _i \lor \psi _i^0)$ , a contradiction.

We have shown that in either case, for some i, both $\Box (\varphi _i \lor \psi _i^0)$ and $\Box \psi _i^1$ are provable in T. Since $\mathbf {PA} \vdash \psi _i^1 \to \neg \psi _i^0$ , we have $T \vdash \Box \neg \psi _i^0$ for such an i. Therefore, we conclude $T \vdash \Box \varphi _i$ .

Proof. We prove the contrapositive. Suppose that $T \nvdash \Box \bot $ and T is not $\Sigma _1$ -sound. Then, there exists a $\Delta _0$ formula $\delta (x)$ such that $T \vdash \exists x \delta (x)$ and $\mathbb {N} \models \forall x \neg \delta (x)$ . Let $\sigma _0$ and $\sigma _1$ be $\Sigma _1$ sentences satisfying the following equivalences:

• • $\mathbf {PA} \vdash \sigma _0 \leftrightarrow \exists x \Bigl ( \bigl (\delta (x) \lor \mathrm {Prf}_T(\ulcorner \sigma _1\urcorner , x) \bigr ) \land \forall y < x \, \neg \mathrm {Prf}_T(\ulcorner \Box \sigma _0\urcorner , y) \Bigr )$ .

• • $\mathbf {PA} \vdash \sigma _1 \leftrightarrow \exists y \Bigl (\mathrm {Prf}_T(\ulcorner \Box \sigma _0\urcorner , y) \land \forall x \leq y \, \bigl (\neg \delta (x) \land \neg \mathrm {Prf}_T(\ulcorner \sigma _1\urcorner , x) \bigr ) \Bigr )$ .

Since $T \vdash \exists x \delta (x)$ , we have $T \vdash \sigma _0 \lor \sigma _1$ . Therefore, $T \vdash (\Box \sigma _0) \lor \sigma _1$ by Theorem 2.8.

Suppose, towards a contradiction, that $T \vdash \Box \sigma _0$ or $T \vdash \sigma _1$ . Let p be the smallest T-proof of $\Box \sigma _0$ or $\sigma _1$ . If p is a proof of $\Box \sigma _0$ , then $\mathbb {N} \models \sigma _1$ by the choice of $\sigma _1$ . Hence, $T \vdash \sigma _1$ and thus $T \vdash \Box \sigma _1$ . Since $T \vdash \sigma _0 \land \sigma _1 \to \bot $ , we have $T \vdash \Box \bot $ because $T \vdash \Box \sigma _0 \land \Box \sigma _1$ . This is a contradiction. If p is a proof of $\sigma _1$ , then it is shown $T \vdash \sigma _0$ . This contradicts the consistency of T. Thus, we have shown that $T \nvdash \Box \sigma _0$ and $T \nvdash \sigma _1$ . This means that T does not have $(\mathrm {B}, \Sigma _1)$ - $\mathrm {DP}$ .

Proof. Suppose that T has $(\Gamma , \Sigma _1)$ - $\mathrm {DP}$ . Let $\varphi $ be any $\Gamma $ sentence such that $T \vdash \varphi \lor \mathrm {Pr}_T(\ulcorner \varphi \urcorner )$ . By $(\Gamma , \Sigma _1)$ - $\mathrm {DP}$ , $T \vdash \varphi $ or $T \vdash \mathrm {Pr}_T(\ulcorner \varphi \urcorner )$ . Since $\mathrm {B} \subseteq \Gamma $ , by Proposition 4.21, T is $\Sigma _1$ -sound. Thus, in either case, we obtain $T \vdash \varphi $ .

Proof. We prove only Clause 1. Clause 2 is proved similarly. Suppose that T is $\Delta (\mathrm {B})$ - $\mathrm {DC}$ . Let $\varphi $ be any $\Delta (\mathrm {B})$ sentence and let $\delta (x)$ be any $\Delta _0$ formula such that $T \vdash \varphi \lor \exists x \delta (x)$ and $T \nvdash \exists x \delta (x)$ . We would like to show $T \vdash \varphi $ . In this case, $\mathbb {N} \models \forall x \neg \delta (x)$ . By Proposition 3.11, we may assume that $\varphi $ is of the form $\Box \psi _0 \lor \cdots \lor \Box \psi _{k-1}$ . By the Fixed Point Lemma, let $\xi _0, \ldots , \xi _{k-1}$ be $\mathcal {L}_A(\Box )$ -sentences satisfying the following equivalences for all $i < k$ :

$$\begin{align*}\mathbf{PA}_{\Box} \vdash \xi_i \leftrightarrow \Bigl[\psi_i \lor \exists x \bigl(\delta(x) \land \forall y < x \, \neg \mathrm{Prf}_T(\ulcorner\Box \xi_0 \lor \cdots \lor \Box \xi_{k-1}\urcorner, y) \bigr)\Bigr]. \end{align*}$$

Since $\mathbf {PA}_{\Box } \vdash \psi _i \to \xi _i$ , we have $\mathbf {PA}(\mathbf {K}) \vdash \Box \psi _i \to \Box \xi _i$ . Also,

$$ \begin{align*} \mathbf{PA}(\mathbf{K}) \vdash \exists x \delta(x) \land & \neg \mathrm{Pr}_T(\ulcorner\Box \xi_0 \lor \cdots \lor \Box \xi_{k-1}\urcorner) \\ & \ \ \ \to \exists x \bigl(\delta(x) \land \forall y < x \, \neg \mathrm{Prf}_T(\ulcorner\Box \xi_0 \lor \cdots \lor \Box \xi_{k-1}\urcorner, y) \bigr), \\ & \ \ \ \to \mathrm{Pr}_T \Bigl(\ulcorner\exists x \bigl(\delta(x) \land \forall y < x \, \neg \mathrm{Prf}_T(\ulcorner\Box \xi_0 \lor \cdots \lor \Box \xi_{k-1}\urcorner, y) \bigr)\urcorner \Bigr), \\ & \ \ \ \to \mathrm{Pr}_T(\ulcorner\xi_i\urcorner). \end{align*} $$

Since $\mathbf {PA}(\mathbf {K}) \vdash \mathrm {Pr}_T(\ulcorner \xi _i\urcorner ) \to \mathrm {Pr}_T(\ulcorner \Box \xi _i\urcorner )$ because $\mathbf {PA}$ can prove that the consequences of T are closed under the rule Nec, we obtain $\mathbf {PA}(\mathbf {K}) \vdash \mathrm {Pr}_T(\ulcorner \xi _i\urcorner ) \to \mathrm {Pr}_T(\ulcorner \Box \xi _0 \lor \cdots \lor \Box \xi _{k-1}\urcorner )$ . Thus, we have

$$\begin{align*}\mathbf{PA}(\mathbf{K}) \vdash \bigl[\exists x \delta(x) \land \neg \mathrm{Pr}_T(\ulcorner\Box \xi_0 \lor \cdots \lor \Box \xi_{k-1}\urcorner) \bigr] \to \mathrm{Pr}_T(\ulcorner\Box \xi_0 \lor \cdots \lor \Box \xi_{k-1}\urcorner), \end{align*}$$

and hence

$$\begin{align*}\mathbf{PA}(\mathbf{K}) \vdash \exists x \delta(x) \to \mathrm{Pr}_T(\ulcorner\Box \xi_0 \lor \cdots \lor \Box \xi_{k-1}\urcorner). \end{align*}$$

Then, by combining this with our assumption that $T \vdash \Box \psi _0 \lor \cdots \lor \Box \psi _{k-1} \lor \exists x \delta (x)$ , we obtain

$$\begin{align*}T \vdash \Box \xi_0 \lor \cdots \lor \Box \xi_{k-1} \lor \mathrm{Pr}_T(\ulcorner\Box \xi_0 \lor \cdots \lor \Box \xi_{k-1}\urcorner). \end{align*}$$

By $\Delta (\mathrm {B})$ - $\mathrm {DC}$ , we have

(3) $$ \begin{align} T \vdash \Box \xi_0 \lor \cdots \lor \Box \xi_{k-1}. \end{align} $$

Since

$$\begin{align*}\mathbb{N} \models \exists y \bigl(\mathrm{Prf}_T(\ulcorner\Box \xi_0 \lor \cdots \lor \Box \xi_{k-1}\urcorner, y) \land \forall x \leq y \, \neg \delta(x) \bigr), \end{align*}$$

this sentence is provable in $\mathbf {PA}(\mathbf {K})$ . Thus,

$$\begin{align*}\mathbf{PA}(\mathbf{K}) \vdash \neg \exists x \bigl(\delta(x) \land \forall y < x \, \neg \mathrm{Prf}_T(\ulcorner\Box \xi_0 \lor \cdots \lor \Box \xi_{k-1}\urcorner, y) \bigr). \end{align*}$$

Then, by the choice of $\xi _i$ , $\mathbf {PA}(\mathbf {K}) \vdash \xi _i \to \psi _i$ for each i. From (3), we conclude $T \vdash \Box \psi _0 \lor \cdots \lor \Box \psi _{k-1}$ and hence $T \vdash \varphi $ .

Proof. $(1 \Rightarrow 2)$ : Suppose that T is $\Delta (\mathrm {B})$ - $\mathrm {DC}$ . Since $T \nvdash \bot $ , we obtain $T \nvdash \mathrm {Pr}_T(\ulcorner \bot \urcorner ) \lor \bot $ . Hence, $T \nvdash \neg \mathrm {Con}_T$ .

$(2 \Rightarrow 1)$ : Suppose $T \nvdash \neg \mathrm {Con}_T$ . Let $\varphi $ be any $\Delta (\mathrm {B})$ sentence with $T \vdash \mathrm {Pr}_T(\ulcorner \varphi \urcorner ) \lor \varphi $ . If $T \vdash \neg \varphi $ , then $\varphi $ is T-equivalent to $\bot $ . We have $T \vdash \mathrm {Pr}_T(\ulcorner \bot \urcorner ) \lor \bot $ , and so $T \vdash \neg \mathrm {Con}_T$ . This is a contradiction. Therefore, $T \vdash \varphi $ .

Proof. 1. Let $\varphi $ be a $\Pi _1$ Gödel sentence of $\mathbf {PA}$ . Since $\mathbf {PA} \vdash \varphi \lor \neg \varphi $ , we have $\mathbf {PA}(\mathbf {Triv}) \vdash \Box \varphi \lor \neg \varphi $ . Since $\mathbf {PA}(\mathbf {Triv})$ is a conservative extension of $\mathbf {PA}$ (Corollary 2.4), $\mathbf {PA}(\mathbf {Triv}) \nvdash \varphi $ and $\mathbf {PA}(\mathbf {Triv}) \nvdash \neg \varphi $ . Then, $\mathbf {PA}(\mathbf {Triv}) \nvdash \Box \varphi $ and $\mathbf {PA}(\mathbf {Triv}) \nvdash \neg \varphi $ .

2. Since U is a subtheory of $\mathbf {PA}(\mathbf {Verum})$ , U is $\mathcal {L}_A$ -sound by Corollary 2.7. Since $U \vdash \mathrm {Pr}_{T}(\ulcorner \Box \bot \urcorner ) \lor \Box \bot $ , we have $U \vdash \mathrm {Pr}_U(\ulcorner \Box \bot \urcorner ) \lor \Box \bot $ . Suppose, towards a contradiction, $U \vdash \Box \bot $ . Since $\mathrm {Pr}_{T}(\ulcorner \Box \bot \urcorner ) \lor \Box \bot $ is a $\Sigma (\mathrm {B})$ sentence, $T \vdash \mathrm {Pr}_{T}(\ulcorner \Box \bot \urcorner ) \lor \Box \bot \to \Box \bot $ by the $\Sigma (\mathrm {B})$ -deduction theorem (Corollary 3.14). In particular, $T \vdash \mathrm {Pr}_{T}(\ulcorner \Box \bot \urcorner ) \to \Box \bot $ . By Löb’s theorem, $T \vdash \Box \bot $ . This is a contradiction. Therefore, $U \nvdash \Box \bot $ . Hence, U is not $\mathrm {B}$ - $\mathrm {DC}$ .

Proof. Since every $\Sigma (\mathrm {B})$ (resp. $\Delta (\mathrm {B})$ ) formula is T-provably equivalent to some $\Sigma _1$ (resp. $\Delta _0$ ) formula, we have $(2 \Leftrightarrow 3)$ . Also by Guaspari’s theorem [Reference Guaspari10] on the equivalence of the $\Sigma _1$ -soundness and $\Sigma _1$ - $\mathrm {DP}$ , the equivalence $(1 \Leftrightarrow 2)$ holds. Moreover, since the implications “ $\Sigma _1$ -sound $\Rightarrow \Sigma _1$ - $\mathrm {EP}$ ,” “ $\Sigma _1$ - $\mathrm {EP} \Rightarrow \Delta _0$ - $\mathrm {EP}$ ,” and “ $\Delta _0$ - $\mathrm {EP} \Rightarrow \Sigma _1$ -sound” are easily verified, we obtain that Clauses 1, 4, and 5 are pairwise equivalent. Finally, since the equivalence of the $\Sigma _1$ -soundness and $\Sigma _1$ - $\mathrm {DC}$ is shown in [Reference Kurahashi15], we get $(1 \Leftrightarrow 6)$ .

Proof. Since $\mathbf {PA}(\mathbf {Verum})$ is $\Sigma _1$ -sound by Corollary 2.7, $\mathbf {PA}(\mathbf {Verum})$ has $\Sigma (\mathrm {B})$ - $\mathrm {EP}$ . On the other hand, $\mathbf {PA}(\mathbf {Verum}) \vdash \Box \bot $ and $\mathbf {PA}(\mathbf {Verum}) \nvdash \bot $ , and thus $\mathbf {PA}(\mathbf {Verum})$ does not have $\mathrm {MDP}$ .

Proof. Suppose that T is $\Sigma (\mathrm {B})$ - $\mathrm {DC}$ . Let $\varphi $ be any $\Sigma (\mathrm {B})$ sentence and let $\delta (x)$ be any $\Delta _0$ formula such that $T \vdash \varphi \lor \exists x \delta (x)$ and $T \nvdash \exists x \delta (x)$ . We would like to show $T \vdash \varphi $ . In this case, $\mathbb {N} \models \forall x \neg \delta (x)$ . Let $\sigma $ be a $\Sigma _1$ sentence satisfying

(4) $$ \begin{align} \mathbf{PA} \vdash \sigma \leftrightarrow \exists x \bigl(\delta(x) \land \forall y < x \, \neg \mathrm{Prf}_T(\ulcorner\varphi \lor \sigma\urcorner, y) \bigr). \end{align} $$

Since T is an extension of $\mathbf {PA}$ and $\sigma $ is $\Sigma _1$ , we have $\mathbf {PA} \vdash \sigma \to \mathrm {Pr}_T(\ulcorner \sigma \urcorner )$ , and hence $\mathbf {PA} \vdash \sigma \to \mathrm {Pr}_T(\ulcorner \varphi \lor \sigma \urcorner )$ . By the equivalence (4), we obtain

$$\begin{align*}\mathbf{PA} \vdash \exists x \delta(x) \land \neg \mathrm{Prf}_T(\ulcorner\varphi \lor \sigma\urcorner) \to \sigma. \end{align*}$$

It follows $\mathbf {PA} \vdash \exists x \delta (x) \land \neg \mathrm {Prf}_T(\ulcorner \varphi \lor \sigma \urcorner ) \to \mathrm {Pr}_T(\ulcorner \varphi \lor \sigma \urcorner )$ , and hence

$$\begin{align*}\mathbf{PA} \vdash \exists x \delta(x) \to \mathrm{Prf}_T(\ulcorner\varphi \lor \sigma\urcorner). \end{align*}$$

Since $T \vdash \varphi \lor \exists x \delta (x)$ , we obtain $T \vdash (\varphi \lor \sigma ) \lor \mathrm {Pr}_T(\ulcorner \varphi \lor \sigma \urcorner )$ . Since $\varphi \lor \sigma $ is a $\Sigma (\mathrm {B})$ sentence, by $\Sigma (\mathrm {B})$ - $\mathrm {DC}$ , we have $T \vdash \varphi \lor \sigma $ . Since $\mathbb {N} \models \forall x \neg \delta (x)$ , $\mathbb {N} \models \exists y \bigl (\mathrm {Prf}_T(\ulcorner \varphi \lor \sigma \urcorner , y) \land \forall x \leq y \, \neg \delta (x) \bigr )$ and this is provable in T. Then, $T \vdash \neg \sigma $ , and thus $T \vdash \varphi $ .

Proof. This lemma is proved by induction on the construction of $\varphi $ as in the proof of Theorem 3.13. Notice that if $\varphi $ is of the form $\Box \psi $ , then $\varphi ^- \equiv \psi $ and thus $\mathbf {PA}(\mathbf {K}) \vdash \varphi \to \Box (\varphi ^-)$ holds.