ch:first-order-proof-theory: ch:first-order-proof-theory

The displayed binder $y$ would capture the free $y$ being inserted. Choose $a\notin \{x,y\}$ fresh and open the existential at $a$: Its free-variable set is $\{y\}$. The occurrences of $a$ are bound by the existential. Naive textual replacement would give $\mathrm{\exists }y(R(y,y)\wedge P(y))$, in which the inserted occurrence of $y$ in the first argument of $R$ has been captured.

Put $H=\mathrm{\forall }x(P(x)\wedge Q(x))$. Choose distinct eigenvariables $a,b$ absent from $H$. The complete cut-free derivation is $$\frac{\begin{array}{c}{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{\phantom{X}}{P(a)\Rightarrow P(a)}}\mathrm{Ax}}{P(a)\wedge Q(a)\Rightarrow P(a)}}{\mathrm{L}}_1}{H\Rightarrow P(a)}}\mathrm{L}}{H\Rightarrow \mathrm{\forall }xP(x)}}\mathrm{R}\\ {\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{{\displaystyle \frac{\phantom{X}}{Q(b)\Rightarrow Q(b)}}\mathrm{Ax}}{P(b)\wedge Q(b)\Rightarrow Q(b)}}{\mathrm{L}}_2}{H\Rightarrow Q(b)}}\mathrm{L}}{H\Rightarrow \mathrm{\forall }xQ(x)}}\mathrm{R}\end{array}}{H\Rightarrow (\mathrm{\forall }xP(x))\wedge (\mathrm{\forall }xQ(x))}\mathrm{R}.$$ The eigenvariable checks are $a\notin \mathrm{fv}(H)$ and $b\notin \mathrm{fv}(H)$. Both Ax leaves already have their full side contexts, which are empty. No ${\mathrm{W}}_L$ application occurs or is needed.

Let $\mathrm{\Gamma }=\{\mathrm{\forall }x(P(x)\to Q(x)),\mathrm{\exists }xP(x)\}$. Translating the outer $\mathrm{\exists }$L gives the following $\mathrm{\exists }$E tree: $$\frac{\begin{array}{c}{\displaystyle \frac{\mathrm{\exists }xP(x)\in \mathrm{\Gamma }}{\mathrm{\Gamma }{⊢}_{\mathsf{N}}\mathrm{\exists }xP(x)}}\mathrm{Hyp}\\ {\displaystyle \frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{{\displaystyle \frac{\mathrm{\forall }x(P(x)\to Q(x))\in \mathrm{\Gamma },P(a)}{\mathrm{\Gamma },P(a){⊢}_{\mathsf{N}}\mathrm{\forall }x(P(x)\to Q(x))}}\mathrm{Hyp}}{\mathrm{\Gamma },P(a){⊢}_{\mathsf{N}}P(a)\to Q(a)}}\mathrm{E}\\ {\displaystyle \frac{P(a)\in \mathrm{\Gamma },P(a)}{\mathrm{\Gamma },P(a){⊢}_{\mathsf{N}}P(a)}}\mathrm{Hyp}\end{array}}{\mathrm{\Gamma },P(a){⊢}_{\mathsf{N}}Q(a)}}\to \mathrm{E}}{\mathrm{\Gamma },P(a){⊢}_{\mathsf{N}}\mathrm{\exists }xQ(x)}}\mathrm{I}\end{array}}{\mathrm{\Gamma }{⊢}_{\mathsf{N}}\mathrm{\exists }xQ(x)}\mathrm{E}.$$ The whole displayed tree is the requested $\mathrm{\exists }$E subderivation. The LJ eigenvariable condition for the final $\mathrm{\exists }$L says that $a$ is absent from $\mathrm{\Gamma }$, the conclusion, and the existential formula being eliminated. Translation changes only rule notation and not any of those formulas or contexts, so exactly the same freshness check licenses $\mathrm{\exists }$E.

