A note on derivability conditions

TL;DR

This paper analyzes various derivability conditions for provability predicates, clarifies their logical relationships, and explores their implications for the second incompleteness theorem and related consistency statements.

Contribution

It classifies known and new derivability conditions, clarifies their implications, and improves proof techniques for provable $oldsymbol{ extSigma_1}$-completeness.

Findings

Hilbert--Bernays' and L"ob's conditions are mutually incomparable.

Neither Hilbert--Bernays' nor L"ob's conditions suffice for G"odel's original second incompleteness theorem.

New sets of conditions are identified that ensure unprovability of Hilbert--Bernays' consistency statement.

Abstract

We investigate relationships between versions of derivability conditions for provability predicates. We show several implications and non-implications between the conditions, and we discuss unprovability of consistency statements induced by derivability conditions. First, we classify already known versions of the second incompleteness theorem, and exhibit some new sets of conditions which are sufficient for unprovability of Hilbert--Bernays' consistency statement. Secondly, we improve Buchholz's schematic proof of provable $\Sigma_1$-completeness. Then among other things, we show that Hilbert--Bernays' conditions and L\"ob's conditions are mutually incomparable. We also show that neither Hilbert--Bernays' conditions nor L\"ob's conditions accomplish G\"odel's original statement of the second incompleteness theorem.

Equations

$$S⊢\neg \phi \to \forall x\Phi (┌\delta (\dot{x})┐).$$

$$S⊢\neg \phi \to \exists x(\Phi (┌\delta (\dot{x})┐)\wedge \Phi (┌\neg \delta (\dot{x})┐)).$$

$$S⊢\forall x({\Sigma }_n(x)\wedge {\mathrm{Pr}}_{\varnothing }(x)\to \Phi (┌{\mathsf{True}}_{{\Sigma }_n}(\dot{x})┐)).$$

$$S⊢\Phi (┌\phi (\vec{\dot{x}})┐)\leftrightarrow \Phi (┌\psi (\vec{\dot{x}})┐).$$

$$\mathsf{PA}⊢┌\phi (\vec{\dot{y}},\dot{v})┐[\mathsf{s}(x)/v]=┌\phi (\vec{\dot{y}},\mathsf{s}(\dot{x}))┐,$$

$$S⊢\underset{i\le k}{\bigwedge }(z_i=x_i)\to \Phi \left(┌\underset{i\le k}{\bigwedge }({\dot{z}}_i={\dot{x}}_i)┐\right).$$

$$S⊢\Phi \left(┌\underset{i\le k}{\bigwedge }({\dot{z}}_i={\dot{z}}_i)┐\right)$$

$$\mathsf{PA}⊢\underset{i\le k}{\bigwedge }(z_i=x_i)\to \left(\Phi \left(┌\underset{i\le k}{\bigwedge }({\dot{v}}_i={\dot{z}}_i)┐\right)\to \Phi \left(┌\underset{i\le k}{\bigwedge }({\dot{v}}_i={\dot{x}}_i)┐\right)\right).$$

$$\mathsf{PA}⊢\underset{i\le k}{\bigwedge }(z_i=x_i)\to \left(\Phi \left(┌\underset{i\le k}{\bigwedge }({\dot{z}}_i={\dot{z}}_i)┐\right)\to \Phi \left(┌\underset{i\le k}{\bigwedge }({\dot{z}}_i={\dot{x}}_i)┐\right)\right).$$

$$S⊢\underset{i\le k}{\bigwedge }(z_i=x_i)\to \Phi \left(┌\underset{i\le k}{\bigwedge }({\dot{z}}_i={\dot{x}}_i)┐\right).$$

$$S⊢\underset{i\le k}{\bigwedge }(z_i=t_i(\vec{x}))\to \Phi \left(┌\underset{i\le k}{\bigwedge }({\dot{z}}_i=t_i(\vec{\dot{x}}))┐\right).$$

$$S⊢\xi (\vec{v})\wedge z_k=y\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\dot{y}┐).$$

$$S⊢\xi (\vec{v})\wedge z_k=0\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\dot{y}┐)[0/y].$$

$$S⊢\xi (\vec{v})\wedge z_k=0\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=0┐).$$

$$S⊢\xi (\vec{v})\wedge z_k=y\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\dot{y}┐).$$

$$S⊢\xi (\vec{v})\wedge z_k=\mathsf{s}(x)\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\dot{y}┐)[\mathsf{s}(x)/y].$$

$$S⊢\xi (\vec{v})\wedge z_k=\mathsf{s}(x)\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\mathsf{s}(\dot{x})┐).$$

$$\forall x(\xi (\vec{v})\wedge z_k=x+y\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\dot{x}+\dot{y}┐)).$$

$$S⊢\xi (\vec{v})\wedge z_k=x\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\dot{x}┐).$$

$$S⊢\xi (\vec{v})\wedge z_k=x+0\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\dot{x}+0┐).$$

$$\mathsf{PA}⊢\phi (y)\wedge \xi (\vec{v})\wedge z_k=\mathsf{s}(x)+y\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\mathsf{s}(\dot{x})+\dot{y}┐).$$

$$S⊢\phi (y)\wedge \xi (\vec{v})\wedge z_k=x+\mathsf{s}(y)\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\dot{x}+\mathsf{s}(\dot{y})┐).$$

$$\forall w(\xi (\vec{v})\wedge z_k=x\times y+w\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\dot{x}\times \dot{y}+\dot{w}┐)).$$

$$S⊢\xi (\vec{v})\wedge z_k=w\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\dot{w}┐).$$

$$S⊢\xi (\vec{v})\wedge z_k=x\times 0+w\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\dot{x}\times 0+\dot{w}┐)$$

$$\forall u(\xi (\vec{v})\wedge z_k=x\times y+(u+w)\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\dot{x}\times \dot{y}+(\dot{u}+\dot{w})┐)).$$

$$S⊢\psi (y)\wedge \xi (\vec{v})\wedge z_k=x\times y+(x+w)\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\dot{x}\times \dot{y}+(\dot{x}+\dot{w})┐).$$

$$S⊢\psi (y)\wedge \xi (\vec{v})\wedge z_k=x\times \mathsf{s}(y)+w\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\dot{x}\times \mathsf{s}(\dot{y})+\dot{w}┐)$$

$$S⊢\xi (\vec{v})\wedge z_k=x\times y+0\to \Phi (┌\xi (\vec{\dot{v}})\wedge {\dot{z}}_k=\dot{x}\times \dot{y}+0┐).$$

$$S⊢\underset{i\le k}{\bigwedge }(z_i=t_i(\vec{x}))\to \Phi \left(┌\underset{i\le k}{\bigwedge }({\dot{z}}_i=t_i(\vec{\dot{x}}))┐\right).$$

Full text

1 Introduction

In his famous paper [8], Gödel proved the second incompleteness theorem with only a sketched proof. Gödel explained that by formalizing his proof of the first incompleteness theorem, the consistency statement $\exists x(\mathsf{Fml}(x)\land\neg\mathrm{Pr}_{T}(x))$ saying “there exists a $T$-unprovable formula” cannot be proved in $T$ if $T$ is consistent. To carry out his idea, it is desirable that the formula $\mathrm{Pr}_{T}(x)$ enjoys some natural properties as a formalization of the notion of $T$-provability. He wrote that a detailed proof would be presented in a forthcoming work, but such a paper was not published after all.

The first detailed proof of the second incompleteness theorem was presented in the second volume of Grundlagen der Mathematik [10] by Hilbert and Bernays. Especially they formulated a set of conditions for provability predicates which is sufficient for the second incompleteness theorem. Let $\mathrm{Pr}_{T}(x)$ be some $\Sigma_{1}$ provability predicate of $T$. They proved that if $\mathrm{Pr}_{T}(x)$ satisfies the following conditions $\mathbf{HB1}$, $\mathbf{HB2}$ and $\mathbf{HB3}$111More precisely, Hilbert–Bernays’ conditions were originally stated on proof predicate $\mathfrak{B}(x,y)$ rather than on provability predicate $\mathrm{Pr}_{T}(x)$. For instance, the original statement of $\mathbf{HB1}$ is: If a formula with the number $j$ is derived from a formula with the number $i$, then $\exists x\mathfrak{B}(x,i)\to\exists x\mathfrak{B}(x,j)$ is provable. , then the consistency statement $\forall x(\mathsf{Fml}(x)\land\mathrm{Pr}_{T}(x)\to\neg\mathrm{Pr}_{T}(\dot{\neg}x))$ cannot be proved in $T$ if $T$ is consistent.

$\mathbf{HB1}$

If $T\vdash\varphi\to\psi$, then $T\vdash\mathrm{Pr}_{T}(\ulcorner\varphi\urcorner)\to\mathrm{Pr}_{T}(\ulcorner\psi\urcorner)$.

$\mathbf{HB2}$

$T\vdash\mathrm{Pr}_{T}(\ulcorner\neg\varphi(x)\urcorner)\to\mathrm{Pr}_{T}(\ulcorner\neg\varphi(\dot{x})\urcorner)$.

$\mathbf{HB3}$

$T\vdash f(x)=0\to\mathrm{Pr}_{T}(\ulcorner f(\dot{x})=0\urcorner)$ for every primitive recursive term $f(x)$.

Here $\ulcorner\varphi(\dot{x})\urcorner$ is a primitive recursive term corresponding to a function calculating the Gödel number of the formula $\varphi(\overline{n})$ from $n$, where $\overline{n}$ is the numeral for $n$. These conditions are called the Hilbert–Bernays derivability conditions.

Löb [18] proved that if $\mathrm{Pr}_{T}(x)$ satisfies the following conditions $\mathbf{D1}$, $\mathbf{D2}$ and $\mathbf{D3}$, then Löb’s theorem holds, that is, for any formula $\varphi$, if $T\vdash\mathrm{Pr}_{T}(\ulcorner\varphi\urcorner)\to\varphi$, then $T\vdash\varphi$.

$\mathbf{D1}$

If $T\vdash\varphi$, then $T\vdash\mathrm{Pr}_{T}(\ulcorner\varphi\urcorner)$.

$\mathbf{D2}$

$T\vdash\mathrm{Pr}_{T}(\ulcorner\varphi\to\psi\urcorner)\to(\mathrm{Pr}_{T}(\ulcorner\varphi\urcorner)\to\mathrm{Pr}_{T}(\ulcorner\psi\urcorner))$.

$\mathbf{D3}$

$T\vdash\mathrm{Pr}_{T}(\ulcorner\varphi\urcorner)\to\mathrm{Pr}_{T}(\ulcorner\mathrm{Pr}_{T}(\ulcorner\varphi\urcorner)\urcorner)$.

Note that every provability predicate automatically satisfies $\mathbf{D1}$. The conditions $\mathbf{D1}$ and $\mathbf{D2}$ were established by Hilbert and Bernays, and the condition $\mathbf{D3}$ was introduced by Löb. The conditions $\mathbf{D1}$, $\mathbf{D2}$ and $\mathbf{D3}$ are nowadays called the Hilbert–Bernays–Löb derivability conditions which are well-known as sufficient conditions for a proof of the second incompleteness theorem. In fact, if $T$ is consistent, then the unprovability of the consistency statement $\neg\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)$ in $T$ is an immediate corollary of Löb’s theorem. The Hilbert–Bernays–Löb derivability conditions together with Löb’s theorem are basis for modal logical investigations of provability predicates (see [2, 5, 12, 22]).

Other sufficient conditions for the second incompleteness theorem were formulated by authors such as Jeroslow, Montagna and Buchholz. Jeroslow [13] proved that the following condition which is a variant of $\mathbf{D3}$ implies the unprovability of $\forall x(\mathsf{Fml}(x)\land\mathrm{Pr}_{T}(x)\to\neg\mathrm{Pr}_{T}(\dot{\neg}x))$.

• •

$T\vdash\mathrm{Pr}_{T}(t)\to\mathrm{Pr}_{T}(\ulcorner\mathrm{Pr}_{T}(t)\urcorner)$ for every primitive recursive term $t$.

Notice that $\mathbf{D3}$ and Jeroslow’s condition are instances of the following provable $\Sigma_{1}$-completeness because $\mathrm{Pr}_{T}(x)$ is $\Sigma_{1}$.

$\mathbf{\Sigma_{1}C}$

If $\varphi$ is a $\Sigma_{1}$ sentence, then $T\vdash\varphi\to\mathrm{Pr}_{T}(\ulcorner\varphi\urcorner)$.

Montagna [19] proved that the following two conditions are sufficient for Löb’s theorem.

• •

$T\vdash\forall x($“$x$ is a logical axiom” $\to\mathrm{Pr}_{T}(x))$.

• •

$T\vdash\forall x\forall y(\mathsf{Fml}(x)\land\mathsf{Fml}(y)\to(\mathrm{Pr}_{T}(x\dot{\to}y)\to(\mathrm{Pr}_{T}(x)\to\mathrm{Pr}_{T}(y))))$.

By Montagna’s argument, we can conclude that these two conditions imply the unprovability of $\exists x(\mathsf{Fml}(x)\land\neg\mathrm{Pr}_{T}(x))$.

At last, in Buchholz’s lecture note [6], the following condition was introduced and it was proved that this condition implies $\mathbf{D2}$ and $\mathbf{\Sigma_{1}C}$.

• •

For all $m\geq 1$,

if $T\vdash\forall\vec{x}(\varphi_{1}(\vec{x})\to(\varphi_{2}(\vec{x})\to(\cdots\to(\varphi_{m-1}(\vec{x})\to\varphi_{m}(\vec{x}))\cdots)))$,

then $T\vdash\forall\vec{x}(\mathrm{Pr}_{T}(\ulcorner\varphi_{1}(\vec{\dot{x}})\urcorner)\to(\mathrm{Pr}_{T}(\ulcorner\varphi_{2}(\vec{\dot{x}})\urcorner)\to\\ \ \ \ \ \ \ \ \ \ \ \ \ \ (\cdots\to(\mathrm{Pr}_{T}(\ulcorner\varphi_{m-1}(\vec{\dot{x}})\urcorner)\to\mathrm{Pr}_{T}(\ulcorner\varphi_{m}(\vec{\dot{x}})\urcorner))\cdots)))$.

Thus Buchholz’s condition implies the unprovability of $\neg\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)$.

Roughly speaking, every set of derivability conditions introduced above is sufficient for unprovability of consistency statements, but such a rough understanding does not allow us to grasp the situation of the second incompleteness theorem accurately. Strictly speaking, these sets of sufficient conditions do not induce the same consequence because there are three different consistency statements $\mathsf{Con}^{H}\equiv\forall x(\mathsf{Fml}(x)\land\mathrm{Pr}_{T}(x)\to\neg\mathrm{Pr}_{T}(\dot{\neg}x))$, $\mathsf{Con}^{L}\equiv\neg\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)$ and $\mathsf{Con}^{G}\equiv\exists x(\mathsf{Fml}(x)\land\neg\mathrm{Pr}_{T}(x))$ in our context, and each of these sets of conditions implies the unprovability of one of these consistency statements. Here superscripts ‘H’, ‘L’ and ‘G’ stand for Hilbert–Bernays, Löb and Gödel, respectively. It is easy to see that $\mathsf{Con}^{H}$ implies $\mathsf{Con}^{L}$, and $\mathsf{Con}^{L}$ implies $\mathsf{Con}^{G}$. However the converse implications do not hold in general.

In order to clarify the situation of several versions of derivability conditions, in this paper, we investigate relationships between the conditions. The following figure shows the situation for implications between prominent sets of conditions for $\Sigma_{1}$ formulas satisfying $\mathbf{D1}$.

\nvdash\mathsf{Con}^{G}$$\nvdash\mathsf{Con}^{\Sigma_{1}}$$\nvdash\mathsf{Con}^{L}$$\nvdash\mathsf{Con}^{H}$$\mathbf{B_{2}},\mathbf{D3}$$\mathbf{\Sigma_{1}C}$$\mathbf{PC}$$\mathbf{B_{2}},\mathbf{CB},\mathbf{\Delta_{0}C^{U}}$$\mathbf{D2},\mathbf{D3}$$\mathbf{B_{2}},\mathbf{\Sigma_{1}C}$$\mathbf{D2},\mathbf{\Sigma_{1}C}$$\mathbf{B_{2}^{U}}$$\mathbf{D1^{U}},\mathbf{D2^{U}}$$\mathbf{D1^{U}},\mathbf{D2^{G}},\mathbf{\Sigma_{1}C^{G}}$$\mathbf{D2^{G}},\mathbf{\Sigma_{1}C^{G}}$$\mathbf{D2^{G}},\mathbf{PC^{G}}

In Section 2, we introduce and investigate versions of derivability conditions. Each of these conditions is classified as one of three versions of derivability conditions, namely, local version, uniform version and global version. Among other things, we show that each of two new sets $\{\mathbf{D1},\mathbf{B_{2}},\mathbf{D3}\}$ and $\{\mathbf{D1},\mathbf{PC}\}$ of derivability conditions is sufficient for the unprovability of the consistency statement $\mathsf{Con}^{H}$ (see the next section for precise definitions of these conditions). Then currently we know that four sets $\{\mathbf{B_{2}},\mathbf{CB},\mathbf{\Delta_{0}C^{U}}\}$, $\{\mathbf{D1},\mathbf{B_{2}},\mathbf{D3}\}$, $\{\mathbf{D1},\mathbf{\Sigma_{1}C}\}$ and $\{\mathbf{D1},\mathbf{PC}\}$ are sufficient for $T\nvdash\mathsf{Con}^{H}$, the set $\{\mathbf{D1},\mathbf{D2},\mathbf{D3}\}$ (Löb’s conditions) is sufficient for $T\nvdash\mathsf{Con}^{L}$, and the set $\{\mathbf{D1},\mathbf{D2^{G}},\mathbf{PC^{G}}\}$ is sufficient for $T\nvdash\mathsf{Con}^{G}$. Here $\{\mathbf{B_{2}},\mathbf{CB},\mathbf{\Delta_{0}C^{U}}\}$, $\{\mathbf{D1},\mathbf{\Sigma_{1}C}\}$ and $\{\mathbf{D1},\mathbf{D2^{G}},\mathbf{PC^{G}}\}$ correspond to Hilbert and Bernays’ conditions, Jeroslow’s conditions and Montagna’s conditions, respectively.

In Section 3, we improve Buchholz’s proof of provable $\Sigma_{1}$-completeness $\mathbf{\Sigma_{1}C}$. More precisely, we prove that if $\mathrm{Pr}_{T}(x)$ satisfies the following condition $\mathbf{B_{2}^{U}}$ which is precisely the $m=2$ case of Buchholz’s condition, then the uniform version of $\mathbf{\Sigma_{1}C}$ holds.

$\mathbf{B_{2}^{U}}$

If $\displaystyle T\vdash\forall\vec{x}\left(\varphi(\vec{x})\to\psi(\vec{x})\right)$, then $\displaystyle T\vdash\forall\vec{x}(\mathrm{Pr}_{T}(\ulcorner\varphi(\vec{\dot{x}})\urcorner)\to\mathrm{Pr}_{T}(\ulcorner\psi(\vec{\dot{x}})\urcorner))$.

In Section 4, we give some examples of formulas, and from these examples, several non-implications between conditions are obtained. For instance, from our examples, we obtain that $\{\mathbf{B_{2}},\mathbf{CB},\mathbf{\Delta_{0}C^{U}}\}$, $\{\mathbf{D1},\mathbf{B_{2}},\mathbf{D3}\}$, $\{\mathbf{D1},\mathbf{\Sigma_{1}C}\}$ and $\{\mathbf{D1},\mathbf{PC}\}$ are pairwise incomparable, and each of them is not sufficient for $T\nvdash\mathsf{Con}^{L}$. Also we obtain that $\{\mathbf{D1},\mathbf{D2},\mathbf{D3}\}$ is not comparable with each of $\{\mathbf{B_{2}},\mathbf{CB},\mathbf{\Delta_{0}C^{U}}\}$, $\{\mathbf{D1},\mathbf{\Sigma_{1}C}\}$ and $\{\mathbf{D1},\mathbf{PC}\}$, and it is not sufficient for $T\nvdash\mathsf{Con}^{G}$. Furthermore, we show that even stronger set $\{\mathbf{D1^{U}},\mathbf{D2^{G}},\mathbf{\Sigma_{1}C^{G}}\}$ is not sufficient for $T\nvdash\mathsf{Con}^{G}$. From the last observation, we can say that both of the Hilbert–Bernays derivability conditions and the Hilbert–Bernays–Löb derivability conditions do not accomplish Gödel’s original statement of the second incompleteness theorem.

2 Derivability conditions

