# A question about the deduction theorem

The deduction theorem states that if $T \cup \{ \psi \} \vdash \varphi$ and the generalisation rule is not used to prove $\varphi$ then $T \vdash \psi \rightarrow \varphi$.

If I apply the generalisation rule, where exactly does it go wrong if I apply the deduction theorem thereafter? Can someone provide an example?

-
What does $\top \to x$ even mean, if $x$ is a variable (as opposed to a proposition or a predicate)? –  Zhen Lin Oct 23 '11 at 12:09
It could be an axiom but I wrote it as an example of the kind of example I'm looking for. –  Rudy the Reindeer Oct 23 '11 at 12:15
@Matt: It can't be an axiom, since it's not even a well-formed formula. –  Chris Eagle Oct 23 '11 at 12:25
@ChrisEagle: True! I'll delete it seeing as it's not relevant for my question. –  Rudy the Reindeer Oct 23 '11 at 12:33
Hint: Forget about $T$ (i.e., take $T = \emptyset$), and take $\psi$ as a formula with free variables (i.e., it is not a setence) such that $\varphi$ is the universal closure of $\psi$. –  boumol Oct 23 '11 at 15:20

The important thing to realise is that whatever is on the RHS of $\vdash$ has got to be an axiom (meaning: a universally true formula). On the other hand, on the LHS we can assume whatever we like. So for example if $T = \emptyset$ we can show that $\{ \varphi (x) \} \vdash \forall x \varphi(x)$. What we can't do is to show that $\emptyset \vdash \varphi(x) \to \forall x \varphi (x)$.

To see why we can't let's consider the example $\varphi (x) = (x = 1)$:

If we assume ($x = 1$) then we get the following formal proof of $\{ x = 1 \} \vdash \forall x (x = 1)$:

$(1) x = 1 ( \in T)$

$(2) \forall x (x = 1)$ (generalisation rule applied to ($1$))

On the other hand, if we use the deduction rule on this to get $\vdash (x = 1) \to \forall x (x = 1)$ then we have $\top \to \bot$ if we replace $x$ with $1$ where it's free. But this is false, hence the formula on the RHS is not universally true.

-
i think it is necessary to mention the Domain of your interpretation which can be natural numbers. –  kiyarash Jan 9 at 13:29
also it would be better to explain why $\vdash (x = 1) \to \forall x (x = 1)$ is not satisfied by your interpretation –  kiyarash Jan 9 at 13:30