Proofs that Modify Proofs, 1/2

We define d_{n\in\mu xX.\phi}(\langle\rangle)=\Omega^\flat_{n\not\in\mu xX.\phi} and d_{n\in\mu xX.\phi}(\langle\top\rangle)=\mathrm{Read}^{\mathsf{ID}_1^{\infty,+}}_{[n\in\mu xX.\phi]^{n\in\mu xX.\phi,\langle\rangle}}.

Suppose that, for some \sigma, we have set d_{n\in\mu xX.\phi}(\sigma)=\mathrm{Read}^{\mathsf{ID}_1^{\infty,+}}_{[\Gamma]^{n\in\mu xX.\phi,\epsilon}}. Then, for each \mathcal{R}, we set d_{n\in\mu xX.\phi}(\sigma\ulcorner\mathcal{R}\urcorner)=\mathcal{R} and, for each \iota\in|\mathcal{R}|, d_{n\in\mu xX.\phi}(\sigma\ulcorner\mathcal{R}\urcorner\iota)=\mathrm{Read}^{\mathsf{ID}_1^{\infty,+}}_{[\Gamma_\iota]^{n\in\mu xX.\phi,\epsilon\iota}} where \Gamma_\iota is \Gamma if \Delta(\mathcal{R})\cap\Gamma=\emptyset, and \Gamma_\iota=\Gamma\cup\Delta_\iota(\mathcal{R}) if \Delta(\mathcal{R})\cap\Gamma\neq\emptyset.

By induction on \phi. The case where \phi is a literal is either immediate using \mathrm{True} or is covered by the previous lemma. The cases where \phi is constructed using \wedge,\vee,\forall, or \exists are standard.

We proceed by induction on d. If d is \mathrm{Def}_\phi then \phi[x_i\mapsto m_i] is a true quantifier-free formula whose only atomic formulas have the form \dot{R}t_1\cdots t_n, and therefore there is a proof of \phi[x_i\mapsto m_i] even in \mathsf{ID}_{1}^{\infty,+}.

If d is \mathrm{Ax}_\eta then either \eta[x_i\mapsto m_i] has the form \dot{R}t_1\cdots t_n, in which case \mathrm{True}_{\eta[x_i\mapsto m_i]} suffices, or \eta[x_i\mapsto m_i] has the form n\in\mu xX.\phi, in which case the deduction d_{n\in\mu xX.\phi} is given above. When the final inference rule of d is \wedgeI, \veeI, \existsI, \mathrm{Cl}, or \mathrm{Cut}, the claim follows immediately from the inductive hypothesis. (In the case of \existsI and \mathrm{Cut}, the premises may have additional free variables; we substitute these free variables with 0’s to apply the inductive hypothesis.)

When the final inference rule of d is \forall^y_{\forall x\,\phi}I, we have a premise d' concluding \Gamma(d),\phi(y) where y is not free in \Gamma(d). For each n, the inductive hypothesis gives a deduction of (\Gamma(d),\phi(n))[x_i\mapsto m_i], and we may apply an \omega rule to obtain the desired deduction.

When d is \mathrm{Ind}^t_{\forall x\,\phi}, we let n be \overline{t[x_i\mapsto m_i]} and proceed by induction on n. For notational convenience, let \phi' be \phi[x_i\mapsto m_i]. When n=0, we may apply the previous lemma to obtain a deduction d^\infty_0 with \Gamma(d^\infty_0)\subseteq \phi'(0),{\sim}\phi(0). So suppose we have a deduction d^\infty_n with \Gamma(d^\infty_n)\subseteq {\sim}\phi'(0), \exists x\,\phi'(x)\wedge{\sim}\phi'(Sx)\, \phi'(n). Then we may take d^\infty_{n+1} to be

d^\infty_n \vdots {\sim}\phi'(0), \exists x\,\phi'(x)\wedge{\sim}\phi'(Sx), \phi'(n) d_{\phi'(n+1)} \vdots {\sim}\phi'(n+1),\phi'(n+1) {\sim}\phi'(0), \exists x\,\phi'(x)\wedge{\sim}\phi'(Sx), \phi'(n)\wedge{\sim}\phi'(n+1), \phi'(n+1) {\sim}\phi'(0), \exists x\,\phi'(x)\wedge{\sim}\phi'(Sx),\phi'(n+1)

The novel case is when d is \mathrm{Ind}^t_{\mu xX\, \phi,\psi(y)}. Again, let us write \phi' for \phi[x_i\mapsto m_i], t' for t[x_i\mapsto m_i], and \psi' for \psi[x_i\mapsto m_i]. In this case we may use an \Omega^\flat inference rule applied to the function \mathrm{Subst}^{t'\in \mu xX.\phi'\mapsto \psi'} from the previous lemma.

Immediate, since no rule in \mathsf{ID}^\infty_{1,0} can introduce a false literal of this form.

We define \mathrm{Inverse}^\wedge_{\phi_L,\phi_R, i}(d)(\sigma) by induction on \sigma, and simultaneously define a function \pi:\operatorname{dom}(\mathrm{Inverse}^\wedge_{\phi_L,\phi_R, i}(d))\rightarrow\operatorname{dom}(d).

We set \pi(\langle\rangle)=\langle\rangle. Let \pi(\sigma) be defined. If \phi_L\wedge\phi_R\not\in\Delta(d(\pi(\sigma)), we set \mathrm{Inverse}^\wedge_{\phi_L,\phi_R, i}(d)(\sigma)=d(\pi(\sigma)) and, for each \iota\in|\mathrm{Inverse}^\wedge_{\phi_L,\phi_R, i}(d)(\sigma)|, \pi(\sigma\iota)=\pi(\sigma)\iota).