Throughout this paper, $S$ and $T$ denote recursively axiomatized consistent extensions of Peano Arithmetic $\mathsf{PA}$ in the language of first-order arithmetic. The theory $S$ is intended as a metatheory, and we assume that $T$ is an extension of $S$. Let $\mathcal{L}_{A}$ be the language of arithmetic including $\{0,\mathsf{s},+,\times\}$, and we can freely use terms corresponding to some primitive recursive functions. The numeral $\overline{n}$ for a natural number $n$ is the closed term $\underbrace{\mathsf{s}(\mathsf{s}(\cdots\mathsf{s}}_{n\ \text{times}}(0)\cdots))$. This explicit form of numerals is used in Section 3. We fix some natural Gödel numbering, and for each $\mathcal{L}_{A}$-formula $\varphi$, let $\ulcorner\varphi\urcorner$ be the numeral for the Gödel number of $\varphi$. Let $x\dot{\to}y$ and $\dot{\neg}x$ denote primitive recursive terms such that for any formulas $\varphi$ and $\psi$, $\mathsf{PA}\vdash\ulcorner\varphi\urcorner\dot{\to}\ulcorner\psi\urcorner=\ulcorner\varphi\to\psi\urcorner$ and $\mathsf{PA}\vdash\neg\ulcorner\varphi\urcorner=\ulcorner\neg\varphi\urcorner$.

Let $\Delta_{0}=\Sigma_{0}=\Pi_{0}$ be the set of all formulas whose quantifiers are all bounded. Let $\Sigma_{n+1}$ and $\Pi_{n+1}$ ($n\geq 0$) be the least sets of formulas satisfying the following conditions:

$\Sigma_{n}\cup\Pi_{n}\subseteq\Sigma_{n+1}\cap\Pi_{n+1}$; 2. 2.

$\Sigma_{n+1}$ (resp. $\Pi_{n+1}$) is closed under conjunction, disjunction, bounded quantification, and existential (resp. universal) quantification; 3. 3.

If $\varphi$ is in $\Sigma_{n+1}$ (resp. $\Pi_{n+1}$), then $\neg\varphi$ is in $\Pi_{n+1}$ (resp. $\Sigma_{n+1}$); 4. 4.

If $\varphi$ is in $\Sigma_{n+1}$ (resp. $\Pi_{n+1}$) and $\psi$ is in $\Pi_{n+1}$ (resp. $\Sigma_{n+1}$), then $\varphi\to\psi$ is in $\Pi_{n+1}$ (resp. $\Sigma_{n+1}$).

Throughout this paper, $\Gamma$ denotes $\Sigma_{n}$ or $\Pi_{n}$ for some $n\geq 0$. We say a formula $\varphi$ is $\Gamma$ if $\varphi\in\Gamma$. A formula $\varphi$ is said to be $\Delta_{1}$ if it is provably equivalent to both some $\Sigma_{1}$ formula and some $\Pi_{1}$ formula in $\mathsf{PA}$. Let $\mathsf{Fml}(x)$, $\mathsf{Sent}(x)$ and $\Sigma_{z}(x)$ be $\Delta_{1}$ formulas saying that “$x$ is the Gödel number of an $\mathcal{L}_{A}$-formula”, “$x$ is the Gödel number of an $\mathcal{L}_{A}$-sentence” and “$x$ is the Gödel number of a $\Sigma_{z}$ formula”, respectively. We assume that $\mathsf{PA}$ can derive natural facts about these formulas such as $\forall z\exists x>z\mathsf{Fml}(x)$.

We say a formula $\mathrm{Pr}(x)$ is a provability predicate of a theory $U$ (in $\mathsf{PA}$) if it weakly represents the set of all theorems of $U$ in $\mathsf{PA}$, that is, for any natural number $n$, $\mathsf{PA}\vdash\mathrm{Pr}(\overline{n})$ if and only if $n$ is the Gödel number of some theorem of $U$. Also we say a formula $\tau(v)$ is a numeration of $U$ (in $\mathsf{PA}$) if it weakly represents the set of all axioms of $U$ in $\mathsf{PA}$, that is, for any natural number $n$, $\mathsf{PA}\vdash\tau(\overline{n})$ if and only if $n$ is the Gödel number of some axiom of $U$. For each numeration $\tau(v)$ of $U$, we can naturally construct a formula $\mathrm{Prf}_{\tau}(x,y)$ saying that “$y$ is the code of a proof of a formula with the Gödel number $x$ from the set of all sentences satisfying $\tau(v)$” (see Feferman [7]). We may assume $\mathsf{PA}\vdash\forall x\forall y(\mathrm{Prf}_{\tau}(x,y)\to x\leq y)$. If $\tau(v)$ is a $\Sigma_{n}$ numeration of $U$ for $n>0$, then the formula $\mathrm{Pr}_{\tau}(x):\equiv\exists y\mathrm{Prf}_{\tau}(x,y)$ is a $\Sigma_{n}$ provability predicate of $U$. If it is not necessary to specify a particular numeration of $U$, $\mathrm{Prf}_{U}(x,y)$ and $\mathrm{Pr}_{U}(x)$ denote $\mathrm{Prf}_{\tau}(x,y)$ and $\mathrm{Pr}_{\tau}(x)$ for some fixed numeration $\tau(v)$ of $U$, respectively.

For each finitely axiomatized theory $T_{0}$, let $[T_{0}](x)$ be the formula $\bigvee_{\varphi\in T_{0}}(x=\ulcorner\varphi\urcorner)$. Then $[T_{0}](x)$ is a numeration of $T_{0}$. Let $\bigwedge T_{0}$ be the conjunction of all axioms of $T_{0}$, and let $\mathrm{Pr}_{\emptyset}(x)$ be a natural provability predicate of first-order predicate calculus in the language $\mathcal{L}_{A}$. Then the following lemma holds (see Feferman [7]).

Lemma 2.1** (Formalized deduction theorem).**

For any finitely axiomatized theory $T_{0}$, $\mathsf{PA}\vdash\forall x(\mathrm{Pr}_{[T_{0}]}(x)\leftrightarrow\mathrm{Pr}_{\emptyset}(\ulcorner\bigwedge T_{0}\urcorner\dot{\to}x))$.

Throughout this paper, the formula $\Phi(x)$ is intended to denote some provability predicate of $T$. However, we deal with more general situations, that is, $\Phi(x)$ may not be any provability predicate of $T$. In this section, we introduce a lot of conditions for $\Phi(x)$ which are satisfied by naturally constructed provability predicates $\mathrm{Pr}_{T}(x)$. The remainder of this section is separated into three subsections, and in each of these subsections, we introduce local derivability conditions, uniform derivability conditions and global derivability conditions, respectively.

For each formula $\Phi(x)$, we define four kinds of consistency statements based on $\Phi(x)$.

Definition 2.2**.**

$\mathsf{Con}_{\Phi}^{H}:\equiv\forall x(\mathsf{Fml}(x)\land\Phi(x)\to\neg\Phi(\dot{\neg}x))$. 2. 2.

$\mathsf{Con}_{\Phi}^{L}:\equiv\neg\Phi(\ulcorner 0\neq 0\urcorner)$. 3. 3.

$\mathsf{Con}_{\Phi}^{G}:\equiv\exists x(\mathsf{Fml}(x)\land\neg\Phi(x))$. 4. 4.

$\mathsf{Con}_{\Phi}^{\Sigma_{1}}:\equiv\exists x(\Sigma_{1}(x)\land\mathsf{Sent}(x)\land\neg\Phi(x))$.

The first consistency statement $\mathsf{Con}_{\Phi}^{H}$ is adopted in Hilbert and Bernays [10] and Feferman [7]. The second sentence $\mathsf{Con}_{\Phi}^{L}$ is the most tractable one, and it is widely used in the context of modal logical investigations of provability predicates. Gödel [8] stated his second incompleteness theorem with the consistency statement $\mathsf{Con}_{\Phi}^{G}$. The last consistency statement $\mathsf{Con}_{\Phi}^{\Sigma_{1}}$ states that there exists a $T$-unprovable $\Sigma_{1}$ sentence.

2.1 Local derivability conditions

We introduce the weakest version of derivability conditions which are called local derivability conditions.

Definition 2.3** (Local derivability conditions).**

$\mathbf{D1}$

If $T\vdash\varphi$, then $S\vdash\Phi(\ulcorner\varphi\urcorner)$ for any formula $\varphi$.

$\mathbf{D2}$

$S\vdash\Phi(\ulcorner\varphi\to\psi\urcorner)\to(\Phi(\ulcorner\varphi\urcorner)\to\Phi(\ulcorner\psi\urcorner))$ for any formulas $\varphi$ and $\psi$.

$\mathbf{D3}$

$S\vdash\Phi(\ulcorner\varphi\urcorner)\to\Phi(\ulcorner\Phi(\ulcorner\varphi\urcorner)\urcorner)$ for any formula $\varphi$.

$\mathbf{\Gamma C}$

$S\vdash\varphi\to\Phi(\ulcorner\varphi\urcorner)$ for any $\Gamma$ sentence $\varphi$.

$\mathbf{B_{m}}$** ($m\geq 1$)**

If $\displaystyle T\vdash\bigwedge_{0<i<m}\varphi_{i}\to\varphi_{m}$, then $\displaystyle S\vdash\bigwedge_{0<i<m}\Phi(\ulcorner\varphi_{i}\urcorner)\to\Phi(\ulcorner\varphi_{m}\urcorner)$ for any formulas $\varphi_{1},\ldots,\varphi_{m}$.

$\mathbf{PC}$

$S\vdash\mathrm{Pr}_{\emptyset}(\ulcorner\varphi\urcorner)\to\Phi(\ulcorner\varphi\urcorner)$ for any formula $\varphi$.

The condition $\mathbf{D1}$ is automatically satisfied by all provability predicates of $T$. The conditions $\mathbf{D2}$, $\mathbf{D3}$ and $\mathbf{\Sigma_{1}C}$ were introduced by Hilbert and Bernays [10], Löb [18] and Feferman [7], respectively. It is known that natural provability predicates $\mathrm{Pr}_{T}(x)$ satisfy full local derivability conditions. In particular, Feferman proved $\mathbf{\Sigma_{1}C}$ for the provability predicate $\mathrm{Pr}_{\mathsf{Q}}(x)$ of Robinson’s arithmetic $\mathsf{Q}$ (cf. [23]). The conditions $\mathbf{B_{m}}$ ($m\geq 1$) were introduced by Buchholz [6]. The condition $\mathbf{B_{1}}$ is precisely $\mathbf{D1}$, and the condition $\mathbf{B_{2}}$ is precisely the condition $\mathbf{HB1}$ described in the introduction. The condition $\mathbf{B_{2}}$ was also discussed by Montagna [19] and Visser [24]. The last condition $\mathbf{PC}$ says that $\Phi(x)$ contains predicate calculus.

We prove the basic implications between local derivability conditions. For example, the first clause of the following proposition says that if a formula $\Phi(x)$ satisfies $\mathbf{D1}$, then it also satisfies $\mathbf{\Delta_{0}C}$.

Proposition 2.4**.**

$\mathbf{D1}\Rightarrow\mathbf{\Delta_{0}C}$. 2. 2.

$\mathbf{\Delta_{0}C}$* and $\mathbf{B_{m}}$ for some $m\geq 1\Rightarrow\mathbf{D1}$.* 3. 3.

$\mathbf{B_{3}}\Rightarrow\mathbf{D2}$. 4. 4.

The following are equivalent:

1. (a)

$\mathbf{D1}$* and $\mathbf{D2}$.* 2. (b)

$\mathbf{B_{m}}$* for all $m\geq 1$.* 3. (c)

$\mathbf{D1}$* and $\mathbf{B_{m}}$ for some $m\geq 3$.* 4. (d)

$\mathbf{\Delta_{0}C}$* and $\mathbf{B_{m}}$ for some $m\geq 3$.* 5. 5.

If $\Phi(x)$ is a $\Gamma$ formula, then $\mathbf{\Gamma C}\Rightarrow\mathbf{D3}$. 6. 6.

$\mathbf{B_{2}}$* and $\mathbf{PC}\iff\mathbf{B_{2}}$ and $\mathbf{\Sigma_{1}C}$.* 7. 7.

$\mathbf{B_{2}}$* and $\mathbf{PC}\Rightarrow\mathbf{D1}$.* 8. 8.

$\mathbf{D1}$, $\mathbf{D2}$ and $\mathbf{PC}\iff\mathbf{D1}$, $\mathbf{D2}$ and $\mathbf{\Sigma_{1}C}$.

Proof.

1. Suppose $\Phi(x)$ satisfies $\mathbf{D1}$. Let $\varphi$ be any $\Delta_{0}$ sentence. Then $\varphi$ is decidable in $\mathsf{PA}$. If $\mathsf{PA}\vdash\varphi$, then $S\vdash\Phi(\ulcorner\varphi\urcorner)$ by $\mathbf{D1}$, and hence $S\vdash\varphi\to\Phi(\ulcorner\varphi\urcorner)$. If $\mathsf{PA}\vdash\neg\varphi$, then $S\vdash\varphi\to\Phi(\ulcorner\varphi\urcorner)$.

2. Suppose $\Phi(x)$ satisfies $\mathbf{\Delta_{0}C}$ and $\mathbf{B_{m}}$ for some $m\geq 1$. Let $\varphi$ be any formula with $T\vdash\varphi$. Then $T\vdash\underbrace{0=0\land\cdots\land 0=0}_{m-1}\to\varphi$. By $\mathbf{B_{m}}$, we have $S\vdash\Phi(\ulcorner 0=0\urcorner)\to\Phi(\ulcorner\varphi\urcorner)$. By $\mathbf{\Delta_{0}C}$, $S\vdash 0=0\to\Phi(\ulcorner 0=0\urcorner)$, and hence $S\vdash\Phi(\ulcorner 0=0\urcorner)$. We conclude $S\vdash\Phi(\ulcorner\varphi\urcorner)$.

3. Since $T\vdash(\varphi\to\psi)\land\varphi\to\psi$, we obtain $S\vdash\Phi(\ulcorner\varphi\to\psi\urcorner)\land\Phi(\ulcorner\varphi\urcorner)\to\Phi(\ulcorner\psi\urcorner)$ by $\mathbf{B_{3}}$.

4. $(a)\Rightarrow(b)$ is well-known in the context of modal logic. $(b)\Rightarrow(c)$ is trivial. $(c)\Leftrightarrow(d)$ follows from clauses 1 and 2. We prove $(c)\Rightarrow(a)$: Suppose $\Phi(x)$ satisfies $\mathbf{D1}$ and $\mathbf{B_{m}}$ for some $m\geq 3$. By clause 3, it suffices to prove that $\Phi(x)$ satisfies $\mathbf{B_{3}}$. Suppose $T\vdash\varphi_{1}\land\varphi_{2}\to\varphi_{3}$. Then $T\vdash\varphi_{1}\land\varphi_{2}\land\underbrace{0=0\land\cdots\land 0=0}_{m-3}\to\varphi_{3}$. By $\mathbf{B_{m}}$, we obtain $S\vdash\Phi(\ulcorner\varphi_{1}\urcorner)\land\Phi(\ulcorner\varphi_{2}\urcorner)\land\Phi(\ulcorner 0=0\urcorner)\to\Phi(\ulcorner\varphi_{3}\urcorner)$. By $\mathbf{D1}$, we have $S\vdash\Phi(\ulcorner 0=0\urcorner)$. Hence $S\vdash\Phi(\ulcorner\varphi_{1}\urcorner)\land\Phi(\ulcorner\varphi_{2}\urcorner)\to\Phi(\ulcorner\varphi_{3}\urcorner)$.

5. Trivial.

6. $(\Rightarrow)$: Assume that $\Phi(x)$ satisfies $\mathbf{B_{2}}$ and $\mathbf{PC}$. Let $\varphi$ be any $\Sigma_{1}$ sentence. Let $T_{0}$ be some finite subtheory of $T$ containing Robinson’s arithmetic $\mathsf{Q}$. By $\mathbf{PC}$, $S\vdash\mathrm{Pr}_{\emptyset}(\ulcorner\bigwedge T_{0}\to\varphi\urcorner)\to\Phi(\ulcorner\bigwedge T_{0}\to\varphi\urcorner)$. Here $\mathrm{Pr}_{\emptyset}(\ulcorner\bigwedge T_{0}\to\varphi\urcorner)$ is equivalent to $\mathrm{Pr}_{[T_{0}]}(\ulcorner\varphi\urcorner)$ by formalized deduction theorem (Lemma 2.1), and therefore we obtain $S\vdash\mathrm{Pr}_{[T_{0}]}(\ulcorner\varphi\urcorner)\to\Phi(\ulcorner\bigwedge T_{0}\to\varphi\urcorner)$. Since $T_{0}$ is a subtheory of $T$, we have $T\vdash(\bigwedge T_{0}\to\varphi)\to\varphi$. By $\mathbf{B_{2}}$, $S\vdash\Phi(\ulcorner\bigwedge T_{0}\to\varphi\urcorner)\to\Phi(\ulcorner\varphi\urcorner)$. Thus we obtain $S\vdash\mathrm{Pr}_{[T_{0}]}(\ulcorner\varphi\urcorner)\to\Phi(\ulcorner\varphi\urcorner)$. Since $T_{0}$ contains $\mathsf{Q}$, $\mathbf{\Sigma_{1}C}$ holds for $\mathrm{Pr}_{[T_{0}]}(x)$, and hence $S\vdash\varphi\to\mathrm{Pr}_{[T_{0}]}(\ulcorner\varphi\urcorner)$. Therefore $S\vdash\varphi\to\Phi(\ulcorner\varphi\urcorner)$.

$(\Leftarrow)$: Suppose $\Phi(x)$ satisfies $\mathbf{B_{2}}$ and $\mathbf{\Sigma_{1}C}$. Let $\varphi$ be any formula. Since $\mathrm{Pr}_{\emptyset}(\ulcorner\varphi\urcorner)$ is a $\Sigma_{1}$ sentence, $S\vdash\mathrm{Pr}_{\emptyset}(\ulcorner\varphi\urcorner)\to\Phi(\ulcorner\mathrm{Pr}_{\emptyset}(\ulcorner\varphi\urcorner)\urcorner)$. Since $T$ is an extension of $\mathsf{PA}$, $T\vdash\mathrm{Pr}_{\emptyset}(\ulcorner\varphi\urcorner)\to\varphi$ by the reflexiveness of $\mathsf{PA}$ (see [17]). By $\mathbf{B_{2}}$, $S\vdash\Phi(\ulcorner\mathrm{Pr}_{\emptyset}(\ulcorner\varphi\urcorner)\urcorner)\to\Phi(\ulcorner\varphi\urcorner)$. Therefore $S\vdash\mathrm{Pr}_{\emptyset}(\ulcorner\varphi\urcorner)\to\Phi(\ulcorner\varphi\urcorner)$.

7. This follows from clauses 2 and 6.

8. This equivalence follows from clauses 4 and 6. ∎

Before describing several versions of the second incompleteness theorem, we prepare two propositions.

Proposition 2.5**.**

If $\Phi(x)$ satisfies $\mathbf{D1}$, then $S\vdash\mathsf{Con}_{\Phi}^{H}\to\mathsf{Con}_{\Phi}^{L}$. 2. 2.

$\mathsf{PA}\vdash\mathsf{Con}_{\Phi}^{L}\to\mathsf{Con}_{\Phi}^{\Sigma_{1}}$. 3. 3.

$\mathsf{PA}\vdash\mathsf{Con}_{\Phi}^{\Sigma_{1}}\to\mathsf{Con}_{\Phi}^{G}$.

Proof.

1. Suppose $\Phi(x)$ satisfies $\mathbf{D1}$, then $S\vdash\Phi(\ulcorner 0=0\urcorner)$. Since $\mathsf{PA}\vdash\mathsf{Con}_{\Phi}^{H}\to(\Phi(\ulcorner 0=0\urcorner)\to\neg\Phi(\ulcorner 0\neq 0\urcorner))$, we have $S\vdash\mathsf{Con}_{\Phi}^{H}\to\mathsf{Con}_{\Phi}^{L}$.

Clauses 2 and 3 are obvious. ∎

The following proposition is a part of Gödel’s first incompleteness theorem.

Proposition 2.6**.**

Let $\varphi$ be a sentence satisfying $\mathsf{PA}\vdash\varphi\leftrightarrow\neg\Phi(\ulcorner\varphi\urcorner)$. If $\Phi(x)$ satisfies $\mathbf{D1}$, then $T\nvdash\varphi$.

Proof.

Suppose $\Phi(x)$ satisfies $\mathbf{D1}$. If $T\vdash\varphi$, then by $\mathbf{D1}$, $S\vdash\Phi(\ulcorner\varphi\urcorner)$. By the choice of $\varphi$, $S\vdash\neg\varphi$. This contradicts the consistency of $T$ because $T$ is an extension of $S$. Therefore $T\nvdash\varphi$. ∎

It is well-known that for proofs of the second incompleteness theorem, the Hilbert–Bernays–Löb derivability conditions $\mathbf{D1}$, $\mathbf{D2}$ and $\mathbf{D3}$ are sufficient. This is essentially due to Löb (see [5, 17]).

