The deduction theorem needs its free-variable restriction

Let the carrier be $M=\{0,1\}$ with $0\mathrm{\ne }1$, and interpret $P$ by $\{0\}$. Set the assignment $s(v)=0$ for every variable $v$. Then $\mathcal{M},s\models P(x)$. But $s[x:=1]$ does not satisfy $P(x)$, so it does satisfy $\mathrm{\neg }P(x)$. Consequently $\mathcal{M},s\models \mathrm{\exists }x\mathrm{\neg }P(x)$ and $\mathcal{M},s\models ̸\mathrm{\forall }xP(x)$ by F1. The implication $P(x)\to \mathrm{\forall }xP(x)$ has true antecedent and false consequent at $s$, so its expanded negated conjunction is false.

The purported unrestricted inference is explicit: start with the open assumption $P(x)$; generalize the very variable $x$ to obtain $\mathrm{\forall }xP(x)$; discharge that assumption to obtain $P(x)\to \mathrm{\forall }xP(x)$. Step 1.1 refutes this final formula in a nonempty set structure. Thus a deduction theorem used after generalization must retain the restriction on free variables of discharged assumptions; replacing the open assumption by a sentence removes this particular offending free variable. This counterexample establishes invalidity directly and does not assume any completeness theorem.