Chapitre 3

Logique et systèmes de preuve

https://xkcd.com/246/

Le cours d’informatique de première année permet l’introduction d’un cadre rigoureux pour l’étude
syntaxique et sémantique des formules logiques. Ils ont notamment permis de considérer la notion de
vérité dans le calcul propositionnel et d’introduire la notion de satisfiabilité. Il en découle l’important
problème SAT, i.e. savoir décider si une formule donnée est satisfiable ou non.
Malheureusement, on se heurte vite à deux problèmes : d’une part, résoudre le problème SAT par
bruteforce semble assez peu efficace (complexité exponentielle), et d’autre part, on ne peut jusqu’ici
tirer profit de la méthode de démonstration utilisée en mathématiques. Ce chapitre vise à palier ces
problèmes, en introduisant le concept de systèmes de preuve.

54
3.1 Rappels : logique propositionnelle
Dans un premier temps, on rappelle des notions de logique propositionnelle vues en première année.

3.1.1 Syntaxe
Définition 3.1 : formules propositionnelles
Soit V un ensemble (fini ou dénombrable) de variables.
On définit l’ensemble des formules propositionnelles par induction :
• > (“vrai” ou “top”) est une formule propositionnelle ;
• ⊥ (“absurde” ou “bot”) est une formule propositionnelle ;
• si x ∈ V, x est une formule propositionnelle ;
• si ϕ et ψ sont des formules propositionnelles, alors :
• ¬ϕ (“non”, opération de négation) est une formule propositionnelle ;
• ϕ ∨ ψ (“ou”, opération de disjonction) est une formule propositionnelle ;
• ϕ ∧ ψ (“et”, opération de conjonction) est une formule propositionnelle ;
• ϕ → ψ (“implique”, opération d’implication) est une formule propositionnelle.
On se donne également le sucre syntaxique suivant : ϕ ↔ ψ désigne la formule
propositionnelle (ϕ → ψ) ∧ (ψ → ϕ).

La nature inductive des formules propositionnelles fait qu’elles admettent naturellement une structure
arborescente, qu’on peut obtenir facilement :
• les formules propositionnelles de base (>, ⊥, x pour x ∈ V) sont des feuilles ;
• les nœuds internes découlent de l’inductivité, et sont étiquetés par les opérateurs ¬ (d’arité 1) ou
∨, ∧, → (d’arité 2).

Définition 3.2 : arbre syntaxique

Soit V un ensemble (fini ou dénombrable) de variables. Soit ϕ une formule propositionnelle sur V.
• On appelle arbre syntaxique de ϕ toute représentation arborescente de ϕ telle que décrite
ci-dessus.
• On appelle hauteur de ϕ la hauteur de son arbre syntaxique.
• On appelle taille de ϕ le nombre de nœuds de son arbre syntaxique.

Exemple 3.1 : arbre syntaxique

On considère la formule propositionnelle suivante :

((a ∧ b) ∨ (c ∧ ¬d)) → (c ∨ d)

Celle-ci a pour arbre syntaxique :

→

∨ ∨

∧ ∧ c d

a b c ¬

55
3.1.2 Sémantique
La sous-partie précédente ne définie qu’une sémantique, qui a priori n’a pas de sens particulier. Dans
cette sous-partie, on rappelle la sémantique associée à cette syntaxe, i.e. une définition formelle du vrai
associé à cette syntaxe.

Définition 3.3 : valuation

Soit V un ensemble (fini ou dénombrable) de variables. On appelle valuation (sur V) une fonction
ν : V → {0, 1}.

Une valuation est donc une “configuration” des différentes variables selon un critère booléen : une variable
x ∈ V est soit vraie (on a alors ν(x) = 1), soit fausse (on a alors ν(x) = 0).

Remarque 3.1 : notation alternative

Dans ce cours, nous avons fait le choix d’utiliser 0 et 1 pour désigner les booléens, mais il est
également courant d’utiliser les lettres F et V .

On étend par la définition suivante cette notion de vérité à n’importe quelle formule propositionnelle.

Définition 3.4 : valeur de vérité, évaluation