Theorem 2.7** (Löb [18]).**

If $\Phi(x)$ satisfies $\mathbf{D1}$, $\mathbf{D2}$ and $\mathbf{D3}$, then $T\nvdash\mathsf{Con}_{\Phi}^{L}$.

Notice that $\{\mathbf{D1},\mathbf{B_{2}},\mathbf{D3}\}$ is weaker than $\{\mathbf{D1},\mathbf{D2},\mathbf{D3}\}$ by Proposition 2.4.4. For the former conditions, we obtain another version of the second incompleteness theorem.

Theorem 2.8**.**

If $\Phi(x)$ satisfies $\mathbf{D1}$, $\mathbf{B_{2}}$ and $\mathbf{D3}$, then $T\nvdash\mathsf{Con}_{\Phi}^{H}$.

Proof.

Suppose $\Phi(x)$ satisfies $\mathbf{D1}$, $\mathbf{B_{2}}$ and $\mathbf{D3}$. Let $\varphi$ be a sentence satisfying $\mathsf{PA}\vdash\varphi\leftrightarrow\neg\Phi(\ulcorner\varphi\urcorner)$. The existence of such a sentence $\varphi$ follows from the Fixed Point Lemma (see [17]). Since $T\vdash\Phi(\ulcorner\varphi\urcorner)\to\neg\varphi$, we have $S\vdash\Phi(\ulcorner\Phi(\ulcorner\varphi\urcorner)\urcorner)\to\Phi(\ulcorner\neg\varphi\urcorner)$ by $\mathbf{B_{2}}$. By $\mathbf{D3}$, $S\vdash\Phi(\ulcorner\varphi\urcorner)\to\Phi(\ulcorner\Phi(\ulcorner\varphi\urcorner)\urcorner)$. Thus $S\vdash\Phi(\ulcorner\varphi\urcorner)\to\Phi(\ulcorner\neg\varphi\urcorner)$, and hence $S\vdash\neg\varphi\to\exists x(\mathsf{Fml}(x)\land\Phi(x)\land\Phi(\dot{\neg}x))$. It follows $S\vdash\mathsf{Con}_{\Phi}^{H}\to\varphi$. By Proposition 2.6, $T\nvdash\varphi$, and thus $T\nvdash\mathsf{Con}_{\Phi}^{H}$. ∎

Jeroslow [13] proved that if $\mathcal{L}_{A}$ contains sufficiently many primitive recursive terms and if $\Phi(x)$ satisfies $\mathbf{D1}$ and $S\vdash\Phi(t)\to\Phi(\ulcorner\Phi(t)\urcorner)$ for all primitive recursive terms $t$, then $T\nvdash\mathsf{Con}_{\Phi}^{H}$. That is to say, in Theorem 2.8, if we strengthen the condition $\mathbf{D3}$ in this way, then the condition $\mathbf{B_{2}}$ can be omitted. As a consequence, Jeroslow remarked that if $\Phi(x)$ is a $\Gamma$ formula, then the conditions $\mathbf{D1}$ and $\mathbf{\Gamma C}$ are sufficient for the unprovability of $\mathsf{Con}_{\Phi}^{H}$ in Jersolow’s setting of language. We show that this is also the case without using such sufficiently many primitive recursive terms.

Theorem 2.9** (Jeroslow [13]; Kreisel and Takeuti [15]).**

If $\Phi(x)$ is a $\Gamma$ formula satisfying $\mathbf{D1}$ and $\mathbf{\Gamma C}$, then $T\nvdash\mathsf{Con}_{\Phi}^{H}$.

Proof.

Let $\varphi$ be a $\Gamma$ sentence such that $\mathsf{PA}\vdash\varphi\leftrightarrow\Phi(\ulcorner\neg\varphi\urcorner)$. By Proposition 2.6, $T\nvdash\neg\varphi$ because of $\mathbf{D1}$. By $\mathbf{\Gamma C}$ and the choice of $\varphi$, $S\vdash\varphi\to\Phi(\ulcorner\varphi\urcorner)\land\Phi(\ulcorner\neg\varphi\urcorner)$. Then we have $S\vdash\varphi\to\neg\mathsf{Con}_{\Phi}^{H}$. Therefore $T\nvdash\mathsf{Con}_{\Phi}^{H}$. ∎

By Proposition 2.4.8 and Theorem 2.7, if $\Phi(x)$ is a $\Sigma_{1}$ formula satisfying $\mathbf{D1}$, $\mathbf{D2}$ and $\mathbf{PC}$, then $T\nvdash\mathsf{Con}_{\Phi}^{L}$. Also by Proposition 2.4.6 and Theorem 2.9, if $\Phi(x)$ is a $\Sigma_{1}$ formula satisfying $\mathbf{D1}$, $\mathbf{B_{2}}$ and $\mathbf{PC}$, then $T\nvdash\mathsf{Con}_{\Phi}^{H}$. We improve the latter statement as follows.

Theorem 2.10**.**

If $\Phi(x)$ is a $\Sigma_{1}$ formula satisfying $\mathbf{D1}$ and $\mathbf{PC}$, then $T\nvdash\mathsf{Con}_{\Phi}^{H}$.

Proof.

Suppose that $\Phi(x)$ is $\Sigma_{1}$ and satisfies $\mathbf{D1}$ and $\mathbf{PC}$. Let $T_{0}$ be a finite subtheory of $T$ containing $\mathsf{Q}$. Let $\varphi$ be a $\Sigma_{1}$ sentence satisfying $\mathsf{PA}\vdash\varphi\leftrightarrow\Phi(\ulcorner\neg(\bigwedge T_{0}\to\varphi)\urcorner)$. By $\mathbf{PC}$ and formalized deduction theorem, we have $S\vdash\mathrm{Pr}_{[T_{0}]}(\ulcorner\varphi\urcorner)\to\Phi(\ulcorner\bigwedge T_{0}\to\varphi\urcorner)$. By $\mathbf{\Sigma_{1}C}$ for $\mathrm{Pr}_{[T_{0}]}(x)$, $S\vdash\varphi\to\Phi(\ulcorner\bigwedge T_{0}\to\varphi\urcorner)$. Since $\mathsf{PA}\vdash\varphi\to\Phi(\ulcorner\neg(\bigwedge T_{0}\to\varphi)\urcorner)$ by the choice of $\varphi$, we obtain $S\vdash\varphi\to\neg\mathsf{Con}_{\Phi}^{H}$.

If $T\vdash\mathsf{Con}_{\Phi}^{H}$, then $T\vdash\neg\varphi$. Also $T\vdash\bigwedge T_{0}\land\neg\varphi$, and this means $T\vdash\neg(\bigwedge T_{0}\to\varphi)$. By $\mathbf{D1}$, $S\vdash\Phi(\ulcorner\neg(\bigwedge T_{0}\to\varphi)\urcorner)$, and hence $S\vdash\varphi$. This is a contradiction. Therefore $T\nvdash\mathsf{Con}_{\Phi}^{H}$. ∎

Remark 2.11**.**

The following makeshift condition $\mathbf{\Sigma_{1}C}^{-}$ is of course weaker than $\mathbf{\Sigma_{1}C}$ if $\bigwedge\emptyset\to\varphi$ is identical to $\varphi$.

$\mathbf{\Sigma_{1}C}^{-}$

There exists a finite subtheory $T_{0}$ of $T$ such that for any $\Sigma_{1}$ sentence $\varphi$, $S\vdash\varphi\to\Phi(\ulcorner\bigwedge T_{0}\to\varphi\urcorner)$.

Our proof of Proposition 2.4.6 $(\Rightarrow)$ actually shows two implications “$\mathbf{PC}\Rightarrow\mathbf{\Sigma_{1}C}^{-}$” and “$\{\mathbf{B_{2}},\mathbf{\Sigma_{1}C}^{-}\}\Rightarrow\mathbf{\Sigma_{1}C}$”. Also our proof of Theorem 2.10 essentially shows that if $\Phi(x)$ is a $\Sigma_{1}$ formula satisfying $\mathbf{D1}$ and $\mathbf{\Sigma_{1}C}^{-}$, then $T\nvdash\mathsf{Con}_{\Phi}^{H}$. Then Theorem 2.9 in the case $\Gamma=\Sigma_{1}$ and Theorem 2.10 directly follow from these observations.

In this section, we have seen that $\{\mathbf{D1},\mathbf{D2},\mathbf{D3}\}$ is sufficient for $T\nvdash\mathsf{Con}_{\Phi}^{L}$ (Theorem 2.7), and $\{\mathbf{D1},\mathbf{B_{2}},\mathbf{D3}\}$ is sufficient for $T\nvdash\mathsf{Con}_{\Phi}^{H}$ (Theorem 2.8). Also for $\Sigma_{1}$ formulas $\Phi(x)$, each of $\{\mathbf{D1},\mathbf{\Sigma_{1}C}\}$ and $\{\mathbf{D1},\mathbf{PC}\}$ is sufficient for $T\nvdash\mathsf{Con}_{\Phi}^{H}$ (Theorems 2.9 and 2.10). From examples of formulas given in Section 4, the following non-implications are obtained. These non-implications show that these unprovability results are optimal. For example, the third clause in the following list means that there exists a $\Sigma_{1}$ formula $\Phi(x)$ satisfying both $\mathbf{D1}$ and $\mathbf{D2}$ such that $T\vdash\mathsf{Con}_{\Phi}^{H}$.

• •

$\{\mathbf{D1},\mathbf{D2},\mathbf{\Sigma_{1}C}\}\not\Rightarrow T\nvdash\mathsf{Con}_{\Phi}^{H}$ (Fact 4.3).

• •

$\{\Phi\in\Sigma_{1},\mathbf{D2},\mathbf{D3},\mathbf{\Sigma_{1}C},\mathbf{PC}\}\not\Rightarrow T\nvdash\mathsf{Con}_{\Phi}^{H}$ (Proposition 4.1).

• •

$\{\Phi\in\Sigma_{1},\mathbf{D1},\mathbf{D2}\}\not\Rightarrow T\nvdash\mathsf{Con}_{\Phi}^{H}$ (Fact 4.5.1).

• •

$\{\Phi\in\Sigma_{1},\mathbf{D1},\mathbf{D3}\}\not\Rightarrow T\nvdash\mathsf{Con}_{\Phi}^{H}$ (Fact 4.5.2).

• •

$\{\Phi\in\Sigma_{1},\mathbf{D1},\mathbf{B_{2}},\mathbf{D3}\}\not\Rightarrow T\nvdash\mathsf{Con}_{\Phi}^{L}$ (Fact 4.6.3).

• •

$\{\Phi\in\Sigma_{1},\mathbf{D1},\mathbf{\Sigma_{1}C},\mathbf{PC}\}\not\Rightarrow T\nvdash\mathsf{Con}_{\Phi}^{L}$ (Proposition 4.4).

• •

$\{\Phi\in\Sigma_{1},\mathbf{D1},\mathbf{D2},\mathbf{\Sigma_{1}C}\}\not\Rightarrow T\nvdash\mathsf{Con}_{\Phi}^{\Sigma_{1}}$ (Proposition 4.10).

These non-implications show that none of $\{\mathbf{D1},\mathbf{B_{2}},\mathbf{D3}\}$, $\{\mathbf{D1},\mathbf{\Sigma_{1}C}\}$ and $\{\mathbf{D1},\mathbf{PC}\}$ implies $\{\mathbf{D1},\mathbf{D2},\mathbf{D3}\}$. Moreover we obtain the following non-implications.

• •

$\{\Phi\in\Sigma_{1},\mathbf{D1},\mathbf{D2},\mathbf{D3}\}\not\Rightarrow\mathbf{\Sigma_{1}C}$ (Proposition 4.12). By Proposition 2.4.6, this is equivalent to $\{\Phi\in\Sigma_{1},\mathbf{D1},\mathbf{D2},\mathbf{D3}\}\not\Rightarrow\mathbf{PC}$.

• •

$\{\Phi\in\Sigma_{1},\mathbf{D1},\mathbf{\Sigma_{1}C},\mathbf{PC}\}\not\Rightarrow\mathbf{B_{2}}$ (Proposition 4.4).

• •

$\{\Phi\in\Sigma_{1},\mathbf{D1},\mathbf{\Sigma_{1}C}\}\not\Rightarrow\mathbf{PC}$ (Proposition 4.13).

• •

$\{\Phi\in\Sigma_{1},\mathbf{D1},\mathbf{PC}\}\not\Rightarrow\mathbf{\Sigma_{1}C}$ (Proposition 4.14).

Consequently, $\{\mathbf{D1},\mathbf{B_{2}},\mathbf{D3}\}$, $\{\mathbf{D1},\mathbf{\Sigma_{1}C}\}$ and $\{\mathbf{D1},\mathbf{PC}\}$ are pairwise incomparable. Also $\{\mathbf{D1},\mathbf{D2},\mathbf{D3}\}$ is incomparable with each of $\{\mathbf{D1},\mathbf{\Sigma_{1}C}\}$ and $\{\mathbf{D1},\mathbf{PC}\}$.

2.2 Uniform derivability conditions

In this subsection, we introduce and investigate uniform derivability conditions. Let $\varphi(\vec{x})$ be an abbreviation for $\varphi(x_{0},\ldots,x_{k})$ for some $k$.

Definition 2.12** (Uniform derivability conditions).**

$\mathbf{D1^{U}}$

If $T\vdash\forall\vec{x}\,\varphi(\vec{x})$, then $S\vdash\forall\vec{x}\,\Phi(\ulcorner\varphi(\vec{\dot{x}})\urcorner)$ for any formula $\varphi(\vec{x})$.

$\mathbf{D2^{U}}$

$S\vdash\forall\vec{x}\,(\Phi(\ulcorner\varphi(\vec{\dot{x}})\to\psi(\vec{\dot{x}})\urcorner)\to(\Phi(\ulcorner\varphi(\vec{\dot{x}})\urcorner)\to\Phi(\ulcorner\psi(\vec{\dot{x}})\urcorner)))$ for any formulas $\varphi(\vec{x})$ and $\psi(\vec{x})$.

$\mathbf{D3^{U}}$

$S\vdash\forall\vec{x}\,(\Phi(\ulcorner\varphi(\vec{\dot{x}})\urcorner)\to\Phi(\ulcorner\Phi(\ulcorner\varphi(\vec{\dot{x}})\urcorner)\urcorner))$ for any formula $\varphi(\vec{x})$.

$\mathbf{\Gamma C^{U}}$

$S\vdash\forall\vec{x}\,(\varphi(\vec{x})\to\Phi(\ulcorner\varphi(\vec{\dot{x}})\urcorner))$ for any $\Gamma$ formula $\varphi(\vec{x})$.

$\mathbf{B_{m}^{U}}$** ($m\geq 1$)**

If $\displaystyle T\vdash\forall\vec{x}\left(\bigwedge_{0<i<m}\varphi_{i}(\vec{x})\to\varphi_{m}(\vec{x})\right)$,

then $\displaystyle S\vdash\forall\vec{x}\left(\bigwedge_{0<i<m}\Phi(\ulcorner\varphi_{i}(\vec{\dot{x}})\urcorner)\to\Phi(\ulcorner\varphi_{m}(\vec{\dot{x}})\urcorner)\right)$

for any formulas $\varphi_{1}(\vec{x}),\ldots,\varphi_{m}(\vec{x})$.

$\mathbf{CB}$

$S\vdash\Phi(\ulcorner\forall\vec{x}\,\varphi(\vec{x})\urcorner)\to\forall\vec{x}\,\Phi(\ulcorner\varphi(\vec{\dot{x}})\urcorner)$ for any formula $\varphi(\vec{x})$.

$\mathbf{PC^{U}}$

$S\vdash\forall\vec{x}(\mathrm{Pr}_{\emptyset}(\ulcorner\varphi(\vec{\dot{x}})\urcorner)\to\Phi(\ulcorner\varphi(\vec{\dot{x}})\urcorner))$ for any formula $\varphi(\vec{x})$.

Usual proofs of the Hilbert–Bernays–Löb derivability conditions $\mathbf{D1}$, $\mathbf{D2}$ and $\mathbf{D3}$ (in books such as [5]) are demonstrated by showing stronger uniform derivability conditions $\mathbf{D1^{U}}$, $\mathbf{D2^{U}}$ and $\mathbf{\Sigma_{1}C^{U}}$. Notice that the natural provability predicates $\mathrm{Pr}_{T}(x)$ satisfy full uniform derivability conditions.

As in the local version, the conditions $\mathbf{B_{m}^{U}}$ ($m\geq 1$) were introduced by Buchholz [6], and $\mathbf{B_{1}^{U}}$ is precisely $\mathbf{D1^{U}}$. The condition $\mathbf{CB}$ claims that sentences corresponding to the Converse Barcan Formula investigated in predicate modal logic (see [11]) are provable. Notice that the condition $\mathbf{HB2}$ described in the introduction seems to be a variant of the condition $\mathbf{CB}$. It is easy to see that each of uniform derivability conditions is stronger than the corresponding local version. Moreover, uniform derivability conditions are strictly stronger than local derivability conditions (see Proposition 4.9 in Section 4).

As in the local version, we obtain the following proposition.

Proposition 2.13**.**

$\mathbf{\Delta_{0}C}$* and $\mathbf{B_{m}^{U}}$ for some $m\geq 1\Rightarrow\mathbf{D1^{U}}$.* 2. 2.

$\mathbf{B_{3}^{U}}\Rightarrow\mathbf{D2^{U}}$. 3. 3.

The following are equivalent:

1. (a)

$\mathbf{D1^{U}}$* and $\mathbf{D2^{U}}$.* 2. (b)

$\mathbf{B_{m}^{U}}$* for all $m\geq 1$.* 3. (c)

$\mathbf{D1^{U}}$* and $\mathbf{B_{m}^{U}}$ for some $m\geq 3$.* 4. 4.

If $\Phi(x)$ is a $\Gamma$ formula, then $\mathbf{\Gamma C^{U}}\Rightarrow\mathbf{D3^{U}}$. 5. 5.

$\mathbf{B_{2}^{U}}$* and $\mathbf{PC^{U}}\iff\mathbf{B_{2}^{U}}$ and $\mathbf{\Sigma_{1}C^{U}}$.* 6. 6.

$\mathbf{B_{2}^{U}}$* and $\mathbf{PC^{U}}\Rightarrow\mathbf{D1^{U}}$.* 7. 7.

$\mathbf{D1^{U}}$, $\mathbf{D2^{U}}$ and $\mathbf{PC^{U}}\iff\mathbf{D1^{U}}$, $\mathbf{D2^{U}}$ and $\mathbf{\Sigma_{1}C^{U}}$.

The condition $\mathbf{CB}$ is related to other conditions.

Proposition 2.14**.**

$\mathbf{D1}$* and $\mathbf{CB}\Rightarrow\mathbf{D1^{U}}$.* 2. 2.

$\mathbf{B_{2}^{U}}\Rightarrow\mathbf{CB}$. 3. 3.

$\mathbf{D2^{U}}$* and $\mathbf{PC^{U}}\Rightarrow\mathbf{CB}$.* 4. 4.

The following are equivalent:

1. (a)

$\mathbf{D1^{U}}$* and $\mathbf{D2^{U}}$.* 2. (b)

$\mathbf{D1}$, $\mathbf{B_{2}^{U}}$ and $\mathbf{D2^{U}}$. 3. (c)

$\mathbf{D1}$, $\mathbf{CB}$ and $\mathbf{D2^{U}}$.

Proof.

1. Suppose that $\Phi(x)$ satisfies $\mathbf{D1}$ and $\mathbf{CB}$. Assume $T\vdash\forall\vec{x}\,\varphi(\vec{x})$. Then $S\vdash\Phi(\ulcorner\forall\vec{x}\,\varphi(\vec{x})\urcorner)$ by $\mathbf{D1}$. Since $S\vdash\Phi(\ulcorner\forall\vec{x}\,\varphi(\vec{x})\urcorner)\to\forall\vec{x}\,\Phi(\ulcorner\varphi(\vec{\dot{x}})\urcorner)$ by $\mathbf{CB}$, we have $S\vdash\forall\vec{x}\,\Phi(\ulcorner\varphi(\vec{\dot{x}})\urcorner)$.

2. Suppose that $\Phi(x)$ satisfies $\mathbf{B_{2}^{U}}$. Since $T\vdash\forall\vec{x}\,\varphi(\vec{x})\to\varphi(\vec{x})$, we have $S\vdash\Phi(\ulcorner\forall\vec{x}\,\varphi(\vec{x})\urcorner)\to\Phi(\ulcorner\varphi(\vec{\dot{x}})\urcorner)$ by $\mathbf{B_{2}^{U}}$. Therefore $S\vdash\Phi(\ulcorner\forall\vec{x}\,\varphi(\vec{x})\urcorner)\to\forall\vec{x}\,\Phi(\ulcorner\varphi(\vec{\dot{x}})\urcorner)$.

