# Deduction Theorem and Closed Formulas

Why in the Deduction Theorem do we require a closed formula?

Deduction Theorem. Let $A$ be a closed formula in $T$. For every formula $B$ of $T$, $\vdash_T A \implies B$ iff $B$ is a theorem of $T[A]$.

I could not find any counterexample.

Can you explain me where is the problem?

Edit:

I found a counterexample.

if $A=C$ and $B=\forall(x)C$

when A is not a closed formula.

• There are many (essentially equivalent)ways to define a deduction in first-order logic. Some ways use only "closed" formulas (sentences). Some ways allow open formulas (formulas with free occurrences of variables. Dec 31 '14 at 21:09
• this is my i.imgur.com/k1UHDdv.png define
– A_l
Dec 31 '14 at 21:28
• I have seen versions of the Deduction Theorem in which "$A$" need not be closed. They are a little more complicated. Dec 31 '14 at 21:49
• What book/source is this from? Dec 31 '14 at 22:30
• Also see this post: math.stackexchange.com/a/580692/630 Jan 1 '15 at 12:47

In the system of Joseph Shoenfield, Mathematical Logic (1967) the restriction on $A$ being closed is needed in the proof of the Deduction Theorem [see page 33] in order to apply the $\exists$-introduction rule [se page 21] :
if $x$ is not free in $B$, infer $\exists x A \rightarrow B$ from $A \rightarrow B$.
Without the proviso on $B$ in the rule, we can derive the invalid $\exists x (x=0) \rightarrow (x=0)$ from the tautology : $(x=0) \rightarrow (x=0)$.