First-Order Proof Theory and Sequent Calculi

Proof. Here formation means that substituting a term for a variable in a term or formula produces another term or formula of the same syntactic category. Prove this claim and both equations simultaneously by structural induction on $E$. Function and predicate applications apply the induction hypothesis to each argument. For the absent-source equation at $E=\mathrm{\forall }zB$, first consider $z=x$. Then $(\mathrm{\forall }xB)[t/x]=\mathrm{\forall }xB$ by the binding clause. If $z\ne x$, alpha-freshen it away from $\mathrm{fv}(t)\cup \{x\}$; the induction hypothesis for $B$ proves the equation under the reattached quantifier. For composition, alpha-freshen $z$ away from $\mathrm{fv}(t)\cup \mathrm{fv}(u)\cup \{x,y\}$. Both sides are $$\mathrm{\forall }z(B[t/x][u/y])\text{and}\mathrm{\forall }z(B[u/y][t[u/y]/x]),$$ which are equal by the induction hypothesis for $B$. The existential case is identical; each propositional connective recurses in both arguments. The rank equation holds in the same induction: replacing individual variables inside terms changes no logical connective or quantifier node. ◻

Proof. Prove all four assertions simultaneously by structural induction on terms and formulas. Variables use agreement directly, constants have fixed denotations, and a function application uses the term hypotheses for all arguments. The atomic case applies the term assertions to its arguments, and each propositional connective applies the formula hypotheses to its immediate subformulas. For $\mathrm{\forall }yB$ and $\mathrm{\exists }yB$, alpha-freshen $y$ away from $x$ and $\mathrm{fv}(u)$. The induction hypothesis for $B$ then applies to each update at $y$. Updates at the distinct variables $x$ and $y$ commute, which gives the substitution equations under the reattached quantifier. ◻

Proof. Fix an interpretation $\mathcal{M}$ and induct on the natural-deduction derivation. Hypothesis and the propositional rules follow directly from the truth clauses in definition 3.5. In the quantifier cases, use assignment agreement and semantic substitution from lemma 3.6.

For $\mathrm{\forall }\mathrm{I}$, the semantic goal is to start from truth of $\mathrm{\Gamma }$ under $\rho$ and prove $A$ under every update $\rho [x\mapsto d]$. Its premise derives $\mathrm{\Gamma }{⊢}_{\mathsf{N}}A[a/x]$, with $a\notin \mathrm{fv}(\mathrm{\Gamma },\mathrm{\forall }xA)$. Suppose $\mathrm{\Gamma }$ is true under $\rho$, and fix $d\in D$. Put ${\rho }^{\prime }=\rho [a\mapsto d]$. Assignment agreement keeps every assumption true under ${\rho }^{\prime }$. The induction hypothesis makes $A[a/x]$ true under ${\rho }^{\prime }$. Semantic substitution makes $A$ true under ${\rho }^{\prime }[x\mapsto d]$. If $a=x$, this is exactly $\rho [x\mapsto d]$. Otherwise it agrees with $\rho [x\mapsto d]$ on the free variables of $A$ because $a\notin \mathrm{fv}(\mathrm{\forall }xA)$. Another application of assignment agreement therefore makes $A$ true under $\rho [x\mapsto d]$. Since $d$ was arbitrary, $\mathrm{\forall }xA$ is true under $\rho$.

For $\mathrm{\forall }\mathrm{E}$, the induction hypothesis makes $\mathrm{\forall }xA$ true under $\rho$. Hence $A$ is true under $\rho [x\mapsto [[t{]]}_{\rho }]$. Semantic substitution makes $A[t/x]$ true under $\rho$, as required. For $\mathrm{\exists }\mathrm{I}$, the premise induction hypothesis makes $A[t/x]$ true under $\rho$. The same equation makes $A$ true under $\rho [x\mapsto [[t{]]}_{\rho }]$, so that denotation is a witness for $\mathrm{\exists }xA$.