3. Suppose $\Phi(x)$ satisfies $\mathbf{D2^{U}}$ and $\mathbf{PC^{U}}$. Let $\varphi(\vec{x})$ be any formula. Since $\forall\vec{x}\varphi(\vec{x})\to\varphi(\vec{x})$ is provable in predicate calculus, $S\vdash\mathrm{Pr}_{\emptyset}(\ulcorner\forall\vec{x}\varphi(\vec{x})\to\varphi(\vec{\dot{x}})\urcorner)$ by $\mathbf{D1^{U}}$ for $\mathrm{Pr}_{\emptyset}(x)$. From $\mathbf{PC^{U}}$, $S\vdash\Phi(\ulcorner\forall\vec{x}\varphi(\vec{x})\to\varphi(\vec{\dot{x}})\urcorner)$. Then by $\mathbf{D2^{U}}$, $S\vdash\Phi(\ulcorner\forall\vec{x}\varphi(\vec{x})\urcorner)\to\Phi(\ulcorner\varphi(\vec{\dot{x}})\urcorner)$. Thus $S\vdash\Phi(\ulcorner\forall\vec{x}\,\varphi(\vec{x})\urcorner)\to\forall\vec{x}\,\Phi(\ulcorner\varphi(\vec{\dot{x}})\urcorner)$.

4. The implications $(a)\Rightarrow(b)$, $(b)\Rightarrow(c)$ and $(c)\Rightarrow(a)$ follow from Proposition 2.13.3, clause 2 and clause 1, respectively. ∎

The following corollary immediately follows from clauses 1, 2 and 3 of Proposition 2.14.

Corollary 2.15**.**

$\mathbf{D1}$* and $\mathbf{B_{2}^{U}}\Rightarrow\mathbf{D1^{U}}$.* 2. 2.

$\mathbf{D1}$, $\mathbf{D2^{U}}$ and $\mathbf{PC^{U}}\Rightarrow\mathbf{D1^{U}}$.

Hilbert and Bernays [10] proved that if a $\Sigma_{1}$ formula $\Phi(x)$ satisfies the conditions $\mathbf{HB1}$, $\mathbf{HB2}$ and $\mathbf{HB3}$ described in the introduction, then $T\nvdash\mathsf{Con}_{\Phi}^{H}$. In our framework, the Hilbert–Bernays derivability conditions can be replaced by the conditions $\mathbf{B_{2}}$, $\mathbf{CB}$ and $\mathbf{\Delta_{0}C^{U}}$ without any substantial change. Then we obtain the following version of the second incompleteness theorem.

Theorem 2.16** (Hilbert and Bernays [10]).**

If $\Phi(x)$ is a $\Sigma_{1}$ formula satisfying $\mathbf{B_{2}}$, $\mathbf{CB}$ and $\mathbf{\Delta_{0}C^{U}}$, then $T\nvdash\mathsf{Con}_{\Phi}^{H}$.

Proof.

Suppose that $\Phi(x)$ is $\Sigma_{1}$ and satisfies $\mathbf{B_{2}}$, $\mathbf{CB}$ and $\mathbf{\Delta_{0}C^{U}}$. Let $\varphi$ be a $\Pi_{1}$ sentence satisfying $\mathsf{PA}\vdash\varphi\leftrightarrow\neg\Phi(\ulcorner\varphi\urcorner)$. Let $\delta(x)$ be a $\Delta_{0}$ formula with $\mathsf{PA}\vdash\varphi\leftrightarrow\forall x\delta(x)$. Then by $\mathbf{B_{2}}$, $S\vdash\Phi(\ulcorner\varphi\urcorner)\to\Phi(\ulcorner\forall x\delta(x)\urcorner)$. By $\mathbf{CB}$, we obtain

[TABLE]

On the other hand, $S\vdash\neg\delta(x)\to\Phi(\ulcorner\neg\delta(\dot{x})\urcorner)$ by $\mathbf{\Delta_{0}C^{U}}$. Then $S\vdash\exists x\neg\delta(x)\to\exists x\Phi(\ulcorner\neg\delta(\dot{x})\urcorner)$. Hence $S\vdash\neg\varphi\to\exists x\Phi(\ulcorner\neg\delta(\dot{x})\urcorner)$. By combining this with (1), we obtain

[TABLE]

It follows $S\vdash\neg\varphi\to\exists x(\mathsf{Fml}(x)\land\Phi(x)\land\Phi(\dot{\neg}x))$, and hence $S\vdash\mathsf{Con}_{\Phi}^{H}\to\varphi$. By Proposition 2.4.2, $\Phi(x)$ satisfies $\mathbf{D1}$. Then by Proposition 2.6, $T\nvdash\varphi$. Therefore we conclude $T\nvdash\mathsf{Con}_{\Phi}^{H}$. ∎

Theorem 2.16 is optimal in the sense of the following non-implications from Section 4.

• •

$\{\mathbf{D1},\mathbf{B_{2}},\mathbf{CB},\mathbf{\Delta_{0}C^{U}}\}\not\Rightarrow T\nvdash\mathsf{Con}_{\Phi}^{H}$ (Fact 4.3).

• •

$\{\Phi\in\Sigma_{1},\mathbf{CB},\mathbf{\Delta_{0}C^{U}}\}\not\Rightarrow T\nvdash\mathsf{Con}_{\Phi}^{H}$ (Proposition 4.1).

• •

$\{\Phi\in\Sigma_{1},\mathbf{B_{2}},\mathbf{CB}\}\not\Rightarrow T\nvdash\mathsf{Con}_{\Phi}^{H}$ (Proposition 4.2).

• •

$\{\Phi\in\Sigma_{1},\mathbf{D1},\mathbf{B_{2}},\mathbf{\Delta_{0}C^{U}}\}\not\Rightarrow T\nvdash\mathsf{Con}_{\Phi}^{H}$ (Fact 4.6.1).

• •

$\{\Phi\in\Sigma_{1},\mathbf{D1},\mathbf{B_{2}},\mathbf{CB},\mathbf{\Delta_{0}C^{U}}\}\not\Rightarrow T\nvdash\mathsf{Con}_{\Phi}^{L}$ (Fact 4.6.2).

Notice that $\{\mathbf{B_{2}},\mathbf{CB},\mathbf{\Delta_{0}C^{U}}\}$ is equivalent to $\{\mathbf{D1},\mathbf{B_{2}},\mathbf{CB},\mathbf{\Delta_{0}C^{U}}\}$ by Proposition 2.4.2. For the latter condition, we do not know if $\{\Phi\in\Sigma_{1},\mathbf{D1},\mathbf{B_{2}},\mathbf{CB},\mathbf{\Delta_{0}C^{U}}\}$ is optimal to conclude $T\nvdash\mathsf{Con}_{\Phi}^{H}$ or not.

Problem 2.17**.**

Is there a $\Sigma_{1}$ provability predicate satisfying $\mathbf{D1}$, $\mathbf{CB}$ and $\mathbf{\Delta_{0}C^{U}}$ such that $T\vdash\mathsf{Con}_{\Phi}^{H}$? 2. 2.

Is there a $\Sigma_{1}$ provability predicate satisfying $\mathbf{D1}$, $\mathbf{B_{2}}$ and $\mathbf{CB}$ such that $T\vdash\mathsf{Con}_{\Phi}^{H}$?

The following two non-implications from Section 4 indicate that $\{\mathbf{B_{2}},\mathbf{CB},\mathbf{\Delta_{0}C^{U}}\}$ is incomparable with each of $\{\mathbf{D1},\mathbf{D2},\mathbf{D3}\}$, $\{\mathbf{D1},\mathbf{B_{2}},\mathbf{D3}\}$, $\{\mathbf{D1},\mathbf{\Sigma_{1}C}\}$ and $\{\mathbf{D1},\mathbf{PC}\}$.

• •

$\{\Phi\in\Sigma_{1},\mathbf{B_{2}},\mathbf{CB},\mathbf{\Delta_{0}C^{U}}\}\not\Rightarrow\mathbf{D3}$ (Fact 4.6.2).

• •

$\{\Phi\in\Sigma_{1},\mathbf{D1},\mathbf{D2},\mathbf{\Sigma_{1}C}\}\not\Rightarrow\mathbf{CB}$ (Proposition 4.9).

Usual proof of $\mathbf{\Sigma_{1}C^{U}}$ (in books such as [5]) proceeds by induction on the construction of $\Sigma_{1}$ formulas, and it requires much effort. In the lecture note [6] by Buchholz, an elegant schematic proof of $\mathbf{\Sigma_{1}C^{U}}$ is presented. More precisely, it is proved that for a proof of $\mathbf{\Sigma_{1}C^{U}}$, the assumption “$\mathbf{B_{m}^{U}}$ for all $m\geq 1$” is sufficient. By Proposition 2.13.3, this assumption is equivalent to $\{\mathbf{D1^{U}},\mathbf{D2^{U}}\}$. Hence Buchholz’s work is stated as follows.

Theorem 2.18** (Buchholz [6]).**

$\mathbf{D1^{U}}$* and $\mathbf{D2^{U}}\Rightarrow\mathbf{\Sigma_{1}C^{U}}$.*

In Rautenberg’s book [21], a schematic proof of $\mathbf{\Sigma_{1}C^{U}}$ based on Buchholz’s argument is presented. As a corollary to Theorem 2.18, we obtain the following version of the second incompleteness theorem.

Corollary 2.19**.**

If $\Phi(x)$ is a $\Sigma_{1}$ formula satisfying $\mathbf{D1^{U}}$ and $\mathbf{D2^{U}}$, then $T\nvdash\mathsf{Con}_{\Phi}^{L}$.

Notice that {$\mathbf{D1^{U}},\mathbf{D2^{U}}\}$ implies $\{\mathbf{D1},\mathbf{B_{2}^{U}}\}$ by Proposition 2.13.3. The following theorem improves Buchholz’s Theorem 2.18 which will be proved in the next section.

Theorem 2.20**.**

$\mathbf{D1}$* and $\mathbf{B_{2}^{U}}\Rightarrow\mathbf{\Sigma_{1}C^{U}}$.*

This theorem says that only the $m=1,2$ cases of Buchholz’s assumption are sufficient to prove $\mathbf{\Sigma_{1}C^{U}}$. We will also prove that Theorem 2.20 is actually an improvement of Theorem 2.18 (see Theorem 4.15 below). Interestingly, for $\Sigma_{1}$ formulas, $\{\mathbf{D1},\mathbf{B_{2}^{U}}\}$ implies $\{\mathbf{D1},\mathbf{B_{2}},\mathbf{D3}\}$, $\{\mathbf{D1},\mathbf{\Sigma_{1}C}\}$, $\{\mathbf{D1},\mathbf{PC}\}$ and $\{\mathbf{B_{2}},\mathbf{CB},\mathbf{\Delta_{0}C^{U}}\}$ by Theorem 2.20 and Proposition 2.13, and each of them is sufficient for $T\nvdash\mathsf{Con}_{\Phi}^{H}$. As a consequence, we obtain the following corollary.

Corollary 2.21**.**

If $\Phi(x)$ is a $\Sigma_{1}$ formula satisfying $\mathbf{D1}$ and $\mathbf{B_{2}^{U}}$, then $T\nvdash\mathsf{Con}_{\Phi}^{H}$.

Related to Corollary 2.21, we propose the following problem.

Problem 2.22**.**

Is there a $\Sigma_{1}$ formula $\Phi(x)$ satisfying $\mathbf{D1}$ and $\mathbf{B_{2}^{U}}$ such that $T\vdash\mathsf{Con}_{\Phi}^{L}$?

In contrast to the consistency statements $\mathsf{Con}_{\Phi}^{H}$ and $\mathsf{Con}_{\Phi}^{L}$, Proposition 4.10 in Section 4 shows that the full uniform derivability conditions are not sufficient for the unprovability of $\mathsf{Con}_{\Phi}^{\Sigma_{1}}$ and $\mathsf{Con}_{\Phi}^{G}$.

From Theorem 2.20 and Proposition 2.13.5, we obtain the following corollary.

Corollary 2.23**.**

$\mathbf{D1}$* and $\mathbf{B_{2}^{U}}\Rightarrow\mathbf{PC^{U}}$.*

Moreover, we show that $\mathbf{D1}$ and $\mathbf{B_{2}^{U}}$ imply a stronger version of $\mathbf{PC^{U}}$. For $n\geq 0$, let $\mathsf{True}_{\Sigma_{n}}(x)$ be a natural formula saying that “$x$ is a true $\Sigma_{n}$ sentence” (cf. Hájek and Pudlák [9]).

Proposition 2.24**.**

If $\Phi(x)$ satisfies $\mathbf{D1}$ and $\mathbf{B_{2}^{U}}$, then for $n\geq 0$,

[TABLE]

Proof.

Suppose that $\Phi(x)$ satisfies $\mathbf{D1}$ and $\mathbf{B_{2}^{U}}$, and let $n\geq 0$. By Theorem 2.20, $\Phi(x)$ satisfies $\mathbf{\Sigma_{1}C^{U}}$, and hence $S\vdash\Sigma_{n}(x)\land\mathrm{Pr}_{\emptyset}(x)\to\Phi(\ulcorner\Sigma_{n}(\dot{x})\land\mathrm{Pr}_{\emptyset}(\dot{x})\urcorner)$. By reflexiveness, $T\vdash\Sigma_{n}(x)\land\mathrm{Pr}_{\emptyset}(x)\to\mathsf{True}_{\Sigma_{n}}(x)$. Then $S\vdash\Phi(\ulcorner\Sigma_{n}(\dot{x})\land\mathrm{Pr}_{\emptyset}(\dot{x})\urcorner)\to\Phi(\ulcorner\mathsf{True}_{\Sigma_{n}}(\dot{x})\urcorner)$ by $\mathbf{B_{2}^{U}}$. We conclude $S\vdash\Sigma_{n}(x)\land\mathrm{Pr}_{\emptyset}(x)\to\Phi(\ulcorner\mathsf{True}_{\Sigma_{n}}(\dot{x})\urcorner)$. ∎

2.3 Global derivability conditions

At last, we introduce the strongest version of derivability conditions. They are called global derivability conditions.

Definition 2.25** (Global derivability conditions).**

$\mathbf{D2^{G}}$

$S\vdash\forall x\forall y(\mathsf{Fml}(x)\land\mathsf{Fml}(y)\to(\Phi(x\dot{\to}y)\to(\Phi(x)\to\Phi(y))))$.

$\mathbf{D3^{G}}$

$S\vdash\forall x(\mathsf{Fml}(x)\to(\Phi(x)\to\Phi(\ulcorner\Phi(\dot{x})\urcorner)))$.

$\mathbf{\Gamma C^{G}}$

$S\vdash\forall x(\mathsf{True}_{\Gamma}(x)\to\Phi(x))$.

$\mathbf{PC^{G}}$

$S\vdash\forall x(\mathsf{Fml}(x)\to(\mathrm{Pr}_{\emptyset}(x)\to\Phi(x)))$.

The condition $\mathbf{D2^{G}}$ for provability predicates $\mathrm{Pr}_{T}(x)$ was proved in Feferman [7]. Montagna [19] investigated the condition $\mathbf{D2^{G}}$. The condition $\mathbf{\Sigma_{1}C^{G}}$ for $\mathrm{Pr}_{\mathsf{Q}}(x)$ is explicitly stated in the book [9]. Global derivability conditions are strictly stronger than uniform derivability conditions (see Proposition 4.10).

We can prove the following proposition as in the uniform version.

Proposition 2.26**.**

If $\Phi(x)$ is a $\Gamma$ formula, then $\mathbf{\Gamma C^{U}}\Rightarrow\mathbf{D3^{G}}$. 2. 2.

$\mathbf{D1}$, $\mathbf{D2^{G}}$ and $\mathbf{PC^{G}}\Rightarrow\mathbf{\Sigma_{1}C^{G}}$.

Proposition 2.26.2 was stated in von Bülow [26] and Visser [25].

Consistency statements are enhanced by global derivability conditions.

Proposition 2.27**.**

If $\Phi(x)$ satisfies $\mathbf{D2^{G}}$ and $\mathbf{PC^{G}}$, then $S\vdash\mathsf{Con}_{\Phi}^{G}\to\mathsf{Con}_{\Phi}^{H}$. 2. 2.

If $\Phi(x)$ satisfies $\mathbf{D1}$, $\mathbf{D2^{G}}$ and $\mathbf{PC^{G}}$, then $\mathsf{Con}_{\Phi}^{H}$, $\mathsf{Con}_{\Phi}^{L}$ and $\mathsf{Con}_{\Phi}^{G}$ are mutually equivalent in $S$. 3. 3.

If $\Phi(x)$ satisfies $\mathbf{D2^{G}}$ and $\mathbf{\Sigma_{1}C^{G}}$, then $\mathsf{Con}_{\Phi}^{L}$ and $\mathsf{Con}_{\Phi}^{\Sigma_{1}}$ are equivalent in $S$.

Proof.

1. Suppose $\Phi(x)$ satisfies $\mathbf{D2^{G}}$ and $\mathbf{PC^{G}}$. Since $\mathsf{PA}\vdash\forall x\forall y(\mathsf{Fml}(x)\land\mathsf{Fml}(y)\to\mathrm{Pr}_{\emptyset}(x\dot{\to}(\dot{\neg}x\dot{\to}y)))$, $S\vdash\forall x\forall y(\mathsf{Fml}(x)\land\mathsf{Fml}(y)\to\Phi(x\dot{\to}(\dot{\neg}x\dot{\to}y)))$ by $\mathbf{PC^{G}}$. Hence $\forall x\forall y(\mathsf{Fml}(x)\land\mathsf{Fml}(y)\land\Phi(x)\land\Phi(\dot{\neg}x)\to\Phi(y))$ is provable in $S$ by $\mathbf{D2^{G}}$. This sentence is equivalent to $\mathsf{Con}_{\Phi}^{G}\to\mathsf{Con}_{\Phi}^{H}$.

2. This follows from Proposition 2.5 and clause 1.

3. Suppose $\Phi(x)$ satisfies $\mathbf{D2^{G}}$ and $\mathbf{\Sigma_{1}C^{G}}$. By Proposition 2.5, it suffices to show $S\vdash\mathsf{Con}_{\Phi}^{\Sigma_{1}}\to\mathsf{Con}_{\Phi}^{L}$. Since $\mathsf{PA}\vdash\neg\mathsf{True}_{\Sigma_{1}}(\ulcorner 0\neq 0\urcorner)$, $\mathsf{PA}\vdash\Sigma_{1}(x)\land\mathsf{Sent}(x)\to\mathsf{True}_{\Sigma_{1}}(\ulcorner 0\neq 0\urcorner\dot{\to}x)$. By $\mathbf{\Sigma_{1}C^{G}}$, $S\vdash\Sigma_{1}(x)\land\mathsf{Sent}(x)\to\Phi(\ulcorner 0\neq 0\urcorner\dot{\to}x)$. By $\mathbf{D2^{G}}$, $S\vdash\Sigma_{1}(x)\land\mathsf{Sent}(x)\to(\Phi(\ulcorner 0\neq 0\urcorner)\to\Phi(x))$. Thus $S\vdash\mathsf{Con}_{\Phi}^{\Sigma_{1}}\to\mathsf{Con}_{\Phi}^{L}$. ∎

From Theorems 2.7 and 2.10, and Proposition 2.27, we obtain the following corollary.

Corollary 2.28**.**

If $\Phi(x)$ is a $\Sigma_{1}$ formula satisfying $\mathbf{D1}$, $\mathbf{D2^{G}}$ and $\mathbf{PC^{G}}$, then $T\nvdash\mathsf{Con}_{\Phi}^{G}$. 2. 2.

If $\Phi(x)$ is a $\Sigma_{1}$ formula satisfying $\mathbf{D1}$, $\mathbf{D2^{G}}$ and $\mathbf{\Sigma_{1}C^{G}}$, then $T\nvdash\mathsf{Con}_{\Phi}^{\Sigma_{1}}$.

Corollary 2.15.2 and Proposition 2.26.2 show that $\{\mathbf{D1^{U}},\mathbf{D2^{G}},\mathbf{\Sigma_{1}C^{G}}\}$ is weaker than $\{\mathbf{D1},\mathbf{D2^{G}},\mathbf{PC^{G}}\}$. Moreover, Proposition 4.11 in Section 4 shows the following interesting non-implication:

• •

$\{\Phi\in\Sigma_{1},\mathbf{D1^{U}},\mathbf{D2^{G}},\mathbf{\Sigma_{1}C^{G}}\}\not\Rightarrow T\nvdash\mathsf{Con}_{\Phi}^{G}$.

