Systèmes de preuve

3 Systèmes de preuve

Les systèmes de preuve pour la logique du premier ordre sont tous des extensions de ceux pour la logique propositionnelle, où la mention ``variable propositionnelle'' doit être remplacée par ``atome'', et où de nouvelles règles sont ajoutées pour tenir compte des quantifications.

Par exemple, la logique classique du premier ordre a des systèmes de Hilbert. Un exemple est SKC₁ :

Axiomes :
- (K) FÞF'ÞF,
- (S) (FÞF'ÞF'') Þ(FÞF') Þ(FÞF''),
- (C) ¬¬FÞF
- (E) (" x·F)Þ F[t/x] pour toute formule F, toute variable x et tout terme t,
- (I) (" x· F Þ F')Þ F Þ " x· F', pour toutes formules F, F' et pour toute variable x telle que x n'est pas libre dans F.
Règles :
- (MP) de F et FÞF', déduire F', pour toutes F, F',
- (Gen) de F, déduire " x·F, pour toute formule F et toute variable x.

où seuls les axiomes (E), (I) et la règle (Gen) sont nouveaux. Comme dans le système SKC, seuls ", Þ et F sont des notations de base dans ce système, de sorte que ¬ F est une abréviation de F Þ F en particulier. En fait, $ est aussi une abréviation : $ x·F est une abréviation de ¬" x·¬F.

La règle (Gen) est la règle de généralisation. Si nous avons réussi à prouver F, alors F est valide (si la logique est cohérente), donc elle est vraie dans toute affectation, donc pour toute valeur de x, de sorte que " x·F doit être valide aussi, donc prouvable (si nous voulons que le système de preuve soit complet).

Figure 1: Déduction naturelle en forme de séquents : règles des quantificateurs

La logique classique du premier ordre a aussi des systèmes de déduction naturelle. Par exemple, nous pouvons ajouter les règles de la figure 1 à celles du système ND du chapitre sur la logique propositionnelle classique.

Figure 2: Le système LK de Gentzen

Dans le but d'analyser la structure des preuves, nous serons davantage intéressés par le système LK de Gentzen (cf. figure 2). C'est une extension du système LK₀ du chapitre sur la logique propositionnelle classique, auquel nous avons ajouté les règles "L, "R, $L, $R sur les quantifications.

Tous ces systèmes sont corrects et complets pour la logique du premier ordre. Nous ne le prouverons que pour LK, en section 5.3 après avoir présenté toutes les notions nécessaires.