Two remarks on proof theory of first-order arithmetic

Theorem 1.1 is a classic result in proof theory of PA, and there are known several proofs of it by G. Kreisel, S. Wainer, H. Schwichtenberg, et al. Let us introduce a derivability relation to bound witnesses for provable $\Sigma_{1}$-formulas in PA, which is a variant of one given in Chapter 4 of Schwichtenberg-Wainer[4]. The latter seems to be inspired from the proof in Buchholz-Wainer[1].

In this section by ordinals we mean ordinals$<\varepsilon_{0}$. When $\gamma+\alpha=\gamma\#\alpha$, we write $\gamma\dot{+}\alpha$ for $\gamma+\alpha$. In this case we say that $\gamma\dot{+}\alpha$ is defined. Also let $0\dot{+}\gamma=\gamma\dot{+}0:=\gamma$.

Fundamental sequences $\{\lambda[x]\}_{x\in\mathbb{N}}$ for limit ordinals $\lambda<\varepsilon_{0}$ are defined as follows. Let $0[x]=0$, $(\alpha+1)[x]=\alpha$. For ordinals $0<\alpha<\varepsilon_{0}$ in Cantor normal form $\alpha=\omega^{\alpha_{0}}m_{0}+\cdots+\omega^{\alpha_{k}}m_{k}\,(\alpha_{0}>\cdots>\alpha_{k}\geq 0,0<m_{0},\ldots,m_{k}<\omega)$, let

$\alpha<_{n}\beta$ denotes the transitive closure of the relation $\{(\alpha,\beta):\alpha=\beta[n]\}$. Let $\alpha\leq_{n}\beta:\Leftrightarrow\alpha<_{n}\beta\lor\alpha=\beta$.

Hardy functions $H_{\alpha}$ are defined by transfinite recursion on ordinals $\alpha<\varepsilon_{0}$: $H_{0}(x)=x$, $H_{\alpha+1}(x)=H_{\alpha}(x+1)$, and $H_{\lambda}(x)=H_{\lambda[x]}(x)$ for limit ordinals $\lambda$.

PA denotes the first-order arithmetic in the language $\{0,1,+,\cdot,\lambda x,y.\,x^{y},<,=\}$. ${\rm dg}(A)<\omega$ for formulas $A$ is defined by ${\rm dg}(A)=0$ if $A\in\Delta_{0}$, ${\rm dg}(A_{0}\circ A_{1})=\max\{{\rm dg}(A_{i}):i<2\}\,(\circ\in\{\lor,\land\})$, and ${\rm dg}(QxA)={\rm dg}(A)+1\,(Q\in\{\exists,\forall\})$.

For natural numbers $k$ and $\Sigma_{1}$-sentences $\exists xA\,(A\in\Delta_{0})$, $k\models\exists xA:\Leftrightarrow\mathbb{N}\models\exists x<k\,A$. For finite sets $\Gamma$ of $\Sigma_{1}$-sentences, $k\models\Gamma$ iff there exists a $B\in\Gamma$ such that $k\models B$.

Proof.  This is seen by induction on ordinals $\alpha$. Consider the case when $(\gamma,k)\vdash^{\alpha}_{0}\Gamma$ follows from an inference rule $(\exists)$. Let $\exists xA(x)$ be its principal (major) formula. We have $\alpha_{0}+1\leq_{k}\alpha$ and $(\gamma,k)\vdash^{\alpha_{0}}_{0}A(m),\Gamma$ with $m<H_{\gamma}(k)$. IH yields $H_{\gamma}(k)\models\{A(m)\}\cup\Gamma$. $\Box$

Proof.  1.4.2. No $\Delta_{0}$-formula is a principal formula of an inference rule.
1.4.4. This is seen from Lemma 1.4.1. $\Box$