Hence in contrast to local and uniform versions, $\{\mathbf{D1^{U}},\mathbf{D2^{G}},\mathbf{\Sigma_{1}C^{G}}\}$ is strictly weaker than $\{\mathbf{D1},\mathbf{D2^{G}},\mathbf{PC^{G}}\}$. Also this non-implication indicates that global derivability conditions except for $\mathbf{PC^{G}}$ are not sufficient for the unprovability of Gödel’s consistency statement $\mathsf{Con}_{\Phi}^{G}$ even if $\Phi$ is $\Sigma_{1}$. This shows that neither Hilbert–Bernays’ conditions nor Löb’s conditions accomplish Gödel’s original statement of the second incompleteness theorem.

Let $\mathsf{LogAx}(x)$ be a suitable $\Delta_{1}$ formula representing the set of all logical axioms of predicate calculus formulated in Feferman’s paper [7]. In Feferman’s formulation, the sole inference rule is modus ponens, and the generalization rule is admissible (see Result 2.1 in [7]). The following condition was introduced by Montagna [19].

Definition 2.29**.**

$\mathbf{Ax}$

$S\vdash\forall x(\mathsf{LogAx}(x)\to\Phi(x))$.

The condition $\mathbf{Ax}$ is related to the condition $\mathbf{PC^{G}}$.

Proposition 2.30**.**

$\mathbf{PC^{G}}\Rightarrow\mathbf{Ax}$. 2. 2.

$\mathbf{D2^{G}}$* and $\mathbf{Ax}\Rightarrow\mathbf{PC^{G}}$.* 3. 3.

If $\Phi(x)$ satisfies $\mathbf{D1}$, then for any sentence $\varphi$, $S\vdash\mathsf{LogAx}(\ulcorner\varphi\urcorner)\to\Phi(\ulcorner\varphi\urcorner)$.

Proof.

1. This is because $\mathsf{PA}\vdash\forall x(\mathsf{LogAx}(x)\to\mathrm{Pr}_{\emptyset}(x))$.

2. Let $\mathrm{Pr}_{\emptyset}^{\prime}(x)$ be a natural provability predicate of the predicate calculus formulated in Feferman’s framework. Then $\mathsf{PA}\vdash\forall x(\mathsf{Fml}(x)\to(\mathrm{Pr}_{\emptyset}(x)\to\mathrm{Pr}_{\emptyset}^{\prime}(x)))$ holds by induction inside $\mathsf{PA}$. Since $S$ proves that $\Phi(x)$ contains axioms of $\mathrm{Pr}_{\emptyset}^{\prime}(x)$ by $\mathbf{Ax}$ and that $\Phi(x)$ is closed under the inference rule of $\mathrm{Pr}_{\emptyset}^{\prime}(x)$ by $\mathbf{D2^{G}}$, $S$ proves $\forall x(\mathsf{Fml}(x)\to(\mathrm{Pr}_{\emptyset}^{\prime}(x)\to\Phi(x)))$ by induction inside $S$. Hence $S\vdash\forall x(\mathsf{Fml}(x)\to(\mathrm{Pr}_{\emptyset}(x)\to\Phi(x)))$ holds.

3. Let $\varphi$ be any sentence. If $\varphi$ is a logical axiom, then $T\vdash\varphi$. By $\mathbf{D1}$, $S\vdash\Phi(\ulcorner\varphi\urcorner)$. If $\varphi$ is not a logical axiom, then $S\vdash\neg\mathsf{LogAx}(\ulcorner\varphi\urcorner)$. In either case, we obtain $S\vdash\mathsf{LogAx}(\ulcorner\varphi\urcorner)\to\Phi(\ulcorner\varphi\urcorner)$. ∎

Montagna [19] proved that if $\Phi(x)$ satisfies $\mathbf{D1}$, $\mathbf{D2^{G}}$ and $\mathbf{Ax}$, then $\mathbf{D3}$ is redundant for a proof of Löb’s theorem. From Propositions 2.26 and 2.30, and Corollaries 2.15.2 and 2.28, we obtain the following improvement of Montagna’s result.

Corollary 2.31** (Montagna [19]).**

$\mathbf{D1}$, $\mathbf{D2^{G}}$ and $\mathbf{Ax}\Rightarrow\mathbf{D1^{U}}$ and $\mathbf{\Sigma_{1}C^{G}}$. 2. 2.

If $\Phi(x)$ is a $\Sigma_{1}$ formula satisfying $\mathbf{D1}$, $\mathbf{D2^{G}}$ and $\mathbf{Ax}$, then $T\nvdash\mathsf{Con}_{\Phi}^{G}$.

3 Proof of Theorem 2.20

In this section, we prove Theorem 2.20, that is, we prove that if $\Phi(x)$ satisfies $\mathbf{D1}$ and $\mathbf{B_{2}^{U}}$, then $\Phi(x)$ satisfies $\mathbf{\Sigma_{1}C^{U}}$. Thus in the rest of this section, we fix a formula $\Phi(x)$ satisfying $\mathbf{D1}$ and $\mathbf{B_{2}^{U}}$. Then by Corollary 2.15.1, $\Phi(x)$ also satisfies $\mathbf{D1^{U}}$. First, we prove a lemma, that is an essential application of the condition $\mathbf{B_{2}^{U}}$.

Lemma 3.1**.**

Let $\varphi(\vec{x})$ and $\psi(\vec{x})$ be any formulas. If $S\vdash\varphi(\vec{x})\to\Phi(\ulcorner\varphi(\vec{\dot{x}})\urcorner)$ and $\mathsf{PA}\vdash\varphi(\vec{x})\leftrightarrow\psi(\vec{x})$, then $S\vdash\psi(\vec{x})\to\Phi(\ulcorner\psi(\vec{\dot{x}})\urcorner)$.

Proof.

If $\mathsf{PA}\vdash\varphi(\vec{x})\leftrightarrow\psi(\vec{x})$, then by $\mathbf{B_{2}^{U}}$, we have

[TABLE]

Then the lemma follows immediately. ∎

We may assume that every $\Sigma_{1}$ $\mathcal{L}_{A}$-formula is $\mathsf{PA}$-provably equivalent to some $\Sigma_{1}$ formula written in the language $\{0,\mathsf{s},+,\times\}$. Therefore, in proving Theorem 2.20, it suffices to show $S\vdash\sigma(\vec{x})\to\Phi(\ulcorner\sigma(\vec{\dot{x}})\urcorner)$ for any $\Sigma_{1}$ formula $\sigma(\vec{x})$ in the language $\{0,\mathsf{s},+,\times\}$. Hence in the rest of this section, we assume that our terms and formulas are written in $\{0,\mathsf{s},+,\times\}$. Before proving Theorem 2.20, we prepare several lemmas.

Lemma 3.2**.**

For any formula $\varphi(\vec{y},v)$,

[TABLE]

where $\ulcorner\varphi(\vec{\dot{y}},\dot{v})\urcorner[\mathsf{s}(x)/v]$ is the result of substituting $\mathsf{s}(x)$ for $v$ of $\ulcorner\varphi(\vec{\dot{y}},\dot{v})\urcorner$.

Proof.

This is because our numeral $\overline{n}$ is defined by applying $\mathsf{s}$ to [math] $n$ times. Then the lemma can be proved by induction on the constructions of terms and formulas. We give only an outline of a proof.

For example, we assume that our Gödel number $\mathsf{gn}(t)$ of a term $t$ is defined so that $\mathsf{gn}(\mathsf{s}(t))=\langle 0,\mathsf{gn}(t)\rangle$, where $\langle\cdot,\cdot\rangle$ is a primitive recursive paring function. Then we can define a primitive recursive function $\mathsf{num}(x)$ calculating $n\mapsto\mathsf{gn}(\overline{n})$ satisfying $\mathsf{num}(\mathsf{s}(x))=\langle 0,\mathsf{num}(x)\rangle$. This is proved in $\mathsf{PA}$ and corresponds to $\ulcorner\dot{v}\urcorner[\mathsf{s}(x)/v]=\ulcorner\mathsf{s}(\dot{x})\urcorner$. Then by using properties of $\ulcorner\cdot\urcorner$ such as $\mathsf{PA}\vdash\ulcorner\mathsf{s}(t)\urcorner=\langle 0,\ulcorner t\urcorner\rangle$, we can show $\mathsf{PA}\vdash\ulcorner t(\vec{\dot{y}},\dot{v})\urcorner[\mathsf{s}(x)/v]=\ulcorner t(\vec{\dot{y}},\mathsf{s}(\dot{x}))\urcorner$ for any term $t(\vec{y},v)$. Then we can prove the lemma by using properties of $\ulcorner\cdot\urcorner$. ∎

Lemma 3.3**.**

Let $\varphi(\vec{x},v)$ be any formula. If $S\vdash\varphi(\vec{x},v)\to\Phi(\ulcorner\varphi(\vec{\dot{x}},\dot{v})\urcorner)$, then $S\vdash\exists v\varphi(\vec{x},v)\to\Phi(\ulcorner\exists v\varphi(\vec{\dot{x}},v)\urcorner)$.

Proof.

Suppose $S\vdash\varphi(\vec{x},v)\to\Phi(\ulcorner\varphi(\vec{\dot{x}},\dot{v})\urcorner)$. Since $T\vdash\varphi(\vec{x},v)\to\exists v\varphi(\vec{x},v)$, we have $S\vdash\Phi(\ulcorner\varphi(\vec{\dot{x}},\dot{v})\urcorner)\to\Phi(\ulcorner\exists v\varphi(\vec{\dot{x}},v)\urcorner)$ by $\mathbf{B_{2}^{U}}$. Hence $S\vdash\varphi(\vec{x},v)\to\Phi(\ulcorner\exists v\varphi(\vec{\dot{x}},v)\urcorner)$. Therefore we conclude $S\vdash\exists v\varphi(\vec{x},v)\to\Phi(\ulcorner\exists v\varphi(\vec{\dot{x}},v)\urcorner)$. ∎

Lemma 3.4**.**

For any natural number $k$ and any variables $x_{0},\ldots,x_{k},z_{0},\ldots,z_{k}$,

[TABLE]

Proof.

Since $T\vdash\bigwedge_{i\leq k}(z_{i}=z_{i})$, we have

[TABLE]

by $\mathbf{D1^{U}}$. Let $v_{0},\ldots,v_{k}$ be fresh variables. By equality axioms of predicate calculus, we have

[TABLE]

By substituting $z_{i}$ for $v_{i}$, we obtain

[TABLE]

By combining this with (2), we now obtain

[TABLE]

∎

For each term $t(\vec{x})$, let $c(t(\vec{x}))$ be the number of constant and function symbols contained in $t(\vec{x})$. We call $c(t(\vec{x}))$ the complexity of $t(\vec{x})$.

Lemma 3.5**.**

For any finite sequence $\{t_{i}(\vec{x})\}_{i\leq k}$ of terms with $\max_{i\leq k}\{c(t_{i}(\vec{x}))\}\leq 1$,

[TABLE]

Proof.

We prove by induction on the number $m$ of terms of complexity $1$ in such sequences. If a sequence does not contain terms of complexity $1$, then it consists of variables, and hence the lemma holds for the sequence by Lemma 3.4.

Suppose that the lemma holds for such sequences with exactly $m$ terms of complexity $1$. Let $\{t_{i}(\vec{x})\}_{i\leq k}$ be any finite sequence consists of terms of complexity less than or equal to $1$ and having exactly $m+1$ terms of complexity $1$. We may assume that $c(t_{k})=1$. Let $\xi(\vec{v}):\equiv\bigwedge_{i<k}(z_{i}=t_{i}(\vec{x}))$. We distinguish the following four cases.

Case 1: $t_{k}(\vec{x})$ is [math]. Then by induction hypothesis,

[TABLE]

By substituting [math] for $y$, we obtain

[TABLE]

Since [math] is a numeral, we have

[TABLE]

Case 2: $t_{k}(\vec{x})$ is $\mathsf{s}(x)$. By induction hypothesis,

[TABLE]

By substituting $\mathsf{s}(x)$ for $y$, we obtain

[TABLE]

By Lemma 3.2, we conclude

[TABLE]

Case 3: $t_{k}(\vec{x})$ is $x+y$. Let $\varphi(y)$ be the formula

[TABLE]

By induction hypothesis,

[TABLE]

Since $\mathsf{PA}\vdash x=x+0$, we have $\mathsf{PA}\vdash(\xi(\vec{v})\land z_{k}=x)\leftrightarrow(\xi(\vec{v})\land z_{k}=x+0)$. Then by Lemma 3.1,

[TABLE]

This means $S\vdash\varphi(0)$.

By Lemma 3.2, we get

[TABLE]

Since $\mathsf{PA}\vdash\mathsf{s}(x)+y=x+\mathsf{s}(y)$, we obtain

[TABLE]

by Lemma 3.1. Then $S\vdash\varphi(y)\to\varphi(\mathsf{s}(y))$. By induction axiom, we conclude $S\vdash\forall y\varphi(y)$.

Case 4: $t_{k}(\vec{x})$ is $x\times y$. Let $\psi(y)$ be the formula

[TABLE]

By induction hypothesis,

[TABLE]

Since $\mathsf{PA}\vdash w=x\times 0+w$, we have

[TABLE]

by Lemma 3.1. Therefore $S\vdash\psi(0)$.

Let $\rho(w)$ be the formula

[TABLE]

Then as in Case 3, we can prove $S\vdash\psi(y)\to\rho(0)$ and $S\vdash\rho(w)\to\rho(\mathsf{s}(w))$. Hence $S\vdash\psi(y)\to\forall w\rho(w)$. Then

[TABLE]

Since $\mathsf{PA}\vdash x\times y+(x+w)=x\times\mathsf{s}(y)+w$, we get

[TABLE]

by Lemma 3.1. Thus $S\vdash\psi(y)\to\psi(\mathsf{s}(y))$, and hence $S\vdash\forall y\psi(y)$. By substituting [math] for $w$ in $\psi(y)$, we obtain

[TABLE]

Then the required conclusion follows from Lemma 3.1. ∎

Lemma 3.6**.**

For any finite sequence $\{t_{i}(\vec{x})\}_{i\leq k}$ of terms,

[TABLE]

Proof.

We prove by induction on $\max_{i\leq k}\{c(t_{i}(\vec{x}))\}$. If $\max_{i\leq k}\{c(t_{i}(\vec{x}))\}\leq 1$, then the lemma follows from Lemma 3.5.

Suppose that the lemma holds for every finite sequence $\{t_{i}(\vec{x})\}_{i\leq k}$ of terms with $\max_{i\leq k}\{c(t_{i}(\vec{x}))\}=n\geq 1$. Then we show that the lemma holds for all finite sequences $\{t_{i}(\vec{x})\}_{i\leq k}$ containing only terms of complexity less than or equal to $n+1$.

As in our proof of Lemma 3.5, this is proved by induction on the number $m$ of terms of complexity $n+1$ in such sequences. If $m=0$, then the lemma follows from induction hypothesis. Then assume that the lemma holds for such sequences with exactly $m$ terms of complexity $n+1$.

Let $\{t_{i}\}_{i\leq k}$ be any finite sequence consists of terms of complexity less than or equal to $n+1$ and having exactly $m+1$ terms of complexity $n+1$. We may assume that $c(t_{k})=n+1$. Let $\xi(\vec{v}):\equiv\bigwedge_{i<k}(z_{i}=t_{i}(\vec{x}))$. We give only a proof of the case that $t_{k}(\vec{x})$ is $\mathsf{s}(t^{\prime}(\vec{x}))$ for some term $t^{\prime}(\vec{x})$ of complexity $n$. Other cases are proved in a similar way.

Notice that $c(\mathsf{s}(w))=1\leq n$ and $c(t^{\prime}(\vec{x}))=n$. Then by induction hypothesis,

[TABLE]

Since $\mathsf{PA}\vdash\exists w(\xi(\vec{v})\land z_{k}=\mathsf{s}(w)\land w=t^{\prime}(\vec{x}))\leftrightarrow(\xi(\vec{v})\land z_{k}=\mathsf{s}(t^{\prime}(\vec{x})))$, we obtain

[TABLE]

by Lemmas 3.4 and 3.1. ∎

Notice that each atomic formula $t_{0}=t_{1}$ is equivalent to $\exists z(z=t_{0}\land z=t_{1})$, and each negated atomic formula $t_{0}\neq t_{1}$ is $\mathsf{PA}$-equivalent to $\exists z_{0}\exists z_{1}(t_{0}+\mathsf{s}(z_{0})=t_{1}\lor t_{1}+\mathsf{s}(z_{1})=t_{0})$. Then we obtain the following lemma.

Lemma 3.7**.**

For any quantifier-free formula $\xi(\vec{x})$, there exists a quantifier-free formula $\delta(\vec{x},\vec{y})$ satisfying the following conditions:

$\mathsf{PA}\vdash\forall\vec{x}(\xi(\vec{x})\leftrightarrow\exists\vec{y}\delta(\vec{x},\vec{y}))$. 2. 2.

$\delta(\vec{x},\vec{y})$* is of the form $\delta_{0}(\vec{x},\vec{y})\lor\cdots\lor\delta_{k}(\vec{x},\vec{y})$ and each disjunct $\delta_{i}(\vec{x},\vec{y})$ is of the form*

[TABLE]

for some terms $t_{i,0}(\vec{x},\vec{y}),\ldots,t_{i,l_{i}}(\vec{x},\vec{y})$ and variables $z_{i,0},\ldots,z_{i,l_{i}}\in\vec{x},\vec{y}$.

Also in our proof of Theorem 2.20, we use the following $\mathsf{PA}$-provable form of the MRDP theorem.

Theorem 3.8** (The MRDP theorem (see [14])).**

For any $\Sigma_{1}$ formula $\varphi(\vec{x})$, there exists a quantifier-free formula $\delta(\vec{x},\vec{y})$ such that $\mathsf{PA}\vdash\forall\vec{x}(\varphi(\vec{x})\leftrightarrow\exists\vec{y}\delta(\vec{x},\vec{y}))$.

Proof of Theorem 2.20.

Let $\sigma(\vec{x})$ be any $\Sigma_{1}$ formula. We would like to prove $S\vdash\forall\vec{x}(\sigma(\vec{x})\to\Phi(\ulcorner\sigma(\vec{\dot{x}})\urcorner))$. By the MRDP theorem (Theorem 3.8), there exists a quantifier-free formula $\delta(\vec{x},\vec{y})$ such that $\mathsf{PA}\vdash\forall\vec{x}(\sigma(\vec{x})\leftrightarrow\exists\vec{y}\delta(\vec{x},\vec{y}))$. By Lemma 3.7, we may assume that $\delta(\vec{x},\vec{y})$ is of the form indicated in the statement of Lemma 3.7. For each $i\leq k$, by Lemma 3.6, we obtain

[TABLE]

This means

[TABLE]

Since $\mathsf{PA}\vdash\delta_{i}(\vec{x},\vec{y})\to\delta(\vec{x},\vec{y})$, $S\vdash\Phi(\ulcorner\delta_{i}(\vec{\dot{x}},\vec{\dot{y}})\urcorner)\to\Phi(\ulcorner\delta(\vec{\dot{x}},\vec{\dot{y}})\urcorner)$ by $\mathbf{B_{2}^{U}}$. Therefore by (3), $S\vdash\delta_{i}(\vec{x},\vec{y})\to\Phi(\ulcorner\delta(\vec{\dot{x}},\vec{\dot{y}})\urcorner)$. Since $i\leq k$ is arbitrary, we have $S\vdash\delta_{0}(\vec{x},\vec{y})\lor\cdots\lor\delta_{k}(\vec{x},\vec{y})\to\Phi(\ulcorner\delta(\vec{\dot{x}},\vec{\dot{y}})\urcorner)$. It follows $S\vdash\delta(\vec{x},\vec{y})\to\Phi(\ulcorner\delta(\vec{\dot{x}},\vec{\dot{y}})\urcorner)$. By Lemmas 3.4 and 3.1, we conclude $S\vdash\sigma(\vec{x})\to\Phi(\ulcorner\sigma(\vec{\dot{x}})\urcorner)$. ∎

4 Witnesses for non-implications

In this section, we exhibit examples of formulas $\Phi(x)$ satisfying and not satisfying certain conditions. From these examples, several non-implications between conditions are concluded.

Our first two propositions give examples of formulas which do not satisfy $\mathbf{D1}$. Proofs are easy and we omit them.

Proposition 4.1**.**

Let $\mathrm{Pr}_{\mathsf{Q}}(x)$ be the provability predicate of Robinson’s arithmetic $\mathsf{Q}$.

$\mathrm{Pr}_{\mathsf{Q}}(x)$* satisfies $\mathbf{D2^{G}}$, $\mathbf{\Sigma_{1}C^{G}}$, $\mathbf{CB}$ and $\mathbf{PC^{G}}$.* 2. 2.

$\mathrm{Pr}_{\mathsf{Q}}(x)$* satisfies neither $\mathbf{D1}$ nor $\mathbf{B_{2}}$.* 3. 3.

