Reverse of Deduction Theorem

Question

Why is it "easy to see" that if $S \vdash (A\to B)$ then $S \cup\{A\} \vdash B$?

Answer 1

It is not so easy to see!

The only axiom we have is the original single axiom DDpDqrDDtDttDDsqDDpsDps, and our only rule of inference other than uniform substitution is

{D$\alpha$D$\beta$$\gamma$, $\alpha$} $\vdash$ $\gamma$.

This "if S⊢(A→B), then S∪{A}⊢B" involves $\rightarrow$. I'll rewrite that as: "if S$\vdash$Cab, then S ∪ {a} $\vdash$b." Thus, using the definition

Cpq := DpDqq, we want to show that:

"if S$\vdash$DaDbb, then S ∪ {a} $\vdash$b."

Suppose that we've proved DaDbb. This means that in the rule above we can substitute $\alpha$ with "a", $\beta$ with "b", and $\gamma$ with "b" yielding:

{DaDbb, a} $\vdash$ b. Now from that since we have $\vdash$DaDbb, and "a" consists of a hypothesis, $\vdash$b.

Answer 2

The statement $S\vdash (A\to B)$ means that there is a formal proof using the assumptions in $S$ (as well as standard axioms, and rules of inference including modus ponens) which ends with the line $A\to B$.

Take this proof and append two more lines:

$A$ (assumption)
$B$ (modus ponens from the previous two lines).

You now have a formal proof using the assumptions in $S$, together with another assumption $A$, and ending with the formula $B$. The existence of such a proof is exactly what is asserted by the statement $S\cup\{A\}\vdash B$.

Answer 3

Let $\langle\varphi_1,\varphi_2,\ldots,\varphi_n\rangle$ be a proof of $(A\to B)$ from $S$: $\varphi_n$ is $(A\to B)$, and each $\varphi_k$ with $k<n$ either is in $S$, is an axiom, or follows from earlier statements in the list by one of your inference rules. Then $\langle\varphi_1,\ldots,\varphi_n=(A\to B),A,B\rangle$ is a proof of $B$ from $S\cup\{A\}$: the presence of $A$ in the list is justified by the fact that $A\in S\cup\{A\}$, and $B$ follows from $(A\to B)$ and $A$ by modus ponens, which is surely one of your rules of inference.