For $\mathrm{\exists }\mathrm{E}$, suppose its major premise proves $\mathrm{\Gamma }{⊢}_{\mathsf{N}}\mathrm{\exists }xA$, its minor premise proves $\mathrm{\Gamma },A[a/x]{⊢}_{\mathsf{N}}C$, and $a\notin \mathrm{fv}(\mathrm{\Gamma },C,\mathrm{\exists }xA)$. If $\mathrm{\Gamma }$ is true under $\rho$, the major induction hypothesis gives $d\in D$ such that $A$ is true under $\rho [x\mapsto d]$. Put ${\rho }^{\prime }=\rho [a\mapsto d]$. The substitution equation makes $A[a/x]$ true under ${\rho }^{\prime }$, while assignment agreement keeps $\mathrm{\Gamma }$ true there. The minor induction hypothesis makes $C$ true under ${\rho }^{\prime }$; assignment agreement and freshness of $a$ for $C$ make $C$ true under $\rho$. These are exactly the two cases using eigenvariable freshness. The four quantifier cases, together with the propositional truth clauses, exhaust the rule induction. ◻

Proof. Hypothesis gives $P(a){⊢}_{\mathsf{N}}P(a)$. The unsound rule would generalize this derivation to $P(a){⊢}_{\mathsf{N}}\mathrm{\forall }xP(x)$. In a two-element interpretation with elements $d_0,d_1$, let the assignment send $a$ to $d_0$, and interpret $P$ by $\{d_0\}$. The premise is true and the conclusion false. The condition $a\notin \mathrm{fv}(\mathrm{\Gamma })$ blocks exactly this derivation.

For the second failure, take $A=P(x)\to P(a)$ and an empty context. Implication identity derives ${⊢}_{\mathsf{N}}P(a)\to P(a)=A[a/x]$. A rule checking only the context would then derive ${⊢}_{\mathsf{N}}\mathrm{\forall }x(P(x)\to P(a))$. Interpret $a$ as one element where $P$ is false and let $P$ hold at another element. The displayed universal formula is false. Requiring $a\notin \mathrm{fv}(\mathrm{\Gamma },\mathrm{\forall }xA)$ blocks this second derivation as well. ◻

Proof. Prove by induction on the derivation the assertion for every finite forbidden set $X$. The induction hypothesis may therefore be applied to each immediate premise with any enlarged finite set. Rebuild every rule without an eigenvariable from the resulting premise derivations.

Suppose the last rule is $\mathrm{\forall }\mathrm{I}$ with eigenvariable $a$; the $\mathrm{\exists }\mathrm{E}$ case has the same two binding positions. Apply the induction hypothesis to each scoped premise with the strengthened forbidden set $X\cup \{a\}$. Let $Z$ be the finite set of all individual variables occurring in that transformed premise derivation. If $a\notin X$, retain $a$. If $a\in X$, choose $b\notin X\cup Z$ and consistently rename the occurrences governed by the outer rule from $a$ to $b$. Structural induction on the transformed premise shows that each rule instance remains valid; in particular, $A[a/x]$ becomes $A[b/x]$. No nested eigenvariable is captured because $b\notin Z$. The outer eigenvariable is absent from the end judgment by the rule’s side condition, so the end judgment is unchanged. The premise height and final rule node are unchanged. Thus every nested eigenvariable avoids $X$, and the outer one does as well. ◻

Proof. Apply lemma 3.9 to each scoped premise with forbidden set $X\cup \{b\}$. The transformed nested eigenvariables therefore avoid $b$. Consistently rename the outer eigenvariable to $b$; the freshness hypothesis keeps the end judgment fixed, and the preceding avoidance prevents capture. Renaming changes no rule node. ◻