The unreduced principal cut has the form $$\frac{\begin{array}{c}{\displaystyle \frac{\mathcal{D}:\mathrm{\Gamma }\Rightarrow B[t/x]}{\mathrm{\Gamma }\Rightarrow \mathrm{\exists }xB}}\mathrm{Some}-\mathrm{R}\\ {\displaystyle \frac{\begin{array}{c}\mathcal{E}:\mathrm{\Delta },B[a/x]\Rightarrow C\\ a\notin \mathrm{fv}(\mathrm{\Delta },C,\mathrm{\exists }xB)\end{array}}{\mathrm{\Delta },\mathrm{\exists }xB\Rightarrow C}}\mathrm{Some}-\mathrm{L}\end{array}}{\mathrm{\Gamma },\mathrm{\Delta }\Rightarrow C}\mathrm{Cut}.$$ First alpha-freshen $a$ away from $t,\mathrm{\Gamma },\mathrm{\Delta },C$. Individual substitution sends $\mathcal{E}$ to a derivation $\mathcal{E}[t/a]:\mathrm{\Delta },B[t/x]\Rightarrow C$; the conclusion is unchanged because $a\notin \mathrm{fv}(\mathrm{\Delta },C)$. The reduct is $$\frac{\begin{array}{c}\mathcal{D}:\mathrm{\Gamma }\Rightarrow B[t/x]\\ \mathcal{E}[t/a]:\mathrm{\Delta },B[t/x]\Rightarrow C\end{array}}{\mathrm{\Gamma },\mathrm{\Delta }\Rightarrow C}\mathrm{Cut}.$$ Its cut formula $B[t/x]$ is a proper instance of the body of the original existential formula, hence has smaller formula rank.

Let $\mathcal{D}:\mathrm{\Gamma }\Rightarrow A$, and suppose the derivation using $A$ ends in a nonprincipal $\vee$L: $$\frac{\begin{array}{c}\mathcal{D}:\mathrm{\Gamma }\Rightarrow A\\ {\displaystyle \frac{\begin{array}{c}{\mathcal{E}}_B:\mathrm{\Delta },A,B\Rightarrow K\\ {\mathcal{E}}_C:\mathrm{\Delta },A,C\Rightarrow K\end{array}}{\mathrm{\Delta },A,B\vee C\Rightarrow K}}\mathrm{L}\end{array}}{\mathrm{\Gamma },\mathrm{\Delta },B\vee C\Rightarrow K}\mathrm{Cut}.$$ Because $B\vee C\ne A$, the cut formula is a side formula of the final rule. Commute the cut into both premises and rebuild $\vee$L: $$\frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}\mathcal{D}:\mathrm{\Gamma }\Rightarrow A\\ {\mathcal{E}}_B:\mathrm{\Delta },A,B\Rightarrow K\end{array}}{\mathrm{\Gamma },\mathrm{\Delta },B\Rightarrow K}}\mathrm{Cut}\\ {\displaystyle \frac{\begin{array}{c}\mathcal{D}:\mathrm{\Gamma }\Rightarrow A\\ {\mathcal{E}}_C:\mathrm{\Delta },A,C\Rightarrow K\end{array}}{\mathrm{\Gamma },\mathrm{\Delta },C\Rightarrow K}}\mathrm{Cut}\end{array}}{\mathrm{\Gamma },\mathrm{\Delta },B\vee C\Rightarrow K}\mathrm{L}.$$ Both new cuts still cut on $A$, so their formula rank is $|A|$. The old height sum is $h(\mathcal{D})+1+max(h({\mathcal{E}}_B),h({\mathcal{E}}_C))$. The two recursive sums are respectively $h(\mathcal{D})+h({\mathcal{E}}_B)$ and $h(\mathcal{D})+h({\mathcal{E}}_C)$, each strictly smaller.

Put $H=\mathrm{\forall }x(P(x)\to Q(x))$. With $T=\{c,d\}$ and $c$ enumerated first, the first $\mathrm{\forall }$L choice adds $P(c)\to Q(c)$. Its $\to$L premises ask for $P(c)$ and continue from $Q(c)$ toward $Q(d)$; neither closes by Ax, so this alternative fails. The next $\mathrm{\forall }$L choice uses $d$, and the remaining branch closes by $\to$L and two axioms: $$\frac{{\displaystyle \frac{\begin{array}{c}P(d)\Rightarrow P(d)\\ Q(d)\Rightarrow Q(d)\end{array}}{P(d),P(d)\to Q(d)\Rightarrow Q(d)}}\mathrm{Imp}-\mathrm{L}}{P(d),H\Rightarrow Q(d)}\mathrm{All}-\mathrm{L}.$$ Counting an axiom as height one gives height three, so a height-first search has an upper bound of three. It cannot have height two: the atomic goal is not Ax in the initial context, so its last rule must first expose the universal assumption by All-L. The resulting atomic goal is still not Ax; its last rule must expose the instantiated implication by Imp-L. Only the two premises of that second logical rule are Ax leaves. Thus every derivation has height at least three, independently of the order in which search tries rule instances. Reversing the enumeration tries $d$ first and removes the failed $c$-sibling. Enumeration order changes failed work before success, not the least derivation height. Enlarging $T$ adds only legal instances and therefore preserves soundness, but each quantifier choice can add branches before the successful instance is tried.

