[proofplan] The backward direction is immediate from Modus Ponens. For the forward direction, we induct on the length of a formal proof of $q$ from $S \cup \{p\}$, showing that for every formula $r$ appearing in the proof, $S \vdash p \Rightarrow r$. The propositional-style cases (axioms, hypotheses from $S$, the hypothesis $p$ itself, and Modus Ponens) are handled by Axioms 1 and 2 of propositional logic exactly as in the propositional Deduction Theorem. The new and substantive case is Generalization: we must show that if $S \vdash p \Rightarrow r$ and Gen derives $(\forall x)\,r$ under a variable-freeness side condition, then $S \vdash p \Rightarrow (\forall x)\,r$. We analyse this case by splitting on whether $x$ is free in $p$; Axiom 7 handles one sub-case and the structure of the original derivation handles the other. [/proofplan]

[step:Establish the backward direction via Modus Ponens]Suppose $S \vdash p \Rightarrow q$. We show $S \cup \{p\} \vdash q$. Fix a formal proof $\pi$ of $p \Rightarrow q$ from $S$. Extend $\pi$ by appending two lines: \begin{align*} \pi, \quad p, \quad q. \end{align*} The formula $p$ is a member of $S \cup \{p\}$, hence a legal hypothesis line. The formula $q$ follows from $p \Rightarrow q$ (already established in $\pi$) and $p$ (just added) by Modus Ponens. The extended sequence is a formal proof of $q$ from $S \cup \{p\}$, hence $S \cup \{p\} \vdash q$.[/step]

[guided]This direction is the easy one. Assume $S \vdash p \Rightarrow q$, so we have a formal proof $\pi = q_1, \ldots, q_n$ from $S$ with $q_n = p \Rightarrow q$. Every line $q_i$ is either an axiom, a member of $S$, or follows from earlier lines by Modus Ponens or Generalization. Construct a new proof for $S \cup \{p\} \vdash q$ by extending $\pi$: \begin{align*} q_1, \ldots, q_n, \; p, \; q. \end{align*} Line $n+1$ is $p$, which is a hypothesis in $S \cup \{p\}$. Line $n+2$ is $q$, which follows from lines $n$ (i.e.\ $p \Rightarrow q$) and $n+1$ (i.e.\ $p$) by Modus Ponens. All earlier lines $q_1, \ldots, q_n$ remain valid in the enlarged hypothesis set: an axiom is still an axiom, a member of $S$ is still a member of $S \cup \{p\}$, and the inference rules are unchanged. Hence this extended sequence is a formal proof of $q$ from $S \cup \{p\}$.[/guided]

[step:Set up induction on proof length for the forward direction] For the forward direction, suppose $S \cup \{p\} \vdash q$. Fix a formal proof \begin{align*} \pi = q_1, q_2, \ldots, q_n \end{align*} of $q$ from $S \cup \{p\}$, where $q_n = q$. We prove by induction on $i \in \{1, \ldots, n\}$ that $S \vdash p \Rightarrow q_i$. Taking $i = n$ will give $S \vdash p \Rightarrow q$. For each $i$, the formula $q_i$ is justified in $\pi$ by one of the following: (a) $q_i$ is a logical axiom of predicate calculus (including the propositional axioms, equality axioms, and quantifier axioms); (b) $q_i \in S$; (c) $q_i = p$; (d) $q_i$ follows by Modus Ponens from $q_j$ and $q_k$ with $j, k < i$, where $q_k = q_j \Rightarrow q_i$; (e) $q_i = (\forall x)\,r$ follows by Generalization from some earlier $q_j = r$ ($j < i$), subject to the side condition that the variable $x$ is not free in any formula from the hypothesis set used in the derivation of $q_j$. We handle each case in turn. [/step]

