[proofplan] We analyze formula occurrences by following branches of the derivation tree, proving the branch decomposition needed for normal propositional intuitionistic natural deduction directly from the definitions. The only delicate rules are $\vee E$ and $\bot E$: their conclusions need not be subformulas of their major premises, so we track those conclusions through the upward continuation of the derivation rather than through the eliminated formula. Normality rules out every detour in which a formula introduced, produced by $\bot E$, or passed through a $\vee E$ segment is later used as the major premise of an elimination. Once this branch structure is fixed, eliminations trace formulas back to assumptions and introductions trace formulas forward to the final conclusion or to a formula already controlled by such a trace. [/proofplan] [step:Define branches, targets, maximal formulas, and maximal segments] A formula occurrence means a node of the derivation tree labelled by a formula. If $X$ is a formula occurrence, write $\ell(X)$ for the formula labelling $X$. We use the standard rule schemata for propositional intuitionistic natural deduction: $\wedge I$, $\wedge E$, $\vee I$, $\vee E$, $\to I$, $\to E$, and $\bot E$. In an elimination rule, the major premise is the compound formula occurrence being eliminated, namely $C \wedge D$, $C \vee D$, $C \to D$, or $\bot$; in $\to E$ the minor premise is the occurrence labelled by the antecedent $C$. A temporary assumption is an assumption occurrence inside a subderivation; it is discharged when a surrounding $\to I$ or $\vee E$ rule binds that assumption and removes it from the open assumptions of the resulting derivation. A branch of $\Pi$ is a finite sequence of formula occurrences \begin{align*} B_0, B_1, \dots, B_m \end{align*} constructed by the following explicit successor relation. The initial occurrence $B_0$ is either an open assumption occurrence or a temporary assumption occurrence discharged by $\to I$ or $\vee E$. Given $B_i$, the next occurrence $B_{i+1}$, if it exists, is determined by exactly one of these cases: First, if $B_i$ is the major premise of an elimination rule, then $B_{i+1}$ is the conclusion of that elimination rule. For $\wedge E$, $\vee E$, $\to E$, and $\bot E$, the major premise is respectively the occurrence labelled by $C \wedge D$, $C \vee D$, $C \to D$, and $\bot$ in that rule instance. Second, if $B_i$ is one of the two premises of a $\wedge I$ rule whose conclusion is labelled by $C \wedge D$, then $B_{i+1}$ is that conclusion occurrence. Thus $\ell(B_i)$ is either $C$ or $D$. Third, if $B_i$ is the premise of a $\vee I$ rule whose conclusion is labelled by $C \vee D$, then $B_{i+1}$ is that conclusion occurrence. Thus $\ell(B_i)$ is either $C$ or $D$. Fourth, if $B_i$ is the conclusion of the subderivation discharged by a $\to I$ rule whose conclusion is labelled by $C \to D$, then $B_{i+1}$ is that conclusion occurrence. Thus $\ell(B_i)=D$, while the temporary assumption discharged by this rule is labelled by $C$. Fifth, if $B_i$ is the common conclusion occurrence of one of the two side derivations in a $\vee E$ rule and the conclusion occurrence of that $\vee E$ rule has the same label, then $B_{i+1}$ is the conclusion occurrence of that $\vee E$ rule. This is called an unchanged $\vee E$ passage. It is neither an elimination transition nor an introduction transition; it is a bookkeeping passage through the rule conclusion preserving the formula label. The construction stops when none of these successor clauses applies, or when the occurrence is used only as a minor premise of an elimination rule. This terminal occurrence $B_m$ is called the target of the branch. Thus the phrase "introduction segment" means a consecutive part of a branch whose non-$\vee E$ transitions are among the three introduction successor clauses above, and "elimination segment" means a consecutive part whose non-$\vee E$ transitions are major-premise-to-conclusion elimination transitions. A transition $B_i \leadsto B_{i+1}$ is an elimination transition if it is obtained by the first successor clause. It is an introduction transition if it is obtained by the second, third, or fourth successor clause. It is an unchanged $\vee E$ passage if it is obtained by the fifth successor clause. These alternatives exhaust all possible branch transitions by definition. A maximal formula is a formula occurrence that is both the conclusion of an introduction rule and the major premise of an elimination rule. A maximal segment is a non-empty sequence of occurrences of the same formula whose first occurrence is the conclusion of an introduction rule or of $\bot E$ or $\vee E$, whose intermediate occurrences are obtained only by unchanged $\vee E$ passages, and whose final occurrence is the major premise of an elimination rule. The derivation $\Pi$ is normal precisely in the sense that it contains no maximal formula and no maximal segment. Every formula occurrence of $\Pi$ lies on at least one branch. To see this, start at the occurrence and move downward in the derivation tree by reversing the successor relation whenever possible: from an introduction conclusion choose the premise on the displayed branch, from an elimination conclusion choose its major premise when applicable, from the conclusion of an unchanged $\vee E$ passage choose the corresponding side-branch conclusion, and stop at an open or temporary assumption. Reversing this finite downward path gives a branch containing the original occurrence. We say that an occurrence $F$ is controlled by an occurrence $G$ if $\ell(F)$ is a subformula of $\ell(G)$. The upward continuation of an occurrence is its successor in the explicit branch relation above, when such a successor exists. This terminology is only bookkeeping for the subformula relation and for the finite upward order of the derivation tree. [/step] [step:Prove that each normal branch has all eliminations before all introductions] [claim:Branch lemma for normal derivations] For every branch \begin{align*} B_0, B_1, \dots, B_m \end{align*} of the normal derivation $\Pi$, there is an index $r$ with $0 \leq r \leq m$ such that the transitions before $B_r$ are elimination transitions or unchanged $\vee E$ passages belonging to elimination segments, and the transitions after $B_r$ are introduction transitions or unchanged $\vee E$ passages belonging to introduction segments. In particular, no occurrence that has been produced by an introduction rule, by $\bot E$, or as the conclusion of a $\vee E$ rule is later used as the major premise of an elimination rule along the same branch. [/claim] [proof] Suppose that the asserted decomposition fails for a branch $B_0,\dots,B_m$. Classify each transition as an elimination transition, an introduction transition, or an unchanged $\vee E$ passage. Ignore unchanged $\vee E$ passages temporarily, since they preserve the formula label and are assigned to whichever adjacent segment contains them. If the non-$\vee E$ transitions are not all eliminations followed by all introductions, then there are indices $a<b$ such that $B_a \leadsto B_{a+1}$ is an introduction transition and $B_b \leadsto B_{b+1}$ is an elimination transition, with no non-$\vee E$ transition of elimination type between an earlier introduction and $B_b$ chosen closer to the beginning. The occurrence $B_{a+1}$ is produced by an introduction rule, and a later occurrence $B_b$ is used as the major premise of an elimination rule. There are two further ways the asserted decomposition can fail without a preceding introduction transition: an occurrence produced by $\bot E$ is later used as the major premise of an elimination rule, or a conclusion occurrence of a $\vee E$ rule, possibly after unchanged $\vee E$ passages, is later used as the major premise of an elimination rule. Thus in every failure case there is an occurrence produced by an introduction rule, by $\bot E$, or as the conclusion of $\vee E$, after which a later occurrence on the same branch is used as the major premise of an elimination rule. Among all such pairs choose one for which the final major-premise occurrence is as early as possible along the branch, and among those choose the starting occurrence as late as possible. Write the chosen subsequence as \begin{align*} B_s, B_{s+1}, \dots, B_t, \end{align*} where $B_s$ is produced by an introduction rule, by $\bot E$, or as the conclusion of $\vee E$, and $B_t$ is the first later occurrence in this chosen pair used as the major premise of an elimination rule. By the explicit definition of branches, each intermediate transition $B_i \leadsto B_{i+1}$ with $s \leq i < t$ is exactly one of three kinds: an elimination transition, an introduction transition, or an unchanged $\vee E$ passage. No such intermediate transition can be an elimination transition, because then its premise $B_i$ would be a major premise of an elimination rule earlier than $B_t$, contradicting the choice of $B_t$ as the earliest final major-premise occurrence in the chosen pair. No such intermediate transition can be an introduction transition. Indeed, the conclusion $B_{i+1}$ of that introduction transition is itself produced by an introduction rule and is still followed by the later major-premise occurrence $B_t$; since $i+1>s$, this contradicts the choice of $B_s$ as late as possible among pairs ending at $B_t$. Therefore every intermediate transition from $B_s$ to $B_t$ is an unchanged $\vee E$ passage. By definition of unchanged $\vee E$ passage, these transitions preserve the formula label, so all occurrences $B_s, \dots, B_t$ have the same formula label. If $s=t$, then one occurrence is both produced by an introduction rule, by $\bot E$, or by $\vee E$, and used as the major premise of an elimination rule. This is a maximal formula in the introduction case and a maximal segment of length one in the $\bot E$ or $\vee E$ case. If $s<t$, then the sequence $B_s, \dots, B_t$ is a maximal segment by definition: it starts with an occurrence produced by an introduction rule, $\bot E$, or $\vee E$, it passes only through unchanged $\vee E$ passages, and it ends at a major premise of an elimination rule. Both alternatives contradict normality of $\Pi$. This proves the branch lemma. [/proof] The branch lemma gives the required branch shape. The index $r$ separates the elimination part from the introduction part: before $B_r$ the branch may decompose formulas or pass an unchanged formula through $\vee E$, while after $B_r$ the branch may build formulas by introductions or pass an unchanged formula through $\vee E$. Thus every normal branch has the form \begin{align*} \text{elimination part first, then introduction part}. \end{align*} [guided] Let \begin{align*} B_0, B_1, \dots, B_m \end{align*} be a branch. We want to prove that eliminations cannot occur after introductions on a normal branch. First separate the genuine rule-changing transitions from unchanged $\vee E$ passages. An unchanged $\vee E$ passage preserves the formula label, so it belongs to the elimination segment if it occurs before the first introduction-type transition and to the introduction segment if it occurs after that point. If the desired branch decomposition fails, then after ignoring unchanged $\vee E$ passages there is a first place where an introduction-side transition has already occurred and a later elimination transition appears. The conclusion of that earlier introduction transition is an occurrence produced by an introduction rule, and the premise of the later elimination transition is a later occurrence used as the major premise of an elimination rule. The same obstruction can also start with an occurrence produced by $\bot E$ or with the conclusion of a $\vee E$ rule, because such an occurrence is not an elimination premise inherited from the lower branch; if it later becomes a major premise, it is exactly the kind of detour normality forbids. Thus every failure gives a formula created by an introduction rule, by $\bot E$, or by the conclusion of $\vee E$, perhaps carried unchanged through one or more $\vee E$ passages, and then later used as the major premise of an elimination rule. Maximal formulas and maximal segments are exactly the formal devices that record such detours. Assume such a detour occurs. Among all detours choose one whose final major-premise occurrence is as early as possible along the branch; among detours ending at that same occurrence, choose the created starting occurrence as late as possible. Denote the resulting subsequence by \begin{align*} B_s, B_{s+1}, \dots, B_t, \end{align*} where $B_s$ is produced by an introduction rule, by $\bot E$, or as the conclusion of $\vee E$, and $B_t$ is the later occurrence used as the major premise of an elimination rule. Now we classify the transitions between $B_s$ and $B_t$. This is not an extra theorem: it follows from the explicit definition of branch successor. Every branch transition is exactly one of the following: a major-premise-to-conclusion elimination transition, a premise-to-conclusion introduction transition for $\wedge I$, $\vee I$, or $\to I$, or an unchanged $\vee E$ passage from a side-branch conclusion to the rule conclusion with the same formula label. There cannot be an elimination transition before $B_t$. If $B_i \leadsto B_{i+1}$ with $s \leq i<t$ were an elimination transition, then $B_i$ would be a major premise of an elimination rule occurring earlier along the branch than $B_t$, contradicting the choice of $B_t$ as the earliest final major premise in the detour. There also cannot be an introduction transition before $B_t$. If $B_i \leadsto B_{i+1}$ were such a transition, then $B_{i+1}$ would itself be produced by an introduction rule and would still be followed by the later major-premise occurrence $B_t$. Since $i+1>s$, this contradicts the choice of $B_s$ as the latest possible starting occurrence among detours ending at $B_t$. The only remaining possibility is that every intermediate transition is an unchanged $\vee E$ passage. Each such passage preserves the formula label by definition, so \begin{align*} \ell(B_s)=\ell(B_{s+1})=\cdots=\ell(B_t). \end{align*} If $s=t$, then a single occurrence is both created and used as the major premise of an elimination. In the introduction case this is a maximal formula; in the $\bot E$ or $\vee E$ case this is a maximal segment of length one. If $s<t$, then the sequence $B_s,\dots,B_t$ is a maximal segment: it starts with an occurrence produced by an introduction rule, $\bot E$, or $\vee E$, passes only through unchanged $\vee E$ passages, and ends as the major premise of an elimination rule. Normality excludes both maximal formulas and maximal segments. Hence the assumed detour cannot exist, and every branch has all elimination transitions before all introduction transitions, with unchanged $\vee E$ passages belonging to the corresponding segment in which they occur. [/guided] [/step] [step:Control every elimination by either its major premise or the branch target] Let $C$, $D$, $E$, $M$, and $T$ denote formula occurrences on a branch of $\Pi$, with $M$ the major premise of an elimination rule, $C$ the conclusion occurrence of that elimination rule, and $T$ the target of the branch containing $C$. For $\wedge E$, there are formula variables $D$ and $E$ such that the major premise $M$ is labelled by $D \wedge E$, and the conclusion $C$ is labelled by either $D$ or $E$. Hence $C$ is controlled by $M$. For $\to E$, there are formula variables $D$ and $E$ such that the major premise $M$ is labelled by $D \to E$, the minor premise is labelled by $D$, and the conclusion $C$ is labelled by $E$. Hence $C$ is controlled by $M$. The minor premise occurrence labelled by $D$ is controlled by the same major premise $M$, because $D$ is a subformula of $D \to E$. For $\vee E$, there are formula variables $D$ and $E$ such that the major premise $M$ is labelled by $D \vee E$. The discharged assumptions at the starts of the two side branches are labelled by $D$ and $E$, so both are controlled by $M$. Let $C$ denote the common conclusion formula of the two side derivations. The two side-branch conclusion occurrences and the conclusion occurrence of the $\vee E$ rule are all labelled by this same formula $C$; the movement from a side-branch conclusion to the rule conclusion is precisely an unchanged $\vee E$ passage. Since the branch lemma forbids an occurrence produced by $\vee E$ or carried through an unchanged $\vee E$ passage from later becoming the major premise of an elimination rule, these occurrences of $C$ lie in the introduction part of their branches and are controlled by their branch targets. For $\bot E$, the major premise is labelled by $\bot$, and the conclusion occurrence $C$ may be labelled by an arbitrary formula. The branch lemma applies directly to this occurrence because it is produced by $\bot E$: it cannot later become the major premise of an elimination rule, even after unchanged $\vee E$ passages. Therefore $C$ lies in the introduction part of its branch and is controlled by the branch target $T$. Therefore an elimination transition has the following exact effect: $\wedge E$ and $\to E$ produce conclusions controlled by their major premises; the minor premise of $\to E$ is also controlled by its major premise; $\vee E$ creates discharged assumptions controlled by its major premise and common-conclusion occurrences controlled by the relevant branch targets; and $\bot E$ produces a conclusion controlled by the relevant branch target. [/step] [step:Show that introductions make earlier formulas subformulas of the branch target] Consider the introduction part of a branch \begin{align*} B_r, B_{r+1}, \dots, B_m. \end{align*} By the branch definition and the branch lemma, every transition $B_i \leadsto B_{i+1}$ with $r \leq i<m$ is either an introduction transition or an unchanged $\vee E$ passage. We verify the subformula relation for each possible transition. For $\wedge I$, the rule conclusion has label $D \wedge E$ and the branch premise has label either $D$ or $E$; hence $\ell(B_i)$ is a subformula of $\ell(B_{i+1})$. This covers either side premise of $\wedge I$, because the branch successor relation explicitly allows either premise to continue to the conjunction conclusion. For $\vee I$, the rule conclusion has label $D \vee E$ and the branch premise has label either $D$ or $E$; hence $\ell(B_i)$ is a subformula of $\ell(B_{i+1})$. For $\to I$, the branch transition is from the conclusion of the discharged subderivation to the implication conclusion. Thus $\ell(B_i)=E$ and $\ell(B_{i+1})=D \to E$ for formula labels $D$ and $E$, so $\ell(B_i)$ is a subformula of $\ell(B_{i+1})$. The discharged temporary assumption labelled by $D$ is not reached by this transition; it is controlled separately as an initial occurrence in the next step. For an unchanged $\vee E$ passage, the side-branch conclusion and the rule conclusion have the same formula label, so $\ell(B_i)=\ell(B_{i+1})$ and hence $\ell(B_i)$ is a subformula of $\ell(B_{i+1})$. The subformula relation is transitive: if $F$ is a subformula of $G$ and $G$ is a subformula of $H$, then $F$ is a subformula of $H$. Applying this transitivity successively along the explicitly classified introduction part shows that every occurrence $B_i$ with $r \leq i \leq m$ is a subformula of the target $B_m$. If $B_m$ is the final conclusion of $\Pi$, then every formula in this introduction part is a subformula of $A$. If $B_m$ is a minor premise of an elimination rule or a side-branch conclusion of $\vee E$, then the next step traces this target through the finite dependency relation of the proof until either the final conclusion or an open assumption is reached. [/step] [step:Trace every initial formula and every target to the conclusion or an open assumption] Let $B$ be any formula occurrence in $\Pi$, and choose a branch \begin{align*} B_0, B_1, \dots, B_m \end{align*} containing $B$. If $B$ lies in the introduction part, then the preceding step shows that $B$ is a subformula of the target $B_m$. If $B$ lies in the elimination part, then the elimination-control step shows that $B$ is either a subformula of the initial formula $B_0$ or is controlled by the target $B_m$ in the exceptional $\vee E$ or $\bot E$ cases. We now prove a stronger statement: every formula occurrence in $\Pi$ is controlled by $A$ or by an open assumption in $\Gamma$. This stronger induction avoids applying the induction hypothesis only to initial or target occurrences. Define a dependency relation $Y \prec X$ between formula occurrences as follows: $Y \prec X$ if $Y$ is the upward continuation of $X$ in the branch successor relation; or if $X$ is a temporary assumption discharged by a $\vee E$ rule and $Y$ is the major premise occurrence of that same $\vee E$ rule; or if $X$ is a minor premise of a $\to E$ rule and $Y$ is the major premise occurrence of that same $\to E$ rule. We justify that the [transitive closure](/theorems/1493) of $\prec$ is well-founded by giving an explicit decreasing measure. For an occurrence $X$, let $h(X)$ be the number of rule-conclusion edges on the unique path in the derivation tree from $X$ to the final conclusion occurrence of $\Pi$. For same-rule dependency edges, use the auxiliary value $q(X)=1$ when $X$ is a temporary assumption of a $\vee E$ side derivation or a minor premise of a $\to E$ rule, and $q(X)=0$ otherwise. Order pairs lexicographically in $\mathbb{N} \times \{0,1\}$ by decreasing first coordinate and then decreasing second coordinate. If $Y$ is the upward continuation of $X$, then $Y$ is a rule conclusion strictly closer to the final conclusion, so $h(Y)<h(X)$. If $X$ is a discharged $\vee E$ temporary assumption and $Y$ is the major premise of that same $\vee E$, then both occurrences feed the same $\vee E$ rule but $Y$ is outside the side derivation; any later dependency path from $Y$ moves upward from the $\vee E$ rule and cannot re-enter the side derivation containing $X$. If $X$ is a minor premise of $\to E$ and $Y$ is the major premise of the same $\to E$, then both premises feed the same rule conclusion, $h(Y)=h(X)$, and $q(Y)=0<1=q(X)$. Thus every dependency chain either strictly decreases $h$, or uses one same-rule edge at fixed $h$ and then must next move to the common rule conclusion with smaller $h$. No directed cycle is possible, and since $\Pi$ has finitely many occurrences, the transitive closure of $\prec$ is well-founded. We argue by induction over this finite well-founded dependency order. Let $X$ be a formula occurrence. Choose a branch \begin{align*} B_0, B_1, \dots, B_m \end{align*} containing $X$. If $X$ lies in the introduction part of this branch, then the preceding step shows that $\ell(X)$ is a subformula of $\ell(B_m)$. Suppose instead that $X$ lies in the elimination part. Let \begin{align*} B_0, B_1, \dots, B_r \end{align*} be the elimination part of the chosen branch, allowing unchanged $\vee E$ passages. We prove by induction on $i$ that each $B_i$ with $0\leq i\leq r$ is either controlled by $B_0$ or, after the first exceptional $\vee E$ or $\bot E$ conclusion on the branch, controlled by the target $B_m$. For $i=0$ this is immediate. If $B_i\leadsto B_{i+1}$ is an unchanged $\vee E$ passage, then $\ell(B_i)=\ell(B_{i+1})$, so the same control passes to $B_{i+1}$. If the transition is a $\wedge E$ or $\to E$ elimination transition, the elimination-control step says that the conclusion is a subformula of the major premise $B_i$; by transitivity it inherits the control already known for $B_i$. If the transition is a $\vee E$ or $\bot E$ transition, the elimination-control step says that the resulting common conclusion or arbitrary conclusion is controlled by the branch target $B_m$, and every later occurrence before $B_r$ is reached from it only by unchanged $\vee E$ passages because the branch lemma forbids a later major-premise elimination from such an occurrence. Hence $\ell(X)$ is either a subformula of $\ell(B_0)$ or a subformula of $\ell(B_m)$ in the exceptional cases. Thus it remains only to control the initial occurrence $B_0$ and the target occurrence $B_m$. For the initial occurrence $B_0$, there are three cases. If $B_0$ is an open assumption, then $\ell(B_0)$ belongs to $\Gamma$. If $B_0$ is discharged by a $\to I$ rule introducing a formula $D \to E$, then $\ell(B_0)=D$, which is a subformula of $D \to E$; the introduced implication occurrence is the upward continuation of the subderivation conclusion and is higher in the dependency order than $B_0$, so the induction hypothesis controls it by $A$ or by an open assumption. If $B_0$ is discharged by a $\vee E$ rule whose major premise is labelled by $D \vee E$, then $\ell(B_0)$ is either $D$ or $E$, hence is a subformula of the major premise; that major premise is higher than $B_0$ by the same-rule dependency edge in the definition of $\prec$, so the induction hypothesis controls the major premise. For the target occurrence $B_m$, again consider cases. If $B_m$ is the final conclusion, then $\ell(B_m)=A$. If $B_m$ is the minor premise of a $\to E$ rule with major premise labelled by $D \to E$, then $\ell(B_m)=D$, a subformula of the major premise; that major premise is higher than $B_m$ by the same-rule dependency edge, so the induction hypothesis controls it. If $B_m$ is a side-branch conclusion of $\vee E$, then the conclusion occurrence of that $\vee E$ rule has the same formula label as $B_m$ and is the upward continuation of $B_m$, so the induction hypothesis controls it. These are the only target types by the definition of branch target. In each case, the occurrence under consideration is either itself labelled by $A$ or by a formula in $\Gamma$, or is a subformula of an occurrence already controlled by $A$ or by a formula in $\Gamma$. Transitivity of the subformula relation therefore gives the same control for the original occurrence. Combining this induction with the branch analysis above, every possible formula occurrence $B$ in $\Pi$ is a subformula of $A$ or of some $G \in \Gamma$. [/step] [step:Conclude the subformula property] Since $B$ was an arbitrary formula occurrence in the normal derivation $\Pi$, the preceding argument applies to every formula occurring in $\Pi$. Therefore every formula occurring in $\Pi$ is a subformula of the conclusion $A$ or a subformula of some open assumption $G \in \Gamma$. This proves the subformula property for normal natural deduction derivations. [/step]