Originally Posted by

**emakarov** I think the "soft" approach uses the soundness and completeness theorems.

The idea of the hard approach is that any parameter or a free variable can be systematically replaced throughout a derivation by something else, and the resulting formula sequence is be a valid derivation. That is, an n-ary predicate symbol P can be replaced by a formula $\displaystyle Q(x_1, ..., x_n)$ in the sense that every occurrence of $\displaystyle Pt_1 ... t_n$ for some terms $\displaystyle t_i$ is replaced by $\displaystyle Q^{x_1,\dots,x_n}_{t_1,\dots,t_n}$. Similarly, a constant can be replaced by any term. The replacement has to be done in every formula of the derivation, including the axioms. So, for example, P can be replaced by the formula x = x (alternatively, by ~(x = x)) for a fresh variable x.

This works because such substitution converts axioms into axioms. Also, if in the original derivation Modus Ponens was aplied to A -> B and A, the substitution converts these formulas into some A' -> B' and A', so MP is again applicable. Formally, one proves that a derivation remains valid by induction on the length of the derivation.

This is just an outline; feel free to discuss the details.