$\mathsf{PA}\vdash\mathsf{Con}_{\mathrm{Pr}_{\mathsf{Q}}}^{H}$.

Proposition 4.2**.**

Let $\Psi(x):\equiv x\neq x$.

$\Psi(x)$* satisfies $\mathbf{D2^{G}}$, $\mathbf{D3^{G}}$, $\mathbf{B_{2}^{U}}$ and $\mathbf{CB}$.* 2. 2.

$\Psi(x)$* does not satisfy any of $\mathbf{D1}$, $\mathbf{\Delta_{0}C}$ and $\mathbf{PC}$.* 3. 3.

$\mathsf{PA}\vdash\mathsf{Con}_{\Psi}^{H}$.

Feferman [7] proved there exists a $\Pi_{1}$ numeration $\pi(v)$ of $T$ in $T$ such that $\mathsf{Con}_{\mathrm{Pr}_{\pi}}^{H}$ is provable in $\mathsf{PA}$.

Fact 4.3** (Feferman [7]).**

Suppose $S=T$.

$\mathrm{Pr}_{\pi}(x)$* is a $\Sigma_{2}$ provability predicate satisfying $\mathbf{D1^{U}}$, $\mathbf{D2^{G}}$, $\mathbf{B_{2}^{U}}$, $\mathbf{\Sigma_{1}C^{G}}$, $\mathbf{CB}$ and $\mathbf{PC^{G}}$.* 2. 2.

$\mathrm{Pr}_{\pi}(x)$* does not satisfy $\mathbf{D3}$.* 3. 3.

$\mathsf{PA}\vdash\mathsf{Con}_{\mathrm{Pr}_{\pi}}^{H}$.

Mostowski (p. 24 in [20]) introduced the formula $\mathrm{Pr}_{T}^{M}(x):\equiv\exists y(\mathrm{Prf}_{T}(x,y)\land\neg\mathrm{Prf}_{T}(\ulcorner 0\neq 0\urcorner,y))$ as an example of a $\Sigma_{1}$ provability predicate for which the second incompleteness theorem does not hold. Notice that $\mathrm{Pr}_{T}^{M}(x)$ is $\mathsf{PA}$-provably equivalent to $\Pr_{T}(x)\land x\neq\ulcorner 0\neq 0\urcorner$ because $\mathsf{PA}\vdash\forall x_{0}\forall x_{1}\forall y(\mathrm{Prf}_{T}(x_{0},y)\land\mathrm{Prf}_{T}(x_{1},y)\to x_{0}=x_{1}$). The following proposition shows the situation for $\mathrm{Pr}_{T}^{M}(x)$.

Proposition 4.4**.**

$\mathrm{Pr}_{T}^{M}(x)$* is a $\Sigma_{1}$ provability predicate satisfying $\mathbf{D1^{U}}$, $\mathbf{\Sigma_{1}C^{G}}$ and $\mathbf{PC^{G}}$.* 2. 2.

$\mathrm{Pr}_{T}^{M}(x)$* does not satisfy any of $\mathbf{D2}$, $\mathbf{B_{2}}$ and $\mathbf{CB}$.* 3. 3.

$\mathsf{PA}\vdash\mathsf{Con}_{\mathrm{Pr}_{T}^{M}}^{L}$* and $T\nvdash\mathsf{Con}_{\mathrm{Pr}_{T}^{M}}^{H}$.*

The existence of Rosser provability predicates satisfying some derivability conditions were discussed by Bernardi and Montagna [4] and Arai [1]. They proved that there exists a Rosser provability predicate satisfying $\mathbf{D2^{G}}$. Also Arai proved the existence of a Rosser provability predicate satisfying $\mathbf{D3^{G}}$. Strictly speaking, in Arai’s arguments, formulas are assumed to be in negation normal form (see [1]). We fix a natural algorithm calculating a negation normal form $\mathsf{nnf}(\varphi)$ of each formula $\varphi$ satisfying $\mathsf{nnf}(\neg\neg\varphi)\equiv\mathsf{nnf}(\varphi)$. Then we can understand that Arai’s Rosser provability predicates $\mathrm{Pr}^{A}(x)$ are of the form $\exists y(\mathrm{Prf}(\mathsf{nnf}(x),y)\land\forall z\leq y\neg\mathrm{Prf}(\mathsf{nnf}(\dot{\neg}x),z))$ for some suitable proof predicate $\mathrm{Prf}(x,y)$. Then $\mathsf{PA}\vdash\mathsf{Con}_{\mathrm{Pr}^{A}}^{H}$ always holds. Summarizing this observation, Arai’s results are stated as follows.

Fact 4.5** (Arai [1]).**

There exist $\Sigma_{1}$ provability predicates $\mathrm{Pr}^{A}_{1}(x)$ and $\mathrm{Pr}^{A}_{2}(x)$ of $T$ with:

$\mathrm{Pr}^{A}_{1}(x)$* satisfies $\mathbf{D1}$, $\mathbf{D2^{G}}$ and $\mathsf{PA}\vdash\mathsf{Con}_{\mathrm{Pr}^{A}_{1}}^{H}$.* 2. 2.

$\mathrm{Pr}^{A}_{2}(x)$* satisfies $\mathbf{D1}$, $\mathbf{D3^{G}}$ and $\mathsf{PA}\vdash\mathsf{Con}_{\mathrm{Pr}^{A}_{2}}^{H}$.*

By Proposition 2.4.4, $\mathrm{Pr}^{A}_{1}(x)$ satisfies $\mathbf{B_{2}}$. By Theorems 2.7 and 2.20, and Propositions 2.4, 2.13 and 2.14, $\mathrm{Pr}^{A}_{1}(x)$ does not satisfy any of $\mathbf{D1^{U}}$, $\mathbf{CB}$, $\mathbf{B_{2}^{U}}$, $\mathbf{D3}$ and $\mathbf{PC}$. By Theorems 2.8, 2.9 and 2.10 and Proposition 2.4.4, $\mathrm{Pr}^{A}_{2}(x)$ does not satisfy any of $\mathbf{D2}$, $\mathbf{B_{2}}$, $\mathbf{\Sigma_{1}C}$ and $\mathbf{PC}$.

In [16], the author proved the existence of usual Rosser provability predicates satisfying additional derivability conditions. That is to say,

Fact 4.6** (Kurahashi [16]).**

Suppose $S=T$. There exist $\Sigma_{1}$ provability predicates $\mathrm{Pr}_{1}^{R}(x)$, $\mathrm{Pr}_{2}^{R}(x)$ and $\mathrm{Pr}_{3}^{R}(x)$ of $T$ with:

$\mathrm{Pr}_{1}^{R}(x)$* satisfies $\mathbf{D1}$, $\mathbf{D2^{G}}$, $\mathbf{\Delta_{0}C^{G}}$ and $\mathsf{PA}\vdash\mathsf{Con}_{\mathrm{Pr}_{1}^{R}}^{H}$.* 2. 2.

$\mathrm{Pr}_{2}^{R}(x)$* satisfies $\mathbf{D1^{U}}$, $\mathbf{CB}$, $\mathbf{D2}$, $\mathbf{\Delta_{0}C^{G}}$ and $\mathsf{PA}\vdash\mathsf{Con}_{\mathrm{Pr}_{2}^{R}}^{L}$.* 3. 3.

$\mathrm{Pr}_{3}^{R}(x)$* satisfies $\mathbf{D1^{U}}$, $\mathbf{CB}$, $\mathbf{B_{2}}$, $\mathbf{D3^{G}}$, $\mathbf{\Delta_{0}C^{G}}$ and $\mathsf{PA}\vdash\mathsf{Con}_{\mathrm{Pr}_{3}^{R}}^{L}$, but does not satisfy $\mathbf{\Sigma_{1}C}$.*

As in Fact 4.5.1, $\mathrm{Pr}_{1}^{R}(x)$ satisfies $\mathbf{B_{2}}$, but does not satisfy any of $\mathbf{D1^{U}}$, $\mathbf{CB}$, $\mathbf{B_{2}^{U}}$, $\mathbf{D3}$ and $\mathbf{PC}$. By Proposition 2.4.4, $\mathrm{Pr}_{2}^{R}(x)$ satisfies $\mathbf{B_{2}}$, but does not satisfy any of $\mathbf{D2^{U}}$, $\mathbf{D3}$, $\mathbf{B_{2}^{U}}$ and $\mathbf{PC}$ by Theorems 2.7 and 2.20, and Propositions 2.4.6 and 2.13.3. By Theorems 2.7 and 2.20 and Proposition 2.4, $\mathrm{Pr}_{3}^{R}(x)$ does not satisfy any of $\mathbf{D2}$, $\mathbf{B_{2}^{U}}$ and $\mathbf{PC}$.

In the remainder of this section, we introduce seven $\Sigma_{1}$ provability predicates $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$, $\mathrm{Pr}_{T}^{\mathrm{II}}(x)$, $\mathrm{Pr}_{T}^{\mathrm{III}}(x)$, $\mathrm{Pr}_{T}^{\mathrm{IV}}(x)$, $\mathrm{Pr}_{T}^{\mathrm{V}}(x)$, $\mathrm{Pr}_{T}^{\mathrm{VI}}(x)$ and $\mathrm{Pr}^{\ast}(x)$ which indicate several non-implications of the conditions. The first three provability predicates are constructed in a similar way. Before introducing them, we prepare a definition and a lemma.

Definition 4.7**.**

Let $\delta(x,z)$ be a $\Delta_{1}$ formula.

$\mathrm{Prf}_{T}[\delta](x,y):\equiv\mathrm{Prf}_{T}(x,y)\land\forall z<y(\mathrm{Prf}_{T}(\ulcorner 0\neq 0\urcorner,z)\to\delta(x,z))$. 2. 2.

$\mathrm{Pr}_{T}[\delta](x):\equiv\exists y\mathrm{Prf}_{T}[\delta](x,y)$.

Lemma 4.8**.**

For any $\Delta_{1}$ formula $\delta(x,z)$,

$\mathrm{Pr}_{T}[\delta](x)$* is a $\Sigma_{1}$ provability predicate of $T$.* 2. 2.

$\mathsf{PA}\vdash\forall x(\forall z(\mathrm{Prf}_{T}(\ulcorner 0\neq 0\urcorner,z)\to\delta(x,z))\to(\mathrm{Pr}_{T}(x)\leftrightarrow\mathrm{Pr}_{T}[\delta](x)))$. 3. 3.

If $\mathsf{PA}\vdash\forall x\forall z(\mathsf{Fml}(x)\land x\leq z\to\delta(x,z))$, then

[TABLE]

Proof.

1. Let $\varphi$ be any formula and let $n$ be any natural number. Since $\mathsf{PA}\vdash\forall z<\overline{n}\neg\mathrm{Prf}_{T}(\ulcorner 0\neq 0\urcorner,z)$, $\mathsf{PA}\vdash\mathrm{Prf}_{T}(\ulcorner\varphi\urcorner,\overline{n})\leftrightarrow\mathrm{Prf}_{T}[\delta](\ulcorner\varphi\urcorner,\overline{n})$. Since this equivalence is true in the standard model of arithmetic, we obtain that $\mathsf{PA}\vdash\mathrm{Pr}_{T}(\ulcorner\varphi\urcorner)$ if and only if $\mathsf{PA}\vdash\mathrm{Pr}_{T}[\delta](\ulcorner\varphi\urcorner)$. It follows that $\mathrm{Pr}_{T}[\delta](x)$ is also a $\Sigma_{1}$ provability predicate of $T$.

2. This is immediate from the definition.

3. Suppose $\mathsf{PA}\vdash\forall x\forall z(\mathsf{Fml}(x)\land x\leq z\to\delta(x,z))$. By the definition of $\mathrm{Prf}_{T}[\delta](x,y)$,

[TABLE]

Since $\mathsf{PA}\vdash\mathrm{Prf}_{T}[\delta](x,y)\to\mathrm{Prf}_{T}(x,y)$ and $\mathsf{PA}\vdash\mathrm{Prf}_{T}(x,y)\to x\leq y$, we have $\mathsf{PA}\vdash\mathrm{Prf}_{T}[\delta](x,y)\to x\leq y$. Thus $\mathsf{PA}\vdash\mathrm{Prf}_{T}[\delta](x,y)\land y\leq z\to x\leq z$. By the supposition, $\mathsf{PA}\vdash\mathsf{Fml}(x)\land\mathrm{Prf}_{T}[\delta](x,y)\land y\leq z\to\delta(x,z)$. From this with (4), we obtain

[TABLE]

and hence

[TABLE]

∎

Let $\mathsf{Even}(x)$ be a natural $\Delta_{1}$ formula saying that “$x$ is the Gödel number of a formula containing an even number of logical symbols”. Proposition 4.9 shows that full local derivability conditions do not imply uniform derivability conditions.

Proposition 4.9**.**

There exists a $\Sigma_{1}$ provability predicate $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$ of $T$ with:

$\mathrm{Pr}_{T}^{\mathrm{I}}(x)$* satisfies $\mathbf{D1}$, $\mathbf{D2}$ and $\mathbf{\Sigma_{1}C}$.* 2. 2.

$\mathrm{Pr}_{T}^{\mathrm{I}}(x)$* does not satisfy any of $\mathbf{D1^{U}}$, $\mathbf{D2^{U}}$, $\mathbf{D3^{U}}$, $\mathbf{\Delta_{0}C^{U}}$ and $\mathbf{PC^{U}}$.*

Proof.

Let $\mathrm{Pr}_{T}^{\mathrm{I}}(x):\equiv\mathrm{Pr}_{T}[x\leq z\lor\mathsf{Even}(x)](x)$. Then $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$ is a $\Sigma_{1}$ provability predicate of $T$ by Lemma 4.8.1. If $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$ contains an even number of logical symbols, we replace $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$ with $\mathrm{Pr}_{T}^{\mathrm{I}}(x)\land 0=0$. Then $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$ contains an odd number of logical symbols, and hence $\mathsf{PA}\vdash\forall x\neg\mathsf{Even}(\ulcorner\mathrm{Pr}_{T}^{\mathrm{I}}(\dot{x})\urcorner)$.

Let $\varphi$ be any formula. Since $\mathsf{PA}\vdash\forall z(\mathrm{Prf}_{T}(\ulcorner 0\neq 0\urcorner,z)\to\ulcorner\varphi\urcorner\leq z\lor\mathsf{Even}(\ulcorner\varphi\urcorner))$, we have $\mathsf{PA}\vdash\mathrm{Pr}_{T}(\ulcorner\varphi\urcorner)\leftrightarrow\mathrm{Pr}_{T}^{\mathrm{I}}(\ulcorner\varphi\urcorner)$ by Lemma 4.8.2. Therefore local derivability conditions for $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$ are inherited from those for $\mathrm{Pr}_{T}(x)$.

We prove that $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$ does not satisfy any of uniform derivability conditions. Since $\mathsf{PA}\vdash\forall x\forall z(\mathsf{Fml}(x)\land x\leq z\to(x\leq z\lor\mathsf{Even}(x)))$,

[TABLE]

by Lemma 4.8.3. For the sake of simplicity, we deal with formulas whose only free variable is $x$. Let $\varphi(x)$ be such a formula. Then

[TABLE]

Since $\mathsf{PA}\vdash x\leq\ulcorner\varphi(\dot{x})\urcorner$, we obtain

[TABLE]

• •

Since $\mathsf{PA}\vdash\forall x\neg\mathsf{Even}(\ulcorner 0=0\land\dot{x}=\dot{x}\urcorner)$,

[TABLE]

by (5). Hence $\mathsf{PA}\vdash\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)\to\exists x\neg\mathrm{Pr}_{T}^{\mathrm{I}}(\ulcorner 0=0\land\dot{x}=\dot{x}\urcorner)$ because $\mathsf{PA}\vdash\forall z\exists x(x>z)$. It follows $S\nvdash\forall x\mathrm{Pr}_{T}^{\mathrm{I}}(\ulcorner 0=0\land\dot{x}=\dot{x}\urcorner)$ because $S\nvdash\neg\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)$. This shows that $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$ does not satisfy $\mathbf{D1^{U}}$.

• •

Let $\varphi(x)$ and $\psi(x)$ be formulas with $\mathsf{PA}\vdash\forall x\mathsf{Even}(\ulcorner\varphi(\dot{x})\urcorner)\land\forall x\neg\mathsf{Even}(\ulcorner\psi(\dot{x})\urcorner)$. Then $\mathsf{PA}\vdash\forall x\mathsf{Even}(\ulcorner\varphi(\dot{x})\to\psi(\dot{x})\urcorner)$. Since $\mathsf{PA}\vdash\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)\to\mathrm{Pr}_{T}(\ulcorner\varphi(\dot{x})\to\psi(\dot{x})\urcorner)\land\mathrm{Pr}_{T}(\ulcorner\varphi(\dot{x})\urcorner)$, we have

[TABLE]

by the choice of $\varphi(x)$ and $\psi(x)$, and the definition of $\mathrm{Prf}_{T}^{\mathrm{I}}(x,y)$. Suppose, towards a contradiction, that $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$ satisfies $\mathbf{D2^{U}}$, then $S\vdash\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)\to\mathrm{Pr}_{T}^{\mathrm{I}}(\ulcorner\psi(\dot{x})\urcorner)$. By (5), $S\vdash\mathrm{Prf}_{T}(\ulcorner 0\neq 0\urcorner,z)\to(x\leq z\lor\mathsf{Even}(\ulcorner\psi(\dot{x})\urcorner))$, and hence $S\vdash\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)\to\exists x\mathsf{Even}(\ulcorner\psi(\dot{x})\urcorner)$. By the choice of $\psi(x)$, we obtain $S\vdash\neg\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)$. This is a contradiction. Therefore $\mathbf{D2^{U}}$ does not hold for $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$.

• •

Let $\varphi(x)$ be a formula with $\mathsf{PA}\vdash\forall x\mathsf{Even}(\ulcorner\varphi(\dot{x})\urcorner)$. Then $\mathsf{PA}\vdash\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)\to\mathrm{Pr}_{T}^{\mathrm{I}}(\ulcorner\varphi(\dot{x})\urcorner)$ as described above. Suppose that $\mathbf{D3^{U}}$ holds for $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$. Then $S\vdash\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)\to\mathrm{Pr}_{T}^{\mathrm{I}}(\ulcorner\mathrm{Pr}_{T}^{\mathrm{I}}(\ulcorner\varphi(\dot{x})\urcorner)\urcorner)$. By (5), we have $S\vdash\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)\to\exists x\mathsf{Even}(\ulcorner\mathrm{Pr}_{T}^{\mathrm{I}}(\ulcorner\varphi(\dot{x})\urcorner)\urcorner)$. Since $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$ contains an odd number of logical symbols, $\neg\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)$ is proved in $S$, and this is a contradiction. Hence $\mathbf{D3^{U}}$ does not hold for $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$.

• •

As described above, $\mathsf{PA}\vdash\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)\to\exists x\neg\mathrm{Pr}_{T}^{\mathrm{I}}(\ulcorner 0=0\land\dot{x}=\dot{x}\urcorner)$. If $S\vdash\forall x(0=0\land x=x\to\mathrm{Pr}_{T}^{\mathrm{I}}(\ulcorner 0=0\land\dot{x}=\dot{x}\urcorner))$, then $S\vdash\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)\to\exists x\neg(0=0\land x=x)$. This implies $S\vdash\neg\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)$, a contradiction. Therefore $S\nvdash\forall x(0=0\land x=x\to\mathrm{Pr}_{T}^{\mathrm{I}}(\ulcorner 0=0\land\dot{x}=\dot{x}\urcorner))$. This shows that $\mathbf{\Delta_{0}C^{U}}$ does not hold for $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$.

• •

$\mathbf{PC^{U}}$ fails to hold because $\mathsf{PA}\vdash\forall x\mathrm{Pr}_{\emptyset}(\ulcorner 0=0\land\dot{x}=\dot{x}\urcorner)$.

∎

By Proposition 2.4, $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$ satisfies $\mathbf{B_{2}}$, $\mathbf{D3}$ and $\mathbf{PC}$. Propositions 2.13.1 and 2.14.1 imply that $\mathrm{Pr}_{T}^{\mathrm{I}}(x)$ satisfies neither $\mathbf{B_{2}^{U}}$ nor $\mathbf{CB}$.

Next we prove that full uniform derivability conditions do not imply any of global derivability conditions except for $\mathbf{D3^{G}}$, and that full derivability conditions are not sufficient for the unprovability of $\mathsf{Con}_{\Phi}^{\Sigma_{1}}$ even if $\Phi\in\Sigma_{1}$.

Proposition 4.10**.**

There exists a $\Sigma_{1}$ provability predicate $\mathrm{Pr}_{T}^{\mathrm{II}}(x)$ of $T$ with:

