Démonstrations formelles

On fixe le système de Hilbert suivant, tel qu'il est exposé par Enderton (A Mathematical Introduction to Logic, 1972, §2.4), dont les deux groupes d'axiomes de l'égalité sont réunis ici en un seul ; l'idée de prendre pour axiomes toutes les généralisations, avec le modus ponens pour seule règle, remonte à Quine (Mathematical Logic, 1940).

Les axiomes logiques sont toutes les généralisations $\forall y_1 \cdots \forall y_k\, \alpha$ des formules $\alpha$ suivantes :

(1) les instances de tautologies, c'est-à-dire les formules obtenues en remplaçant les lettres d'une tautologie propositionnelle par des formules du premier ordre ;

(2) $\forall x\, \alpha \to \alpha[t/x]$, si $t$ est substituable à $x$ dans $\alpha$ ;

(3) $\forall x\, (\alpha \to \beta) \to (\forall x\, \alpha \to \forall x\, \beta)$ ;

(4) $\alpha \to \forall x\, \alpha$, si $x$ n'est pas libre dans $\alpha$ ;

(5) $x = x$, et $x = y \to (\alpha \to \alpha')$, si $\alpha$ est atomique et si $\alpha'$ s'obtient en remplaçant certaines occurrences de $x$ par $y$.

Une démonstration formelle de $\varphi$ à partir de $T$ est une suite finie de formules, terminée par $\varphi$, dont chacune est un axiome logique, un élément de $T$, ou se déduit de deux formules précédentes $\alpha$ et $\alpha \to \beta$ par la seule règle, le modus ponens. On note alors $T \vdash \varphi$.

Plus généralement, on définit de la même façon une démonstration formelle à partir d'un ensemble $\Gamma$ de formules, closes ou non, et l'on note $\Gamma \vdash \varphi$.