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?


I found a counterexample.

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

when A is not a closed formula.

  • $\begingroup$ 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. $\endgroup$ Dec 31 '14 at 21:09
  • $\begingroup$ this is my i.imgur.com/k1UHDdv.png define $\endgroup$
    – A_l
    Dec 31 '14 at 21:28
  • 1
    $\begingroup$ I have seen versions of the Deduction Theorem in which "$A$" need not be closed. They are a little more complicated. $\endgroup$ Dec 31 '14 at 21:49
  • $\begingroup$ What book/source is this from? $\endgroup$ Dec 31 '14 at 22:30
  • 1
    $\begingroup$ Also see this post: math.stackexchange.com/a/580692/630 $\endgroup$ 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)$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.