Soit V un ensemble (fini ou dénombrable) de variables propositionnelles, soit ν une valuation sur V.
On appelle évaluation sur ν la fonction ν qui étend la valuation ν sur l’ensemble des formules
propositionnelles sur V, et qui est définie par induction structurelle sur les formules :
• ν(>) = 1 ;
• ν(⊥) = 0 ;
• ν(x) = ν(x) pour x ∈ V ;
• pour toutes formules propositionnelles ϕ et ψ :
( (
1 si ν(ϕ) = 0 1 si ν(ϕ) = 1 ou ν(ψ) = 1
ν(¬ϕ) = ν(ϕ ∨ ψ) =
0 sinon 0 sinon
( (
1 si ν(ϕ) = 1 et ν(ψ) = 1 1 si ν(ϕ) = 0 ou ν(ψ) = 1
ν(ϕ ∧ ψ) = ν(ϕ → ψ) =
0 sinon 0 sinon

Pour toute formule propositionnelle ϕ sur V, ν(ϕ) est appelée valeur de vérité de ϕ par ν.

Notation
Par soucis de simplicité, on notera souvent ν(ϕ) au lieu de ν(ϕ) pour une formule ϕ quelconque.

Définition 3.5 : satisfiabilité, validité

Soit V un ensemble (fini ou dénombrable) de variables propositionnelles, soit ϕ une formule
propositionnelle sur V.
• On dit que ϕ est satisfiable s’il existe une valuation ν sur V telle que ν(ϕ) = 1. Dans ce cas,
on dit également que ν satisfait ϕ, ou encore que ν est un modèle de ϕ, et on note ν ⊨ ϕ.
• On dit que ϕ est valide (ou que c’est une tautologie) si pour toute valuation ν sur V, on
a ν(ϕ) = 1.
• On dit que ϕ est insatisfiable (ou que c’est une antilogie) si pour toute valuation ν sur V,
on a ν(ϕ) = 0.

56
 Définition 3.6 : équivalence logique
Soit V un ensemble (fini ou dénombrable) de variables propositionnelles, soit ϕ et ψ deux formules
propositionnelles sur V.
On dit que ϕ et ψ sont logiquement équivalentes si pour toute valuation ν sur V, on a
ν(ϕ) = ν(ψ). Dans ce cas, on note ϕ ≡ ψ.

Définition 3.7 : conséquence logique

Soit V un ensemble (fini ou dénombrable) de variables propositionnelles, soit Γ un ensemble de
formules propositionnelles sur V, et soit ϕ une formule propositionnelle sur V.
On dit que ϕ est une conséquence logique de Γ si pour toute valuation ν sur V, on a :

(∀ψ ∈ Γ, ν ⊨ ψ) ⇒ ν ⊨ ϕ

Dans ce cas, on note Γ ⊨ ϕ.

Exemple 3.2 : lois de De Morgan

Soit V un ensemble (fini ou dénombrable) de variables propositionnelles, soit ϕ et ψ deux formules
propositionnelles sur V. On a les équivalences suivantes (appelées lois de De Morgan) :

¬(ϕ ∧ ψ) ≡ ¬ϕ ∨ ¬ψ
¬(ϕ ∨ ψ) ≡ ¬ϕ ∧ ¬ψ

Exemple 3.3
Soit V un ensemble (fini ou dénombrable) de variables propositionnelles, soit ϕ et ψ deux formules
propositionnelles sur V. On a les équivalences suivantes :

ϕ → ψ ≡ ¬ϕ ∨ ψ
¬¬ϕ ≡ ϕ

Il faut bien comprendre que, dans les exemples précédents, même si les formules de gauche et de droite sont
logiquement équivalentes, elles sont syntaxiquement différentes, et sont donc des formules distinctes.
Ainsi, même si certaines formules peuvent nous sembler trivialement les mêmes sémantiquement, il est
a priori difficile pour un ordinateur de l’établir (complexité exponentielle : dresser la table de vérité).
En effet, un algorithme n’a aucune intuition sur la sémantique de ce qu’il manipule, mais va analyser
mécaniquement la syntaxe de la formule.

3.1.3 Le problème SAT

Les concepts précédemment introduits amènent naturellement la question de la satisfiabilité d’une formule
propositionnelle ϕ quelconque, i.e. de décider si ϕ est satisfiable ou non. Deux méthodes permettant de
résoudre ce problème figurent au programme de première année :
• dresser la table de vérité de ϕ ;
• l’algorithme de Quine.
Le problème de ces deux méthodes est leur complexité : de manière évidente, calculer la table de vérité
de ϕ requiert de tester chaque valuation possible de V, et demande donc 2|V| lignes. Sa complexité est
donc exponentielle. L’algorithme de Quine peut certes s’avérer plus efficace en pratique que le calcul de
la table de vérité, mais sa complexité dans le pire des cas es elle aussi exponentielle.

57
Un autre point commun entre ces deux méthodes est que l’on raisonne sur la sémantique des formules.
Dans la suite de ce chapitre, nous allons voir une nouvelle approche pour résoudre le problème SAT qui
utilise une analyse purement syntaxique des formules, tout en s’inspirant des principes de
démonstrations/preuves utilisés en mathématiques : les systèmes de preuve.

3.2 Systèmes de preuve

On commence par introduire quelques notions qui seront nécessaires à ces systèmes de preuve.

3.2.1 Définitions
Définition 3.8 : séquent
Un séquent, noté Γ ` ϕ, est la donnée d’un contexte Γ (qui est un ensemble de formules), et
d’un but ϕ (qui est une formule).

Remarque 3.2 : prononciation

Le symbole ` se lit “thèse”.

Notation
La virgule est souvent utilisée pour dénoter l’union dans le contexte d’un séquent : ainsi, l’ensemble
Γ ∪ {ϕ} sera noté Γ, ϕ.

Définition 3.9 : séquent valide

Un séquent Γ ` ϕ est dit valide si Γ ⊨ ϕ.

Ainsi, dans un séquent, le contexte Γ peut être vu comme des hypothèses : un tel séquent est alors valide
si le but ϕ est une conséquence logique des formules de Γ ; autrement dit : si toutes les hypothèses de Γ
sont vraies, alors ϕ est vraie.

Définition 3.10 : règle d’inférence

Une règle d’inférence est la donnée d’un séquent appelé “conclusion”, et d’un nombre fixé
(potentiellement 0) de séquents appelés “prémisses”.
Une telle règle est en général représentée à l’aide d’une barre horizontale au dessus de laquelle se
trouvent les prémisses, et en dessous de laquelle se trouve la conclusion :
prémisses
z }| {
Γ1 ` ϕ1 Γ2 ` ϕ2 · · · Γn ` ϕn
(nom de la règle)
Γ`ϕ

Une telle règle d’inférence présente en général deux choses :

• un motif syntaxique particulier dans le séquent conclusion : ainsi, si un séquent donné possède
ce motif, la règle d’inférence en question est alors applicable à ce séquent ;
• certaines parties des prémisses sont des formules ou sous-formules présentes dans le séquent
conclusion : l’application de la règle d’inférence en question sur un séquent conclusion donné va
alors générer les prémisses associées.

Définition 3.11 : système de preuve

Un système de preuve est un ensemble fini de règles d’inférence.

58
 Définition 3.12 : arbre de preuve
Un arbre de preuve est un arbre tel que :
• chaque nœud de l’arbre est étiqueté par un séquent ;
• chaque nœud interne est également étiqueté du nom d’une des règles du système de preuve ;
• si un nœud interne est étiqueté par une règle ayant n prémisses, alors cette règle est applicable
au séquent de ce nœud, et ce nœud possède n fils étiquetés par les n prémisses générées par
cette règle.
Une branche d’un tel arbre de preuve est dite fermée si sa feuille est étiquetée par une règle ayant
0 prémisses.
Un arbre de preuve est dit terminé si toutes ses branches sont fermées.
Un arbre de preuve terminé est également appelé une dérivation.

Définition 3.13 : séquent prouvable

Un séquent Γ ` ϕ est dit prouvable dans un système de preuve s’il existe un arbre de preuve
terminé tel que Γ ` ϕ est l’étiquette de la racine.

Tout l’enjeu de ce chapitre est de mettre au point des règles afin d’obtenir un système de preuve ou les
séquents prouvables coïncident exactement avec les séquents valides.

Définition 3.14 : système de preuve correct/complet

Un système de preuve est dit correct si tout séquent prouvable dans ce système est valide.
Un système de preuve est dit complet si tout séquent valide est prouvable dans ce système.

Les avantages des systèmes de preuve sont multiples :

• ils sont uniquement basés sur la syntaxe, et ne raisonnent pas directement sur la sémantique (le
lien entre syntaxe et sémantique est cependant garanti si le système est correct et complet) : les
systèmes de preuve sont donc faciles à implémenter pour faire :
• de la preuve automatique ;
• des assistants de preuve ;
• ...
• il y a en général peu de règles, et celles-ci sont simples : il est donc facile d’analyser et de prouver
certaines propriétés d’un système de preuve donné ;
• modularité : enlever ou ajouter quelques règles à un système de preuve permet de l’adapter pour
obtenir un système correct et complet pour une autre logique.

3.2.2 La déduction naturelle

Nous présentons maintenant l’un des premiers systèmes de preuve historiquement développé pour la
logique propositionnelle : la déduction naturelle. Bien que des systèmes plus faciles à manipuler aient
été mis au point depuis, ce système est le seul officiellement au programme de MPI.
Dans les règles de la déduction naturelle (cf. page suivante), la plupart des règles sont soit :
• des règles d’introduction d’un connecteur logique (dénotées avec un i), et s’appliquent à un séquent
dont le but est une formule ayant ce connecteur logique comme connecteur principal : une telle règle
permet alors de “casser” cette formule en ses sous-formules, qui vont apparaître dans les prémisses ;
• des règles d’élimination d’un connecteur logique (dénotées avec un e), qui permettent de générer
une prémisse dont le but est une nouvelle formule ayant ce connecteur logique comme connecteur
principal : cela est utile si cette formule apparaît dans le contexte du séquent conclusion : on pourra
alors fermer cette prémisse à l’aide de la règle de l’axiome.

59
À ces règles s’ajoutent quelques règles permettant de gérer les symboles > et ⊥, de simplifier un contexte
(règle (Af f )) si certaines hypothèses ne sont plus utiles, de fermer des branches dont le séquent est
trivialement valide (règle (Ax)).
Une dernière règle, cruciale au système, permet de faire des raisonnements par l’absurde (règle (Abs)).

Définition 3.15 : règles d’inférence de la déduction naturelle propositionnelle

Voici les règles d’inférence de la déduction naturelle pour la logique propositionnelle :

Γ`ϕ
(Ax) (>) (Af f )
Γ, ϕ ` ϕ Γ`> Γ, ψ ` ϕ

Γ, ϕ ` ψ Γ`ϕ→ψ Γ`ϕ
(→i ) (→e )
Γ`ϕ→ψ Γ`ψ

Γ`ϕ Γ`ψ Γ`ϕ∧ψ Γ`ϕ∧ψ

(∧i ) (∧ge ) (∧de )
Γ`ϕ∧ψ Γ`ϕ Γ`ψ

Γ`ϕ Γ`ψ Γ`ϕ∨ψ Γ, ϕ ` θ Γ, ψ ` θ

(∨gi ) (∨di ) (∨e )
Γ`ϕ∨ψ Γ`ϕ∨ψ Γ`θ

Γ, ϕ ` ⊥ Γ ` ¬ϕ Γ ` ϕ
(¬i ) (¬e )
Γ ` ¬ϕ Γ`⊥

Γ ` ⊥ (⊥) Γ, ¬ϕ ` ⊥
(Abs)
Γ`ϕ Γ`ϕ

Exemple 3.4 : modus ponens

Prouvons la règle du modus ponens : p, p → q ` q.

(Ax) (Ax)
p, p → q ` p → q p, p → q ` p
(→e )
p, p → q ` q

Exemple 3.5 : syllogisme Barbara

Prouvons la règle du syllogisme Barbara : p → q, q → r ` p → r.

(Ax) (Ax)
p → q, q → r, p ` p → q p → q, q → r, p ` p
(Ax) (→e )
p → q, q → r, p ` q → r p → q, q → r, p ` q
(→e )
p → q, q → r, p ` r
(→i )
p → q, q → r ` p → r

Insistons désormais à nouveau sur la distinction entre syntaxe et sémantique : la règle (Ax) n’est applicable
que si le but ϕ apparaît dans Γ de manière rigoureusement identique d’un point de vue syntaxique,
et uniquement dans ce cas.

60
 Exemple 3.6 : commutativité de la conjonction
Le séquent séquent ϕ ∧ ψ ` ψ ∧ ϕ, bien qu’il semble trivial sémantiquement, ne peut être prouvé
directement en appliquant la règle (Ax). . . Voici une manière correcte de le prouver :

(Ax) (Ax)
ϕ∧ψ `ϕ∧ψ ϕ∧ψ `ϕ∧ψ
(∧de ) (∧ge )
ϕ∧ψ `ψ ϕ∧ψ `ϕ
(∧i )
ϕ∧ψ `ψ∧ϕ

Continuons avec des exemples illustrant l’utilisation d’autres règles.

Exemple 3.7
Prouvons le séquent suivant : ¬ϕ ∨ ψ ` ϕ → ψ.

(Ax) (Ax)
ϕ, ¬ϕ ` ¬ϕ ϕ, ¬ϕ ` ϕ
(¬e )
ϕ, ¬ϕ ` ⊥
(Af f )
¬ϕ∨
 ψ, ϕ, ¬ϕ ` ⊥
(Ax) (⊥) (Ax)
¬ϕ ∨ ψ, ϕ ` ¬ϕ ∨ ψ ¬ϕ ∨ ψ, ϕ, ¬ϕ ` ψ ¬ϕ ∨ ψ, ϕ, ψ ` ψ
(∨e )
¬ϕ ∨ ψ, ϕ ` ψ
(→i )
¬ϕ ∨ ψ ` ϕ → ψ

Exemple 3.8
Prouvons le séquent suivant : ϕ ` ¬¬ϕ.

(Ax) (Ax)
ϕ, ¬ϕ ` ¬ϕ ϕ, ¬ϕ ` ϕ
(¬e )
ϕ, ¬ϕ ` ⊥
(¬i )
ϕ ` ¬¬ϕ

Prouvons maintenant sa réciproque : ¬¬ϕ ` ϕ.

(Ax) (Ax)
¬¬ϕ, ¬ϕ ` ¬¬ϕ ¬¬ϕ, ¬ϕ ` ¬ϕ
(¬e )
¬¬ϕ, ¬ϕ ` ⊥
(Abs)
¬¬ϕ ` ϕ

Finissons avec un exemple célèbre pour n’être prouvable qu’à l’aide de la règle (Abs). Le défaut de cette
règle est qu’elle est toujours applicable, mais qu’il faut trouver le moment pour l’appliquer sans quoi on
risque d’être bloqué, ou de tourner en rond.

Exemple 3.9 : loi de Peirce

Montrons la formule suivante (appelée loi de Peirce) : ((p → q) → p) → p.
(Ax) (Ax)
(p → q) → p, ¬p, p ⊢ ¬p (p → q) → p, ¬p, p ⊢ p
(¬e )
(p → q) → p, ¬p, p ⊢ ⊥
(⊥)
(p → q) → p, ¬p, p ⊢ q
(Ax) (→i )
(p → q) → p, ¬p ⊢ (p → q) → p (p → q) → p, ¬p ⊢ p → q
(Ax) (→e )
(p → q) → p, ¬p ⊢ ¬p (p → q) → p, ¬p ⊢ p
(¬e )
(p → q) → p, ¬p ⊢ ⊥
(Abs)
(p → q) → p ⊢ p
(→i )
⊢ ((p → q) → p) → p

On montre maintenant que la déduction naturelle est un système de preuve correct et complet, i.e. qu’un
séquent est valide si et seulement s’il est prouvable en déduction naturelle.

61
On commence par montrer qu’on ne peut prouver que des choses qui sont vraies !

Théorème 3.1 : correction de la déduction naturelle

Soit Γ ` ϕ un séquent composé de formules de la logique propositionnelle.
Si Γ ` ϕ est prouvable en déduction naturelle, alors Γ ⊨ ϕ.

On commence par montrer un lemme sur chaque règle de la déduction naturelle prise individuellement.

Lemme 3.2 : correction des règles

Chaque règle de la déduction naturelle est correcte : si une règle est appliquée à un séquent
conclusion Γ ` ϕ et que toutes les prémisses générées par la règle sont valides, alors Γ ⊨ ϕ.

Preuve. On traite chaque règle les unes après les autres.

• (Ax) : soit ν une valuation satisfaisant toutes les formules du contexte Γ, ϕ, alors en particulier
ν ⊨ ϕ. Donc Γ, ϕ ⊨ ϕ. La règle (Ax) est donc correcte.
• (>) : peu importe le contenu de Γ, on a toujours Γ ⊨ >. La règle (>) est donc correcte.
• (Af f ) : soit ν une valuation satisfaisant toutes les formules du contexte Γ, ψ, alors en particulier
ν satisfait toutes les formules de Γ, et comme la prémisse Γ ` ϕ est valide, on a Γ ⊨ ϕ, donc
ν ⊨ ϕ. Ainsi, on a bien Γ, ψ ⊨ ϕ. La règle (Af f ) est donc correcte.
• (→i ) : soit ν une valuation satisfaisant toutes les formules du contexte Γ.
• Si ν ⊭ ϕ, alors ν ⊨ ϕ → ψ par la sémantique de →.
• Sinon, ν ⊨ ϕ, et comme la prémisse Γ, ϕ ` ψ est supposée valide, on a alors ν ⊨ ψ, et donc
finalement ν ⊨ ϕ → ψ.
Au final, dans tous les cas on a ν ⊨ ϕ → ψ, donc Γ ⊨ ϕ → ψ. La règle (→i ) est donc correcte.
• (→e ) : soit ν une valuation satisfaisant toutes les formules du contexte Γ. Par validité de la
première prémisse, on a ν ⊨ ϕ → ψ, et par la validité de la seconde prémisse, on a ν ⊨ ϕ. Ainsi,
ν ⊨ ψ, et on a donc Γ ⊨ ψ. La règle (→e ) est donc correcte.
• (∧i ) : soit ν une valuation satisfaisant toutes les formules du contexte Γ. Par validité de la
première prémisse, on a ν ⊨ ϕ, et par la validité de la seconde prémisse, on a ν ⊨ ψ. Ainsi,
ν ⊨ ϕ ∧ ψ, et on a donc Γ ⊨ ϕ ∧ ψ. La règle (∧i ) est donc correcte.
• (∧ge ) : soit ν une valuation satisfaisant toutes les formules du contexte Γ. Par validité de la
prémisse, on a ν ⊨ ϕ ∧ ψ, donc en particulier ν ⊨ ϕ. Ainsi, Γ ⊨ ϕ. La règle (∧ge ) est donc correcte.
• (∧de ) : soit ν une valuation satisfaisant toutes les formules du contexte Γ. Par validité de la
prémisse, on a ν ⊨ ϕ ∧ ψ, donc en particulier ν ⊨ ψ. Ainsi, Γ ⊨ ψ. La règle (∧de ) est donc correcte.
• (∨gi ) : soit ν une valuation satisfaisant toutes les formules du contexte Γ. Par hypothèse, la
prémisse est valide, donc on a ν ⊨ ϕ, et par conséquent ν ⊨ ϕ ∨ ψ. Ainsi, Γ ⊨ ϕ ∨ ψ. La règle
(∨gi ) est donc correcte.
• (∨di ) : soit ν une valuation satisfaisant toutes les formules du contexte Γ. Par hypothèse, la
prémisse est valide, donc on a ν ⊨ ψ, et par conséquent ν ⊨ ϕ ∨ ψ. Ainsi, Γ ⊨ ϕ ∨ ψ. La règle
(∨di ) est donc correcte.
• (∨e ) : soit ν une valuation satisfaisant toutes les formules du contexte Γ. Par validité de la
première prémisse, on a ν ⊨ ϕ ∨ ψ, donc ν ⊨ ϕ ou ν ⊨ ψ.
• Si ν ⊨ ϕ, alors par validité de la deuxième prémisse, on a ν ⊨ θ.
• Si ν ⊨ ψ, alors par validité de la troisième prémisse, on a ν ⊨ θ.
Ainsi, par disjonction de cas, on a ν ⊨ θ dans tous les cas. Donc Γ ⊨ θ. La règle (∨e ) est donc
correcte.
• (¬i ) : soit ν une valuation satisfaisant toutes les formules du contexte Γ. Par hypothèse, la
prémisse de la règle est valide, donc Γ, ϕ ⊨ ⊥. Or ⊥ est insatisfiable, il n’existe donc pas de
valuation satisfaisant à la fois toutes les formules de Γ et ϕ. Donc ν ⊭ ϕ, i.e. ν ⊨ ¬ϕ. Ainsi,
Γ ⊨ ¬ϕ. La règle (¬i ) est donc correcte.

62
 • (¬e ) : soit ν une valuation satisfaisant toutes les formules du contexte Γ. Par validité de la
première prémisse on a ν ⊨ ¬ϕ, et par validité de la seconde prémisse on a ν ⊨ ϕ. Cela est
impossible : il n’existe donc pas de telle valuation ν (Γ est incohérent). Autrement dit, on a
Γ ⊨ ⊥. La règle (¬e ) est donc correcte.
• (⊥) : par validité de la prémisse, on a Γ ⊨ ⊥, et il n’existe donc pas de valuation satisfaisant
toutes les formules de Γ (Γ est incohérent). Dans ce cas particulier, on a Γ ⊨ ϕ. La règle (⊥)
est donc correcte.
• (Abs) : soit ν une valuation satisfaisant toutes les formules du contexte Γ. Par l’absurde,
supposons que Γ ⊭ ϕ, i.e. considérons une valuation ν satisfaisant toutes les formules de Γ
et ne satisfaisant pas ϕ. Autrement dit, pour une telle valuation ν, on a ν ⊨ ¬ϕ. Or, par validité
de la prémisse, on a Γ, ¬ϕ ⊨ ⊥, donc ν ⊨ ⊥ : impossible. Ainsi, par l’absurde, on a bien Γ ⊨ ϕ.
La règle (Abs) est donc correcte. □

Remarque 3.3 : règles inversibles

Une notion réciproque de la notion de règle correcte est celle de règle inversible : une règle
d’inférence est dite inversible si, lorsqu’on l’applique sur un séquent conclusion valide, toutes les
prémisses générées sont elles aussi des séquents valides. L’intérêt d’avoir des règles inversibles est
que l’on est sûr de ne jamais appliquer une règle au “mauvais” moment.
Malheureusement, toutes les règles de la déduction naturelle ne sont pas inversibles. En effet,
certaines règles introduisent de nouvelles formules arbitraires dans les prémisses, et un mauvais
choix de cette formule quelconque peut conduire à une prémisse non valide alors que le séquent
conclusion était valide. La difficulté en déduction naturelle est donc souvent de trouver le bon
moment pour appliquer une règle, et faire le bon choix concernant la formule arbitraire à introduire,
sans quoi l’on risque d’être bloqué. Cela demande de l’intuition, et donc de l’entrainement. . . Mais
un bon réflexe à avoir lorsqu’on cherche une preuve en déduction naturelle est de toujours vérifier
de tête si les séquents que l’on génère sont bien toujours valides.
Il existe d’autres systèmes de preuve pour la logique propositionnelle, dont le calcul des séquents
qui a la bonne propriété de n’avoir que des règles inversibles (cf. devoir maison) : cela simplifie
grandement la recherche de preuve, ainsi que la preuve de complétude du système (en fait, les deux
sont liés !).

Preuve (du théorème 3.1). Soit Γ ` ϕ un séquent prouvable en déduction naturelle, i.e. qui est
l’étiquette de la racine d’une arbre de preuve terminé (notons le A).
Montrons que Γ ⊨ ϕ par induction structurelle sur A.
• Si la racine de A ne possède aucun fils, comme A est terminé, c’est qu’on a pu appliquer l’une
des règles (Ax) ou (>) à Γ ` ϕ. Or, d’après le lemme 3.2, ces règles sont valides, donc Γ ⊨ ϕ.
• Si la racine de A possède n ≥ 1 fils, c’est que la règle appliquée à Γ ` ϕ possède n prémisses.
De plus, comme A est terminé, ces n prémisses générées sont toutes prouvables (par les
sous-arbres respectifs de A). Ainsi, par hypothèse d’induction, ces n prémisses sont valides.
Or, d’après le lemme 3.2, la règle appliquée à la racine de A est correcte, donc Γ ⊨ ϕ.
Ainsi, la déduction naturelle est un système de preuve correct. □
Un résultat remarquable concernant la déduction naturelle est que la réciproque du théorème 3.1 est vraie,
i.e. que tout ce qui est vrai (en logique propositionnelle) peut être prouvé dans la déduction naturelle.

Théorème 3.3 : complétude de la déduction naturelle

Soit Γ ` ϕ un séquent composé de formules de la logique propositionnelle.
Si Γ ⊨ ϕ, alors Γ ` ϕ est prouvable en déduction naturelle.

Preuve. Admis. □

63
Bien que la preuve de ce théorème ne soit pas à votre programme, une preuve constructive du
théorème 3.3 permettrait l’élaboration d’un algorithme qui calculerait automatiquement une preuve en
déduction naturelle de n’importe quel séquent valide pris en entrée (et qui échouerait sur les séquents
non valides, et uniquement ceux-ci). Malheureusement, concernant la déduction naturelle, les preuves
constructives de ce théorème sont toutes très compliquées, et mènent à des algorithmes très peu
efficaces (les preuves calculées automatiquement sont souvent très tordues et très longues).
Cependant, d’autres systèmes de preuve possèdent des preuves de complétudes bien plus simples, ce qui
donne alors des algorithmes de recherche de preuve automatiques bien moins complexes et beaucoup plus
efficaces. C’est le cas par exemple du calcul des séquents (cf. devoir maison) ; pour ce système de preuve,
la simplicité vient surtout du fait que toutes ses règles sont inversibles (cf. remarque 3.3).

3.2.3 La logique intuitionniste (HP)

L’un des intérêts de la déduction naturelle est que ce système de preuve s’adapte très bien à une autre
logique, appelée logique intuitionniste. Cette logique reprend la même syntaxe que la logique
propositionnelle classique, mais modifie un peu la sémantique : elle ne considère comme vrai que les
formules qui ont une preuve constructive.
La notion de preuve constructive est très importante en informatique : lorsqu’on prouve un énoncé
mathématiques ayant un “il existe” et que la preuve est constructive, la preuve décrit en fait un algorithme
permettant de calculer la valeur de la variable de ce “il existe”. Et réciproquement, un algorithme peut
également être vu comme une preuve constructive d’une certaine propriété. Il y a donc un lien très étroit
entre l’étude de preuves constructives et l’algorithmique.

Exemple 3.10 : TVI et recherche dichotomique

La preuve du théorème des valeurs intermédiaires que vous avez vu en première année est
constructive : elle décrit en fait l’algorithme de recherche dichotomique.

Malheureusement, toutes les preuves ne sont pas constructives. C’est le cas par exemple lorsqu’on utilise
le tiers exclu.

Exemple 3.11 : preuve non constructive

Montrons l’énoncé mathématiques suivant : ∃(α, β) ∈ R2 tel que α ∈
/ Q, β ∈
/ Q et αβ ∈ Q.
√ √2 √
Preuve. Considérons la valeur 2 (on suppose connu le fait que 2 ∈
/ Q) :
√ √2 √
• si 2 ∈ Q, alors α = β = 2 conviennent ;
 √ √ 2
√ 2 √ 2 √ √2 √
• sinon, 2 = 2 = 2 ∈ Q, et dans ce cas α = 2 et β = 2 conviennent.

Finalement, par le principe du tiers exclu, la propriété est vraie. □

À la fin de cette preuve, l’énoncé est bien démontré, mais on ne sait toujours pas quelles valeurs
de α et β conviennent.

Ainsi, puisque le tiers exclus pose problème, la formule p ∨ ¬p par exemple n’est pas considérée comme
valide en logique intuitionniste. Si l’on essaye de prouver cette formule en déduction naturelle, c’est
d’ailleurs assez compliqué (alors que la formule semble triviale), et on est obligé d’utiliser la règle (Abs).
La définition de la sémantique d’une telle logique est assez compliquée, et on ne la détaillera pas ici. On
énoncera simplement le théorème suivant.

64
 Théorème 3.4 : déduction naturelle intuitionniste (HP)
Si l’on enlève la règle (Abs) de la déduction naturelle, on obtient un système de preuve correct et
complet pour la logique intuitionniste.

Preuve. Admis. □
Ce théorème illustre bien la modularité des systèmes de preuve : ici, le simple fait d’enlever une règle à
un système correct et complet pour une première logique permet d’obtenir un système correct et complet
pour une autre logique.
On finit cette petite parenthèse sur la logique intuitionniste en faisant un lien fort avec OCaml !
Considérons ici les formules de la logique propositionnelle n’utilisant que le connecteur logique →. On a
en fait une bijection très simple entre de telles formules et les types OCaml : les variables propositionnelles
peuvent être vus comme des types simples, et les → comme des -> typant des fonctions. On a alors le
théorème suivant.

Exemple 3.12
La formule (a → b) → c → a peut être vue comme le type OCaml ('a -> 'b) -> 'c -> 'a.

Théorème 3.5 : correspondance de Curry-Howard (HP)

Soit ϕ une formule n’utilisant que le connecteur logique →.
ϕ est vraie en logique intuitionniste si et seulement s’il existe une fonction OCaml ayant pour
type ϕ.

Preuve. Admis. □
Cette correspondance va même plus loin : à partir d’une fonction OCaml ayant pour type ϕ, on peut en
réalité construire la preuve de ϕ en déduction naturelle intuitionniste ! Ainsi, une fonction OCaml peut
être considérée comme une preuve de son propre type.

3.3 Logique du premier ordre

Dans cette partie, on considère toujours un ensemble V (fini ou infini dénombrable) de variables.

Attention
Nous utilisons le même symbole V que dans la partie 3.1, car c’est ce qui est usuel dans la littérature.
Mais dans cette partie, les variables de V ne sont pas de la même nature que dans la partie 3.1.
En effet, dans les parties précédentes, une variable x ∈ V était de type booléen (variable
propositionnelle), alors que dans cette partie une variable x ∈ V sera d’un autre type quelconque
(entier, réel, . . . ) : les éléments de V sont désormais des variables du premier ordre.
Nous reviendrons plus tard sur ce détail (cf. remarque 3.4).

La logique propositionnelle a le mérite d’être simple, mais n’est pas très expressive. On définit maintenant
une extension de cette logique : la logique du premier ordre. La grosse nouveauté dans cette logique
est la présence de quantificateurs dans la syntaxe. Cependant, nous n’aurons pas encore quantifier sur
des sous-ensembles, voire même sur différents ensembles. Pour cela, il faut aller plus loin dans l’extension
de l’expressivité : c’est la logique du second ordre. Mais cette dernière n’est pas au programme de
MPI.

65
3.3.1 Syntaxe
Définition 3.16 : signature
On appelle signature un triplet S = (C, F, R) de trois ensembles de symboles, où :
• C est l’ensemble des symboles de constantes ;
• F est l’ensemble des symboles de fonctions ;
• R est l’ensemble des symboles de relations (ou de prédicats).
À chaque symbole de F et R, on associe un entier > 0 appelé arité.

Lorsqu’on utilise le mot “prédicat” plutôt que le mot “relation”, on parle alors de “calcul des prédicats”
plutôt que de “logique du premier ordre”.

Notation
• Il est usuel de noter entre parenthèses l’arité de chaque symbole lors de la définition de F et R.
• Pour n ∈ N⋆ , on note Fn l’ensemble des symboles de F d’arité n.

Remarque 3.4
• Un symbole de constante peut être vu comme un symbole de fonction d’arité 0.
• Les symboles de relation d’arité 0 sont l’équivalent des variables propositionnelles de la
partie 3.1, à savoir des constantes de type booléen.

Exemple 3.13 : signatures de quelques théories usuelles

• La signature de la théorie des groupes est :

C = {e} F = {?(2), ·−1 (1)} R = {= (2)}

• La signature de la théorie des corps ordonnés est :

C = {0, 1} F = {+(2), ×(2), −(1), ·−1 (1)} R = {= (2), ≤ (2)}

• La signature de la théorie des espaces vectoriels sur R est :

C = {0} F = {+(2), −(1)} ∪ {x 7→ λx, λ ∈ R} R = {= (2)}

• La signature de la théorie des ensembles est :

C = {∅} F = {∪(2), ∩(2), · (1)} R = {= (2), ⊂ (2), ∈ (2)}

• La signature de l’analyse réelle est :

C=R F = {+(2), ×(2), −(1), ·−1 (1), | · |(1), sin(1), ln(1), . . . } R = {= (2), ≤ (2), . . . }

Définition 3.17 : terme, terme clos

Soit S = (C, F, R) une signature. L’ensemble T (S) des termes sur S est défini inductivement :
• ∀x ∈ V, on a x ∈ T (S) ;
• ∀c ∈ C, on a c ∈ T (S) ;
• ∀f ∈ F , f d’arité n ∈ N⋆ , ∀(t1 , . . . , tn ) ∈ T (S)n , on a f (t1 , . . . , tn ) ∈ T (S).
Un terme clos est un terme qui ne contient pas de variables.

66
 Remarque 3.5
On notera parfois T plutôt que T (S) s’il n’y a pas d’ambiguïté possible sur la signature S.

Exemple 3.14
Pour la signature de la théorie des groupes :

−1
• x ? y et x−1 ? y ? x−1 sont des termes ;
• e−1 ? e est un terme clos.

Définition 3.18 : hauteur, taille d’un terme

• La hauteur d’un terme est la hauteur de son arbre syntaxique.
• La taille (ou longueur) d’un terme est le nombre de nœuds internes de son arbre syntaxique.

Proposition 3.6 : calcul inductif de la hauteur et de la taille

La hauteur d’un terme peut être définie par induction structurelle :
• ∀x ∈ V, h(x) = 0 ;
• ∀c ∈ C, h(c) = 0 ;
• ∀f ∈ Fn , h(f (t1 , . . . , tn )) = 1 + max{h(t1 ), . . . , h(tn )}.
La taille d’un terme peut être définie par induction structurelle :
• ∀x ∈ V, t(x) = 0 ;
• ∀c ∈ C, t(c) = 0 ;
• ∀f ∈ Fn , t(f (t1 , . . . , tn )) = 1 + t(t1 ) + · · · + t(tn ).

Remarque 3.6
• La taille d’un terme t est le nombre de symboles de fonction dans t.
• La hauteur d’un terme t est le nombre maximal de fonctions imbriquées dans t.

Définition 3.19 : formules atomiques, formules du premier ordre

Soit S = (C, F, R) une signature.
• Une formule atomique de S est une formule de la forme R(t1 , . . . , tn ), où R ∈ R d’arité n,
et (t1 , . . . , tn ) ∈ T (S)n .
On note Atom (S) l’ensemble des formules atomiques de S.
• L’ensemble FO(S) (pour “first order”) des formules de la logique du premier ordre sur S est
défini inductivement :
• > ∈ F O(S) ;
• ⊥ ∈ F O(S) ;
• si ϕ ∈ Atom (S), alors ϕ ∈ F O(S) ;
• si (ϕ, ψ) ∈ F O(S)2 et x ∈ V, alors les expressions suivantes sont dans FO(S) :

ϕ∨ψ ϕ∧ψ ϕ→ψ ¬ϕ ∃x ϕ ∀x ϕ

Nous allons bientôt définir la sémantique de la logique du premier ordre, mais donnons déjà quelques
intuitions. Les constantes de C seront évaluées dans un ensemble quelconque, disons par exemple R, et
dans ce cas les fonctions de Fn seront évaluées par des fonctions de Rn → R. Ainsi, les termes représentent
des valeurs de R : ce ne sont pas des booléens.

67
À l’inverse, les formules sont les objets syntaxiques qui vont être vus comme des booléens : les éléments de
base sont les formules atomiques, obtenues par relation entre des termes ; et ces formules de base peuvent
être combinées à l’aide des connecteurs logiques usuels. La nouveauté est que des variables du premier
ordre peuvent apparaître à l’intérieur des termes constituant la formule, et peuvent être quantifiées
existentiellement ou universellement.

Attention
Ne pas confondre terme et formule : les termes peuvent être vus comme des entiers ou des réels
selon le contexte, et les formules peuvent être vues comme des booléens.

Exemple 3.15
Considérons la signature de l’analyse réelle :
• sin(x) est un terme ;
• x = 3 est une formule ;
• ∀x (x > 0 → ∃y (y > 0 ∧ (x = y × y))) est une formule ;
• sin(x) ∧ x = 3 n’a pas de sens.

Attention
Si ϕ ∈ F O(S), alors dans l’arbre syntaxique de ϕ :
• certains sous-arbres sont des formules (appelées sous-formules de ϕ) ;
• certains sous-arbres sont des termes !

On finit cette sous-partie avec quelques définitions concernant les variables.

Définition 3.20 : variables libres, variables liées

Soit ϕ ∈ F O(S).
On définit l’ensemble FV(ϕ) des variables libres de ϕ (“free variables”) par induction structurelle
sur ϕ :
• si ϕ = R(t1 , . . . , tn ), FV(ϕ) est l’ensemble des variables apparaissant dans les ti ;
• si ϕ = ϕ1  ϕ2 avec  ∈ {∨, ∧, →}, alors FV(ϕ) = FV(ϕ1 ) ∪ FV(ϕ2 ) ;
• si ϕ = ¬ϕ0 , alors FV(ϕ) = FV(ϕ0 ) ;
• si ϕ = Qx ϕ0 avec Q ∈ {∃, ∀}, alors FV(ϕ) = FV(ϕ0 ) \ {x}.
On définit l’ensemble BV(ϕ) des variables liées de ϕ (“bound variables”) par induction
structurelle sur ϕ :
• si ϕ = R(t1 , . . . , tn ), BV(ϕ) = ∅ ;
• si ϕ = ϕ1  ϕ2 avec  ∈ {∨, ∧, →}, alors BV(ϕ) = BV(ϕ1 ) ∪ BV(ϕ2 ) ;
• si ϕ = ¬ϕ0 , alors BV(ϕ) = BV(ϕ0 ) ;
• si ϕ = Qx ϕ0 avec Q ∈ {∃, ∀}, alors BV(ϕ) = BV(ϕ0 ) ∪ {x}.

Exemple 3.16
ϕ1 = ∀x (x ? y = y ? x) FV(ϕ1 ) = {y} BV(ϕ1 ) = {x}
ϕ2 = ∀x∃y (y = 0) FV(ϕ2 ) = ∅ BV(ϕ2 ) = {x, y}


ϕ3 = ∀x∃y (x ? z = z ? y) ∧ (x = z ? z) FV(ϕ3 ) = {x, z} BV(ϕ3 ) = {x, y}

68
 Attention
Comme le montre ce dernier exemple, on a pas forcément FV(ϕ) ∩ BV(ϕ) = ∅, même si en général
on préfère écrire des formules satisfaisant cette condition.

On peut toujours se ramener à une formule satisfaisant cette condition, grâce à la définition suivante.

Définition 3.21 : α-équivalence

Deux formules ϕ et ψ sont dites α-équivalentes si elles sont syntaxiquement identiques, à un
renommage près des occurrences liées des variables.
Lorsqu’on transforme une formule ϕ en une formule ψ qui lui est α-équivalente, on dit qu’on
effectue un α-renommage.

Exemple 3.17
Les deux formules suivantes sont α-équivalentes :


∀x∃y (x ? z = z ? y) ∧ (x = z ? z)


∀a∃b (a ? z = z ? b) ∧ (x = z ? z)

Définition 3.22 : substitution

Soit ϕ ∈ F O(S), x ∈ V, et t ∈ T (S).
On note ϕ[x := t] la formule obtenue en remplaçant dans ϕ toutes les occurrences libres de x par t,
après α-renommage éventuel des variables liées de ϕ pour avoir BV(ϕ) ∩ FV(t) = ∅.
On dit qu’on a effectué une substitution de x par t dans ϕ.

Attention
Si jamais BV(ϕ) ∩ FV(t) 6= ∅, il ne faut pas oublier de faire l’α-renommage !

Exemple 3.18
Si ϕ : ∀y x = y et t : f (y), on a ϕ[x := t] : ∀z f (y) = z.
Attention, si on avait oublié de faire l’α-renommage, on aurait obtenu la formule ∀y f (y) = y, qui
n’exprime plus la même chose !

Définition 3.23 : clôture

• Une formule close est une formule sans variable libre.
• Soit ϕ une formule telle que FV(ϕ) = {x1 , . . . , xn }.
La clôture universelle de ϕ est la formule (close) suivante : ∀x1 . . . ∀xn ϕ.

3.3.2 Sémantique (HP)

La sémantique de la logique du premier ordre est un peu technique, et elle est donc hors programme.
Plutôt que de se contenter de quelques intuitions, nous présentons tout de même dans cette sous-partie
la sémantique formelle de cette logique.

69
 Définition 3.24 : modèle
Soit S = (C, F, R) une signature.
On appelle modèle de S l’ensemble M des données suivantes :
• EM : un ensemble non vide appelé domaine de M (ou ensemble de base de M) ;
• pour chaque symbole de constante c ∈ C, un élément cM ∈ EM ;
• pour chaque symbole de fonction f ∈ F d’arité n, une fonction fM : EM
n →E
M;
• pour chaque symbole de relation R ∈ R d’arité n, un sous-ensemble RM ⊆ EM
n .

Remarque 3.7 : symbole d’égalité

Lorsque le symbole = (2) est dans R, il arrive qu’on impose que =M corresponde à l’égalité dans
la définition précédente.

Définition 3.25 : environnement

Soit M un modèle de S.
• Un environnement est une fonction V → EM .
• Si e est un environnement, x ∈ V, et a ∈ EM , on note e[x 7→ a] l’environnement e0 tel que :
(
e0 (x) = a
e0 (y) = e(y) pour y 6= x

Citation
Ce qu’il faut comprendre, d’abord, c’est les valeurs.
– Perceval, Kaamelott livre II, Perceval et le Contre-sirop

Définition 3.26 : valeur

Soit M un modèle de S, t ∈ T (S), et e un environnement.
La valeur de t dans M et e, notée ValM,e (t), est définie par induction structurelle sur t :
• ValM,e (x) = e(x) si x ∈ V ;
• ValM,e (c) = cM si c ∈ C ;



• ValM,e f (t1 , . . . , tn ) = fM ValM,e (t1 ), . . . , ValM,e (tn ) .

Exemple 3.19
Soit S la signature de l’arithmétique :
C = {0, 1} F = {+(2), ×(2)} R = {= (2)}
On peut prendre comme modèle M :
• EM = N, en interprétant les symboles avec leur sens habituel ;
• EM = Z (ou Q, R, C, . . . ), toujours en interprétant les symboles avec leur sens habituel ;
• Mais on peut également prendre :
• EM = N ;
• 0M = 12 ;
• 1M = 12 ;
• n +M m = 3n + 5m ;
• n ×M m = 42. . .
Bien sûr, dans ce cas, le choix des symboles n’était peut être pas judicieux. . .

70
 Définition 3.27 : valeur de vérité
Soit M un modèle de S, et e un environnement.
On définit la valeur de vérité d’une formule ϕ, notée également ValM,e (ϕ), par induction
structurelle sur ϕ :
• ValM,e (⊥) = 0 ;
• ValM,e (>) = 1 ;



• ValM,e R(t1 , . . . , tn ) = 1 ssi ValM,e (t1 ), . . . , ValM,e (tn ) ∈ RM ;
• ValM,e (¬ϕ0 ) = 1 si et seulement si ValM,e (ϕ0 ) = 0 ;
• ValM,e (ϕ1 ∧ ϕ2 ) = 1 si et seulement si ValM,e (ϕ1 ) = 1 et ValM,e (ϕ2 ) = 1 ;
• ValM,e (ϕ1 ∨ ϕ2 ) = 1 si et seulement si ValM,e (ϕ1 ) = 1 ou ValM,e (ϕ2 ) = 1 ;
• ValM,e (ϕ1 → ϕ2 ) = 1 si et seulement si ValM,e (ϕ1 ) = 0 ou ValM,e (ϕ2 ) = 1 ;
• ValM,e (∀x ϕ0 ) = 1 si et seulement si pour tout a ∈ EM , ValM,e[x7→a] (ϕ0 ) = 1 ;
• ValM,e (∃x ϕ0 ) = 1 si et seulement s’il existe a ∈ EM , ValM,e[x7→a] (ϕ0 ) = 1.

Définition 3.28 : satisfiabilité

Soit M un modèle de S, e un environnement, et ϕ ∈ F O(S).
• Si ValM,e (ϕ) = 1, on dit que M satisfait ϕ dans l’environnement e, et on note M, e ⊨ ϕ.
• Si M, e ⊨ ϕ pour tout environnement e, on note M ⊨ ϕ, et on dit que M est un modèle
de ϕ.
• Si M ⊨ ϕ pour tout modèle M de S, on note ⊨ ϕ, et on dit que ϕ est un théorème (ou que
ϕ est valide).

On peut maintenant justifier l’intérêt de la clôture universelle d’une formule.

Théorème 3.7 : équisatisfiabilité (HP)

Soit S une signature, M un modèle de S, ϕ ∈ F O(S), et ϕ
e la clôture universelle de ϕ. On a :

M ⊨ ϕ si et seulement si M ⊨ ϕ
e

3.3.3 Théorie des modèles (HP)

On vient de définir un notion de modèle très large : les symboles peuvent a priori être interprétés par
n’importe quoi (cf. exemple 3.19). C’est pourquoi on se donne en pratique des axiomes, c’est à dire un
ensemble de formules qui doivent être des théorèmes dans le modèle. Cela force les symboles à ne pas
être interprétés n’importe comment. C’est ce qu’on appelle la théorie des modèles. Un ensemble de
tels axiomes est appelée une théorie. On en présente ici rapidement quelques unes.

Exemple 3.20 : théorie de l’égalité

Voici les axiomes de la théorie de l’égalité :
• ∀x x = x •∀x∀y x = y → y = x •∀x∀y∀z (x = y ∧ y = z) → x = z
• Pour chaque f ∈ F d’arité n :

∀x1 . . . ∀xn ∀y1 . . . ∀yn (x1 = y1 ∧ · · · ∧ xn = yn ) → f (x1 , . . . , xn ) = f (y1 , . . . , yn )

• Pour chaque R ∈ R d’arité n :

∀x1 . . . ∀xn ∀y1 . . . ∀yn (x1 = y1 ∧ · · · ∧ xn = yn ) → R(x1 , . . . , xn ) → R(y1 , . . . , yn )

Les axiomes de la théorie de l’égalité forcent à interpréter = (2) comme l’égalité dans EM .

71
 Exemple 3.21 : théorie des groupes
Voici les axiomes de la théorie des groupes :
• les axiomes de la théorie de l’égalité (cf. exemple 3.20) ;
• ∀x∀y∀z x ? (y ? z) = (x ? y) ? z
• ∀x e ? x = x ∧ x ? e = x
• ∀x x ? x−1 = e ∧ x−1 ? x = e
• ∀x∀y x ? y = y ? x

Exemple 3.22 : théorie de l’arithmétique élémentaire

Dans cet exemple, on travaille avec la signature suivante (où S est la fonction successeur) :

C = {0} F = {+(2), S(1), ×(2)} R = {= (2)}

Voici les axiomes de l’arithmétique élémentaire :

• les axiomes d’associativité et de commutativité pour + et pour × (cf. exemple 3.21) ;
• ∀x ¬(S(x) = 0)
• ∀x (x = 0 ∨ (∃y x = S(y)))
• ∀x∀y S(x) = S(y) → x = y
• ∀x x + 0 = x
• ∀x∀y x + S(y) = S(x + y)
• ∀x x × 0 = 0
• ∀x∀y x × S(y) = x × y + x

Il manque une dernière chose à l’arithmétique élémentaire : le principe de récurrence. Voici comment
le rajouter.
Soit S la signature de l’arithmétique élémentaire, ϕ ∈ F O(S), et x ∈ V. On note Recφ,x la clôture
universelle de la formule :
 
ϕ[x := 0] ∧ ∀y (ϕ[x := y] → ϕ[x := S(y)]) → ∀x ϕ

Et on note Rec = {Recφ,x | ϕ ∈ F O(S), x ∈ V}. C’est un ensemble infini d’axiomes, qu’on appelle un
schéma axiomatique.

Exemple 3.23 : arithmétique de Peano, arithmétique de Presburger

L’arithmétique de Peano est la théorie de l’arithmétique élémentaire à laquelle on rajoute le
schéma axiomatique Rec.
Si l’on retire le symbole de fonction × (ainsi que les axiomes faisant intervenir ×), on obtient une
autre théorie appelée arithmétique de Presburger.

3.3.4 Déduction naturelle

On revient maintenant dans le cadre du programme, pour observer une nouvelle illustration de la
modularité des systèmes de preuve : il suffit de rajouter quelques règles à la déduction naturelle vue
dans la partie 3.2.2 pour l’adapter à la logique du premier ordre.

72
 Théorème 3.8 : déduction naturelle pour la logique du premier ordre
Rajouter les règles suivantes aux règles de la déduction naturelle permet d’obtenir un système de
preuve correct et complet :

Γ`ϕ x∈ / F V (Γ) Γ ` ∀x ϕ F V (t) ∩ BV (ϕ) = ∅

(∀i ) (∀e )
Γ ` ∀x ϕ Γ ` ϕ[x := t]

Γ ` ϕ[x := t] Γ ` ∃x ϕ Γ, ϕ[x := y] ` ψ y ∈
/ F V (Γ ∪ {ϕ, ψ})
(∃i ) (∃e )
Γ ` ∃x ϕ Γ`ψ

Preuve. Admis. □

Attention : fausses prémisses

Attention, la plupart de ces règles ne sont applicables que si certaines conditions sur certaines des
variables du séquent sont vérifiées : il est alors usuel (et c’est ce qui est fait ci-dessus) d’expliciter
cette condition comme si c’était une dernière prémisse lors de la présentation de la règle.
Mais ce n’est en fait pas une prémisse (ce n’est même pas un séquent. . . ), il faut juste bien faire
attention à respecter cette contrainte lorsqu’on se sert de ces règles, sans quoi on va réussir à
prouver des choses fausses !

Voici enfin un dernier exemple de cette modularité : si l’on travaille dans la théorie de l’égalité, nous
pouvons à nouveau rajouter quelques règles pour adapter le système de preuve.

Théorème 3.9 : déduction naturelle pour la théorie de l’égalité

Si = (2) ∈ R, et si l’on veut imposer que = (2) soit interprété comme l’égalité dans tout modèle,
alors rajouter les règles suivantes permet d’obtenir un système de preuve correct et complet :

Γ ` ϕ[x := t] Γ ` t = u
(=i ) (=e )
Γ`t=t Γ ` ϕ[x := u]

Preuve. Admis. □

Remarque 3.8
On pourrait aussi travailler sans ces règles, mais avec les axiomes de l’égalité toujours présents
dans le contexte des séquents manipulés, mais cela sera beaucoup plus lourd et beaucoup plus
compliqué.

Voyons maintenant comment utiliser ces règles sur quelques exemples.

Exemple 3.24
Illustrons sur un exemple simple que renommer une variable liée ne change pas la sémantique d’une
formule :
(Ax)
∀x R(x) ` ∀x R(x)
(∀e )
∀x R(x) ` R(y)
(∀i )
∀x R(x) ` ∀y R(y)

73
 Exemple 3.25
Voici un autre exemple sur le renommage de variables, cette fois-ci avec des quantificateurs
existentiels. Essayons de prouver le séquent suivant : ∃x R(x) ` ∃y R(y).
Commençons par essayer de s’inspirer de l’exemple 3.24 :
On est bloqué !
(Ax)
∃x R(x) ` ∃x R(x) ∃x R(x), R(y) ` R(x)
(∃e )
∃x R(x) ` R(x)
(∃i )
∃x R(x) ` ∃y R(y)

L’astuce avec les règles du symbole ∃ et de les utiliser dans l’ordre inverse :

(Ax)
∃x R(x), R(y) ` R(y)
(Ax) (∃i )
∃x R(x) ` ∃x R(x) ∃x R(x), R(y) ` ∃y R(y)
(∃e )
∃x R(x) ` ∃y R(y)

3.4 Régles dérivables et règles dérivées

IL existe en fait plusieurs versions de la déduction naturelle, où certaines règles peuvent être remplacées
par des variantes ; mais toutes ces versions sont équivalentes les unes avec les autres. Par exemple, on
pourrait se passer de la règle (⊥) puisqu’elle peut être obtenue à l’aide des règles (Abs) et (Af f ).
Dans cette dernière partie, on formalise ce que cela signifie.

Définition 3.29 : règle dérivable, règle équivalente

Soit R un système de preuve.
• Une règle (r) ∈
/ R est dit dérivable dans R si elle peut être obtenue à partir des règles de R, i.e.
tout arbre de preuve terminé d’un séquent utilisant les règles de R ∪ {(r)} peut être transformé
en un autre arbre de preuve terminé (du même séquent) utilisant les règles de R.
• Soit (r) ∈ R et (r0 ) ∈
/ R. (r) et (r0 ) sont dites équivalentes si :
• (r0 ) est dérivable dans R ;
• (r) est dérivable dans (R \ {(r)}) ∪ {(r0 )}.

On illustre cette notion avec deux variantes de la règle (Abs).

Théorème 3.10 : règle du tiers exclu

La règle (Abs) est équivalente à la règle suivante (dite règle du tiers-exclu) :

(T E)
Γ ` ϕ ∨ ¬ϕ

Preuve. Considérons un arbre de preuve terminé dont une branche est fermée par la règle (T E).
Cet arbre de preuve possède donc une feuille de la forme :

(T E)
Γ ` ϕ ∨ ¬ϕ

74
On peut remplacer cette feuille par l’arbre suivant :

(Ax)
¬(ϕ ∨ ¬ϕ), ϕ ` ϕ
(Ax) (∨gi )
¬(ϕ ∨ ¬ϕ), ϕ ` ¬(ϕ ∨ ¬ϕ) ¬(ϕ ∨ ¬ϕ), ϕ ` ϕ ∨ ¬ϕ
(¬e )
¬(ϕ ∨ ¬ϕ), ϕ ` ⊥
(¬i )
¬(ϕ ∨ ¬ϕ) ` ¬ϕ
(Ax) (∨di )
¬(ϕ ∨ ¬ϕ) ` ¬(ϕ ∨ ¬ϕ) ¬(ϕ ∨ ¬ϕ) ` ϕ ∨ ¬ϕ
(¬e )
¬(ϕ ∨ ¬ϕ) ` ⊥
(Abs)
` ϕ ∨ ¬ϕ
(Af f )
Γ ` ϕ ∨ ¬ϕ

Ainsi, en réitérant ce processus pour toutes les feuilles fermées par (T E), on peut obtenir un arbre
de preuve terminé n’utilisant pas cette règle : la règle (T E) est dérivable dans la déduction naturelle.
Réciproquement, considérons un arbre de preuve terminé utilisant la règle (Abs). Cet arbre de
preuve possède donc un nœud interne étiqueté par (Abs), dont le sous-arbre de preuve est de la
forme suivante (où Π est le reste de la preuve) :

Π
..
..
Γ, ¬ϕ ` ⊥
(Abs)
Γ`ϕ

On peut remplacer le sous-arbre de preuve enraciné en ce nœud par l’arbre de preuve suivant (qui
n’utilise pas (Abs) mais (T E)) :

Π
..
..
Γ, ¬ϕ ` ⊥
(T E) (Ax) (⊥)
Γ ` ϕ ∨ ¬ϕ Γ, ϕ ` ϕ Γ, ¬ϕ ` ϕ
(∨e )
Γ`ϕ

Ainsi, en réitérant ce processus pour tous les autres nœuds de Π et du reste de l’arbre étiquetés
par (Abs), on obtient un arbre de preuve terminé n’utilisant pas (Abs) mais utilisant (T E).
Finalement, (Abs) et (T E) sont bien équivalentes. □

Théorème 3.11 : règle de la double négation

La règle (Abs) est équivalente à la règle suivante (dite règle de la double négation) :

Γ ` ¬¬ϕ
(¬¬e )
Γ`ϕ

Preuve. Considérons un arbre de preuve terminé utilisant la règle (¬¬e ). Cet arbre de preuve
possède donc un nœud interne étiqueté par (¬¬e ), dont le sous-arbre de preuve est de la forme
suivante (où Π est le reste de la preuve) :

Π..
..
Γ ` ¬¬ϕ
(¬¬e )
Γ`ϕ

On peut remplacer le sous-arbre de preuve enraciné en ce nœud par l’arbre de preuve suivant (qui

75
 n’utilise pas (¬¬e ) mais (Abs)) :

Π..
..
Γ ` ¬¬ϕ
(Af f ) (Ax)
Γ, ¬ϕ ` ¬¬ϕ Γ, ¬ϕ ` ¬ϕ
(¬e )
Γ, ¬ϕ ` ⊥
(Abs)
Γ`ϕ

Ainsi, en réitérant ce processus pour tous les autres nœuds de Π et du reste de l’arbre étiquetés
par (¬¬e ), on obtient un arbre de preuve terminé n’utilisant pas (¬¬e ) mais utilisant (Abs).
La règle (¬¬e ) est dont dérivable dans la déduction naturelle.
Réciproquement, considérons un arbre de preuve terminé utilisant la règle (Abs). Cet arbre de
preuve possède donc un nœud interne étiqueté par (Abs), dont le sous-arbre de preuve est de la
forme suivante (où Π est le reste de la preuve) :

Π
..
..
Γ, ¬ϕ ` ⊥
(Abs)
Γ`ϕ

On peut remplacer le sous-arbre de preuve enraciné en ce nœud par l’arbre de preuve suivant (qui
n’utilise pas (Abs) mais (¬¬e )) :
Π
...
.
Γ, ¬ϕ ` ⊥
(¬i )
Γ ` ¬¬ϕ
(¬¬e )
Γ`ϕ
Ainsi, en réitérant ce processus pour tous les autres nœuds de Π et du reste de l’arbre étiquetés
par (Abs), on obtient un arbre de preuve terminé n’utilisant pas (Abs) mais utilisant (¬¬e ).
Finalement, (Abs) et (¬¬e ) sont bien équivalentes. □

Cette dernière partie nous montre donc bien qu’on aurait pu faire des choix de règles différents dans
la définition 3.15. Aux concours, rien ne garantie que ce seront précisément ces règles qui vous seront
introduites : il y aura peut être des variantes. Il faudra alors faire preuve d’adaptation, et prouver que
certaines règles alternatives sont dérivables dans notre système est un bon moyen de s’y préparer.

76