[proofplan] We replace the given derivation by a normal derivation of the same existential sentence. Normality gives the canonical last-rule property: a closed normal derivation of an existential formula must end by existential introduction, not by an elimination rule or by an introduction rule for another connective. The final existential-introduction rule displays a witness term $t$ and a closed derivation of $A(t)$; the closedness of the whole derivation forces this term to be closed. [/proofplan] [step:Normalize the closed derivation without changing its conclusion] Let $\Pi$ be a closed $\mathsf{NJ}_{\mathcal L}$-derivation of $\exists y:S\,A(y)$. We invoke the [Normalization Theorem for First-Order Intuitionistic Natural Deduction](/page/Normalization%20in%20Natural%20Deduction) over the fixed language $\mathcal L$, with equality if equality is part of $\mathsf{NJ}_{\mathcal L}$: normalization sends any derivation to a normal derivation with the same final conclusion, the same undischarged assumptions, and no new free individual variables, free term variables, or eigenparameters. Applying this theorem to $\Pi$, define $\Pi_{\mathrm{nf}}$ to be the resulting normal $\mathsf{NJ}_{\mathcal L}$-derivation. Since $\Pi$ has no undischarged assumptions and contains no free individual variables or eigenparameters, $\Pi_{\mathrm{nf}}$ is a closed normal derivation of $\exists y:S\,A(y)$. [guided] We start from the closed derivation supplied by the hypothesis. Denote it by $\Pi$, so its final formula is \begin{align*} \exists y:S\,A(y). \end{align*} The theorem used here is the [Normalization Theorem for First-Order Intuitionistic Natural Deduction](/page/Normalization%20in%20Natural%20Deduction), in its many-sorted form over the fixed language $\mathcal L$, with equality included if equality is one of the rules of $\mathsf{NJ}_{\mathcal L}$. Its conclusion is not only that the final formula is preserved. It also preserves the undischarged assumptions and does not introduce new free individual variables, free term variables, or eigenparameters. Applying this theorem to $\Pi$, define $\Pi_{\mathrm{nf}}$ to be the resulting normal derivation. Its final formula is still \begin{align*} \exists y:S\,A(y). \end{align*} Because normalization preserves undischarged assumptions, and $\Pi$ has none, $\Pi_{\mathrm{nf}}$ also has no undischarged assumptions. Because normalization introduces no new free individual variables or eigenparameters, and $\Pi$ was closed in that stronger sense, no such variable or eigenparameter occurs in $\Pi_{\mathrm{nf}}$. Thus $\Pi_{\mathrm{nf}}$ is a closed normal derivation of the same existential sentence. [/guided] [/step] [step:Use the canonical last-rule property for normal existential derivations] We invoke the [Canonical Forms Theorem for Normal First-Order Intuitionistic Natural Deduction](/page/Canonical%20Forms%20for%20Normal%20Natural%20Deductions): if a normal closed derivation in many-sorted first-order intuitionistic natural deduction has a closed conclusion whose outermost connective is $\exists$, then its final inference is the existential-introduction rule for that existential formula. This is the precise last-rule result for normal derivations; it covers derivations whose final branch is an elimination chain and also covers bottom elimination and equality elimination according to the rules present in $\mathsf{NJ}_{\mathcal L}$. The hypotheses apply because $\Pi_{\mathrm{nf}}$ is closed, normal, and has closed final formula $\exists y:S\,A(y)$. Therefore the final inference of $\Pi_{\mathrm{nf}}$ is existential introduction. [guided] We now use the [Canonical Forms Theorem for Normal First-Order Intuitionistic Natural Deduction](/page/Canonical%20Forms%20for%20Normal%20Natural%20Deductions) rather than trying to classify the last rule informally. The theorem says: in many-sorted first-order intuitionistic natural deduction, if a derivation is normal and closed, and if its closed final formula has outermost connective $\exists$, then the last inference is the existential-introduction rule for that final existential formula. This is the correct form of the last-rule principle because a final elimination rule need not have its principal formula supplied immediately by an assumption or immediately by an introduction; in a normal derivation it may lie on a longer elimination chain. The canonical-forms theorem analyzes that whole normal structure at once. It also treats special rules such as bottom elimination and equality elimination according to the exact rule set of $\mathsf{NJ}_{\mathcal L}$, so no separate informal exclusion of those rules is needed here. We verify the hypotheses of the canonical-forms theorem. From the previous step, $\Pi_{\mathrm{nf}}$ is normal. It is closed: it has no undischarged assumptions and no free individual variables or eigenparameters. Its final formula is the closed existential formula \begin{align*} \exists y:S\,A(y). \end{align*} The outermost logical symbol of this formula is $\exists$. Hence the canonical-forms theorem applies and yields that the final inference of $\Pi_{\mathrm{nf}}$ is existential introduction. [/guided] [/step] [step:Read the witness term from the final existential introduction] Since the final rule is existential introduction, there is an $\mathcal L$-term $t$ of sort $S$, free for $y$ in $A(y)$, and a subderivation $\Pi_t$ whose final formula is $A(t)$, such that the last inference has the form \begin{align*} \frac{\Pi_t \; \vdash \; A(t)}{\exists y:S\,A(y)} \; \exists\mathrm{I}. \end{align*} Existential introduction discharges no assumptions. Hence every undischarged assumption of $\Pi_t$ would also be an undischarged assumption of $\Pi_{\mathrm{nf}}$, and there are none. Therefore $\Pi_t$ is a closed derivation of $A(t)$, except possibly for free variables occurring in the displayed term $t$. [guided] The existential-introduction rule is the rule that introduces a formula of the form $\exists y:S\,A(y)$ from a particular instance $A(t)$. Therefore, since the last rule of $\Pi_{\mathrm{nf}}$ is existential introduction, the derivation has a final inference of the form \begin{align*} \frac{\Pi_t \; \vdash \; A(t)}{\exists y:S\,A(y)} \; \exists\mathrm{I}, \end{align*} where $t$ is an $\mathcal L$-term of sort $S$ and $t$ is free for substitution for $y$ in $A(y)$. This rule is important because it displays the witness term explicitly. The derivation does not merely assert that some object exists; its final rule was obtained from a concrete instance $A(t)$. We also record the assumption status of the premise derivation $\Pi_t$. Existential introduction does not discharge any formula assumptions. Thus any undischarged assumption appearing in $\Pi_t$ would remain undischarged in the whole derivation $\Pi_{\mathrm{nf}}$. Since $\Pi_{\mathrm{nf}}$ is closed, $\Pi_t$ has no undischarged assumptions. The only remaining issue is whether the displayed witness term $t$ is a closed term. [/guided] [/step] [step:Use closedness to show that the displayed witness is a closed term] The normalized derivation $\Pi_{\mathrm{nf}}$ is closed, so no free individual variable or eigenparameter occurs in it. The term $t$ occurs in the premise formula $A(t)$ of the final inference. Therefore $t$ contains no free individual variable or eigenparameter. Hence $t$ is a closed $\mathcal L$-term of sort $S$. Since $\exists y:S\,A(y)$ is closed, every free variable of $A(y)$ is the displayed variable $y$; substituting the closed term $t$ for $y$ therefore makes $A(t)$ closed. Thus there exists a closed $\mathcal L$-term $t$ of sort $S$ such that $\mathsf{NJ}_{\mathcal L}$ has a closed derivation $\Pi_t$ of the closed formula $A(t)$, as required. [guided] It remains to justify that the witness term extracted from the final rule is closed. By the closedness conclusion obtained from the strengthened normalization theorem, the derivation $\Pi_{\mathrm{nf}}$ contains no free individual variables or eigenparameters. The term $t$ occurs in the displayed premise formula $A(t)$ immediately above the final existential-introduction rule. Therefore every variable or parameter occurring in $t$ would also occur freely in the derivation $\Pi_{\mathrm{nf}}$. But there are no such free variables or eigenparameters in $\Pi_{\mathrm{nf}}$. Hence $t$ has no free variables and no free eigenparameters. Since $t$ is already known from the existential-introduction rule to be an $\mathcal L$-term of sort $S$, it follows that $t$ is a closed $\mathcal L$-term of sort $S$. We also check that the instance $A(t)$ is closed. The theorem assumes that $\exists y:S\,A(y)$ is a closed formula, so the only possible free occurrences in $A(y)$ are occurrences of the displayed variable $y$. Replacing $y$ by the closed term $t$ leaves no free variable in $A(t)$. The premise subderivation $\Pi_t$ has final formula $A(t)$ and no undischarged assumptions. Therefore $\mathsf{NJ}_{\mathcal L}$ proves the closed formula $A(t)$ by a closed derivation. This is exactly the existence property asserted in the theorem. [/guided] [/step]