Proof. For (a), induct on the derivation and enlarge every context. In a quantifier case use lemma 3.9 with $X=\mathrm{fv}(\mathrm{\Delta })$ before applying the induction hypothesis. For (b), induct again. The only binder case is $\mathrm{\forall }$I or $\mathrm{\exists }$E; choose its eigenvariable $b$ outside $\mathrm{fv}(t)\cup \{a\}$. Thus $b\ne a$, so substitution passes through the eigenbinder rather than stopping at it. Then lemma 3.3 gives the required commutation of formula substitution with the binder, while freshness preserves the rule’s side condition. For (c), induct on the derivation of $\mathrm{\Gamma },A{⊢}_{\mathsf{N}}C$. A use of the distinguished hypothesis is replaced by the given derivation. If the leaf occurs under local assumptions $\mathrm{\Theta }$, clause (a) first weakens $\mathrm{\Delta }{⊢}_{\mathsf{N}}A$ to $\mathrm{\Delta },\mathrm{\Theta }{⊢}_{\mathsf{N}}A$; the replacement therefore has exactly the leaf’s local context. At that leaf the transformation is $$\frac{A\in \mathrm{\Gamma },A,\mathrm{\Theta }}{\mathrm{\Gamma },A,\mathrm{\Theta }{⊢}_{\mathsf{N}}A}\mathrm{Hyp}\text{is replaced by}{\mathcal{W}}_{\mathrm{\Gamma },\mathrm{\Theta }}(\mathcal{D}):\mathrm{\Gamma },\mathrm{\Delta },\mathrm{\Theta }{⊢}_{\mathsf{N}}A,$$ where $\mathcal{D}:\mathrm{\Delta }{⊢}_{\mathsf{N}}A$ and ${\mathcal{W}}_{\mathrm{\Gamma },\mathrm{\Theta }}$ is weakening by clause (a). Every rule above that leaf is reconstructed from the transformed premises. In an $\mathrm{\exists }$E case freshen the local eigenvariable away from $\mathrm{\Delta }$ before using the induction hypotheses. For clause (d), induct on the derivation. A hypothesis leaf depends only on membership, so replacing two copies of $A$ by one preserves it. Rebuild every connective rule from the induction hypotheses. In a quantifier rule, alpha-freshen its eigenvariable away from $A$ before rebuilding the rule; the side condition is then unchanged. ◻

Proof. Prove by induction on the LJ derivation the assertion for every finite forbidden set $X$. The induction hypothesis may therefore be applied to an immediate premise with any enlarged finite set. Rebuild a rule without an eigenvariable from the resulting premises.

Suppose the final rule has outer eigenvariable $a$. Apply the induction hypothesis to its scoped premise with forbidden set $X\cup \{a\}$. Let $Z$ contain every individual variable occurring in the transformed premise derivation. Retain $a$ if $a\notin X$. Otherwise choose $b\notin X\cup Z$ and rename the occurrences governed by the final rule from $a$ to $b$. Structural induction on the premise preserves every LJ rule instance and changes $A[a/x]$ to $A[b/x]$. The side condition keeps the outer name absent from the end sequent, and $b\notin Z$ prevents capture of nested eigenvariables. No rule node is added or deleted. ◻

Proof. Freshen the scoped premise by lemma 3.13 with forbidden set $X\cup \{b\}$, and then consistently rename the outer eigenvariable to $b$. The rule’s freshness condition fixes the end sequent, and the nested avoidance condition prevents capture. ◻

Proof. Fix an interpretation and assignment $\rho$, and induct on the derivation. Ax selects a true antecedent formula. Weakening and contraction preserve the conditions imposed by antecedent truth. For Cut, antecedent truth and the left induction hypothesis make the cut formula true; the right induction hypothesis then makes the succedent true. For a representative branching propositional case, suppose the last rule is $\vee \mathrm{L}$. Truth of $A\vee B$ gives either truth of $A$ or truth of $B$; apply the induction hypothesis for the corresponding premise. Rule $\to \mathrm{L}$ first uses its left induction hypothesis to make $A$ true. Truth of $A\to B$ then makes $B$ true, so the right induction hypothesis yields the succedent. The remaining propositional rules apply the displayed truth clause for their principal connective.