$\mathrm{Pr}_{T}^{\mathrm{II}}(x)$* satisfies $\mathbf{D1^{U}}$, $\mathbf{D2^{U}}$, and $\mathbf{\Sigma_{1}C^{U}}$.* 2. 2.

$\mathrm{Pr}_{T}^{\mathrm{II}}(x)$* does not satisfy any of $\mathbf{D2^{G}}$, $\mathbf{\Delta_{0}C^{G}}$ and $\mathbf{PC^{G}}$.* 3. 3.

$\mathsf{PA}\vdash\mathsf{Con}_{\mathrm{Pr}_{T}^{\mathrm{II}}}^{\Sigma_{1}}$.

Proof.

For each formula $\varphi$, let $n(\varphi)$ be the number of occurrences of the symbol $\neg$ in $\varphi$. We may use a function symbol $n(x)$ corresponding to this function such that $\mathsf{PA}\vdash\forall x(\mathsf{Fml}(x)\to n(x)\leq x)$.

Let $\mathrm{Pr}_{T}^{\mathrm{II}}(x)$ be the $\Sigma_{1}$ formula $\mathrm{Pr}_{T}[n(x)\leq z\lor\mathsf{Even}(x)](x)$. Then $\mathrm{Pr}_{T}^{\mathrm{II}}(x)$ is a $\Sigma_{1}$ provability predicate of $T$ by Lemma 4.8.1. Let $\varphi(\vec{x})$ be any formula. Then $\mathsf{PA}\vdash\forall\vec{x}(n(\ulcorner\varphi(\vec{\dot{x}})\urcorner)=\overline{k})$ for some natural number $k$. Since $\mathsf{PA}\vdash\forall z(\mathrm{Prf}_{T}(\ulcorner 0\neq 0\urcorner,z)\to n(\ulcorner\varphi(\vec{\dot{x}})\urcorner)\leq z\lor\mathsf{Even}(\ulcorner\varphi(\vec{\dot{x}})\urcorner))$, we obtain $\mathsf{PA}\vdash\forall\vec{x}(\mathrm{Pr}_{T}(\ulcorner\varphi(\vec{\dot{x}})\urcorner)\leftrightarrow\mathrm{Pr}_{T}^{\mathrm{II}}(\ulcorner\varphi(\vec{\dot{x}})\urcorner))$ by Lemma 4.8.2. Therefore $\mathrm{Pr}_{T}^{\mathrm{II}}(x)$ satisfies $\mathbf{D1^{U}}$, $\mathbf{D2^{U}}$ and $\mathbf{\Sigma_{1}C^{U}}$.

By Lemma 4.8.3, we have

[TABLE]

because $\mathsf{PA}\vdash\forall x(\mathsf{Fml}(x)\land x\leq z\to n(x)\leq z\lor\mathsf{Even}(x))$.

As in Proposition 4.9, failure of $\mathbf{D2^{G}}$, $\mathbf{\Delta_{0}C^{G}}$ and $\mathbf{PC^{G}}$ for $\mathrm{Pr}_{T}^{\mathrm{II}}(x)$ follow from (6) and the facts $\mathsf{PA}\vdash\forall z\exists y(\mathsf{Fml}(y)\land n(y)>z\land\neg\mathsf{Even}(y))$, $\mathsf{PA}\vdash\forall z\exists y(\mathsf{True}_{\Delta_{0}}(y)\land n(y)>z\land\neg\mathsf{Even}(y))$ and $\mathsf{PA}\vdash\forall z\exists y(\mathrm{Pr}_{\emptyset}(y)\land n(y)>z\land\neg\mathsf{Even}(y))$, respectively.

We prove $\mathsf{PA}\vdash\mathsf{Con}_{\mathrm{Pr}_{T}^{\mathrm{II}}}^{\Sigma_{1}}$. By (6) and $\mathsf{PA}\vdash\forall z\exists x(\Sigma_{1}(x)\land\mathsf{Sent}(x)\land n(x)>z\land\neg\mathsf{Even}(x))$, we have

[TABLE]

It follows $\mathsf{PA}\vdash\mathrm{Pr}_{T}^{\mathrm{II}}(\ulcorner 0\neq 0\urcorner)\to\mathsf{Con}_{\mathrm{Pr}_{T}^{\mathrm{II}}}^{\Sigma_{1}}$. On the other hand, obviously $\mathsf{PA}\vdash\neg\mathrm{Pr}_{T}^{\mathrm{II}}(\ulcorner 0\neq 0\urcorner)\to\mathsf{Con}_{\mathrm{Pr}_{T}^{\mathrm{II}}}^{\Sigma_{1}}$. Therefore we conclude $\mathsf{PA}\vdash\mathsf{Con}_{\mathrm{Pr}_{T}^{\mathrm{II}}}^{\Sigma_{1}}$. ∎

From Propositions 2.13 and 2.14, $\mathrm{Pr}_{T}^{\mathrm{II}}(x)$ satisfies $\mathbf{B_{2}^{U}}$, $\mathbf{CB}$ and $\mathbf{PC^{U}}$. By Theorem 2.7, $T\nvdash\mathsf{Con}_{\mathrm{Pr}_{T}^{\mathrm{II}}}^{L}$.

We prove that the conditions $\Phi\in\Sigma_{1}$, $\mathbf{D1^{U}}$, $\mathbf{D2^{G}}$ and $\mathbf{\Sigma_{1}C^{G}}$ are not sufficient for the unprovability of Gödel’s consistency statement $\mathsf{Con}_{\Phi}^{G}$.

Proposition 4.11**.**

There exists a $\Sigma_{1}$ provability predicate $\mathrm{Pr}_{T}^{\mathrm{III}}(x)$ of $T$ with:

$\mathrm{Pr}_{T}^{\mathrm{III}}(x)$* satisfies $\mathbf{D1^{U}}$, $\mathbf{D2^{G}}$ and $\mathbf{\Sigma_{1}C^{G}}$.* 2. 2.

$\mathsf{PA}\vdash\mathsf{Con}_{\mathrm{Pr}_{T}^{\mathrm{III}}}^{G}$.

Proof.

Let $\mathrm{Pr}_{T}^{\mathrm{III}}(x)$ be the formula $\mathrm{Pr}_{T}[\Sigma_{z}(x)](x)$. Then by Lemma 4.8.1, $\mathrm{Pr}_{T}^{\mathrm{III}}(x)$ is a $\Sigma_{1}$ provability predicate of $T$. For any formula $\varphi(\vec{x})$, we have $\mathsf{PA}\vdash\forall z\forall\vec{x}(\mathrm{Prf}_{T}(\ulcorner 0\neq 0\urcorner,z)\to\Sigma_{z}(\ulcorner\varphi(\vec{\dot{x}})\urcorner))$ because $\mathsf{PA}\vdash\forall z\geq\overline{k}\Sigma_{z}(\ulcorner\varphi(\vec{\dot{x}})\urcorner)$ for some natural number $k$. Hence $\mathsf{PA}\vdash\mathrm{Pr}_{T}(\ulcorner\varphi(\vec{\dot{x}})\urcorner)\leftrightarrow\mathrm{Pr}_{T}^{\mathrm{III}}(\ulcorner\varphi(\vec{\dot{x}})\urcorner)$ by Lemma 4.8.2. Thus $\mathbf{D1^{U}}$ holds for $\mathrm{Pr}_{T}^{\mathrm{III}}(x)$.

Since $\mathsf{PA}\vdash\forall x\forall z(\mathsf{Fml}(x)\land x\leq z\to\Sigma_{z}(x))$, we have

[TABLE]

by Lemma 4.8.3. Then

[TABLE]

Thus

[TABLE]

By Lemma 4.8.2,

[TABLE]

Since $\mathsf{PA}\vdash\mathrm{Pr}_{T}^{\mathrm{III}}(x\dot{\to}y)\land\mathrm{Pr}_{T}^{\mathrm{III}}(x)\to\mathrm{Pr}_{T}(x\dot{\to}y)\land\mathrm{Pr}_{T}(x)$, we have

[TABLE]

by $\mathbf{D2^{G}}$ for $\mathrm{Pr}_{T}(x)$. From this with (8),

[TABLE]

This means $\mathbf{D2^{G}}$ holds for $\mathrm{Pr}_{T}^{\mathrm{III}}(x)$.

Since $\mathsf{PA}\vdash\mathsf{True}_{\Sigma_{1}}(x)\to\Sigma_{1}(x)$, $\mathsf{PA}\vdash\mathsf{True}_{\Sigma_{1}}(x)\to(\mathrm{Prf}_{T}(\ulcorner 0\neq 0\urcorner,z)\to\Sigma_{z}(x))$. By Lemma 4.8.2, $\mathsf{PA}\vdash\mathsf{True}_{\Sigma_{1}}(x)\to(\mathrm{Pr}_{T}(x)\leftrightarrow\mathrm{Pr}_{T}^{\mathrm{III}}(x))$. By $\mathbf{\Sigma_{1}C^{G}}$ for $\mathrm{Pr}_{T}(x)$, we obtain $\mathsf{PA}\vdash\mathsf{True}_{\Sigma_{1}}(x)\to\mathrm{Pr}_{T}^{\mathrm{III}}(x)$.

By (7) and $\mathsf{PA}\vdash\forall z\exists x(\mathsf{Fml}(x)\land\neg\Sigma_{z}(x))$, we have $\mathsf{PA}\vdash\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)\to\exists x(\mathsf{Fml}(x)\land\neg\mathrm{Pr}_{T}^{\mathrm{III}}(x))$. Thus $\mathsf{PA}\vdash\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)\to\mathsf{Con}_{\mathrm{Pr}_{T}^{\mathrm{III}}}^{G}$. On the other hand, since $\mathsf{PA}\vdash\neg\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)\to\neg\mathrm{Pr}_{T}^{\mathrm{III}}(\ulcorner 0\neq 0\urcorner)$, we have $\mathsf{PA}\vdash\neg\mathrm{Pr}_{T}(\ulcorner 0\neq 0\urcorner)\to\mathsf{Con}_{\mathrm{Pr}_{T}^{\mathrm{III}}}^{G}$. Therefore $\mathsf{PA}\vdash\mathsf{Con}_{\mathrm{Pr}_{T}^{\mathrm{III}}}^{G}$. ∎

By Propositions 2.13 and 2.14, $\mathrm{Pr}_{T}^{\mathrm{III}}(x)$ satisfies $\mathbf{B_{2}^{U}}$, $\mathbf{CB}$ and $\mathbf{PC^{U}}$. Corollary 2.28 implies that $\mathbf{PC^{G}}$ fails to hold for $\mathrm{Pr}_{T}^{\mathrm{III}}(x)$ and $T\nvdash\mathsf{Con}_{\mathrm{Pr}_{T}^{\mathrm{III}}}^{\Sigma_{1}}$.

We prove that there exists a $\Sigma_{1}$ provability predicate which satisfies the Hilbert–Bernays–Löb derivability conditions, but does not satisfy $\mathbf{\Sigma_{1}C}$. The following proof is based on the construction presented in Section 5 of Visser [24].

Proposition 4.12**.**

There exists a $\Sigma_{1}$ provability predicate $\mathrm{Pr}_{T}^{\mathrm{IV}}(x)$ of $T$ which satisfies $\mathbf{D1}$, $\mathbf{D2^{G}}$ and $\mathbf{D3^{G}}$, but does not satisfy $\mathbf{\Sigma_{1}C}$.

Proof.

We say an $\mathcal{L}_{A}$-formula $\varphi$ is propositionally atomic if it is not a Boolean combination of proper subformulas of $\varphi$. We fix a bijective mapping $f$ from the set of all propositional variables to the set of all propositionally atomic formulas. For each propositionally atomic formula $\Phi(x)$, the mapping $f$ can be extended to the mapping $f_{\Phi}$ from the set of all modal formulas to the set of all $\mathcal{L}_{A}$-formulas satisfying the following clauses:

$f_{\Phi}(p)$ is $f(p)$ for each propositional variable $p$; 2. 2.

$f_{\Phi}$ commutes with every propositional connective; 3. 3.

$f_{\Phi}(\Box A)$ is $\Phi(\ulcorner f_{\Phi}(A)\urcorner)$.

For any finite set $X$ of modal formulas and any modal formula $A$, $A$ is said to be derived in $X$ if $A$ is provable in the system whose axioms are elements of $X$ and whose inference rules are Modus Ponens $\dfrac{B\ \ B\to C}{C}$ and Necessitation $\dfrac{B}{\Box B}$.

For each natural number $n$, let $\mathrm{Th}_{n}(T)$ be the finite set of all $\mathcal{L}_{A}$-formulas having a $T$-proof whose Gödel number is less than or equal to $n$. We write $T\vdash_{\Phi,n}\varphi$ if there exist a finite set $X$ of modal formulas and a modal formula $A$ such that $f_{\Phi}(X)=\mathrm{Th}_{n}(T)$, $f_{\Phi}(A)$ is $\varphi$ and $A$ is derived in $X$. For $m<n$, $T\vdash_{\Phi,m}\varphi$ implies $T\vdash_{\Phi,n}\varphi$ because $\mathrm{Th}_{m}(T)\subseteq\mathrm{Th}_{n}(T)$. As shown in Visser [24], the ternary relation $T\vdash_{\Phi,n}\varphi$ is computable. Thus we obtain a $\Delta_{1}$ formula $P_{T}(\ulcorner\Phi\urcorner,x,y)$ saying that $x$ is the Gödel number of a formula $\varphi$ satisfying $T\vdash_{\Phi,y}\varphi$.

By the Fixed Point Lemma, there exist a $\Sigma_{1}$ formula $\mathrm{Pr}_{T}^{\mathrm{IV}}(x)$ and a $\Sigma_{1}$ sentence $\sigma$ satisfying the following equivalences:

$P^{\prime}_{T}(x,y)\equiv P_{T}(\ulcorner\mathrm{Pr}_{T}^{\mathrm{IV}}\urcorner,x,y)$; 2. 2.

$\mathsf{PA}\vdash\mathrm{Pr}_{T}^{\mathrm{IV}}(x)\leftrightarrow\exists y(P_{T}^{\prime}(x,y)\land\forall z<y\neg P_{T}^{\prime}(\ulcorner\neg\sigma\urcorner,z))$; 3. 3.

$\mathsf{PA}\vdash\sigma\leftrightarrow\exists z(P_{T}^{\prime}(\ulcorner\neg\sigma\urcorner,z)\land\forall y\leq z\neg P_{T}^{\prime}(\ulcorner\sigma\urcorner,y))$.

First, we prove $T\nvdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},n}\neg\sigma$ for all $n$ by induction on $n$. Suppose $T\nvdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},m}\neg\sigma$ for all $m<n$. Then $\mathsf{PA}\vdash\forall z<\overline{n}\neg P_{T}^{\prime}(\ulcorner\neg\sigma\urcorner,z)$.

Let $X$ be any finite set of modal formulas with $f_{\mathrm{Pr}_{T}^{\mathrm{IV}}}(X)=\mathrm{Th}_{n}(T)$. Let $A$ be any modal formula derived in $X$, then $T\vdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},n}f_{\mathrm{Pr}_{T}^{\mathrm{IV}}}(A)$. Hence we have $\mathsf{PA}\vdash P_{T}^{\prime}(\ulcorner f_{\mathrm{Pr}_{T}^{\mathrm{IV}}}(A)\urcorner,\overline{n})$, and thus $\mathsf{PA}\vdash\mathrm{Pr}_{T}^{\mathrm{IV}}(\ulcorner f_{\mathrm{Pr}_{T}^{\mathrm{IV}}}(A)\urcorner)$. Moreover, we show $T\vdash f_{\mathrm{Pr}_{T}^{\mathrm{IV}}}(A)$. This is proved by induction on the length of derivation in $X$. If $A\in X$, then $f_{\mathrm{Pr}_{T}^{\mathrm{IV}}}(A)\in\mathrm{Th}_{n}(T)$, and $f_{\mathrm{Pr}_{T}^{\mathrm{IV}}}(A)$ has a $T$-proof. If $A$ is derived from $B$ and $B\to A$ by Modus Ponens and $T\vdash f_{\mathrm{Pr}_{T}^{\mathrm{IV}}}(B)\land f_{\mathrm{Pr}_{T}^{\mathrm{IV}}}(B\to A)$, then $T\vdash f_{\mathrm{Pr}_{T}^{\mathrm{IV}}}(A)$. If $A$ is derived from $B$ by Necessitation, then $A$ is of the form $\Box B$. Since $\mathsf{PA}\vdash\mathrm{Pr}_{T}^{\mathrm{IV}}(\ulcorner f_{\mathrm{Pr}_{T}^{\mathrm{IV}}}(B)\urcorner)$ as above, we get $\mathsf{PA}\vdash f_{\mathrm{Pr}_{T}^{\mathrm{IV}}}(A)$. In this paragraph, we have shown that if $T\vdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},n}\varphi$, then $T\vdash\varphi$.

Suppose, towards a contradiction, $T\vdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},n}\neg\sigma$. Then $T\vdash\neg\sigma$. Since $T\nvdash\sigma$, $T\nvdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},m}\sigma$ for all $m\leq n$. Therefore $\mathsf{PA}\vdash P_{T}^{\prime}(\ulcorner\neg\sigma\urcorner,\overline{n})\land\forall y\leq\overline{n}\neg P_{T}^{\prime}(\ulcorner\sigma\urcorner,y)$. By the definition of $\sigma$, we have $\mathsf{PA}\vdash\sigma$. This is a contradiction. We obtain $T\nvdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},n}\neg\sigma$.

If $T\vdash\varphi$, then $\varphi\in\mathrm{Th}_{n}(T)$ for some $n$. Then $T\vdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},n}\varphi$ trivially holds, and hence $\mathsf{PA}\vdash P_{T}^{\prime}(\ulcorner\varphi\urcorner,\overline{n})$. Since $\mathsf{PA}\vdash\forall z<\overline{n}P_{T}^{\prime}(\ulcorner\neg\sigma\urcorner,z)$, we obtain $\mathsf{PA}\vdash\mathrm{Pr}_{T}^{\mathrm{IV}}(\ulcorner\varphi\urcorner)$. On the other hand, we assume $\mathsf{PA}\vdash\mathrm{Pr}_{T}^{\mathrm{IV}}(\ulcorner\varphi\urcorner)$. Then $P_{T}^{\prime}(\ulcorner\varphi\urcorner,\overline{n})$ is true in the standard model of arithmetic for some $n$. This means $T\vdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},n}\varphi$. Then we obtain $T\vdash\varphi$. Therefore we have shown that $\mathrm{Pr}_{T}^{\mathrm{IV}}(x)$ is a $\Sigma_{1}$ provability predicate of $T$.

We prove $\mathbf{D2^{G}}$ for $\mathrm{Pr}_{T}^{\mathrm{IV}}(x)$. We work in $S$. Suppose $\mathrm{Pr}_{T}^{\mathrm{IV}}(\ulcorner\varphi\urcorner)$ and $\mathrm{Pr}_{T}^{\mathrm{IV}}(\ulcorner\varphi\to\psi\urcorner)$ are true. Then for some $n$, $T\vdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},n}\varphi$, $T\vdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},n}\varphi\to\psi$ and $T\nvdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},m}\neg\sigma$ for all $m<n$. Then $T\vdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},n}\psi$. Thus $\mathrm{Pr}_{T}^{\mathrm{IV}}(\ulcorner\psi\urcorner)$ is true.

We prove $\mathbf{D3^{G}}$ for $\mathrm{Pr}_{T}^{\mathrm{IV}}(x)$. We proceed in $S$. Suppose $\mathrm{Pr}_{T}^{\mathrm{IV}}(\ulcorner\varphi\urcorner)$ is true. Then for some $n$, $T\vdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},n}\varphi$ and $T\nvdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},m}\neg\sigma$ for all $m<n$. Then $T\vdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},n}\mathrm{Pr}_{T}^{\mathrm{IV}}(\ulcorner\varphi\urcorner)$. Thus $\mathrm{Pr}_{T}^{\mathrm{IV}}(\ulcorner\mathrm{Pr}_{T}^{\mathrm{IV}}(\ulcorner\varphi\urcorner)\urcorner)$ is true.

At last, we prove that $\mathbf{\Sigma_{1}C}$ fails to hold. Suppose, for a contradiction, $T\vdash\sigma\to\mathrm{Pr}_{T}^{\mathrm{IV}}(\ulcorner\sigma\urcorner)$. By witness comparison argument, we have $\mathsf{PA}\vdash\sigma\to\neg\mathrm{Pr}_{T}^{\mathrm{IV}}(\ulcorner\sigma\urcorner)$. Thus $T\vdash\neg\sigma$. Then $T\vdash_{\mathrm{Pr}_{T}^{\mathrm{IV}},n}\neg\sigma$ for some $n$. This is a contradiction. Therefore we conclude $T\nvdash\sigma\to\mathrm{Pr}_{T}^{\mathrm{IV}}(\ulcorner\sigma\urcorner)$. ∎