Suppose \phi_L\wedge\phi_R\in\Delta(d(\pi(\sigma))). If d(\pi(\sigma)) is \wedge\mathrm{I}_{\phi_L\wedge\phi_R} then we set \mathrm{Inverse}^\wedge_{\phi_L,\phi_R, i}(d)(\sigma)=\mathrm{Rep} and \pi(\sigma\top)=\pi(\sigma)i.

The only other rule in \mathsf{ID}^\infty_{1,<n} with \phi_L\wedge\phi_R\in\Delta(d(\pi(\sigma)) is \mathrm{Read}^{\mathsf{ID}^{\infty,+}_1}_{[\Theta]^{n\in\mu xX.\phi,\epsilon}} with \phi_L\wedge\phi_R\in\Delta(\epsilon)\setminus\Theta. We set \mathrm{Inverse}^\wedge_{\phi_L,\phi_R, i}(d)(\sigma)=\mathrm{Read}^{\mathsf{ID}^{\infty,+}_1}_{[\Theta\cup\{\phi_L\wedge\phi_R\}]^{n\in\mu xX.\phi,\epsilon}} and, for all \mathcal{R}, \pi(\sigma\mathcal{R})=\pi(\sigma)\mathcal{R}.

We define \mathrm{Inverse}^\forall_{\phi(y),m} (d)(\sigma) by induction on \sigma, and simultaneously define a function \pi:\operatorname{dom}(\mathrm{Inverse}^\forall_{\phi(y),m} (d))\rightarrow\operatorname{dom}(d).

We set \pi(\langle\rangle)=\langle\rangle. Let \pi(\sigma) be defined. If \forall x\,\phi(x)\not\in\Delta(d(\pi(\sigma))) then we set \mathrm{Inverse}^\forall_{\phi(y),m} (d) (\sigma)=d(\pi(\sigma)) and, for each \iota\in|\mathrm{Inverse}^\forall_{\phi(y),m} (d) (\sigma)|, \pi(\sigma\iota)=\pi(\sigma)\iota).

If d(\pi(\sigma)) is \omega_{\forall x\,\phi} then we set \mathrm{Inverse}^\forall_{\phi(y),m} (d) (\sigma)=\mathrm{Rep} and \pi(\sigma\top)=\pi(\sigma)m.

The only other rule with \forall x\,\phi(x)\in\Delta(d(\pi(\sigma))) is \mathrm{Read}^{\mathsf{ID}^{\infty,+}_1}_{[\Theta]^{n\in\mu xX.\phi,\epsilon}} with \forall x\,\phi(x)\in\Delta(\epsilon)\setminus\Theta. We set \mathrm{Inverse}^\forall_{\phi(y),m} (d)(\sigma)=\mathrm{Read}^{\mathsf{ID}^{\infty,+}_1}_{[\Theta\cup\{\forall x\,\phi\}]^{n\in\mu xX.\phi,\epsilon}} and, for all \mathcal{R}, \pi(\sigma\mathcal{R})=\pi(\sigma)\mathcal{R}.

We define a partial function \pi:\operatorname{dom}(\mathrm{Elim}^\vee_{\phi_L,\phi_R}(d_\vee,d_\wedge))\rightarrow\operatorname{dom}(d_\vee). We define \pi(\langle\rangle)=\langle\rangle. Suppose we have defined \pi(\sigma). If {\sim}\phi_L\vee{\sim}\phi_R\not\in\Delta(d_\vee(\pi(\sigma))) then we set \mathrm{Elim}^\vee_{\phi_L,\phi_R}(d_\vee,d_\wedge)(\sigma)=d_\vee(\pi(\sigma)) and, for all \iota\in|\mathrm{Elim}^\vee_{\phi_L,\phi_R}(d_\vee,d_\wedge)(\sigma)|, \pi(\sigma\iota)=\pi(\sigma)\iota.

If d_\vee(\pi(\sigma)) is \vee\mathrm{I}^i_{{\sim}\phi_L\vee{\sim}\phi_R}, we set \mathrm{Elim}^\vee_{\phi_L,\phi_R}(d_\vee,d_\wedge)(\sigma)=\mathrm{Cut}_{\phi_i}. We set \pi(\sigma R)=\pi(\sigma), and for all \upsilon\in\operatorname{dom}(\mathrm{Inverse}^\wedge_{\phi_L,\phi_R,i}(d_\wedge)), we set \mathrm{Elim}^\vee_{\phi_L,\phi_R}(d_\vee,d_\wedge)(\sigma L\upsilon)=\mathrm{Inverse}^\wedge_{\phi_L,\phi_R,i}(d_\wedge)(\upsilon).

If d_\vee(\pi(\sigma)) is \mathrm{Read}^{\mathsf{ID}^{\infty,+}_1}_{[\Theta]^{n\in\mu xX.\phi,\epsilon}} with {\sim}\phi_L\vee{\sim}\phi_R\in\Delta(\epsilon)\setminus\Theta then we set \mathrm{Elim}^\vee_{\phi_L,\phi_R}(d_\vee,d_\wedge)(\sigma)=\mathrm{Read}^{\mathsf{ID}^{\infty,+}_1}_{[\Theta\cup\{{\sim}\phi_L\vee{\sim}\phi_R\}]^{n\in\mu xX.\phi,\epsilon}} and, for all \mathcal{R}, \pi(\sigma\mathcal{R})=\pi(\sigma)\mathcal{R}.