For $\mathrm{\forall }\mathrm{L}$, truth of $\mathrm{\forall }xA$ gives truth of $A$ under $\rho [x\mapsto [[t{]]}_{\rho }]$. Semantic substitution makes $A[t/x]$ true under $\rho$, so the premise induction hypothesis applies. For $\mathrm{\exists }\mathrm{R}$, the premise makes $A[t/x]$ true; semantic substitution makes $[[t{]]}_{\rho }$ a witness. The $\mathrm{\forall }\mathrm{R}$ argument is the $\mathrm{\forall }\mathrm{I}$ argument of lemma 3.7 with sequents in place of natural-deduction judgments. The $\mathrm{\exists }\mathrm{L}$ argument is its $\mathrm{\exists }\mathrm{E}$ minor-premise argument: update the fresh eigenvariable to the witness supplied by the true existential. These cases exhaust LJ. ◻

Proof. Individual substitution is induction on the derivation, with eigenvariables freshened by lemma 3.13 away from the source variable and the free variables of the inserted term. In a final $\mathrm{\forall }\mathrm{R}$ or $\mathrm{\exists }\mathrm{L}$ case, choose the eigenvariable $b$ outside that set, apply the induction hypothesis to the premise, use lemma 3.3 to commute the two individual substitutions, and rebuild the same quantified rule. Each weakening or contraction is already a primitive LJ rule. Append the required rule instances one at a time. None is Cut, so the result remains cut-free. ◻

Proof. For implication, weaken both premises to $\mathrm{\Gamma },\mathrm{\Delta }$, apply the shared-context $\to \mathrm{E}$ rule, and obtain exactly $\mathrm{\Gamma },\mathrm{\Delta }{⊢}_{\mathsf{N}}B$. For disjunction, weaken all three premises to $\mathrm{\Gamma },\mathrm{\Delta },\mathrm{\Theta }$, preserving the temporary assumption in each minor premise; the shared-context $\vee \mathrm{E}$ rule already has the required conclusion. For existential elimination, first use corollary 3.10 to choose its eigenvariable away from $\mathrm{\Gamma },\mathrm{\Delta },C,\mathrm{\exists }xA$. Weaken the major and minor premises to $\mathrm{\Gamma },\mathrm{\Delta }$ and apply $\mathrm{\exists }\mathrm{E}$; again the shared rule has exactly the required context. Bottom elimination is followed by weakening. The unary forms are the original rule instances. ◻

Proof. From natural deduction to LJ, induct on the natural-deduction derivation. Use the admissible forms of lemma 3.17; a shared-context source rule is their instance with equal contexts. Introduction rules become the corresponding right rules. For implication elimination, translate the premises to $\mathrm{\Gamma }\Rightarrow A\to B$ and $\mathrm{\Delta }\Rightarrow A$. Rule $\to \mathrm{L}$, with the second premise $B\Rightarrow B$, derives $\mathrm{\Delta },A\to B\Rightarrow B$; Cut against the first translation derives $\mathrm{\Gamma },\mathrm{\Delta }\Rightarrow B$. When the source is the primitive shared-context rule, $\mathrm{\Gamma }=\mathrm{\Delta }$; contract the duplicated assumption occurrences to recover its one-copy source context.

Disjunction elimination is different because it has two minor branches. Translations $$\mathrm{\Gamma }\Rightarrow A\vee B,\mathrm{\Delta },A\Rightarrow C,\mathrm{\Theta },B\Rightarrow C$$ are first weakened so that the two minor premises share $\mathrm{\Delta },\mathrm{\Theta }$. Rule $\vee \mathrm{L}$ then derives $\mathrm{\Delta },\mathrm{\Theta },A\vee B\Rightarrow C$, and Cut with the major translation derives $\mathrm{\Gamma },\mathrm{\Delta },\mathrm{\Theta }\Rightarrow C$. Contract precisely the occurrences duplicated when source contexts coincide.

