[proofplan] The forward direction is straightforward: given a proof of $p \Rightarrow q$ from $S$, append the line $p$ (a hypothesis in $S \cup \{p\}$) and apply modus ponens to obtain $q$. The backward direction is the substantive content. Given a proof $t_1, \ldots, t_n = q$ of $q$ from $S \cup \{p\}$, we show by induction on $i$ that $S \vdash (p \Rightarrow t_i)$. The induction splits into three cases according to how $t_i$ is justified: (a) $t_i$ is an axiom or belongs to $S$, handled by Axiom (A1); (b) $t_i = p$, handled by the provable tautology $\vdash p \Rightarrow p$; (c) $t_i$ is obtained by modus ponens from earlier lines, handled by Axiom (A2). Taking $i = n$ gives $S \vdash (p \Rightarrow q)$. [/proofplan] [step:Prove the forward direction by appending $p$ and applying modus ponens] Suppose $S \vdash (p \Rightarrow q)$. Let $t_1, t_2, \ldots, t_k = (p \Rightarrow q)$ be a formal proof of $(p \Rightarrow q)$ from $S$. Extend this to a sequence \begin{align*} t_1, t_2, \ldots, t_k, \, t_{k+1}, \, t_{k+2}, \end{align*} where $t_{k+1} := p$ and $t_{k+2} := q$. We verify each new line is justified as a proof step from $S \cup \{p\}$: - $t_1, \ldots, t_k$ remain valid, since every line that was an axiom or lay in $S$ is still an axiom or lies in $S \cup \{p\}$, and every modus-ponens step remains a modus-ponens step. - $t_{k+1} = p$ is a hypothesis, since $p \in S \cup \{p\}$. - $t_{k+2} = q$ follows by modus ponens from $t_{k+1} = p$ and $t_k = (p \Rightarrow q)$. Hence the extended sequence is a proof of $q$ from $S \cup \{p\}$, i.e., $S \cup \{p\} \vdash q$. [/step] [step:Set up the backward direction by induction on the length of a proof of $q$ from $S \cup \{p\}$] Suppose $S \cup \{p\} \vdash q$. Fix a proof $t_1, t_2, \ldots, t_n = q$ of $q$ from $S \cup \{p\}$. We prove by induction on $i \in \{1, 2, \ldots, n\}$ that \begin{align*} S &\vdash (p \Rightarrow t_i). \end{align*} Taking $i = n$ then yields $S \vdash (p \Rightarrow q)$, as required. Each line $t_i$ is justified in exactly one of the following ways in the proof from $S \cup \{p\}$: 1. $t_i$ is an axiom of propositional calculus (i.e., an instance of (A1), (A2), or (A3)); 2. $t_i \in S$; 3. $t_i = p$ (the distinguished extra hypothesis); 4. $t_i$ is obtained by modus ponens from two earlier lines $t_j$ and $t_k$ with $j, k < i$ and $t_k = (t_j \Rightarrow t_i)$. We handle each case separately in the next steps. We use Axiom schemes \begin{align*} \text{(A1)} &\quad a \Rightarrow (b \Rightarrow a), \\ \text{(A2)} &\quad [a \Rightarrow (b \Rightarrow c)] \Rightarrow [(a \Rightarrow b) \Rightarrow (a \Rightarrow c)], \end{align*} each valid for any substitution of formulas. [/step] [step:Handle cases (1) and (2) — $t_i$ is an axiom or lies in $S$ — using Axiom (A1)] Suppose $t_i$ is an axiom or $t_i \in S$. We construct a proof of $(p \Rightarrow t_i)$ from $S$ in three lines: \begin{align*} &\text{line } 1: \quad t_i && (\text{axiom or hypothesis in } S), \\ &\text{line } 2: \quad t_i \Rightarrow (p \Rightarrow t_i) && (\text{instance of (A1) with } a := t_i, \, b := p), \\ &\text{line } 3: \quad p \Rightarrow t_i && (\text{modus ponens on lines 1 and 2}). \end{align*} This is a valid proof from $S$, so $S \vdash (p \Rightarrow t_i)$. [/step] [step:Handle case (3) — $t_i = p$ — using the provable tautology $\vdash p \Rightarrow p$] Suppose $t_i = p$. Then $(p \Rightarrow t_i) = (p \Rightarrow p)$. The formula $p \Rightarrow p$ is provable in propositional calculus from no assumptions — this is the standard "theorem of reflexivity" derived from (A1) and (A2). Explicitly, one standard proof (taking $a = p$, $b = (p \Rightarrow p)$, $c = p$ in (A2), and substituting $p \Rightarrow p$ for $b$ and $p$ for $a$ appropriately) is: \begin{align*} &\text{line } 1: \quad [p \Rightarrow ((p \Rightarrow p) \Rightarrow p)] \Rightarrow [(p \Rightarrow (p \Rightarrow p)) \Rightarrow (p \Rightarrow p)] && (\text{(A2)}), \\ &\text{line } 2: \quad p \Rightarrow ((p \Rightarrow p) \Rightarrow p) && (\text{(A1) with } a := p, \, b := (p \Rightarrow p)), \\ &\text{line } 3: \quad (p \Rightarrow (p \Rightarrow p)) \Rightarrow (p \Rightarrow p) && (\text{MP on lines 1 and 2}), \\ &\text{line } 4: \quad p \Rightarrow (p \Rightarrow p) && (\text{(A1) with } a := p, \, b := p), \\ &\text{line } 5: \quad p \Rightarrow p && (\text{MP on lines 3 and 4}). \end{align*} Since $\vdash p \Rightarrow p$, any proof of $p \Rightarrow p$ is also a proof from $S$ (add no hypotheses). Therefore $S \vdash (p \Rightarrow t_i)$. [/step] [step:Handle case (4) — $t_i$ is obtained by modus ponens — using Axiom (A2) and the induction hypothesis] Suppose $t_i$ is obtained by modus ponens from earlier lines $t_j$ and $t_k$ with $j, k < i$ and $t_k = (t_j \Rightarrow t_i)$. By the induction hypothesis applied to $j$ and $k$, \begin{align*} S &\vdash (p \Rightarrow t_j), \\ S &\vdash (p \Rightarrow (t_j \Rightarrow t_i)). \end{align*} Let $\pi_1, \pi_2$ be proofs from $S$ witnessing these two deductions, respectively. Concatenate them and extend as follows: \begin{align*} &\pi_1 && (\text{proof from } S \text{ ending in } p \Rightarrow t_j), \\ &\pi_2 && (\text{proof from } S \text{ ending in } p \Rightarrow (t_j \Rightarrow t_i)), \\ &\text{line } \alpha: \quad [p \Rightarrow (t_j \Rightarrow t_i)] \Rightarrow [(p \Rightarrow t_j) \Rightarrow (p \Rightarrow t_i)] && (\text{(A2) with } a := p, \, b := t_j, \, c := t_i), \\ &\text{line } \beta: \quad (p \Rightarrow t_j) \Rightarrow (p \Rightarrow t_i) && (\text{MP on line } \alpha \text{ and last line of } \pi_2), \\ &\text{line } \gamma: \quad p \Rightarrow t_i && (\text{MP on line } \beta \text{ and last line of } \pi_1). \end{align*} This is a valid proof from $S$, so $S \vdash (p \Rightarrow t_i)$. [guided] By the induction hypothesis, we know \begin{align*} S \vdash (p \Rightarrow t_j) \quad \text{and} \quad S \vdash (p \Rightarrow (t_j \Rightarrow t_i)). \end{align*} We want to combine these to deduce $S \vdash (p \Rightarrow t_i)$. The obstacle is that modus ponens acts on $t_j$ and $t_j \Rightarrow t_i$, not on their "$(p \Rightarrow \cdot)$-shifted" versions. We need a way to **distribute** the hypothesis $p \Rightarrow (\cdot)$ over modus ponens. This is precisely what Axiom (A2) says: \begin{align*} [p \Rightarrow (t_j \Rightarrow t_i)] \Rightarrow [(p \Rightarrow t_j) \Rightarrow (p \Rightarrow t_i)]. \end{align*} Applying MP to (A2) and $p \Rightarrow (t_j \Rightarrow t_i)$ strips off the outer implication to give $(p \Rightarrow t_j) \Rightarrow (p \Rightarrow t_i)$. Applying MP again with $p \Rightarrow t_j$ yields $p \Rightarrow t_i$. Why (A2)? Because (A2) is precisely the **distribution axiom** for $\Rightarrow$: it lets us push an implication-hypothesis through another implication. Without (A2), there is no way to transfer the hypothesis $p$ through the modus ponens step. This is the deep reason the Deduction Theorem requires (A2): the axioms (A1) and (A2) together are *exactly* what is needed to simulate hypothesis management. Concretely, we build a proof from $S$ of length $|\pi_1| + |\pi_2| + 3$: - First write out $\pi_1$ (a proof from $S$ ending in the line $p \Rightarrow t_j$). - Then write out $\pi_2$ (a proof from $S$ ending in the line $p \Rightarrow (t_j \Rightarrow t_i)$). - Add line $\alpha$: the instance of (A2) with $a := p$, $b := t_j$, $c := t_i$, namely \begin{align*} [p \Rightarrow (t_j \Rightarrow t_i)] \Rightarrow [(p \Rightarrow t_j) \Rightarrow (p \Rightarrow t_i)]. \end{align*} - Add line $\beta$: by MP on line $\alpha$ and the last line of $\pi_2$, we get $(p \Rightarrow t_j) \Rightarrow (p \Rightarrow t_i)$. - Add line $\gamma$: by MP on line $\beta$ and the last line of $\pi_1$, we get $p \Rightarrow t_i$. Each added line is either an axiom or follows by MP from two earlier lines, so this is a valid formal proof from $S$. The conclusion is $p \Rightarrow t_i$, so $S \vdash (p \Rightarrow t_i)$. [/guided] [/step] [step:Conclude by taking $i = n$] We have shown $S \vdash (p \Rightarrow t_i)$ for all $i \in \{1, \ldots, n\}$. Taking $i = n$ and using $t_n = q$, \begin{align*} S &\vdash (p \Rightarrow q). \end{align*} Combined with the forward direction proved in the first step, this establishes the biconditional $S \vdash (p \Rightarrow q) \iff S \cup \{p\} \vdash q$. [/step]