We define \pi(\langle\rangle)=\langle\rangle. Suppose we have defined \pi(\sigma). If \exists\mathrm{I}^t_{\exists y\,{\sim}\phi} is not in \Delta(d_\exists(\pi(\sigma))) then we set \mathrm{Elim}^\exists_{\phi(y)}(d_\exists,d_\forall)(\sigma)=d_\exists(\pi(\sigma)) and, for all \iota\in|\mathrm{Elim}^\exists_{\phi(y)}(d_\exists,d_\forall)(\sigma)|, \pi(\sigma\iota)=\pi(\sigma)\iota.

If d_\exists(\pi(\sigma)) is \exists\mathrm{I}^t_{\exists y\,{\sim}\phi} then, since t is closed, t=m for some numeral m. We set \mathrm{Elim}^\exists_{\phi(y)}(d_\exists,d_\forall)(\sigma)=\mathrm{Cut}_{\phi(m)}. We set \pi(\sigma R)=\pi(\sigma)\top and, for all \upsilon\in\operatorname{dom}(\mathrm{Inverse}^\forall_{\phi(y),m}(d_\forall)), we set \mathrm{Elim}^\exists_{\phi(y)}(d_\exists,d_\forall)(\sigma L\upsilon)=\mathrm{Inverse}^\forall_{\phi(y),m}(d_\forall)(\upsilon).

If d_\exists(\pi(\sigma)) is \mathrm{Read}^{\mathsf{ID}_1^{\infty,+}}_{[\Theta]^{n\in\mu xX.\phi,\epsilon}} with \exists y\,{\sim}\phi\in\Delta(\epsilon)\setminus\Theta then we set \mathrm{Elim}^\exists_{\phi(y)}(d_\exists,d_\forall)(\sigma)=\mathrm{Read}^{\mathsf{ID}_1^{\infty,+}}_{[\Theta\cup\{\exists y\,{\sim}\phi\}]^{n\in\mu xX.\phi,\epsilon}} and, for all \mathcal{R}, \pi(\sigma\mathcal{R})=\pi(\sigma)\mathcal{R}.

We define \pi(\langle\rangle)=\langle\rangle.

Suppose we have defined \pi(\sigma). If n\not\in\mu xX.\phi\not\in\Delta(d_\neg(\pi(\sigma))) then we set \mathrm{Elim}^\mu_{n\in\mu xX.\phi}(d_\mu,d_\neg) (\sigma)=d_\neg(\pi(\sigma)) and, for all \iota\in|\mathrm{Elim}^\mu_{n\in\mu xX.\phi}(d_\mu,d_\neg) (\sigma)|, \pi(\sigma\iota)=\pi(\sigma)\iota.

If n\not\in\mu xX.\phi\in\Delta(d_\neg(\pi(\sigma))) then if d_\neg(\pi(\sigma)) is \Omega^\flat_{n\not\in\mu xX.\phi}, we set \mathrm{Elim}^\mu_{n\in\mu xX.\phi}(d_\mu,d_\neg) (\sigma)=\mathrm{Cut}\Omega^\flat_{n\not\in\mu xX.\phi}, \pi(\sigma R)=\pi(\sigma)\top, and \mathrm{Elim}^\mu_{n\in\mu xX.\phi}(d_\mu,d_\neg)(\sigma L \upsilon)=d_\mu(\upsilon).

The final case is that d_\neg(\pi(\sigma)) is \mathrm{Read}^{\mathsf{ID}_1^{\infty,+}}_{[\Theta]^{m\in yY.\phi,\epsilon}} with n\not\in\mu xX.\phi\in\Delta(\epsilon)\setminus\Theta. In this case we set \mathrm{Elim}^\mu_{n\in\mu xX.\phi}(d_\mu,d_\neg) (\sigma)=\mathrm{Read}^{\mathsf{ID}_1^{\infty,+}}_{[\Theta\cup\{n\not\in\mu xX.\phi\}]^{m\in yY.\phi,\epsilon}} and, for all \mathcal{R}, \pi(\sigma\mathcal{R})=\pi(\sigma)\mathcal{R}.

For every \tau\in\operatorname{dom}(d), we need to define a proof tree \mathrm{Reduce}_n(d,\tau), which represents beginning the cut reduction process above the position \tau.

As always, we define \mathrm{Reduce}_n(d,\tau)(\sigma) by induction on \sigma while simultaneously defining a partial function \pi_\tau:\operatorname{dom}(\mathrm{Reduce}_n(d,\tau))\rightarrow\operatorname{dom}(d). Initially, we set \pi_\tau(\langle\rangle)=\tau.

If d(\pi_\tau(\sigma)) is any rule other than a \mathrm{Cut}_\phi with rk(\phi)=n, we set \mathrm{Reduce}_n(d,\tau)(\sigma)=d(\pi(\sigma)) and \pi_\tau(\sigma\iota)=\pi_\tau(\sigma)\iota for all \iota\in|d'(\sigma)|.

So suppose d(\pi_\tau(\sigma)) is \mathrm{Cut}_\phi with rk(\phi)=n. We set \mathrm{Reduce}_n(d,\tau)(\sigma)=\mathrm{Rep} and consider cases on \phi. Without loss of generality, we assume \phi is either an atomic formula, a conjunction, or a universal formula. (Otherwise \phi is the negation of such a formula and we apply the same arguments after swapping the input branches.)

