Artificial intelligent assistant

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? Many thanks for your help.

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.

xcX3v84RxoQ-4GxG32940ukFUIEgYdPy 06090c76f6fb3214ae413723f2d667f8