Proof.  By induction on $\beta$. Consider the case when $(\gamma,k)\vdash^{\beta}_{c}\lnot C,\Delta$ follows from an inference rule $(\exists)$ with its principal formula $\lnot C\equiv(\exists x\lnot A(x))$. There are $\beta_{0}+1\leq_{\ell}\beta$, $n<\ell=H_{\gamma}(k)$ for which $(\gamma,k)\vdash^{\beta_{0}}_{c}\Delta,\lnot C,\lnot A(n)$. IH yields $(\gamma\cdot 2,k)\vdash^{\alpha\dot{+}\beta_{0}}_{c}\Gamma,\Delta,\lnot A(n)$. On the other hand we have $(\gamma,\max\{k,n\})\vdash^{\alpha}_{c}\Gamma,A(n)$ by Lemma 1.4.3. Lemma 1.4.4 with $n<\ell$ yields $(\gamma\cdot 2k)\vdash^{\alpha}_{c}\Gamma,A(n)$. Since ${\rm dg}(A(n))<c$, we obtain $(\gamma\cdot 2,k)\vdash^{\alpha\dot{+}\beta}_{c}\Gamma,\Delta$ by a $(cut)$. $\Box$

Proof.  By induction on $\alpha$. Suppose that $(\gamma,k)\vdash^{\alpha}_{c+1}\Gamma$ follows from an inference rule $I$. Let $\ell=H_{\gamma}(k)$.

First consider the case when $I$ is an $(\exists)$. We have $(\gamma,k)\vdash^{\beta}_{c+1}\Gamma,B(n)$ for $\beta+1\leq_{\ell}\alpha$, $n<\ell$, and $(\exists xB(x))\in\Gamma$. IH yields $(\omega^{\gamma\dot{+}\beta}+\gamma,k)\vdash^{\omega^{\beta}}_{c}\Gamma,B(n)$. By $\beta+1\leq_{\ell}\alpha$, we obtain $\omega^{\beta}+1<_{k^{\prime}}\omega^{\alpha}$ and $\omega^{\gamma\dot{+}\beta}<_{k^{\prime}}\omega^{\gamma\dot{+}\alpha}$ for any $k^{\prime}\geq H_{\gamma}(k)\geq 2$. Hence for $n\geq k$ we obtain $H_{\omega^{\gamma\dot{+}\beta}}(H_{\gamma}(n))\leq H_{\omega^{\gamma\dot{+}\alpha}}(H_{\gamma}(n))$, and $(\omega^{\gamma\dot{+}\alpha}+\gamma,k)\vdash^{\omega^{\beta}}_{c}\Gamma,B(n)$ by Lemma 1.4.1. An $(\exists)$ yields $(\omega^{\gamma\dot{+}\alpha}+\gamma,k)\vdash^{\omega^{\alpha}}_{c}\Gamma$.

Next consider the case when $I$ is a $(\forall\omega)$. We have $(\gamma,\max\{k,n\})\vdash^{\beta}_{c+1}\Gamma,B(n)$ for $\beta<_{\ell}\alpha$ and $(\forall xB(x))\in\Gamma$. IH yields $(\omega^{\gamma\dot{+}\beta}+\gamma,\max\{k,n\})\vdash^{\omega^{\beta}}_{c}\Gamma,B(n)$. We see $(\omega^{\gamma\dot{+}\alpha}+\gamma,\max\{k,n\})\vdash^{\omega^{\beta}}_{c}\Gamma,B(n)$ similarly for the case $(\exists)$. A $(\forall\omega)$ yields $(\omega^{\gamma\dot{+}\alpha}+\gamma,k)\vdash^{\omega^{\alpha}}_{c}\Gamma$.