For existential elimination, first use corollary 3.10 to choose its eigenvariable away from both source contexts. Translate its major and minor premises to $$\mathrm{\Gamma }\Rightarrow \mathrm{\exists }xA,\mathrm{\Delta },A[a/x]\Rightarrow C.$$ Then $\mathrm{\exists }\mathrm{L}$ derives $\mathrm{\Delta },\mathrm{\exists }xA\Rightarrow C$, and Cut derives $\mathrm{\Gamma },\mathrm{\Delta }\Rightarrow C$. The source freshness condition is now exactly the LJ condition on the rebuilt left rule. Conjunction and universal elimination follow the same unary schema: use the matching left rule on an Ax leaf for the selected component or instance, then Cut the translated major premise. If the source existential elimination used one shared context, contract the two translated copies after the Cut. Bottom elimination uses $\mathrm{\perp }\mathrm{L}$ followed by Cut. These are all natural-deduction rule families.

From LJ to natural deduction, induct on the sequent derivation. Right rules are the corresponding introductions. For $\to \mathrm{L}$, the induction hypotheses give $\mathrm{\Gamma }{⊢}_{\mathsf{N}}A$ and $\mathrm{\Delta },B{⊢}_{\mathsf{N}}C$. Under $\mathrm{\Gamma },\mathrm{\Delta },A\to B$, implication elimination applied to the principal hypothesis and the weakened proof of $A$ gives $B$; proof substitution from lemma 3.11(c) inserts that proof into the translated right premise.

For $\vee \mathrm{L}$, use the principal hypothesis $A\vee B$ as the major premise of $\vee \mathrm{E}$ and the two translated premises as its minor branches. For $\mathrm{\exists }\mathrm{L}$, use the principal hypothesis $\mathrm{\exists }xA$ as the major premise of $\mathrm{\exists }\mathrm{E}$ and the translated LJ premise as its minor premise. The LJ side condition is literally the natural-deduction side condition. Conjunction left, universal left use the matching unary elimination on the principal hypothesis and then clause (c) to insert the result into the translated premise. The nullary $\mathrm{\perp }\mathrm{L}$ case is direct: from the principal hypothesis $h:\mathrm{\perp }$, rule $\mathrm{\perp }\mathrm{E}$ derives the required conclusion, with no translated premise to substitute into. Cut is clause (c) itself. Weakening uses clause (a), contraction uses clause (d), and Ax uses Hyp. The displayed constructions cover every branching and binding form; the unary schema covers exactly $\wedge {\mathrm{L}}_i$ and $\mathrm{\forall }\mathrm{L}$. ◻

Proof. The reductions are determined by the outer constructor of $A$.

For $A=A_1\wedge A_2$, the derivation producing $A$ ends in $\wedge$R and the derivation using $A$ ends in $\wedge {\mathrm{L}}_i$. The complete local replacement is $$\frac{\begin{array}{c}{\displaystyle \frac{\begin{array}{c}{\mathcal{D}}_1:\mathrm{\Gamma }\Rightarrow A_1\\ {\mathcal{D}}_2:\mathrm{\Gamma }\Rightarrow A_2\end{array}}{\mathrm{\Gamma }\Rightarrow A_1\wedge A_2}}\mathrm{R}\\ {\displaystyle \frac{\mathcal{E}:\mathrm{\Delta },A_i\Rightarrow C}{\mathrm{\Delta },A_1\wedge A_2\Rightarrow C}}{\mathrm{L}}_{\mathrm{i}}\end{array}}{\mathrm{\Gamma },\mathrm{\Delta }\Rightarrow C}\mathrm{Cut}.$$ Replace it by $$\frac{\begin{array}{c}{\mathcal{D}}_i:\mathrm{\Gamma }\Rightarrow A_i\\ \mathcal{E}:\mathrm{\Delta },A_i\Rightarrow C\end{array}}{\mathrm{\Gamma },\mathrm{\Delta }\Rightarrow C}\mathrm{Cut}.$$ The replacement cuts on the proper subformula $A_i$.