If \phi is an atomic formula \dot{R}t_1\cdots t_n then \phi is either true or false. If \phi is false, we define \mathrm{Reduce}_n(d,\tau)(\sigma \top\upsilon)=\mathrm{Reduce}_n(d, \pi_\tau(\sigma)L)(\upsilon) for all \upsilon. If \phi is true, so \neg \phi is false, we define \mathrm{Reduce}_n(d,\tau)(\sigma\top\upsilon)=\mathrm{Reduce}_n(d, \pi_\tau(\sigma)R)(\upsilon).

If \phi is a conjunction \phi_L\wedge\phi_R (respectively, a universal \forall x\,\phi(x) or atomic formula t\in\mu xX.\phi), we take \mathrm{Reduce}_n(d,\tau)(\sigma\top\upsilon) to be

or

or

We need to define \mathcal{D} (d)(\sigma) by induction on |\sigma| for all d satisfying the assumptions simultaneously, and we simultaneously define partial functions \pi_d:\operatorname{dom}(\mathcal{D}(d))\rightarrow \operatorname{dom}(d). We also need to ensure that, for all \sigma\in\operatorname{dom}(\mathcal{D}(d)) for which \pi_d(\sigma) is defined, \Gamma(d,\pi_d(\sigma)) does not contain n\not\in\mu xX.\phi or [\Sigma]^{n\in\mu xX.\phi,\epsilon}. As usual, we set \pi_d(\langle\rangle)=\langle\rangle.

Suppose we have defined \pi_{d}(\sigma). Observe that d(\pi_d(\sigma)) cannot be \mathrm{Read} or \Omega^\flat. So if d(\pi_d(\sigma)) is any rule other than \mathrm{Cut}\Omega^\flat, it must be a rule in \mathsf{ID}^{\infty,+}_1, so we can set \mathcal{D} (d)(\sigma)=d(\pi_d(\sigma)) and, for \iota\in |\mathcal{D} (d)(\sigma)|, \pi_d(\sigma\iota)=\pi_d(\sigma)\iota.