Finally consider the case when $I$ is a $(cut)$ with the cut formula $C$. We have ${\rm dg}(C)\leq c$, $(\gamma,k)\vdash^{\beta}_{c+1}\Gamma,C$ and $(\gamma,k)\vdash^{\beta}_{c+1}\Gamma,\lnot C$ for $\beta+1\leq_{\ell}\alpha$. IH yields $(\omega^{\gamma\dot{+}\beta}+\gamma,k)\vdash^{\omega^{\beta}}_{c}\Gamma,C$ and $(\omega^{\gamma\dot{+}\beta}+\gamma,k)\vdash^{\omega^{\beta}}_{c}\Gamma,\lnot C$. We have $H_{\gamma}(k^{\prime})<H_{\omega^{\gamma\dot{+}\beta}}(k^{\prime})$ for $k^{\prime}\geq 2$. Lemma 1.4.1 yields for $k\geq 2$, $(\omega^{\gamma\dot{+}\beta}\cdot 2,k)\vdash^{\omega^{\beta}}_{c}\Gamma,C$ and $(\omega^{\gamma\dot{+}\beta}\cdot 2,k)\vdash^{\omega^{\beta}}_{c}\Gamma,\lnot C$. Lemma 1.5 yields $(\omega^{\gamma\dot{+}\beta}\cdot 4,k)\vdash^{\omega^{\beta}\cdot 2}_{c}\Gamma$. On the other hand we have $\omega^{\gamma\dot{+}\beta}\cdot 4<_{H_{\gamma}(k^{\prime})}\omega^{\gamma\dot{+}\alpha}$ and $\omega^{\beta}\cdot 2<_{H_{\gamma}(k)}\omega^{\alpha}$ for $k^{\prime}\geq k$ with $H_{\gamma}(k)\geq H_{\omega}(k)=2k\geq 4$, $k\geq 2=|\omega|$, and $\gamma\geq\omega$. This yields $H_{\omega^{\gamma\dot{+}\beta}\cdot 4}(k^{\prime})\leq H_{\omega^{\gamma\dot{+}\beta}\cdot 4}(H_{\gamma}(k^{\prime}))<H_{\omega^{\gamma\dot{+}\alpha}}(H_{\gamma}(k^{\prime}))$. Lemma 1.4.1 yields $(\omega^{\gamma\dot{+}\alpha}+\gamma,k)\vdash^{\omega^{\alpha}}_{c}\Gamma$. $\Box$

Proof.  Let $n^{\prime}=\max(\{1\}\cup\vec{n})$. Consider the case when $\Gamma$ follows from an $(\exists)$ with its principal formula $(\exists x\,A(x))\in\Gamma$.

IH yields $\omega^{2}\ell,n^{\prime}\vdash^{\omega\cdot d+m}_{c}\Gamma,A(t(\vec{n}))$. Pick a $k$ so that $t(\vec{n})<H_{\omega^{2}k}(n^{\prime})$ with $H_{\omega^{2}}(x)\geq 2^{x}$. An inference rule $(\exists)$ with $\ell_{1}=\max\{\ell,k\}$ yields $(\omega^{2}\ell_{1},n^{\prime})\vdash^{\omega\cdot d+m+1}_{c}\Gamma$. $\Box$

Let us prove Theorem 1.1. Assume ${\sf PA}\vdash\exists y\,\theta(x,y)\,(\theta\in\Delta_{0})$. By Lemma 1.7 pick natural numbers $\ell>0,d,m,c$ so that for any $n\in\mathbb{N}$, $\omega^{2}\ell,\max\{1,n\}\vdash^{\omega\cdot d+m}_{c}\exists y\,A(n,y)$. Define ordinals $\gamma_{c}$ by $\gamma_{0}=\omega^{2}\ell$, $\gamma_{c+1}=\omega^{\gamma_{c}\dot{+}\omega_{c}(\omega\cdot d+m)}\cdot 2$. Lemma 1.6 yields $\gamma_{c},n\vdash^{\alpha}_{0}\exists u\exists y,zA(n,y,z)$ for $n\geq 2$ and $\alpha=\omega_{c}(\omega\cdot d+m)$. We obtain $\exists y<H_{\gamma_{c}}(n)\,A(n,y)$ by Lemma 1.3 for $n\geq 2$.

It is easy to see that the infinite Ramsey theorem together with König’s lemma implies DH.

Proof.  Let $P:[K]^{1+n}\to 2^{m}$ be the partion $P(b_{0},b_{1},\ldots,b_{n})=\{i<m:\varphi_{i}[b_{0},b_{1},\ldots,b_{n}]\}$, and $D=\{a_{1}<\cdots<a_{k}\}\subset K$ be a diagonal homogeneous set for the partition $P$. $\Box$

