[proofplan] We prove a stronger local invariant: for every inference in a cut-free derivation, every formula in each premise belongs to the quantifier-instance subformula closure of the formulas in the conclusion, except for formulas already carried unchanged from the surrounding context. Structural rules preserve the invariant because they only permute, delete, duplicate, or add context formulas in the downward direction. Logical rules preserve it because their premises replace the principal formula in the conclusion by its immediate constituent formulas, with quantifier rules replacing a quantified formula by an allowed instance of its matrix. Iterating this local invariant upward from the end-sequent proves the global subformula property for the whole derivation. [/proofplan] [step:Define the closure relative to the end-sequent] Let $S_0$ denote the end-sequent of $\mathcal{D}$. Write $F(S_0)$ for the set of formula occurrences in $S_0$. Define $\operatorname{Sub}_{q}(S_0)$ to be the least class of formulas satisfying the following four conditions: 1. If $A \in F(S_0)$, then $A \in \operatorname{Sub}_{q}(S_0)$. 2. If $A \circ B \in \operatorname{Sub}_{q}(S_0)$, where $\circ \in \{\wedge,\vee,\to\}$, then $A,B \in \operatorname{Sub}_{q}(S_0)$. 3. If $\neg A \in \operatorname{Sub}_{q}(S_0)$, then $A \in \operatorname{Sub}_{q}(S_0)$. 4. If $Qx\,A \in \operatorname{Sub}_{q}(S_0)$, where $Q \in \{\forall,\exists\}$, and $t$ is a term permitted by the corresponding quantifier rule at the inference under consideration, then $A[t/x] \in \operatorname{Sub}_{q}(S_0)$. In the eigenvariable cases, $t$ is the eigenvariable required by the rule, and the usual condition is imposed: that eigenvariable is fresh for the appropriate conclusion sequent. Thus $\operatorname{Sub}_{q}(S_0)$ records ordinary subformulas together with exactly the quantifier instances generated by the first-order rules of $LK$ or $LJ$. [/step] [step:Establish the local invariant for structural rules] Consider a structural inference in the derivation. Exchange changes only the order of formula occurrences in the antecedent or succedent. Contraction replaces two occurrences of the same formula by one occurrence in the conclusion, so every formula in the premise already occurs in the conclusion. Weakening adds a formula to the conclusion; hence, when the inference is read upward from conclusion to premise, the premise contains only formulas already present in the conclusion. Therefore every structural rule has the following property: every formula occurrence in its premise is either unchanged from a formula occurrence in its conclusion or is a duplicate of such a formula. Consequently, if every formula in the conclusion belongs to $\operatorname{Sub}_{q}(S_0)$, then every formula in the premise also belongs to $\operatorname{Sub}_{q}(S_0)$. [/step] [step:Check propositional logical rules by principal formula decomposition] Consider a propositional logical inference of $LK$ or $LJ$. In each such rule, all side formulas in the premises are copied unchanged from the conclusion, and the only new formulas appearing in the premises are immediate subformulas of the principal formula in the conclusion. For example, in the left conjunction rule, the conclusion contains a principal formula $A \wedge B$, and the premise contains $A$ and $B$ in its place. Since $A \wedge B \in \operatorname{Sub}_{q}(S_0)$ implies $A,B \in \operatorname{Sub}_{q}(S_0)$ by the definition of the closure, the premise formulas remain in $\operatorname{Sub}_{q}(S_0)$. The right conjunction rule has premises containing $A$ and $B$ separately, both immediate subformulas of the conclusion formula $A \wedge B$. The same verification applies to disjunction, implication, and negation. In every case, the premise formulas introduced by the rule are immediate subformulas of the conclusion's principal formula, while all context formulas are inherited unchanged. Hence the local invariant holds for every propositional logical rule of both $LK$ and $LJ$. [/step] [step:Check quantifier rules using the permitted instances] Consider a quantifier inference. The side formulas in the premises are copied unchanged from the conclusion, so only the principal formula must be checked. For the universal-left rule, the conclusion contains $\forall x\,A$, and the premise contains $A[t/x]$ for a term $t$ allowed by the rule. Since $\forall x\,A \in \operatorname{Sub}_{q}(S_0)$ and the closure is closed under such permitted instances, $A[t/x] \in \operatorname{Sub}_{q}(S_0)$. For the existential-right rule, the same argument applies to the premise formula $A[t/x]$ arising from the conclusion formula $\exists x\,A$. For the universal-right rule, the conclusion contains $\forall x\,A$, and the premise contains $A[y/x]$, where $y$ is an eigenvariable fresh for the appropriate conclusion sequent. By the eigenvariable clause in the definition of $\operatorname{Sub}_{q}(S_0)$, this formula belongs to $\operatorname{Sub}_{q}(S_0)$. The existential-left rule is identical in form: the conclusion contains $\exists x\,A$, and the premise contains $A[y/x]$ for a fresh eigenvariable $y$. Thus every quantifier rule replaces a quantified principal formula by an allowed instance of its matrix, and the local invariant holds for all first-order quantifier rules. [/step] [step:Propagate the invariant through the cut-free derivation] We now prove by induction on the distance of a sequent from the end-sequent $S_0$, measured upward in the derivation tree, that every formula in that sequent belongs to $\operatorname{Sub}_{q}(S_0)$. The base case is the end-sequent $S_0$ itself. Every formula in $S_0$ belongs to $\operatorname{Sub}_{q}(S_0)$ by definition. For the induction step, suppose the conclusion of an inference satisfies the assertion. If the inference is structural, the result follows from the structural-rule verification above. If the inference is propositional logical, the result follows from principal formula decomposition. If the inference is a quantifier rule, the result follows from the closure under the corresponding permitted term or eigenvariable instance. Since the derivation is cut-free, there is no cut rule to consider; no inference can introduce an arbitrary formula unrelated to its conclusion. Therefore every premise of every inference above $S_0$ satisfies the assertion whenever its conclusion does. By induction, every sequent occurring in $\mathcal{D}$ contains only formulas from $\operatorname{Sub}_{q}(S_0)$. [/step] [step:Conclude the subformula property for LK and LJ] The argument used only the shared structural, propositional, and quantifier behavior of $LK$ and $LJ$. The intuitionistic restriction in $LJ$ that the succedent contain at most one formula does not affect any step of the proof, because the verification is formula-by-formula and rule-by-rule. Hence, in either $LK$ or $LJ$, every formula occurrence in a cut-free derivation belongs to the quantifier-instance subformula closure of the end-sequent. This is exactly the asserted subformula property, with the standard allowance for term instances and eigenvariable substitutions in the quantifier rules. [/step]