So suppose d(\pi_d(\sigma))=\mathrm{Cut}\Omega^\flat_{n\in\mu xX.\phi}. We will set \mathcal{D} (d)(\sigma)=\mathrm{Rep} and, for all \upsilon, \mathcal{D} (d)(\sigma\top \upsilon)=\mathcal{D} (\bar d_\bot(\mathcal{D} (d_\top)))(\upsilon). Note that this is well-defined using the inductive hypothesis since |\upsilon|<|\sigma\top\upsilon| and \mathcal{D} (\bar d_\bot(\mathcal{D} (d_\top)))(\upsilon) depends only on \bar d_\bot(\mathcal{D} (d_\top))(\upsilon') with |\upsilon'|\leq|\upsilon|, which in turn depends on \mathcal{D} (d_\top)(\upsilon'') for \upsilon'' with |\upsilon''|\leq|\upsilon'|\leq|\upsilon|<|\sigma\top\upsilon|.

We have \omega^{\Omega\#\alpha}\#\gamma<\omega^{\Omega\#\beta}\#\gamma, so consider some \vartheta\zeta\in K(\omega^{\Omega\#\alpha}\#\gamma)=K\gamma\cup K\alpha. We must show that \vartheta\zeta<\vartheta_\gamma(\beta).

If \vartheta\zeta\in K\gamma then we have \vartheta\zeta\in K(\omega^{\Omega\#\beta}\#\gamma), and therefore \vartheta\zeta<\vartheta_\gamma(\beta). So we may assume \vartheta\zeta\in K\alpha with \gamma<\vartheta\zeta (since, similarly, \gamma<\vartheta_\gamma(\beta)). We have \vartheta\zeta<\vartheta\beta<\vartheta(\omega^{\Omega\#\beta}\#\gamma), as needed.

First we show that \alpha[f]<\beta[f] by induction on \alpha and \beta. Most cases follow immediately from either the inductive hypothesis or the fact that f is order-preserving, as well as the fact that we don’t make further substitutions inside a \vartheta\alpha' subterm.

Now consider some \theta\in K\alpha[f]; we have \theta\in K\alpha\cup\operatorname{rng}(f), so \theta<\max\{\vartheta\beta,\gamma,\delta\}.

Since \delta[v\mapsto \vartheta_\gamma(\alpha)]<\beta by the previous lemma, we have \omega^{\Omega\#\delta[v\mapsto \vartheta_\gamma(\alpha)]}\#\vartheta_{\gamma}(\alpha)<\omega^{\Omega\#\beta}\#\gamma as needed.

We also have \vartheta_\gamma(\alpha)<\vartheta_\gamma(\beta). If \zeta\in K(\omega^{\Omega\#\delta[v\mapsto \vartheta_\gamma(\alpha)]}\#\vartheta_\gamma(\alpha)) then either \zeta=\vartheta_\gamma(\alpha)<\vartheta_\gamma(\beta) or \zeta\in K(\delta[v\mapsto \vartheta_\gamma(\alpha)]), so \zeta\in K\delta\cup\{\vartheta_\gamma(\alpha)\} (because v cannot appear in an element of K\delta), so again \zeta<\vartheta_\gamma(\beta).

For each \sigma, we define o^{\bar F(d)}(\sigma)=o^{F}(h(\sigma))[v_{n\in\mu xX.\phi,\epsilon}\mapsto o^d(\epsilon)].

Consider any \sigma\sqsubset\tau. We have o^{\bar F(d)}(\sigma)=o^F(h(\sigma)) [v_{n\in\mu xX.\phi,\epsilon}\mapsto o^d(\epsilon)]\ll_{\max\{\gamma,\beta\}}o^F(h(\tau)) [v_{n\in\mu xX.\phi,\epsilon}\mapsto o^d(\epsilon)]=o^{\bar F(d)}(\tau).

We define o^{d_{n\in\mu xX.\phi}}(\langle\rangle)=\Omega. Given \sigma such that d_{n\in\mu xX.\phi}(\sigma)=\mathrm{Read}^{\mathsf{ID}_1^{\infty,+}}_{[n\in\mu xX.\phi]^{n\in\mu xX.\phi,\epsilon}}, we set o^{d_{n\in\mu xX.\phi}}(\sigma)=v_{n\in\mu xX.\phi,\epsilon}\#1 and, for each \mathcal{R}, o^{d_{n\in\mu xX.\phi}}(\sigma\mathcal{R})=v_{n\in\mu xX.\phi,\epsilon}.

A straightforward induction on \phi.

We construct an ordinal bound o^{\mathrm{Subst}^{n \in \mu xX. \phi\mapsto \psi(n)}} on \operatorname{dom}(\mathrm{Subst}^{n \in \mu xX. \phi\mapsto \psi(n)}) as follows.

For any \sigma such that \mathrm{Subst}^{n \in \mu xX. \phi\mapsto \psi(n)}(\sigma)=\mathrm{Read}^{\mathsf{ID}_1^{\infty,+}}_{[\Theta_\sigma[Z\mapsto \mu xX.\phi]]^{n\in\mu xX.\phi,\epsilon,r}}, we set o^{\mathrm{Subst}^{n \in \mu xX. \phi\mapsto \psi(n)}}(\sigma)=rk(\psi)\cdot 2\# v_{n\in\mu xX.\phi,\epsilon}\# 2. If \mathcal{R} is any rule other than \mathrm{Cl}_{k\in\mu xX.\phi} with Z k\in\Theta_\sigma then we may assign o^{\mathrm{Subst}^{n \in \mu xX. \phi\mapsto \psi(n)}}(\sigma\ulcorner\mathcal{R}\urcorner)=rk(\psi)\# v_{n\in\mu xX.\phi,\epsilon}. (Since we have assigned o^{\mathrm{Subst}^{n \in \mu xX. \phi\mapsto \psi(n)}}(\sigma\ulcorner\mathcal{R}\urcorner\iota)=rk(\psi)\# v_{n\in\mu xX.\phi,\epsilon\iota}\# 2, the comparison is satisfied.)

If \mathcal{R}=\mathrm{Cl}_{k\in\mu xX.\phi} with Z k\in\Theta_\sigma then we may set (recall that, above \sigma\ulcorner\mathcal{R}\urcorner, we have the proof tree shown in the proof of Lemma 4.4):

• o^{\mathrm{Subst}^{n \in \mu xX. \phi\mapsto \psi(n)}}(\sigma\ulcorner\mathcal{R}\urcorner)=rk(\psi)\# v_{n\in\mu xX.\phi,\epsilon}\# 1,

• o^{\mathrm{Subst}^{n \in \mu xX. \phi\mapsto \psi(n)}}(\sigma\ulcorner\mathcal{R}\urcorner\top)=rk(\psi)\# v_{n\in\mu xX.\phi,\epsilon}

• o^{\mathrm{Subst}^{n \in \mu xX. \phi\mapsto \psi(n)}}(\sigma\ulcorner\mathcal{R}\urcorner\top \mathrm{R}\upsilon)=o^{d_{\psi(k)}}(\upsilon).

The branch o^{\mathrm{Subst}^{n \in \mu xX. \phi\mapsto \psi(n)}}(\sigma\ulcorner\mathcal{R}\urcorner\top \mathrm{L}) is handled as above since \mathrm{Subst}^{n \in \mu xX. \phi\mapsto \psi(n)}(\sigma\ulcorner\mathcal{R}\urcorner\top \mathrm{L}) is a \mathrm{Read} rule.

We define o^{d^\infty} by induction on d. Since d is finite, the induction is straightforward. In the base cases, a bound can be constructed directly or by using the previous lemma.

For (1), we may take o^{\mathrm{Inverse}^\wedge_{\phi_L,\phi_R, i}(d)}(\sigma)=o^d(\pi(\sigma)). Similarly for (2).

For (3), when \pi(\sigma) is defined, we again set o^{\mathrm{Elim}^\vee_{\phi_L,\phi_R}(d_\vee,d_\wedge)}(\sigma)=\alpha+o^{d_\vee}(\pi(\sigma)). If \pi(\sigma) is not defined then \sigma has the form \sigma' L\upsilon where d_\vee(\pi(\sigma')) is \vee\mathrm{I}^i_{{\sim}\phi_L\vee{\sim}\phi_R} and \upsilon\in\operatorname{dom}(d_\wedge); in this case we set o^{\mathrm{Elim}^\vee_{\phi_L,\phi_R}(d_\vee,d_\wedge)}(\sigma' L\upsilon)=o^{d_\wedge}(\upsilon). (4) and (5) are similar.

For (6), we need to define o^{\mathrm{Reduce}_n(d,\tau)} for all \tau simultaneously. When \pi_\tau(\sigma) is defined, we will take o^{\mathrm{Reduce}_n(d,\tau)}(\sigma)=\omega^{o^d(\pi_\tau(\sigma))}. Since \alpha\ll_\gamma\beta implies \omega^\alpha\ll_\gamma\omega^\beta, this immediately ensures the order preserving property when d(\pi_\tau(\sigma)) is anything other than \mathrm{Cut}_\phi with rk(\phi)=n.

If d(\pi_\tau(\sigma)) is \mathrm{Cut}_\phi with rk(\phi)=n, if \phi is \dot{R}t_1\cdots t_n then we take o^{\mathrm{Reduce}_n(d,\tau)}(\sigma \top\upsilon)=o^{\mathrm{Reduce}_n(d,\pi_\tau(\sigma) b)}(\upsilon) for all \upsilon (with b=\top if \phi is false and b=\bot if \phi is true). Since o^{\mathrm{Reduce}_n(d,\tau) }(\sigma \top)=o^{\mathrm{Reduce}_n(d,\pi_\tau(\sigma) b)}(\langle\rangle)=\omega^{o^d(\pi_\tau(\sigma) b)}\ll_\gamma \omega^{o^d(\tau)}=o^{\mathrm{Reduce}_n(d,\tau)}(\sigma), the order preserving property holds. (The case where \phi is \neg\dot{R}t_1\cdots t_n is identical.)

If \phi is a conjunction, we take o^{\mathrm{Reduce}_n(d,\tau)}(\sigma \top\upsilon)=o^{\mathrm{Elim}^\vee_{\phi_L,\phi_R}(\mathrm{Reduce}_n(d,\pi_\tau(\sigma) R),\mathrm{Reduce}_n(d,\pi_\tau(\sigma) L))}(\upsilon). We have

as needed.

When \pi_d(\sigma) is defined, we set o^{D(d)}(\sigma)=\vartheta_\gamma(o^d(\pi_d(\sigma))). When d(\pi_d(\sigma)) is not a \mathrm{Cut}\Omega^\flat, we have o^d(\pi_d(\sigma\iota))\ll_\gamma o^d(\pi_d(\sigma)), so also o^{D(d)}(\sigma\iota)=\vartheta_\gamma(o^d(\pi_d(\sigma\iota)))< \vartheta_\gamma (o^d(\sigma))=o^{D(d)}(\sigma).

When d(\pi_d(\sigma)) is a \mathrm{Cut}\Omega^\flat rule, observe that \bar d_\bot(D(d_\top)) is bounded by o^{d}(\pi_d(\sigma)\bot)[v_{n\in\mu xX.\phi,\langle\rangle}\mapsto \vartheta_\gamma(o^d(\pi_d(\sigma)\top))] above \vartheta_\gamma(o^d(\pi_d(\sigma)\top)), and therefore we may set

By Lemma 4.19, we have o^{D(d)}(\sigma\top)<o^{D(d)}(\sigma) as needed.

First we show that \alpha[f]<\beta[f] by induction. The main case is when \alpha=\vartheta_{c'}\alpha' and \beta=\vartheta_{c'}\beta'.

If c'\leq c then \alpha',\beta' may not contain any elements of \mathbb{V}_c, so \alpha[f]=\alpha and \beta[f]=\beta, so \alpha<\beta immediately implies \alpha[f]<\beta[f].

So suppose c<c'. Say \alpha'<\beta'; by the inductive hypothesis, \alpha'[f]<\beta'[f] as well. If \zeta\in K_{c'}\alpha'[f] then either \zeta=\zeta'[f] with \zeta'\in K_{c'}\alpha' or \zeta=\theta for some \theta\in\operatorname{rng}(f). In the former case, the inductive hypothesis applies since \zeta<\vartheta_{c'}\beta'. In the latter case, we have \theta\leq\delta<\Omega_c, so \theta<\vartheta_{c'}\beta'[f], as needed.

Otherwise, \beta'<\alpha', and again by the inductive hypothesis, \beta'[f]<\alpha'[f]. There is a \zeta\in K_{c'}\alpha' so that \vartheta_{c'}\beta'\leq \zeta, and then by the inductive hypothesis, \vartheta_{c'}\beta'[f]\leq\zeta[f].

Now we strengthen this to \alpha[f]\ll^c_{\max\{\gamma,\delta\}}\beta[f]. Take c'\leq c and suppose \delta\in K_{c'}\alpha[f]. Then \delta\in K_{c'}\alpha\cup \bigcup_v K_{c'}f(v), and so is bounded by K_{c'}\beta\cup K_{c'}\gamma\cup K_{c'}\delta.

We certainly have \omega^{\Omega_c\#\alpha}\#\gamma<\omega^{\Omega_c\#\beta}\#\gamma.

Consider \vartheta_c\zeta\in K_c(\omega^{\Omega_c\#\alpha}\#\gamma)=K\alpha\cup K\gamma. Then this is bounded by some element of K_c\beta\cup K_c\gamma, and therefore by \vartheta_{c,\gamma}(\beta).

Now consider \zeta\in K_{c'}\vartheta_{c,\gamma}(\alpha) with c'<c. We have \zeta\in K_{c'}\alpha\cup K_{c'}\gamma as well, so again this is bounded in K_{c'}\vartheta_{c,\gamma}(\beta)=K_{c'}\beta\cup K_{c'}\gamma.

Observe that \delta[v\mapsto\vartheta_{c,\gamma}(\alpha)]<\beta, since \delta<\beta. Therefore we also have \omega^{\Omega_c\#\delta[v\mapsto\vartheta_{c,\gamma}(\alpha)]}\#\gamma<\omega^{\Omega_c\#\beta}\#\gamma.

Any \zeta\in K_{c} \omega^{\Omega_c\#\delta[v\mapsto\vartheta_{c,\gamma}(\alpha)]}\#\gamma is in K_c\delta\cup K_c\gamma\cup\{\vartheta_{c,\gamma}(\alpha)\} (recall that we do not substitute inside elements of K_c\delta), and therefore bounded by \vartheta_{c,\gamma}(\beta).

Similarly, any element of K_{c'}\vartheta_{c,\vartheta_{c,\gamma}(\alpha)}(\delta[v\mapsto\vartheta_{c,\gamma}(\alpha)]) is in K_{c'}\delta\cup K_{c'}\gamma\cup K_{c'}\vartheta_{c,\gamma}(\alpha), so also bounded in K_{c'}\vartheta_{c,\gamma}(\beta).

The only new step is producing a proof of \{n\in\mu xX.\phi,n\not\in\mu xX.\phi\} when dp(\mu xX.\phi)>1. The proof is similar to Lemma 4.2, except that when d_{n\in\mu xX.\phi}(\sigma)=\mathrm{Read}^{\mathsf{ID}_0^{\infty,+}}_{[\Gamma]^{n\in\mu xX.\phi,\epsilon}}, we could have m\not\in\mu yY.\psi\in\Gamma where dp(\mu yY.\psi)<dp(\mu xX.\phi). In this case we set d_{n\in\mu xX.\phi}(\sigma\ulcorner m\in\mu yY.\psi\urcorner\tau)=d_{m\in\mu yY.\psi}(\tau) for all \tau.

This is unchanged from Lemma 4.4 since the theory the \mathrm{Read} rules branch over is essentially unchanged. (Note that we never have any n\not\in\mu xX.\phi\in\Theta'_\sigma.)

As in the proof of Theorem 4.5.

The proofs are largely unchanged except for (?).

In the definition of \mathrm{Elim}^\mu_{n\in\mu xX.\phi}(d_\mu,d_\neg), we need to address the possibility that n\not\in\mu xX.\phi\in\Delta(d_\neg(\pi(\sigma))) but d_{\neg}(\pi(\sigma)) is not \Omega^\flat_{n\not\in\mu xX.\phi}, because d_\neg(\pi(\sigma)) could now be \mathrm{Read}^{\mathsf{ID}_{0,<0}^{\infty}}_{[\Theta]^{m\in\mu yY.\psi,\epsilon'}} with n\not\in\mu xX.\phi\in\Delta(\epsilon')\setminus\Theta.

In this case, we set \mathrm{Elim}^\mu_{n\in\mu xX.\phi}(d_\mu,d_\neg)(\sigma)=\mathrm{Read}^{\mathsf{ID}_{0,<0}^{\infty}}_{[\Theta,n\not\in\mu xX.\phi]^{m\in\mu yY.\psi,\epsilon'}}. For each \iota\in|\mathrm{Read}^{\mathsf{ID}_{0,<0}^{\infty}}_{[\Theta]^{m\in\mu yY.\psi,\epsilon'}}| we set \pi(\sigma\iota)=\pi(\sigma)\iota and continue as before.

However there is a new element \ulcorner n\in\mu xX.\phi\urcorner\in|\mathrm{Read}^{\mathsf{ID}_{0,<0}^{\infty}}_{[\Theta]^{m\in\mu yY.\psi,\epsilon'}}|\setminus|\mathrm{Read}^{\mathsf{ID}_{0,<0}^{\infty}}_{[\Theta]^{m\in\mu yY.\psi,\epsilon'}}|; we set \mathrm{Elim}^\mu_{n\in\mu xX.\phi}(d_\mu,d_\neg)(\sigma\ulcorner n\in\mu xX.\phi\urcorner\tau)=d_\mu(\tau) for all \tau.

Fix some ordinal bound o^F on F. We define an ordinal bound o^{F^{\uparrow}} on F^{\uparrow} by setting o^{F^\uparrow}(\sigma)=o^F(\pi(\sigma))[v_{\epsilon}\mapsto v_{\rho_\sigma(\epsilon)}].

As in the proof of Theorem 4.14, we define D_c(d)(\sigma) by induction on |\sigma| for all d simultaneously, as well as partial functions \pi_d:\operatorname{dom}(D_c(d))\rightarrow\operatorname{dom}(d). The assignment of ordinals, o^{D_c(d)}, is similar to Lemma 4.27, setting o^{D_c(d)}(\sigma)=\vartheta_{c+1,\gamma} o^d(\sigma)[\Omega_{c+1}\mapsto\beta] when \pi_d(\sigma) is defined, and copying over o^{D_c(d)}(\sigma\top\upsilon)=o^{D_c(\bar d^{\uparrow \mathsf{ID}^\infty_{c,<0}}_\bot(D_m(d_\top)))}(\upsilon) after removing a \mathrm{Cut}\Omega^\flat at d(\pi_d(\sigma)).

When d(\pi_d(\sigma)) is not \mathrm{Cut}\Omega^\flat_{n\in\mu xX.\phi} where \phi has depth c+1, we need to check that o^{D_m(d)}(\sigma\iota)=\vartheta_{c+1,\gamma}(o^d(\pi_d(\sigma\iota))[\Omega_{c+1}\mapsto\beta])\ll^{c}_0\vartheta_{c+1,\gamma} (o^d(\pi_d(\sigma))[\Omega_{m+1}\mapsto\beta])=o^{D_c(d)}(\sigma).

The significant case is when d(\pi_d(\sigma))=\mathrm{Cut}\Omega^\flat_{n\in\mu xX.\phi} where \phi has depth c+1. We set D_m(d)(\sigma)=\mathrm{Rep} and D_c(d)(\sigma\top\upsilon)=D_c(\bar d^{\uparrow \mathsf{ID}^\infty_{c,<0}}_\bot(D_c(d_\top)))(\upsilon)—the only difference is that \bar d_\bot is only a function on proofs in \mathsf{ID}^{\infty,+}_{c+1,<0}, and we use lifting to extend it to a function on proofs in \mathsf{ID}^{\infty,+}_{c+1,<0}\cup\mathsf{ID}^\infty_{c,<0} as needed.

The ordinal bound o^{D_c(d)}(\sigma\top)\ll^{c}_0 o^{D_m(d)}(\sigma) is as above. We can then check that

is \ll^{c}_0 o^{D_c(d)}(\sigma).

We set o^{d_{n\in\mu xX.\phi}}(\langle\top\rangle)=v_{n\in\mu xX.\phi,\langle\rangle}(v_{\mu yY.\phi'})\#1. In general, at some \sigma deducing

we set o^{d_{n\in\mu xX.\phi}}(\sigma)=v_{n\in\mu xX.\phi,\epsilon}(v_{\mu yY.\phi'},v_{m_1\in\mu yY.\phi',\epsilon_1},\ldots, v_{m_k\in\mu yY.\phi',\epsilon_k}).

The argument is essentially the same as before. Once again we define D_{\underline{\mathtt{\Omega}}}(d)(\sigma) by induction on |\sigma| for all d simultaneously along with the partial function \pi_d:\operatorname{dom}(D_{\underline{\mathtt{\Omega}}}(d))\rightarrow\operatorname{dom}(d). We can then define the ordinal assignment o^{D_{\underline{\mathtt{\Omega}}}(d)}:\operatorname{dom}(D_{\underline{\mathtt{\Omega}}}(d))\rightarrow\operatorname{dom}(d). Naturally we begin by setting \pi_d(\langle\rangle)=\langle\rangle.

As long as d(\pi_d(\sigma)) is anything other than a \mathrm{Cut}\Omega^\flat_{n\in\mu xX.\phi} where n\in\mu xX.\phi has depth \underline{\mathtt{\Omega}}, we may set D_{\underline{\mathtt{\Omega}}}(d)(\sigma)=d(\pi_d(\sigma)) and set \pi_d(\sigma\iota)=\pi_d(\sigma)\iota.

The main case is when d(\pi_d(\sigma)) is a \mathrm{Cut}\Omega^\flat_{n\in\mu xX.\phi} where n\in\mu xX.\phi has depth \underline{\mathtt{\Omega}}. As always, we set D_{\underline{\mathtt{\Omega}}}(d)(\sigma)=\mathrm{Rep} and D_{\underline{\mathtt{\Omega}}}(d)(\sigma\top\upsilon)=D_{\underline{\mathtt{\Omega}}}(\overline{d}^{\uparrow \mathsf{ID}^{\infty}_{C_0-1,<0}}_{\pi_d(\sigma)\bot}(D_{\underline{\mathtt{\Omega}}}(d_{\pi_d(\sigma)\top})))(\upsilon).

When \pi_d(\sigma) is defined, we set o^{D_{\underline{\mathtt{\Omega}}}(d)}(\sigma)=\vartheta_{\underline{\mathtt{\Omega}},\gamma}(o^d(\pi_d(\sigma))). Otherwise we copy over o^{D_{\underline{\mathtt{\Omega}}}(d)}(\sigma\top\upsilon)=o^{D_{\underline{\mathtt{\Omega}}}(\overline{d}^{\uparrow \mathsf{ID}^{\infty}_{C_0-1,<0}}_{\pi_d(\sigma)\bot}(D_{\underline{\mathtt{\Omega}}}(d_{\pi_d(\sigma)\top})))}(\upsilon).

When d(\pi_d(\sigma)) is not \mathrm{Cut}\Omega^\flat_{n\in\mu xX.\phi}, we have o^{D_d(d)}(\sigma\iota)=\vartheta_{\underline{\mathtt{\Omega}},\gamma}o^d(\pi_d(\sigma\iota)), and since o^d(\pi_d(\sigma\iota))\ll_\gamma o^d(\pi_d(\sigma)), we have o^{D_d(d)}(\sigma\iota)\ll_0\vartheta_{\underline{\mathtt{\Omega}},\gamma}o^d(\pi_d(\sigma))=o^{D_d(d)}(\sigma).

When d(\pi_d(\sigma)) is \mathrm{Cut}\Omega^\flat_{n\in\mu xX.\phi} we have

Since o^d(\pi_d(\sigma)\top)\ll_{\gamma} o^d(\pi_d(\sigma)) and o^d(\pi_d(\sigma)\bot)\ll_{\underline{\mathtt{\Omega}},\gamma} o^d(\pi_d(\sigma)), we have o^{D_d}(\sigma\top)\ll_0o^{D_d}(\sigma) as needed.