Pari-Harrington’s principle PH states that $\forall n,m,c\exists K>n[K\to_{*}(m)^{n}_{c}]$, where $K\to_{*}(m)^{n}_{c}$ designates that for any partition $P:[K]^{n}\to c$ there exists a homogeneous set $H\subset K$ with $\#H\geq\min H$. The proof in Paris-Harrington[3] of the independence of PH from PA consists of two steps. First ${\rm Con}(T)\to{\rm Con}({\sf PA})$ for an extension $T$ of PA, and ${\rm PH}\to{\rm Con}(T)$. $T$ is obtained from PA by adding an infinite list $\{c_{i}\}_{i<\omega}$ of (individual constants intended to denote) diagonal indiscernibles $c_{i}$. The purely model-theoretic proof of the independence is given in Kanamori-McAloon[2]. In these proofs the principle DH is implicit, and crucial.

Let us reformulate the proof of ${\rm Con}(T)\to{\rm Con}({\sf PA})$ in [3] to get a purely proof-theoretic result for PA, cf. Theorem 2.5.

A formula $\varphi\equiv\left(Q_{1}z_{1}Q_{2}z_{2}\cdots Q_{n}z_{n}\theta\right)$ with a $\Delta_{0}$-matrix $\theta$ and alternating quantifiers $Q_{1},Q_{2},\ldots,Q_{n}$ is a $\Sigma_{n}$-formula [$\Pi_{n}$-formula] if $Q_{1}\equiv\exists$ [$Q_{1}\equiv\forall$], resp.

In this section PA is formulated in an applied one-sided sequent calculus. Besides usual inference rules for first-order logic, there are two inference rules for complete induction and axioms for constants. The inference rule for complete induction is stated as follows.

where $A\in\bigcup_{n}(\Sigma_{n}\cup\Pi_{n})$.

Let $\forall\vec{x}\theta(\vec{x})$ be a $\Pi_{1}$-axiom for constants $0,1,+,\cdot,\lambda x,y.\,x^{y},<,=$. Then for each list $\vec{t}$ of terms, the following is an inference rule in PA:

The applied calculus admits a cut-elimination. ${\sf PA}\vdash^{d}\Gamma$ designates that there exists a derivation of the sequent $\Gamma$ in depth$\leq d$.

In what follows argue in ${\sf EA}+\forall x\exists y(2_{x}=y)$. Let $\pi$ be a (cut-free) derivation of a $\Sigma_{1}$-sentence $\exists x\,\theta_{0}(x)$ in PA. Each formula in $\pi$ is in $\bigcup_{n}(\Sigma_{n}\cup\Pi_{n})$.

For a formula $\varphi\equiv\left(Q_{1}z_{1}Q_{2}z_{2}\cdots Q_{n}z_{n}\theta\right)\in\Sigma_{n}\cup\Pi_{n}$, let $q(\varphi)=n$. $q(\theta)=0$ for $\theta\in\Delta_{0}$. Let $Fml(\pi)$ denote the set of all formulas $\varphi$ appearing in $\pi$. Then $q(\pi):=\max\{q(\varphi):\varphi\in Fml(\pi)\}$.

Second $m(\pi)=\#\left(\{\varphi\in Fml(\pi):q(\varphi)>0\}\right)$. Third $d(\pi)$ denotes the depth of $\pi$: ${\sf PA}\vdash^{d(\pi)}\exists x\,\theta_{0}(x)$. Moreover let $(y_{0},\ldots,y_{\ell-1})$ be a list of all free variables occurring in $\pi$. $Tm(\pi)$ denotes the set of all terms $t$, which is either the (induction) term $t$ in (1), or the (witnessing) term $t$ in

Let $c(\pi)\geq 2$ be the number defined as follows. First let $e_{1}(x)=x$, $e_{c+1}(x)=x^{e_{c}(x)}$. Then $c=c(\pi)$ denotes a number for which the following holds for $e_{c}(x)$:

with a code $\langle y_{0},\ldots,y_{\ell-1}\rangle$ of the sequence $(y_{0},\ldots,y_{\ell-1})$.

By invoking the principle DH, let $K$ be a positive integer such that

