[proofplan] We argue by contradiction. If there were a closed derivation of $\bot$, weak normalization would transform it into a closed normal derivation of $\bot$. We then use the structural form of normal natural-deduction derivations: a normal derivation of an atomic formula or $\bot$ cannot end with an introduction rule, and if it ends with an elimination rule then its principal branch begins at an undischarged assumption. Since the derivation is closed and $\bot$ has no introduction rule, both possibilities are impossible. [/proofplan] [step:Normalize a hypothetical closed derivation of $\bot$] Assume, for contradiction, that there exists a derivation $\Pi$ in propositional intuitionistic natural deduction whose conclusion is $\bot$ and whose set of undischarged assumptions is empty. We invoke the external metatheorem **Weak Normalization for Propositional Intuitionistic Natural Deduction** in the following precise form: for the same propositional intuitionistic natural-deduction system used in the statement, every derivation $\Delta$ has a normal derivation $\Delta^{\mathrm{nf}}$ with exactly the same conclusion formula and exactly the same set of undischarged assumptions as $\Delta$. The derivation $\Pi$ satisfies the hypothesis of this metatheorem because $\Pi$ is a derivation in that system. Therefore there exists a normal derivation $\Pi^{\mathrm{nf}}$ whose conclusion is $\bot$ and whose set of undischarged assumptions is empty. Hence $\Pi^{\mathrm{nf}}$ is a closed normal derivation of $\bot$. Here a derivation is **normal** when it contains no maximal formula, meaning no formula occurrence that is first obtained as the conclusion of an introduction rule and is then used as the major premise of an elimination rule. The **major premise** of an elimination rule is the premise whose outermost connective is eliminated: the conjunction premise for $\wedge$-elimination, the disjunction premise for $\vee$-elimination, the implication premise for $\to$-elimination, and the premise $\bot$ for $\bot$-elimination if that rule is included in the chosen presentation. A **principal branch** is obtained by starting from the major premise of an elimination rule and repeatedly moving upward to the major premise of the elimination rule that produced the current formula, as long as the current formula is itself the conclusion of an elimination rule. The resulting sequence of elimination inferences is the corresponding **elimination chain**. [guided] Suppose that $\bot$ is derivable without assumptions. This means that there is a natural-deduction derivation $\Pi$ with conclusion $\bot$ and no undischarged assumptions. We now use weak normalization in a form that states exactly what the proof needs. The external metatheorem **Weak Normalization for Propositional Intuitionistic Natural Deduction** says: for the same propositional intuitionistic natural-deduction system used in the statement, every derivation $\Delta$ can be transformed into a normal derivation $\Delta^{\mathrm{nf}}$ with the same conclusion formula and the same set of undischarged assumptions. The hypothesis is not merely that some normalization theorem exists; it must apply to this exact rule system, and its conclusion must preserve both the final formula and the open assumptions. The derivation $\Pi$ is a derivation in this exact system, so the theorem applies to $\Pi$. We obtain a normal derivation $\Pi^{\mathrm{nf}}$ whose conclusion is still $\bot$ and whose set of undischarged assumptions is still empty. Thus the contradiction will follow once we prove that no closed normal derivation can have conclusion $\bot$. We also fix the structural vocabulary used below. A derivation is **normal** when it contains no maximal formula, meaning no formula occurrence that is first produced by an introduction rule and then used as the major premise of an elimination rule. The **major premise** of an elimination rule is the premise carrying the connective being eliminated: the conjunction in $\wedge$-elimination, the disjunction in $\vee$-elimination, the implication in $\to$-elimination, and the premise $\bot$ in $\bot$-elimination if the presentation includes ex falso as an elimination rule. A **principal branch** is the branch obtained by starting at the major premise of an elimination rule and repeatedly tracing upward through major premises of earlier elimination rules. The elimination rules encountered in this trace form the associated **elimination chain**. [/guided] [/step] [step:Classify the possible final rule of a normal derivation of $\bot$] The final inference rule of $\Pi^{\mathrm{nf}}$ cannot be an introduction rule. The introduction rules of propositional intuitionistic natural deduction introduce formulas whose outermost connective is $\wedge$, $\vee$, or $\to$. There is no introduction rule whose conclusion is the falsity constant $\bot$. Therefore the final rule of $\Pi^{\mathrm{nf}}$, if there is one, must be an elimination rule. The only remaining possibility is that $\Pi^{\mathrm{nf}}$ consists of a single assumption occurrence with conclusion $\bot$. [guided] We inspect the last line of the normal derivation $\Pi^{\mathrm{nf}}$. First, the last rule cannot be an introduction rule. In propositional intuitionistic natural deduction, introduction rules are tied to connectives: $\wedge$-introduction concludes a conjunction, $\vee$-introduction concludes a disjunction, and $\to$-introduction concludes an implication. The falsity constant $\bot$ is atomic in the sense that it has no outermost connective, and the system has no rule that introduces $\bot$ directly. Thus a normal derivation ending in $\bot$ has only two formal possibilities: either the last line is obtained by an elimination rule, or the whole derivation is just an assumption occurrence of $\bot$. Since $\Pi^{\mathrm{nf}}$ is closed, the single-assumption case is already impossible, but we keep it visible because it is one of the structural cases for a derivation ending in an atomic formula. [/guided] [/step] [step:Prove that a normal elimination ending in $\bot$ forces an open assumption] Suppose that the final rule of $\Pi^{\mathrm{nf}}$ is an elimination rule. Let $B$ be the principal branch obtained by starting from the major premise of this final elimination rule and tracing upward through major premises of elimination rules until no further such upward move is possible. [claim:Initial occurrence on the principal branch] The first formula occurrence on $B$ is an assumption occurrence. [/claim] [proof] By construction, the first formula occurrence on $B$ is not the conclusion of an elimination rule; otherwise the branch construction would continue upward through the major premise of that elimination rule. If it were the conclusion of an introduction rule, then that occurrence would immediately be used downward as the major premise of the next elimination rule on $B$. This would be a maximal formula, contradicting normality of $\Pi^{\mathrm{nf}}$. The remaining possible kind of initial formula occurrence in natural deduction is an assumption occurrence. Therefore the first formula occurrence on $B$ is an assumption occurrence. [/proof] Let $A$ denote this initial assumption occurrence on $B$. We prove that $A$ is undischarged. Along $B$, every downward inference is an elimination rule in which the current formula is the major premise. The conjunction elimination rules and implication elimination rule discharge no assumptions. The falsity elimination rule, if included in the presentation, also discharges no assumptions. For [disjunction elimination](/theorems/4625), the only discharged assumptions are the temporary assumptions at the tops of its two minor subderivations; the major premise occurrence is outside those minor subderivations and is not discharged by that rule. Hence no elimination rule on $B$ discharges $A$. Since the final inference of $\Pi^{\mathrm{nf}}$ is itself an elimination rule and its conclusion is the final conclusion of the whole derivation, there is no lower rule outside the elimination chain that could discharge $A$. Therefore $A$ is an undischarged assumption of $\Pi^{\mathrm{nf}}$. This contradicts the fact that $\Pi^{\mathrm{nf}}$ is closed. [guided] Assume that the final inference in $\Pi^{\mathrm{nf}}$ is an elimination rule. We form the principal branch $B$ by starting at the major premise of the final elimination rule and then repeatedly moving upward through major premises of earlier elimination rules. This construction stops because the derivation is finite. The first point to prove is that the top of this branch is an assumption. By definition of where the construction stops, the first formula occurrence on $B$ is not itself the conclusion of an elimination rule; if it were, we would move one step farther upward through the major premise of that elimination. Could it be the conclusion of an introduction rule? No. The next downward use of that occurrence on $B$ is as the major premise of an elimination rule. Thus an introduction would be followed by an elimination of the formula just introduced, which is exactly a maximal formula. Since $\Pi^{\mathrm{nf}}$ is normal, no maximal formula occurs. The only remaining source for the first formula occurrence is therefore an assumption occurrence. Let $A$ denote that assumption occurrence. It remains to check, rule by rule, that $A$ is not discharged while the branch descends to the final conclusion $\bot$. In $\wedge$-elimination, the major premise is a conjunction and the rule discharges no assumptions. In $\to$-elimination, the major premise is an implication and the rule discharges no assumptions. If $\bot$-elimination is included in the presentation, its major premise is $\bot$ and it discharges no assumptions. The only elimination rule with discharge is $\vee$-elimination, so this is the case that needs care. In $\vee$-elimination, the disjunction is the major premise, while the discharged assumptions occur at the tops of the two minor subderivations. A formula occurrence lying on the principal branch through the major premise is not one of those minor-subderivation assumptions, so that $\vee$-elimination does not discharge $A$. Thus no elimination rule on the principal branch discharges $A$. There is also no rule below the final elimination rule, because its conclusion is the final conclusion of the whole derivation $\Pi^{\mathrm{nf}}$. Consequently no later inference can discharge $A$. Therefore $A$ is an undischarged assumption of $\Pi^{\mathrm{nf}}$. This contradicts closedness: $\Pi^{\mathrm{nf}}$ was obtained by weak normalization from a closed derivation and has empty set of undischarged assumptions. Hence the final rule of $\Pi^{\mathrm{nf}}$ cannot be an elimination rule. [/guided] [/step] [step:Exclude the assumption case and conclude consistency] The remaining possibility is that $\Pi^{\mathrm{nf}}$ is a one-line derivation whose only line is the assumption $\bot$. That derivation has $\bot$ as an undischarged assumption, so it is not closed. This again contradicts the fact that $\Pi^{\mathrm{nf}}$ is closed. All possible forms of a closed normal derivation of $\bot$ have been excluded. Therefore no closed derivation of $\bot$ exists in propositional intuitionistic natural deduction. [/step]