By Proposition 2.4, Theorem 2.20, Proposition 2.13.3 and Proposition 2.14.1, $\mathrm{Pr}_{T}^{\mathrm{IV}}(x)$ does not satisfy any of $\mathbf{PC}$, $\mathbf{B_{2}^{U}}$, $\mathbf{D1^{U}}$ and $\mathbf{CB}$.

The next two propositions show that $\{\mathbf{D1},\mathbf{\Sigma_{1}C}\}$ and $\{\mathbf{D1},\mathbf{PC}\}$ are incomparable.

Proposition 4.13**.**

There exists a $\Sigma_{1}$ provability predicate $\mathrm{Pr}_{T}^{\mathrm{V}}(x)$ of $T$ which satisfies $\mathbf{\Sigma_{1}C^{G}}$, but does not satisfy any of $\mathbf{D1^{U}}$ and $\mathbf{PC}$.

Proof.

Let $T_{0}$ be any finite subtheory of $T$ containing $\mathsf{Q}$ with $\bigwedge T_{0}$ is not a $\Pi_{1}$ sentence. Let $\mathrm{Prf}_{T}^{\prime}(v,x,y)$ be the $\Delta_{1}$ formula

[TABLE]

By the Fixed Point Lemma, there exists a $\Sigma_{1}$ sentence $\sigma$ satisfying

[TABLE]

Let $\mathrm{Prf}_{T}^{\mathrm{V}}(x,y):\equiv\mathrm{Prf}_{T}^{\prime}(\ulcorner\sigma\urcorner,x,y)$ and let $\mathrm{Pr}_{T}^{\mathrm{V}}(x):\equiv\exists y\mathrm{Prf}_{T}^{\mathrm{V}}(x,y)$. Then

• •

$\mathsf{PA}\vdash\mathrm{Prf}_{T}^{\mathrm{V}}(x,y)\leftrightarrow\mathrm{Prf}_{T}(x,y)\land(\exists z<y\mathrm{Prf}_{T}(\ulcorner\neg\sigma\urcorner,z)\to\Sigma_{1}(x))$.

• •

$\mathsf{PA}\vdash\sigma\leftrightarrow\exists z(\mathrm{Prf}_{T}(\ulcorner\neg\sigma\urcorner,z)\land\forall y\leq z\neg\mathrm{Prf}_{T}^{\mathrm{V}}(\ulcorner\bigwedge T_{0}\to\sigma\urcorner,y))$.

First, we prove $T\nvdash\neg\sigma$. If $T\vdash\neg\sigma$, then for some natural number $p$, $\mathsf{PA}\vdash\mathrm{Prf}_{T}(\ulcorner\neg\sigma\urcorner,\overline{p})$. Since $T\nvdash\sigma$, obviously $T\nvdash\bigwedge T_{0}\to\sigma$. Then $\mathsf{PA}\vdash\forall y\leq\overline{p}\neg\mathrm{Prf}_{T}(\ulcorner\bigwedge T_{0}\to\sigma\urcorner,y)$. Since $\mathrm{Prf}_{T}^{\mathrm{V}}(x,y)$ implies $\mathrm{Prf}_{T}(x,y)$, we have $\mathsf{PA}\vdash\forall y\leq\overline{p}\neg\mathrm{Prf}_{T}^{\mathrm{V}}(\ulcorner\bigwedge T_{0}\to\sigma\urcorner,y)$. Then $\mathsf{PA}\vdash\sigma$ by the definition of $\sigma$. This is a contradiction. Therefore $T\nvdash\neg\sigma$.

It follows that for any natural number $n$, $\mathsf{PA}\vdash\neg\mathrm{Prf}_{T}(\ulcorner\neg\sigma\urcorner,\overline{n})$. Then for any formula $\varphi$, $\mathsf{PA}\vdash\mathrm{Prf}_{T}(\ulcorner\varphi\urcorner,\overline{n})\leftrightarrow\mathrm{Prf}_{T}^{\mathrm{V}}(\ulcorner\varphi\urcorner,\overline{n})$. Thus $\mathrm{Pr}_{T}^{\mathrm{V}}(x)$ is a $\Sigma_{1}$ provability predicate of $T$.

Since $\mathsf{PA}\vdash\Sigma_{1}(x)\to(\mathrm{Pr}_{T}(x)\leftrightarrow\mathrm{Pr}_{T}^{\mathrm{V}}(x))$ by the definition, $\mathbf{\Sigma_{1}C^{G}}$ for $\mathrm{Pr}_{T}^{\mathrm{V}}(x)$ easily follows from $\mathbf{\Sigma_{1}C^{G}}$ for $\mathrm{Pr}_{T}(x)$.

We prove that $\mathbf{PC}$ fails to hold for $\mathrm{Pr}_{T}^{\mathrm{V}}(x)$. If $\mathrm{Pr}_{T}^{\mathrm{V}}(x)$ satisfied $\mathbf{PC}$, then $S\vdash\mathrm{Pr}_{\emptyset}(\ulcorner\bigwedge T_{0}\to\sigma\urcorner)\to\mathrm{Pr}_{T}^{\mathrm{V}}(\ulcorner\bigwedge T_{0}\to\sigma\urcorner)$. By formalized deduction theorem, $S\vdash\mathrm{Pr}_{[T_{0}]}(\ulcorner\sigma\urcorner)\to\mathrm{Pr}_{T}^{\mathrm{V}}(\ulcorner\bigwedge T_{0}\to\sigma\urcorner)$. By $\mathbf{\Sigma_{1}C}$ for $\mathrm{Pr}_{[T_{0}]}(x)$,

[TABLE]

By the definition of $\mathrm{Prf}_{T}^{\mathrm{V}}(x,y)$, we obtain

[TABLE]

Since $\bigwedge T_{0}\to\sigma$ is not $\Sigma_{1}$,

[TABLE]

It follows

[TABLE]

This means $\mathsf{PA}\vdash\mathrm{Pr}_{T}^{\mathrm{V}}(\ulcorner\bigwedge T_{0}\to\sigma\urcorner)\to\neg\sigma$. From this with (9), $S\vdash\sigma\to\neg\sigma$, and hence $S\vdash\neg\sigma$. This is a contradiction. Therefore $\mathrm{Pr}_{T}^{\mathrm{V}}(x)$ does not satisfy $\mathbf{PC}$.

Finally, we prove that $\mathrm{Pr}_{T}^{\mathrm{V}}(x)$ does not satisfy $\mathbf{D1^{U}}$. Let $\varphi(x)$ be any formula such that $\mathsf{PA}\vdash\forall x\neg\Sigma_{1}(\ulcorner\varphi(\dot{x})\urcorner)$ and $T\vdash\forall x\varphi(x)$. Since $\mathsf{PA}\vdash\mathrm{Prf}_{T}(\ulcorner\varphi(\dot{z})\urcorner,y)\to z<y$, we have $\mathsf{PA}\vdash\mathrm{Pr}_{T}^{\mathrm{V}}(\ulcorner\varphi(\dot{z})\urcorner)\land\mathrm{Prf}_{T}(\ulcorner\neg\sigma\urcorner,z)\to\Sigma_{1}(\ulcorner\varphi(\dot{z})\urcorner)$ by the definition of $\mathrm{Prf}_{T}^{\mathrm{V}}(x,y)$. Hence $\mathsf{PA}\vdash\mathrm{Pr}_{T}^{\mathrm{V}}(\ulcorner\varphi(\dot{z})\urcorner)\to\neg\mathrm{Prf}_{T}(\ulcorner\neg\sigma\urcorner,z)$. Then $\mathsf{PA}\vdash\forall x\mathrm{Pr}_{T}^{\mathrm{V}}(\ulcorner\varphi(\dot{x})\urcorner)\to\neg\mathrm{Pr}_{T}(\ulcorner\neg\sigma\urcorner)$. Since $T\nvdash\neg\mathrm{Pr}_{T}(\ulcorner\neg\sigma\urcorner)$, we conclude that $T\nvdash\forall x\mathrm{Pr}_{T}^{\mathrm{V}}(\ulcorner\varphi(\dot{x})\urcorner)$. ∎

By Propositions 2.4 and 2.14. $\mathrm{Pr}_{T}^{\mathrm{V}}(x)$ does not satisfy any of $\mathbf{D2}$, $\mathbf{B_{2}}$ and $\mathbf{CB}$.

We give an example of Mostowski-like $\Sigma_{1}$ provability predicate which satisfies $\mathbf{PC^{G}}$ but does not satisfy $\mathbf{\Sigma_{1}C}$.

Proposition 4.14**.**

There exists a $\Sigma_{1}$ provability predicate $\mathrm{Pr}_{T}^{\mathrm{VI}}(x)$ of $T$ with:

$\mathrm{Pr}_{T}^{\mathrm{VI}}(x)$* satisfies $\mathbf{D1^{U}}$, $\mathbf{D3^{G}}$, $\mathbf{\Delta_{0}C^{G}}$ and $\mathbf{PC^{G}}$.* 2. 2.

$\mathrm{Pr}_{T}^{\mathrm{VI}}(x)$* satisfies neither $\mathbf{\Sigma_{1}C}$ nor $\mathbf{CB}$.*

Proof.

Let $\xi$ be a $\Pi_{1}$ sentence undecidable in $T$ such as Rosser’s sentence (see [17]), and let $\xi^{\prime}$ be the sentence $\xi\lor 0=\mathsf{s}(0)$ which is also undecidable in $T$. Let $\mathrm{Pr}_{T}^{\mathrm{VI}}(x):\equiv\mathrm{Pr}_{T}(x)\land x\neq\ulcorner\neg\xi^{\prime}\urcorner$. Obviously,

[TABLE]

Since $\neg\xi^{\prime}$ is not provable in $T$, $\mathrm{Pr}_{T}^{\mathrm{VI}}(x)$ is a $\Sigma_{1}$ provability predicate of $T$, and also $\mathbf{D1^{U}}$ holds for $\mathrm{Pr}_{T}^{\mathrm{VI}}(x)$. The conditions $\mathbf{D3^{G}}$ and $\mathbf{\Delta_{0}C^{G}}$ follow from $\mathsf{PA}\vdash\forall x(\ulcorner\mathrm{Pr}_{T}^{\mathrm{VI}}(\dot{x})\urcorner\neq\ulcorner\neg\xi^{\prime}\urcorner)$ and $\mathsf{PA}\vdash\forall x(\mathsf{True}_{\Delta_{0}}(x)\to x\neq\ulcorner\neg\xi^{\prime}\urcorner)$, respectively.

We prove $\mathbf{PC^{G}}$. Let $M$ be an $\mathcal{L}_{A}$-structure whose domain is a singleton $\{e\}$. Then for every closed $\mathcal{L}_{A}$-term $t$, $t^{M}=e$. Thus $M\models\xi\lor 0=\mathsf{s}(0)$. Therefore $\neg\xi^{\prime}$ is not provable in predicate calculus. The above argument can be formalized in $\mathsf{PA}$, and so $\mathsf{PA}\vdash\forall x(\mathsf{Fml}(x)\to(\mathrm{Pr}_{\emptyset}(x)\to x\neq\ulcorner\neg\xi^{\prime}\urcorner))$. Then by $\mathbf{PC^{G}}$ for $\mathrm{Pr}_{T}(x)$, we conclude $\mathsf{PA}\vdash\forall x(\mathsf{Fml}(x)\to(\mathrm{Pr}_{\emptyset}(x)\to\mathrm{Pr}_{T}^{\mathrm{VI}}(x)))$.

Since $\mathsf{PA}\vdash\neg\mathrm{Pr}_{T}^{\mathrm{VI}}(\ulcorner\neg\xi^{\prime}\urcorner)$ and $T\nvdash\xi^{\prime}$, we can prove $S\nvdash\mathrm{Pr}_{T}^{\mathrm{VI}}(\ulcorner\forall x\neg(\xi\lor x=\mathsf{s}(0))\urcorner)\to\forall x\mathrm{Pr}_{T}^{\mathrm{VI}}(\ulcorner\neg(\xi\lor\dot{x}=\mathsf{s}(0))\urcorner)$ by (10). The conditions $\mathbf{\Sigma_{1}C}$ and $\mathbf{CB}$ fail to hold because of them. ∎

By Proposition 2.4, $\mathrm{Pr}_{T}^{\mathrm{VI}}(x)$ satisfies neither $\mathbf{D2}$ nor $\mathbf{B_{2}}$.

At last, we prove that our Theorem 2.20 is actually an improvement of Buchholz’s theorem (Theorem 2.18).

Theorem 4.15**.**

There exists a $\Sigma_{1}$ provability predicate $\mathrm{Pr}^{\ast}(x)$ of $\mathsf{PA}$ which satisfies $\mathbf{D1^{U}}$, $\mathbf{B_{2}^{U}}$, $\mathbf{\Sigma_{1}C^{G}}$ and $\mathbf{PC^{G}}$ but does not satisfy $\mathbf{D2}$.

This theorem is proved by using Beklemishev’s arithmetical completeness theorem of the bimodal logic $\mathsf{CS}_{2}$ with respect to independent $\Sigma_{1}$ numerations (see Beklemishev [3]). For this, we need some preparations. The language of $\mathsf{CS}_{2}$ is that of propositional logic equipped with two unary modal operators $[0]$ and $[1]$. Formulas in this language are called $\mathsf{CS}_{2}$-formulas. The axioms of the bimodal logic $\mathsf{CS}_{2}$ are propositional tautologies and the formulas $[i](p\to q)\to([i]p\to[i]q)$, $[i]p\to[j][i]p$ and $[i]([i]p\to p)\to[i]p$ for $i,j\in\{0,1\}$. The inference rules of $\mathsf{CS}_{2}$ are modus ponens $\dfrac{A,\ \ A\to B}{B}$, necessitation $\dfrac{A}{[i]A}$ for $i\in\{0,1\}$, and uniform substitution.

We say a structure $M=(W,K_{0},K_{1},\prec,\Vdash,b)$ is a $\mathsf{CS}_{2}$-model if it satisfies the following conditions:

$W$ is a nonempty finite set. 2. 2.

$K_{0}$ and $K_{1}$ are subsets of $W$ with $W=K_{0}\cup K_{1}$. 3. 3.

$\prec$ is a strict partial ordering over $W$. 4. 4.

$b\in K_{0}\cap K_{1}$ and $b\prec x$ for all $x\in W\setminus\{b\}$. 5. 5.

$\Vdash$ is a binary relation between $W$ and the set of all $\mathsf{CS}_{2}$-formulas such that $\Vdash$ satisfies the usual conditions for satisfaction and the following condition: for $i\in\{0,1\}$, $x\Vdash[i]A$ if and only if for all $y\in K_{i}$, if $x\prec y$, then $y\Vdash A$.

A $\mathsf{CS}_{2}$-formula $A$ is said to be true in a $\mathsf{CS}_{2}$-model $M=(W,K_{0},K_{1},\prec,\Vdash,b)$ if $b\Vdash A$. The modal logic $\mathsf{CS}_{2}$ is sound and complete with respect to $\mathsf{CS}_{2}$ models.

Theorem 4.16** (See Smoryński [22]).**

For any $\mathsf{CS}_{2}$-formula $A$, the following are equivalent:

$\mathsf{CS}_{2}\vdash A$. 2. 2.

$A$* is true in all $\mathsf{CS}_{2}$-models.*

Let $\alpha_{0}(v)$ and $\alpha_{1}(v)$ be any $\Sigma_{1}$ numerations of $\mathsf{PA}$. A mapping $f$ from $\mathsf{CS}_{2}$-formulas to $\mathcal{L}_{A}$-sentences is a $(\alpha_{0},\alpha_{1})$-interpretation if $f$ commutes with each propositional connective, and $f([i]A)\equiv\mathrm{Pr}_{\alpha_{i}}(\ulcorner f(A)\urcorner)$ for $i\in\{0,1\}$. Beklemishev proved that $\mathsf{CS}_{2}$ is sound and complete with respect to this kind of interpretations.

Theorem 4.17** (The arithmetical completeness theorem of $\mathsf{CS}_{2}$ (Beklemishev [3])).**

For any $\mathsf{CS}_{2}$-formula $A$, the following are equivalent:

$\mathsf{CS}_{2}\vdash A$. 2. 2.

For any $\Sigma_{1}$ numerations $\alpha_{0}(v)$ and $\alpha_{1}(v)$ of $\mathsf{PA}$ and any $(\alpha_{0},\alpha_{1})$-interpretation $f$, $\mathsf{PA}\vdash f(A)$.

We are ready to prove Theorem 4.15.

Proof of Theorem 4.15.

Let us consider a $\mathsf{CS}_{2}$-model $M=(W,K_{0},K_{1},\prec,\Vdash,b)$ satisfying the following conditions:

$W=\{b,x_{0},x_{1}\}$, 2. 2.

$K_{0}=\{b,x_{0}\}$ and $K_{1}=\{b,x_{1}\}$, 3. 3.

$\prec=\{(b,x_{0}),(b,x_{1})\}$, 4. 4.

$x_{0}\Vdash p$ and $x_{1}\nVdash p$.

Then $b\Vdash[0]p\land[1]\neg p\land\neg[0]\bot\land\neg[1]\bot$. Thus $\mathsf{CS}_{2}\nvdash[0]p\land[1]\neg p\to[0]\bot\lor[1]\bot$. By the arithmetical completeness theorem of $\mathsf{CS}_{2}$, there are $\Sigma_{1}$ numerations $\alpha_{0}(v)$ and $\alpha_{1}(v)$ of $\mathsf{PA}$, and a $(\alpha_{0},\alpha_{1})$-interpretation $f$ such that $\mathsf{PA}\nvdash f([0]p\land[1]\neg p\to[0]\bot\lor[1]\bot)$. Let $\xi:\equiv f(p)$, then

[TABLE]

Let $\mathrm{Pr}^{\ast}(x)$ be the $\Sigma_{1}$ formula $\mathrm{Pr}_{\alpha_{0}}(x)\lor\mathrm{Pr}_{\alpha_{1}}(x)$. Then $\mathrm{Pr}^{\ast}(x)$ is obviously a $\Sigma_{1}$ provability predicate of $\mathsf{PA}$. Moreover $\mathbf{D1^{U}}$, $\mathbf{\Sigma_{1}C^{G}}$ and $\mathbf{PC^{G}}$ are inherited from $\mathrm{Pr}_{\alpha_{0}}(x)$.

First, we prove that $\mathrm{Pr}^{\ast}(x)$ satisfies $\mathbf{B_{2}^{U}}$. Suppose $\mathsf{PA}\vdash\forall\vec{x}(\varphi(\vec{x})\to\psi(\vec{x}))$. Then since both $\mathrm{Pr}_{\alpha_{0}}(x)$ and $\mathrm{Pr}_{\alpha_{1}}(x)$ satisfy $\mathbf{B_{2}^{U}}$, we have

[TABLE]

By the definition of $\mathrm{Pr}^{\ast}(x)$,

[TABLE]

Therefore we conclude

[TABLE]

At last, we prove that $\mathrm{Pr}^{\ast}(x)$ does not satisfy $\mathbf{D2}$. Suppose, towards a contradiction,

[TABLE]

Then by the definition of $\mathrm{Pr}^{\ast}(x)$,

[TABLE]

By logic, we obtain

[TABLE]

This contradicts (11). Therefore we conclude

[TABLE]

∎

By Proposition 2.14.2, $\mathrm{Pr}^{\ast}(x)$ satisfies $\mathbf{CB}$.

As we have seen, examples of formulas given in this section show several non-implications between conditions. For instance, the following non-implications related to Proposition 2.4 are also obtained.

$\mathbf{\Delta_{0}C}\not\Rightarrow\mathbf{D1}$ (Proposition 4.1). 2. 2.

$\{\mathbf{B_{m}}:m\geq 2\}\not\Rightarrow\mathbf{D1}$ (Proposition 4.2).

For all $m\geq 2$, $\mathbf{D1}\not\Rightarrow\mathbf{B_{m}}$ (Proposition 4.4). 3. 3.

For all $m\geq 1$, $\mathbf{D2}\not\Rightarrow\mathbf{B_{m}}$ (Proposition 4.1). 4. 4.

$\mathbf{D3}\not\Rightarrow\mathbf{\Delta_{0}C}$ (Proposition 4.2).

However, we do not have enough such non-implications between conditions including uniform and global versions. We close this paper with the following problem.

Problem 4.18**.**

Study further non-implications between derivability conditions.

5 Acknowledgments

This work was partly supported by JSPS KAKENHI Grant Numbers 16K17653 and 19K14586. The author would like to thank Toshiyasu Arai, Yong Cheng, Makoto Kikuchi, Hidenori Kurokawa, Yuya Okawa and Albert Visser for their valuable comments. The author would also like to thank the anonymous referee for pointing out an error in an earlier version of the manuscript.