where $n=q(\pi)$, $m=m(\pi)+6$, $c=c(\pi)$, $k=\max\{n,3,2d(\pi)+5-c\}$ with $K=\{0,1,\ldots,K-1\}$.

Let $Fml(\pi)=\{\varphi_{j}:j<m(\pi)\}$ be the set of all formulas occurring in $\pi$ other than $\Delta_{0}$-formulas. For formulas $\varphi_{j}\equiv\varphi_{j}(y_{0},\ldots,y_{\ell-1})$, let $\varphi_{j}^{\prime}(y)\equiv\varphi_{j}((y)_{0},\ldots,(y)_{\ell-1})$. Also for lists $X=(x_{1},\ldots,x_{n})$ of variables, let $\left(\varphi_{j}^{\prime}\right)^{(X)}(x_{0}):\equiv Q_{1}z_{1}<x_{1}Q_{2}z_{2}<x_{2}\cdots Q_{n}z_{n}<x_{n}\theta((x_{0})_{0},\ldots,(x_{0})_{\ell-1})$. Then $\Gamma_{0}=\Gamma_{0}(x_{0},x_{1},\ldots,x_{n})$ denotes the set of formulas $\{\left(\varphi_{j}^{\prime}\right)^{(X)}(x_{0}):j<m(\pi)\}$ augmented with the six formulas $\{c<x_{1},x_{2}=x_{1}+x_{0}+1,x_{1}(x_{0}+1)<x_{2},x_{1}^{x_{0}+1}<x_{2},x_{1}^{x_{1}}<x_{2},e_{c}(x_{1})<x_{2}\}$.

Let $D=\{\alpha_{-1}<\alpha_{0}<\alpha_{1}<\cdots<\alpha_{k}<\alpha_{k+1}<\cdots<\alpha_{k+c+n-4}\}$ be a diagonal indiscernible subset of $K$ with respect to $\Gamma_{0}$, cf. Proposition 2.2.

Proof.  First we see that $c<\alpha_{1}$ from the fact that $D$ is indiscernible for $c<x_{1}$. Second we see that $0\leq i<j<p\leq k+3\Rightarrow\alpha_{j}+\alpha_{i}<\alpha_{p}$, $0\leq i<j<p\leq k+2\Rightarrow\alpha_{j}\alpha_{i}<\alpha_{p}$, and $0\leq i<j<p\leq k+1\Rightarrow\alpha_{j}^{\alpha_{i}}<\alpha_{p}$ from the indiscerniblity for $x_{2}=x_{1}+x_{0}+1,x_{1}(x_{0}+1)<x_{2},x_{1}^{x_{0}+1}<x_{2}$. Third $0<i<j\leq k\Rightarrow\alpha_{i}^{\alpha_{i}}<\alpha_{j}$ follows from the indiscernibility for $x_{1}^{x_{1}}<x_{2}$. Finally by the third and the indiscernibility for $e_{c}(x_{1})<x_{2}$ we obtain $e_{c}(\alpha_{i})<\alpha_{i+1}$. (2) yields the proposition. $\Box$

For formulas $\sigma\equiv\left(Q_{m}x_{m}\cdots Q_{n}x_{n}\theta\right)\,(1\leq m\leq n+1)$ and $I=\{\alpha_{1}<\cdots<\alpha_{n}\}\in[\mathbb{N}]^{n}$, let $\sigma^{(I)}$ be the $\Delta_{0}$-formula

We write $\sigma^{(I)}$ for $\mathbb{N}\models\sigma^{(I)}$.

For any formula $\varphi$ occurring in the derivation $\pi$, the following holds by the indiscernibiity for $\left(\varphi_{j}^{\prime}\right)^{(X)}(x_{0})$.

To show Theorem 2.3, it suffices to show the following Theorem 2.5. Let $\Gamma$ be a sequent in the derivation $\pi$. For $J=\{\alpha_{j},\alpha_{j+1},\ldots,\alpha_{j+n-1}\}\,(0<j\leq k)$, let $\varphi^{(j)}:\equiv\varphi^{(J)}$.