Label the universal assumption by $h$ and the existential assumption by $k$. A proof term for the running derivation is $$\mathsf{unpack}(k;a,p.\mathsf{pack}(a,h[a]p)).$$ Indeed, inside the unpack body, $h[a]:P(a)\to Q(a)$, so $h[a]p:Q(a)$, and packing witness $a$ gives $\mathrm{\exists }xQ(x)$. The unpack eigenvariable is absent from the outer context and result formula.

Replace $k$ by a package $\mathsf{pack}(c,p)$, where $p:P(c)$. The existential beta step is In the corresponding principal cut, the producing derivation ends with $\mathrm{\exists }$R from $P(c)$, while the using derivation ends with $\mathrm{\exists }$L from a premise using $P(a)$. Freshen $a$, substitute $c/a$ through the using premise, and replace the cut on $\mathrm{\exists }xP(x)$ by a cut on the smaller formula $P(c)$. The final proof-label substitution of $p$ for $u$ is exactly the existential beta contraction displayed above; it is not the structural rule C-L.

Delete the side condition from $\mathrm{\exists }$E. From the second assumption and a temporary assumption $P(a)$, implication elimination yields $R(a)$: $$\frac{\begin{array}{c}\mathrm{\exists }xP(x)\\ {\displaystyle \frac{\begin{array}{c}P(a)\to R(a)\\ P(a)\end{array}}{R(a)}}\to \mathrm{E}\end{array}}{R(a)}\mathrm{E}.$$ The displayed derivation is invalid in the real system because $a$ occurs free in the undischarged assumption and in the conclusion. To see the semantic failure, use a two-element domain with $a=0$, let $P(1)$ be true and $P(0)$ false, and let $R(0)$ be false. Then $\mathrm{\exists }xP(x)$ is true and $P(a)\to R(a)$ is vacuously true, while $R(a)$ is false.

Write $H=\mathrm{\forall }x(P(x)\to Q(x))$, and choose $a\notin \mathrm{fv}(H,c)$. The producing and using derivations are $$\mathcal{D}=\frac{{\displaystyle \frac{\phantom{X}}{P(c)\Rightarrow P(c)}}\mathrm{Ax}}{P(c)\Rightarrow \mathrm{\exists }xP(x)}\mathrm{R},$$ $${\mathcal{E}}_a=\frac{{\displaystyle \frac{{\displaystyle \frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{P(a)\Rightarrow P(a)}}\mathrm{Ax}\\ {\displaystyle \frac{{\displaystyle \frac{\phantom{X}}{Q(a)\Rightarrow Q(a)}}\mathrm{Ax}}{Q(a)\Rightarrow \mathrm{\exists }xQ(x)}}\mathrm{R}\end{array}}{P(a),P(a)\to Q(a)\Rightarrow \mathrm{\exists }xQ(x)}}\to \mathrm{L}}{H,P(a)\Rightarrow \mathrm{\exists }xQ(x)}}\mathrm{L}}{H,\mathrm{\exists }xP(x)\Rightarrow \mathrm{\exists }xQ(x)}\mathrm{L}.$$

Cutting $\mathcal{D}$ against ${\mathcal{E}}_a$ on $\mathrm{\exists }xP(x)$ derives $P(c),H\Rightarrow \mathrm{\exists }xQ(x)$. With axioms at height one, $h(\mathcal{D})=2$ and $h({\mathcal{E}}_a)=5$. The quantified cut formula has rank one, so the initial measure is $(1,7)$.

Both last rules are principal. Substitute $c$ for the fresh eigenvariable $a$ in the minor premise of $\mathrm{\exists }$L and replace the original cut by $$\frac{\begin{array}{c}{\displaystyle \frac{\phantom{X}}{P(c)\Rightarrow P(c)}}\mathrm{Ax}\\ H,P(c)\Rightarrow \mathrm{\exists }xQ(x)\end{array}}{P(c),H\Rightarrow \mathrm{\exists }xQ(x)}\mathrm{Cut}.$$ The new cut formula $P(c)$ has rank zero. Its premises have heights one and four, so the measure is . The left premise is Ax; eliminating this identity cut leaves the instantiated minor derivation and no residual cuts.

Bounded cut-free search with pool $\{c\}$ can return that same minor derivation after the substitution $c/a$: instantiate $H$ by $c$, use $\to$L, and introduce the existential with witness $c$. A different rule order may introduce the existential earlier or print exchanges and weakenings explicitly. Both trees prove the same end sequent and contain no Cut, but the calculus does not make their printed syntax canonical.