[proofplan] We turn the closed proof of the universal-existential statement into a proof with a concrete input by universal elimination. We then normalize that proof effectively; the assumed canonical existential form property for this system exposes an explicit witness term from the closed normal existential proof. The representation soundness hypothesis transfers the internal proof of $\rho(a,t_a)$ to the intended relation $R(\llbracket a \rrbracket_{\mathcal{M}},\llbracket t_a \rrbracket_{\mathcal{M}})$ in the standard term model $\mathcal{M}$. Since each operation used is mechanical, reading off the witness gives an effective algorithm on closed input terms. The theorem is therefore proved at the level of the fixed closed-term representation of $D$, without claiming that the extracted witness is independent of the chosen name for an element of $D$. [/proofplan] [step:Instantiate the universal proof at a closed input term] Let $\mathcal{L}$ denote the computable term language of $S$, and let $\mathcal{M}$ denote the standard term model. Let $\rho(u,v)$ denote the formula of $S$ that represents the relation $R$ in the sense stated in the theorem. Let \begin{align*} \pi \end{align*} be the given closed $S$-proof of $\forall x\,\exists y\,\rho(x,y)$. Let $a$ be a closed input term of $\mathcal{L}$, and let $x := \llbracket a \rrbracket_{\mathcal{M}} \in D$ be its denotation in $\mathcal{M}$. By universal elimination in the natural deduction system $S$, applying $\pi$ to the closed term $a$ gives an effectively constructed closed $S$-proof \begin{align*} \pi(a) \end{align*} of the formula \begin{align*} \exists y\,\rho(a,y). \end{align*} [guided] The symbols used here are the ones fixed in the theorem statement: $\mathcal{L}$ is the computable term language of $S$, $\mathcal{M}$ is the standard term model, and $\rho(u,v)$ is the formula of $S$ representing the relation $R$. Fix a concrete input. Since inputs are represented by closed input terms, choose a closed input term $a$ of $\mathcal{L}$ and write $x := \llbracket a \rrbracket_{\mathcal{M}}$ for the element of $D$ denoted by $a$ in $\mathcal{M}$. The proof $\pi$ proves the universally quantified formula \begin{align*} \forall x\,\exists y\,\rho(x,y). \end{align*} The elimination rule for the universal quantifier allows us to substitute any closed term for the universally quantified variable. Substituting the closed input term $a$ gives a closed proof, denoted $\pi(a)$, of \begin{align*} \exists y\,\rho(a,y). \end{align*} This construction is effective because proof substitution by a closed term is a syntactic operation on a finite proof object. [/guided] [/step] [step:Normalize the instantiated existential proof] Apply the effective conclusion-preserving normalization procedure of $S$ to the closed proof $\pi(a)$. This produces a closed normal $S$-proof \begin{align*} \nu(a) \end{align*} of the same formula \begin{align*} \exists y\,\rho(a,y). \end{align*} Because $\nu(a)$ is a closed normal $S$-proof of an existential formula, the canonical existential form property assumed in the theorem applies to $\nu(a)$. Its hypotheses are satisfied: the proof is closed, normal, belongs to the same system $S$, and has existential conclusion $\exists y\,\rho(a,y)$. Therefore $\nu(a)$ ends with existential introduction. Hence there is a closed term $t_a$ and a closed $S$-proof \begin{align*} \sigma(a) \end{align*} of \begin{align*} \rho(a,t_a), \end{align*} and $\nu(a)$ is obtained from $\sigma(a)$ by introducing the existential quantifier. [guided] The instantiated proof $\pi(a)$ proves an existential statement, but it may not visibly display a witness. Normalization is the step that removes detours in the proof and puts it into canonical form. By hypothesis, $S$ has an effective conclusion-preserving normalization procedure for closed proofs. Applying this procedure to $\pi(a)$ gives a closed normal proof $\nu(a)$ of the same conclusion: \begin{align*} \exists y\,\rho(a,y). \end{align*} The same conclusion is preserved because normalization is assumed to be a proof transformation inside $S$. Now we use the canonical existential form property assumed for the system $S$. The property applies because $\nu(a)$ is a closed normal proof in $S$ and its conclusion is the existential formula $\exists y\,\rho(a,y)$. It says that such a proof must end by existential introduction. Therefore the final inference of $\nu(a)$ has the form: from a proof of $\rho(a,t_a)$, infer $\exists y\,\rho(a,y)$, for some closed term $t_a$. Thus $\nu(a)$ explicitly contains both a closed witness term $t_a$ and a closed subproof $\sigma(a)$ of \begin{align*} \rho(a,t_a). \end{align*} This is the point where constructivity is used: the proof of existence does not merely certify that some witness exists; after normalization, it exposes the witness term syntactically. [/guided] [/step] [step:Read the witness term as the value of the extracted computation] Define the extraction procedure \begin{align*} E: \{\text{closed input terms of }\mathcal{L}\} &\to \{\text{closed terms of }\mathcal{L}\} \end{align*} as follows: for a closed input term $a$, construct $\pi(a)$ by universal elimination, normalize it to $\nu(a)$, inspect the final existential introduction in $\nu(a)$, and output its witness term $t_a$. Thus \begin{align*} E(a) := t_a. \end{align*} Each operation in the definition of $E$ is effective: universal elimination is a finite syntactic transformation, normalization is effective by hypothesis, and reading the witness term from the final existential introduction is a finite inspection of the normal proof tree. Therefore $E$ is an algorithm on closed input terms. [guided] We now define the actual extracted computation. The input to the computation is not an abstract element of $D$ by itself, but a closed input term naming that element. This is the representation of $D$ fixed in the statement. Define \begin{align*} E: \{\text{closed input terms of }\mathcal{L}\} &\to \{\text{closed terms of }\mathcal{L}\} \end{align*} by the following finite procedure. Given a closed input term $a$, first form the proof $\pi(a)$ of $\exists y\,\rho(a,y)$ by universal elimination. Next normalize $\pi(a)$ to obtain the closed normal proof $\nu(a)$. Finally inspect the last inference of $\nu(a)$. Since $\nu(a)$ is a normal proof of an existential formula, its last inference is existential introduction, and that inference displays a closed witness term $t_a$. Set \begin{align*} E(a) := t_a. \end{align*} This is an algorithm because every step is mechanical. Universal elimination rewrites a finite proof object. Normalization is effective by assumption. Inspecting the last inference and copying the witness term are finite syntactic operations. Hence the proof $\pi$ determines an effective procedure that computes a witness term from an input term. [/guided] [/step] [step:Use soundness to verify the extracted witness in the standard model] Let $a$ be a closed input term with denotation $x := \llbracket a \rrbracket \in D$, and let $t_a := E(a)$. Since $\sigma(a)$ is a closed $S$-proof of $\rho(a,t_a)$, the representation soundness hypothesis for $R$ implies \begin{align*} R(\llbracket a \rrbracket_{\mathcal{M}},\llbracket t_a \rrbracket_{\mathcal{M}}). \end{align*} Since $\llbracket a \rrbracket_{\mathcal{M}} = x$, this gives \begin{align*} R(x,\llbracket t_a \rrbracket_{\mathcal{M}}). \end{align*} The truth of the relation follows from the represented proof and the representation soundness assumption. [guided] The extracted term $t_a$ must now be connected to the intended relation on the domain $D$. The normal proof gave us a closed proof $\sigma(a)$ of the internal formula \begin{align*} \rho(a,t_a). \end{align*} The representation soundness hypothesis for $R$ says precisely that whenever $S$ proves $\rho(a,b)$ for closed terms $a,b$ of $\mathcal{L}$, the intended relation holds of their denotations in $\mathcal{M}$: \begin{align*} S \vdash \rho(a,b) \quad \Longrightarrow \quad R(\llbracket a \rrbracket_{\mathcal{M}},\llbracket b \rrbracket_{\mathcal{M}}). \end{align*} Applying this implication with $b := t_a$ yields \begin{align*} R(\llbracket a \rrbracket_{\mathcal{M}},\llbracket t_a \rrbracket_{\mathcal{M}}). \end{align*} Since $x$ was defined by $x := \llbracket a \rrbracket_{\mathcal{M}}$, this is exactly \begin{align*} R(x,\llbracket t_a \rrbracket_{\mathcal{M}}). \end{align*} Correctness comes from the representation hypothesis: the proof of $\rho(a,t_a)$ certifies the intended semantic relation for the denotations of the two closed terms. [/guided] [/step] [step:State the represented-input algorithm and its correctness] Define the extracted algorithm on closed input terms by \begin{align*} F: \{\text{closed input terms of }\mathcal{L}\} &\to \{\text{closed terms of }\mathcal{L}\}, \\ a &\mapsto E(a). \end{align*} The previous construction proves that $F$ is effective, because $E$ is computed by universal elimination, conclusion-preserving normalization, and finite inspection of the final existential introduction. For every closed input term $a$, setting $t_a := F(a)$ gives \begin{align*} R(\llbracket a \rrbracket_{\mathcal{M}},\llbracket F(a) \rrbracket_{\mathcal{M}}). \end{align*} Thus the extracted algorithm computes a witness from each closed input term naming an element of $D$. This is exactly the represented-input conclusion asserted by the updated theorem statement; no extensional well-definedness claim is made for two distinct closed input terms with the same denotation. [/step]