# Some Metatheorems of Deduction

Generalization Theorem. If $$\Gamma \vdash \varphi$$ and $$x$$ does not occur free in any formula in $$\Gamma$$, then $$\Gamma \vdash \forall x \varphi$$.

Proof. (By induction on $$\varphi$$.)

Rule T. If $$\Gamma \vdash \alpha_1, \dots, \Gamma \vdash \alpha_n$$ and $$\{\alpha_1, \dots, \alpha_n\} \models_t \beta$$, then $$\Gamma \vdash \beta$$.

Deduction Theorem. $$\Gamma; \gamma \vdash \varphi \iff \Gamma \vdash (\gamma \to \varphi)$$.

Proof. (By induction on $$\varphi$$.)

Contraposition. $$\Gamma; \varphi \vdash \lnot \psi \iff \Gamma; \psi \vdash \lnot \varphi$$.

If for some $$\beta$$, both $$\beta$$ and $$\lnot \beta$$ are theorems of the set $$\Gamma$$, we say that $$\Gamma$$ is inconsistent. In this case, any arbitrary formula $$\alpha$$ is a theorem since $$\beta \to \lnot \beta \to \alpha$$ is a tautology.

Reductio ad Absurdum. If $$\Gamma; \varphi$$ is inconsistent, then $$\Gamma \vdash \lnot \varphi$$.

Generalization on Constants. Assume that $$\Gamma \vdash \varphi$$ and that $$c$$ is a constant symbol that does not occur in $$\Gamma$$. Then there is a variable $$y$$ (which does not occur on $$\varphi$$) such that $$\Gamma \vdash \forall y \varphi^c_y$$. Furthermore, there is a deduction of $$\forall y \varphi^c_y$$ from $$\Gamma$$ in which $$c$$ does not occur.

Corollary 1. Assume that $$\Gamma \vdash \varphi^x_c$$, where the constant symbol $$c$$ does not occur in $$\Gamma$$ or in $$\varphi$$. Then $$\Gamma \vdash \forall x \varphi$$, and there is deduction of $$\forall x \varphi$$ from $$\Gamma$$ in which $$c$$ does not occur.

Existence of Alphabetic Variants. Let $$\varphi$$ be a formula, $$t$$ be a term, and $$x$$ be a variable. Then we can find a formula $$\varphi'$$ (called an alphabetic variant of $$\varphi$$), which differs from $$\varphi$$ only in the choice of quantified variables such that

1. $$\varphi \vdash \varphi'$$ and $$\varphi' \vdash \varphi$$.
2. $$t$$ is substitutable for $$x$$ in $$\varphi'$$.