For $A=A_1\vee A_2$, the producing rule is $\vee {\mathrm{R}}_i$ and the using rule is $\vee$L. The reduction is $$\frac{\begin{array}{c}{\displaystyle \frac{{\mathcal{D}}_i:\mathrm{\Gamma }\Rightarrow A_i}{\mathrm{\Gamma }\Rightarrow A_1\vee A_2}}{\mathrm{R}}_{\mathrm{i}}\\ {\displaystyle \frac{\begin{array}{c}{\mathcal{E}}_1:\mathrm{\Delta },A_1\Rightarrow C\\ {\mathcal{E}}_2:\mathrm{\Delta },A_2\Rightarrow C\end{array}}{\mathrm{\Delta },A_1\vee A_2\Rightarrow C}}\mathrm{L}\end{array}}{\mathrm{\Gamma },\mathrm{\Delta }\Rightarrow C}\mathrm{Cut}.$$ Replace it by $$\frac{\begin{array}{c}{\mathcal{D}}_i:\mathrm{\Gamma }\Rightarrow A_i\\ {\mathcal{E}}_i:\mathrm{\Delta },A_i\Rightarrow C\end{array}}{\mathrm{\Gamma },\mathrm{\Delta }\Rightarrow C}\mathrm{Cut}.$$ The unused branch disappears.

For $A=A_1\to A_2$, write the final rules as $$\frac{\mathrm{\Gamma },A_1\Rightarrow A_2}{\mathrm{\Gamma }\Rightarrow A_1\to A_2}\to \mathrm{R},\frac{\begin{array}{c}\mathrm{\Delta }\Rightarrow A_1\\ \mathrm{\Theta },A_2\Rightarrow C\end{array}}{\mathrm{\Delta },\mathrm{\Theta },A_1\to A_2\Rightarrow C}\to \mathrm{L}.$$ First cut $\mathrm{\Delta }\Rightarrow A_1$ into $\mathrm{\Gamma },A_1\Rightarrow A_2$, obtaining $\mathrm{\Gamma },\mathrm{\Delta }\Rightarrow A_2$. Eliminate this lower-rank cut by the lemma’s assumption before the second is formed. Then cut its cut-free result into $\mathrm{\Theta },A_2\Rightarrow C$, and eliminate that lower-rank cut by the same assumption. The two new cut formulas are $A_1$ and $A_2$.

For $A=\mathrm{\forall }xB$, the derivation producing $A$ ends in $\mathrm{\forall }$R with a fresh $a$, and the derivation using $A$ ends in $\mathrm{\forall }$L at a term $t$. Freshen $a$ away from $\mathrm{\Gamma },\mathrm{\Delta },C,t$, apply individual substitution $t/a$ to the $\mathrm{\forall }$R premise, and cut the resulting proof of $B[t/x]$ against the $\mathrm{\forall }$L premise: $$\frac{\begin{array}{c}\mathcal{D}[t/a]:\mathrm{\Gamma }\Rightarrow B[t/x]\\ \mathcal{E}:\mathrm{\Delta },B[t/x]\Rightarrow C\end{array}}{\mathrm{\Gamma },\mathrm{\Delta }\Rightarrow C}\mathrm{Cut}.$$ Here by lemma 3.3, so the new cut has smaller rank. For $A=\mathrm{\exists }xB$, the producing rule has premise $\mathcal{D}:\mathrm{\Gamma }\Rightarrow B[t/x]$ for a witness $t$, and the using rule opens an eigenvariable $a$. Freshen $a$ away from the producing derivation, substitute $t/a$ through the using premise, and cut $$\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}.$$ Again by lemma 3.3. In every displayed case, eliminate the new lower-rank cuts by the lemma’s assumption. Atomic formulas have no principal introduction pair, and $\mathrm{\perp }$ has no right introduction. ◻