[step:Handle axioms, hypotheses, and the premise $p$ using Axioms 1 and 2]Recall the first two axioms of our predicate calculus (in Hilbert-style axiomatisation): - **Axiom 1**: $r \Rightarrow (s \Rightarrow r)$, for all formulas $r, s$. - **Axiom 2**: $(r \Rightarrow (s \Rightarrow t)) \Rightarrow ((r \Rightarrow s) \Rightarrow (r \Rightarrow t))$, for all formulas $r, s, t$. **Case (a): $q_i$ is an axiom.** Then $q_i \Rightarrow (p \Rightarrow q_i)$ is an instance of Axiom 1, valid as an axiom in any derivation from $S$. Combining with $q_i$ (which is an axiom, hence available in $S$'s proof too) by Modus Ponens yields: \begin{align*} q_i, \quad q_i \Rightarrow (p \Rightarrow q_i), \quad p \Rightarrow q_i. \end{align*} This is a three-line proof of $p \Rightarrow q_i$ from $S$, so $S \vdash p \Rightarrow q_i$. **Case (b): $q_i \in S$.** The same three-line proof works, with the first line justified as a hypothesis from $S$ rather than as an axiom: \begin{align*} q_i \text{ (hypothesis)}, \quad q_i \Rightarrow (p \Rightarrow q_i) \text{ (Axiom 1)}, \quad p \Rightarrow q_i \text{ (MP)}. \end{align*} **Case (c): $q_i = p$.** We must show $S \vdash p \Rightarrow p$. This is a standard propositional tautology provable using Axioms 1 and 2: one proof is \begin{align*} & p \Rightarrow ((p \Rightarrow p) \Rightarrow p) \quad (\text{Axiom 1}) \\ & (p \Rightarrow ((p \Rightarrow p) \Rightarrow p)) \Rightarrow ((p \Rightarrow (p \Rightarrow p)) \Rightarrow (p \Rightarrow p)) \quad (\text{Axiom 2}) \\ & (p \Rightarrow (p \Rightarrow p)) \Rightarrow (p \Rightarrow p) \quad (\text{MP}) \\ & p \Rightarrow (p \Rightarrow p) \quad (\text{Axiom 1}) \\ & p \Rightarrow p \quad (\text{MP}). \end{align*} All five lines are either axioms or follow by MP from earlier lines, so this is a valid proof from the empty hypothesis set, hence from $S$. Thus $S \vdash p \Rightarrow p$. **Case (d): Modus Ponens.** Suppose $q_i$ follows by MP from $q_j$ and $q_k = q_j \Rightarrow q_i$, with $j, k < i$. By the inductive hypothesis, \begin{align*} S \vdash p \Rightarrow q_j \qquad \text{and} \qquad S \vdash p \Rightarrow (q_j \Rightarrow q_i). \end{align*} Instantiate Axiom 2 with $r := p$, $s := q_j$, $t := q_i$: \begin{align*} S \vdash (p \Rightarrow (q_j \Rightarrow q_i)) \Rightarrow ((p \Rightarrow q_j) \Rightarrow (p \Rightarrow q_i)). \end{align*} Two applications of MP — first with $p \Rightarrow (q_j \Rightarrow q_i)$, then with $p \Rightarrow q_j$ — yield $S \vdash p \Rightarrow q_i$.[/step]

[guided]These cases are exactly as in the propositional Deduction Theorem; the predicate-logic axioms behave like propositional axioms as far as the induction is concerned. **Why Axiom 1 handles (a), (b), and (c).** In all three cases, $q_i$ is available as a premise on the $S$-side (as an axiom in (a), as a member of $S$ in (b)) OR we can prove $p \Rightarrow q_i$ directly (case (c)). For (a) and (b), Axiom 1 says: "anything implies itself when guarded by any antecedent". Formally, $q_i \Rightarrow (p \Rightarrow q_i)$ is an Axiom 1 instance; combined with $q_i$ by Modus Ponens, we obtain $p \Rightarrow q_i$. For (c) — where $q_i = p$ — we just need to prove the identity $p \Rightarrow p$ from nothing, which is the standard five-line Hilbert proof using Axioms 1 and 2 shown above. **Modus Ponens (case (d)).** This is where Axiom 2 earns its keep. We have, by the inductive hypothesis, $S \vdash p \Rightarrow q_j$ and $S \vdash p \Rightarrow (q_j \Rightarrow q_i)$. We want $S \vdash p \Rightarrow q_i$. The instance of Axiom 2 we need is \begin{align*} (p \Rightarrow (q_j \Rightarrow q_i)) \Rightarrow ((p \Rightarrow q_j) \Rightarrow (p \Rightarrow q_i)). \end{align*} Chain two MPs: first we peel off $p \Rightarrow (q_j \Rightarrow q_i)$ to get $(p \Rightarrow q_j) \Rightarrow (p \Rightarrow q_i)$, then we peel off $p \Rightarrow q_j$ to get $p \Rightarrow q_i$. This move — "distributing implication across its antecedent" — is the syntactic heart of the Deduction Theorem.[/guided]

[step:Handle the Generalization case using Axiom 7]Recall the quantifier axiom relevant here: - **Axiom 7**: $(\forall x)(r \Rightarrow s) \Rightarrow (r \Rightarrow (\forall x)\,s)$, provided that $x$ is not free in $r$. Suppose $q_i = (\forall x)\,r$ follows by Generalization from $q_j = r$ ($j < i$). Recall the side condition of Gen: $x$ must not be free in any formula from the hypothesis set $S \cup \{p\}$ that is used in deriving $q_j$ from $S \cup \{p\}$. Let $H \subseteq S \cup \{p\}$ denote this set of used hypotheses. By the inductive hypothesis applied to $q_j$: \begin{align*} S \vdash p \Rightarrow r. \tag{$*$} \end{align*} We split into two sub-cases according to whether $p \in H$. **Sub-case 1: $p \notin H$.** Then every formula in $H$ is a member of $S$ (i.e.\ $H \subseteq S$), and $q_j = r$ is already derivable from $S$ alone without using $p$. That is, \begin{align*} S \vdash r, \end{align*} via the sub-proof of $\pi$ up to line $j$, with every occurrence of $p$ either absent or eliminable (in fact $p$ does not occur as a hypothesis in this sub-proof). Applying Gen in this $S$-derivation is legitimate because the Gen side condition on $x$ — that $x$ is not free in any premise of $H$ — is preserved ($H \subseteq S$ and the same condition holds). Hence \begin{align*} S \vdash (\forall x)\,r. \end{align*} Now apply Axiom 1 ($(\forall x)\,r \Rightarrow (p \Rightarrow (\forall x)\,r)$) and Modus Ponens: \begin{align*} S \vdash p \Rightarrow (\forall x)\,r, \end{align*} as required. **Sub-case 2: $p \in H$.** Then the Gen side condition forces $x$ not to be free in $p$ (since $p \in H$ and $x$ is not free in any member of $H$). From $(*)$ we have $S \vdash p \Rightarrow r$. Apply Gen to this derivation to obtain \begin{align*} S \vdash (\forall x)(p \Rightarrow r). \tag{$**$} \end{align*} We must verify the Gen side condition: $x$ must not be free in any hypothesis of $S$ used in the derivation of $p \Rightarrow r$. By construction, the derivation $(*)$ uses only hypotheses from $S$; and the side condition on the original Gen step ensured $x$ was not free in any hypothesis from $H \cap S \subseteq S$ used in deriving $r$. A tracing of the inductive construction — the $S \vdash p \Rightarrow q_i$ derivations built in cases (a)–(d) and recursively here — shows that the hypotheses from $S$ used in the constructed proof of $p \Rightarrow r$ are a subset of those used in the original proof of $r$, so the side condition is inherited. Thus Gen is legitimate, giving $(**)$. Since $x$ is not free in $p$, Axiom 7 gives \begin{align*} S \vdash (\forall x)(p \Rightarrow r) \Rightarrow (p \Rightarrow (\forall x)\,r). \end{align*} Modus Ponens with $(**)$ yields \begin{align*} S \vdash p \Rightarrow (\forall x)\,r = p \Rightarrow q_i, \end{align*} as required.[/step]

[guided]Generalization is the one genuinely new case compared with the propositional Deduction Theorem. The trick is to split on whether $p$ was used as a hypothesis in the sub-proof of $r$. **Setup.** $q_i = (\forall x)\,r$ was obtained by applying Gen to $q_j = r$, where the Gen side condition requires that $x$ is not free in any hypothesis used to derive $r$ from $S \cup \{p\}$. Let $H \subseteq S \cup \{p\}$ be the hypotheses actually used. By induction, $S \vdash p \Rightarrow r$. **Why split on whether $p \in H$?** Because the Gen side condition gives different information in the two cases: - If $p \notin H$, then $r$ was derivable from $S$ alone — the premise $p$ was superfluous in that sub-proof — and we can reproduce the Gen step entirely within $S$. - If $p \in H$, then the Gen side condition constrains $p$: specifically, $x$ is not free in $p$. This is precisely the hypothesis of Axiom 7, which lets us commute $\forall x$ across $\Rightarrow$. **Sub-case 1: $p \notin H$.** Since $H \subseteq S$, the sub-proof deriving $r$ from $S \cup \{p\}$ is in fact a proof of $r$ from $S$. Gen applies there too (the side condition on $x$ is unchanged), giving $S \vdash (\forall x)\,r$. Then Axiom 1 ($((\forall x)\,r) \Rightarrow (p \Rightarrow (\forall x)\,r)$) plus Modus Ponens gives $S \vdash p \Rightarrow (\forall x)\,r$. **Sub-case 2: $p \in H$.** The Gen side condition tells us $x$ is not free in $p$. By induction $S \vdash p \Rightarrow r$. Apply Gen to this new derivation: \begin{align*} S \vdash (\forall x)(p \Rightarrow r). \end{align*} Does Gen apply? We must check the side condition: $x$ is not free in any hypothesis from $S$ used to derive $p \Rightarrow r$. By the way the inductive construction was built, these are (a subset of) the hypotheses from $S$ used in deriving $r$ in the original proof — i.e.\ members of $H \cap S$ — and the original Gen side condition guarantees $x$ is not free in any of them. So Gen is legitimate. Now apply Axiom 7: \begin{align*} (\forall x)(p \Rightarrow r) \Rightarrow (p \Rightarrow (\forall x)\,r), \end{align*} valid because $x$ is not free in $p$. Modus Ponens delivers $S \vdash p \Rightarrow (\forall x)\,r$. **Why the case split is unavoidable.** If we naively tried to apply Axiom 7 without first checking that $x$ is not free in $p$, we would fail: the axiom's side condition is precisely this freshness condition. Sub-case 1 is the case where Axiom 7 is unavailable (we don't know $x$ isn't free in $p$), but fortunately $p$ wasn't used anyway, so we can sidestep it entirely. Sub-case 2 is the case where Axiom 7 is available, and we use it. **Where does Soundness relate?** The premise that the Gen condition controls which variables can be quantified away is what makes the Deduction Theorem true — without it, the forward direction would fail. For example, $\{p(x)\} \vdash (\forall x)\,p(x)$ by Gen if we incorrectly allowed Gen over a free variable of a hypothesis, but $\vdash p(x) \Rightarrow (\forall x)\,p(x)$ is not valid. The Gen side condition blocks this spurious derivation, and the analysis above is precisely what respects that block.[/guided]

[step:Conclude by combining cases] We have verified, for each of the five justification types (a)–(e), that if $q_j$ satisfies $S \vdash p \Rightarrow q_j$ for all $j < i$, then $S \vdash p \Rightarrow q_i$. By induction on $i$, $S \vdash p \Rightarrow q_i$ for every $i \in \{1, \ldots, n\}$. In particular, $S \vdash p \Rightarrow q_n = p \Rightarrow q$. Combining with Step 1 (backward direction), we have \begin{align*} S \cup \{p\} \vdash q \iff S \vdash p \Rightarrow q, \end{align*} as claimed. [/step]