Institut Galilée Département d’informatique

2002 MM

TRAVAUX DIRIGÉS DE LOGIQUE

Ceci est un recueil d’exercices de base, utilisés en TD, de problèmes qui peuvent aussi servir à rédiger
des énoncés de devoirs, et de notes d’ordre pédagogique, dépourvues de prétention didactique et
d’originalité; par contre et en revanche, il manque d’exemples : il faut les produire face à son public,
en n’oubliant jamais que les plus simples passent généralement pour simplistes et les autres pour
incompréhensibles!

PETIT MANUEL DE LOGIQUE NAÏVE À L’USAGE DES FAMILLES.

Un étudiant arrivant en troisième année d’université n’est pas sans avoir déjà eu l’occasion de raison-
ner plusieurs fois, avec plus ou moins de bonheur; mais, le paradoxe le plus apparent de l’étude de
la logique est que l’on y est toujours en train de raisonner. Ceci suppose que l’on ait déjà une logique
présente à l’esprit, procédant du simple bon sens, légèrement instrumentalisé.
La logique naı̈ve dont il est question ici, et dont l’usage est recommandé en toute circonstance,
est justement une tentative d’instrumentalisation de ce bon sens si bien partagé ... où l’on pourra
reconnaı̂tre une présentation informelle d’un système de déduction fort bien qualifiée, par Gentzen
soi–même, de naturelle.

Les mots sont d’abord pris dans leur sens commun, mais l’usage répété et systématique de certains
d’entre eux ne manquera pas de préciser ce sens de façon utile pour la suite.
• La logique naı̈ve s’applique à démontrer des énoncés par le moyen de déductions, qui préservent
la vérité : un énoncé déduit à partir d’énoncés vrais, est lui–même vrai. On choisit donc tout d’abord
une collection d’énoncés de base A, B , ... (dont la nature dépend du domaine considéré) à partir
desquels on construira d’autres énoncés, par des opérations grammaticales. En dehors des énoncés
démontrés à la faveur de précédents exercices (qui sont des acquis définitifs) et des ressources propres
au domaine auquel on s’intéresse (qui sont des énoncés vrais dans le domaine en question), les
ressources disponibles à un moment donné d’une déduction sont des énoncés de deux ordres :
– des hypothèses posées temporairement;
– les énoncés que l’on en a déduit.
Une ressource peut être utilisée autant de fois que l’on veut, voire pas du tout.
Une déduction n’est une démonstration que lorsqu’elle ne dispose d’aucune hypothèse temporaire.
• Les déductions élémentaires qui sont proposées ici (sous une forme schématique pour des raisons
de commodité), montrent comment on peut utiliser des ressources disponibles, figurées au dessus
de la barre, pour en déduire une nouvelle, figurée dessous. Pris isolément, chacun des schémas en
question (sauf peut–être ceux d’entre eux qui disposent de ressources occultes) sera d’abord regardé
comme l’expression d’une trivialité; mais c’est leur ensemble, et l’usage cumulatif qu’on en fait, qui a
de l’intérêt et n’est pas toujours facile à maı̂triser : on passe encore du simpliste à l’incompréhensible,
comme d’habitude ...

2002
Voici la liste des opérations grammaticales qui permettent de construire de nouveaux énoncés à partir
d’énoncés déjà connus et des commentaires sur les schémas de déduction qui leur sont attachés.

Il ne faut évidemment pas utiliser les schémas sous cette forme dans une démonstration, mais les
rédiger, en un français (plus ou moins) digeste, et ce n’est pas la moindre affaire.

Schémas ”propositionnels” naı̈fs

L′ absurde
A
A et B
A B A
A et B A et B
B
A [[A]] [[B]]
A ou B .. ..
. .
B A ou B C C
A ou B C

[[A]]
..
.
B A A⇒B
A⇒B B

• L′ absurde est un énoncé qui se présente dans tous les domaines! et qui est faux, absolument. Le
schéma qui lui est directement attaché signifie que l’on peut en déduire n’importe quel énoncé.
• Lorsque A et B sont des énoncés, leur conjonction A et B est un énoncé. Les trois schémas qui
sont directement attachés à la conjonction sont sans surprise.
• Lorsque A et B sont des énoncés, leur disjonction A ou B est un énoncé : cette disjonction ne
doit pas être comprise dans un sens exclusif mais comme le barbarisme post–moderne et/ou souvent
utilisé de nos jours. L’un des trois schémas qui lui sont attachés demande des explications :

[[A]] [[B]] il décrit le raisonnement par disjonction des cas : il permet, de déduire un
.. .. énoncé C d’une ressource de la forme A ou B . Il peut se rédiger en deux
. . temps, et se comprendre de la façon suivante :
A ou B C C — Si A (adjonction temporaire de l’hypothèse A), . . . et il faut déduire C :
C ce travail accompli, l’hypothèse A est éliminée des ressources, ainsi que les
énoncés dont la déduction dépend de cette hypothèse;
— Si B (adjonction temporaire de l’hypothèse B ), . . . et il faut déduire C : ce travail accompli,
l’hypothèse B est éliminée des ressources, ainsi que les énoncés dont la déduction dépend de cette
hypothèse.

Ceci fait, on n’utilise que la ressource A ou B pour déduire C .

• Lorsque A et B sont des énoncés, l’implication A ⇒ B est un énoncé : l’usage d’un verbe,
dans l’expression A implique B (au lieu d’une conjonction de coordination comme dans les cas
précédents) est certainement à l’origine de nombreux malentendus. Le schéma de droite, tradition-
nellement appelé modus ponens, est la figure la plus célèbre du monde du raisonnement. L’autre
schéma mérite quelques explications :

Institut Galilée 2 MM
 [[A]] il est essentiel au point qu’on l’appelle généralement la déduction, ce qui n’est pas peu
.. dire. Il peut se rédiger de la façon suivante :
. — Supposons A (adjonction temporaire de l’hypothèse A),. . . il faut alors déduire B .
B Lorsque ce travail est accompli, l’hypothèse A est éliminée des ressources, ainsi que les
A⇒B énoncés dont la déduction dépend de cette hypothèse; et l’on a bien déduit l’énoncé
A ⇒ B sans usage propre d’une ressource.
Ce raisonnement qui paraı̂t naturel à ceux qui l’ont assimilé, peut produire des résultats fort gracieux,
lorsqu’il tombe de mains moins habiles!
• Lorsque A est un énoncé, sa négation non A désigne l’énoncé A ⇒ L′ absurde.
De A et non A on peut évidemment déduire L′ absurde, par application du modus ponens.

A ou non A Le principe du tiers exclu, selon lequel cet énoncé est vrai, quel que soit l’énoncé
A, est nécessaire pour donner son caractère ”classique” à la logique. Même
lorsque ce principe est vérifié par les énoncés de bases, il n’est pas possible de l’étendre à tous
les autres, par application des schémas. Montrons comment le tiers exclu permet de justifier deux
schémas d’usage courant :

[[non A]] Le raisonnement par l’absurde, dont le schéma est présenté ici, est une consé-
.. quence du principe du tiers exclu. En effet, si l’on sait déduire L′ absurde sous
. l’hypothèse non A alors, on peut faire le raisonnement par cas suivant :
L′ absurde — Si A alors A !
A — Si non A alors on sait déduire L′ absurde, d’où l’on peut déduire n’importe
quel énoncé, en particulier A.

ATTENTION. Si après avoir temporairement posé l’hypothèse A on est capable de déduire L′ absurde,
on pourra en conclure A ⇒ L′ absurde, c’est–à–dire non A : ceci tient à la définition de la négation,
mais n’a rien à voir avec un quelconque raisonnement par l’absurde!

[[non A]] Enfin voici le schéma d’un raisonnement qui peut être utile pour démontrer un énoncé
.. de la forme A ou B , qui est encore une conséquence du principe du tiers exclu. En
. effet, si l’on sait déduire B sous l’hypothèse non A on peut faire le raisonnement par
B cas suivant :
A ou B — Si A alors on a aussi A ou B ;
— Si non A alors on sait déduire B , donc aussi A ou B .

MM 3 Institut Galilée
Les énoncés que l’on est couramment conduit à manipuler sont des prédicats, disons, des phrases, qui
expriment des relations entre des individus (dont la nature dépend du domaine considéré).
On utilise des variables x, y , ... pour désigner des individus de façon générique (par exemple, dans
l’expression ”soit x un entier ... ”); mais il peut aussi intervenir des individus particuliers (par exemple,
l’entier 1) ou bien calculés à partir d’autres (par exemple, les entiers de la forme (x + 1) × x). Nous
utiliserons des lettres comme t, u, ... pour désigner des individus de l’une quelconque des sortes
précédentes.
Pour insister sur le fait qu’un énoncé A dépend éventuellement de la variable x, nous utiliserons la
notation A[x] et, si t est l’expression d’un individu, A[t] s’obtiendra en remplaçant x par t partout où
il se trouve dans A.
Une quantification est une opération qui fait disparaı̂tre une variable : si Qx est un quantificateur sur
x, QxA[x] est un énoncé qui ne dépend plus de x. On dit de façon imagée que toute apparition de x
qui est à la portée d’un quantificateur Qx est muette ou liée.
ATTENTION. A proprement parler, on ne peut pas prétendre qu’un énoncé qui dépend de variables
soit vrai! Si nous insinuons tout de même que A[x] est vrai, c’est pour dire qu’on obtient toujours un
énoncé vrai lorsque l’on remplace x par un individu particulier.

Voici les quantifications et les schémas qui s’y rapportent.

• Lorsque A[x] est un énoncé dépendant éventuellement de la variable x alors ∀xA[x] est un énoncé
ne dépendant plus de la variable x et qui se lit, se comprend et même peut s’écrire ou bien pour tout x
A[x] ou bien A[x] quel que soit x.

A[x] Ce schéma de généralisation ne peut s’appliquer que lorsqu’aucune des hypothèses

∀xA[x] actuellement disponibles ne dépend de x, car il faut évidemment que x soit quelconque
pour que la déduction soit correcte! En vue de l’application de ce schéma on sera
conduit à écrire quelque chose comme :
— soit x quelconque . . .

∀xA[x] Ce schéma de spécialisation exprime qu’un énoncé vrai pour tout individu x l’est aussi
A[t] pour l’individu particulier désigné par t.
On se souviendra cependant que l’expression t ne doit pas dépendre d’une variable qui
deviendrait muette dans l’énoncé A[t].
• Lorsque A[x] est un énoncé dépendant éventuellement de la variable x alors ∃xA[x] est un énoncé
ne dépendant plus de la variable x et qui se lit, se comprend et même peut s’écrire il existe x tel que
A[x].

A[t] La signification de ce schéma est claire : connaissant un individu particulier t qui permet
∃xA[x] d’affirmer l’énoncé A[t], on est bien en droit d’en déduire ∃xA[x] !
On se souviendra cependant que l’expression t ne doit pas dépendre d’une variable qui
deviendrait muette dans l’énoncé A[t].

[[A[x]]] Ce schéma peut se rédiger de la façon suivante :

.. — Si x est tel que A[x] (adjonction temporaire de l’hypothèse A[x]),. . . il faut
. alors déduire B .
∃xA[x] B Lorsque ce travail est accompli, l’hypothèse A[x] est éliminée des ressources,
B ainsi que les énoncés dont la déduction dépend de cette hypothèse; et l’on a
bien déduit l’énoncé B de la seule ressource ∃xA[x]. L’individu désigné par
x est caractérisé par le fait qu’il vérifie l’hypothèse A[x], il ne pouvait pas apparaı̂tre avant cette
hypothèse, ni ne peut survivre à sa disparition : aucune des hypothèses qui sont encore disponibles
maintenant, ni B elle–même, ne peuvent donc dépendre de la variable x.

Institut Galilée 4 MM
REMARQUE. La restriction sur l’usage des expressions t dans deux des schémas ne peut se justifier ici
que par le fameux bon sens dont il a été question au début, mais on peut voir facilement qu’elle est
nécessaire, en observant un contre–exemple.
Considérons l’énoncé A[x] qui s’écrit ∀y(y = x), par exemple dans le domaine des entiers, t
l’expression x + y , alors A[t] est égal à ∀y(y = x + y). Si l’on ne tient pas compte du fait que t ne vérifie
pas la restriction relativement à A[x], on peut ”démontrer” l’énoncé ∃x∀y(y = x+y) ⇒ ∃x∀y(y = x)
de la manière suivante :
supposons ∃x∀y(y = x + y), si x est tel que ∀y(y = x + y) on peut en ”déduire” ∃x∀y(y = x), ce qui
permet de conclure.
Or, cette implication est fausse car on a bien m = 0 + m pour tout entier m mais, il n’existe pas d’entier
n tel que m = n pour tout m car, il y a plusieurs entiers!

Exercice 0. Rédaction de démonstrations.

L’équivalence A ⇔ B désigne l’énoncé (A ⇒ B) et (B ⇒ A) qui signifie que A et B sont synonymes.
La démonstration d’une équivalence nécessite la démonstration de deux implications.
Rédiger des démonstrations d’implications et d’équivalences bien connues, par exemple celles qui
relient certaines opérations par le truchement de la négation.
Dans cet exercice, on évitera tout usage involontaire du principe du tiers exclu, et tout raisonnement
abusif par l’absurde : d’une façon générale, on signale explicitement que l’on s’apprête à faire un
raisonnement par l’absurde, car il n’est pas si naı̈f que ça, comme disait le grand lapin blanc.

L’INDUCTION.
On est souvent conduit, et spécialement en logique, à considérer des expressions appelées termes ou
formules, qui sont construites à partir de symboles dépendant du domaine considéré.
Chacun de ces symboles admet une arité, c’est–à–dire un entier naturel qui indique le nombre
d’arguments auxquels il s’applique :
– les symboles d’arité 0 désignent des individus, par exemple : les variables et les constantes de
toute nature;
– les autres, des relations ou des fonctions, et sont appelés opérateurs, par exemple : les opéra-
teurs arithmétiques et logiques, ...
Les expressions définies par un tel système, sont construites en appliquant un symbole à des expres-
sions déjà construites (le nombre de ces expressions doit être égal à l’arité du symbole).
Cette phrase bonne enfant cache trop bien la difficulté du sujet : la définition d’une classe d’objets
par induction (ou même par récurrence) et la récursivité, au sens informatique du terme, et le
type de raisonnements qui leur est attaché. L’expérience montre que nos étudiants en informatique,
sont généralement réfractaires à un tel feu, et qu’ils lui préfèrent les points de suspension (signe de
ponctuation qui tend à s’énoncer ”trois petits points”, ce qui est déjà très révélateur d’une déperdition
de sens!); or, il n’existe pas de langage de programmation comprenant lesdits points dans leur syntaxe
de façon active, sauf à les définir ... par exemple, dans le cas simple d’une liste (x1 , . . . , xn ), par la
récurrence suivante, sur l’entier naturel n :
– (x1 , . . . , x0 ) = (), c’est–à–dire, la liste vide, base de la construction de toute liste;
– (x1 , . . . , xn+1 ) = ((x1 , . . . , xn ), xn+1 ) obtenue par adjonction de xn+1 à la fin de la liste
(x1 , . . . , xn ).

MM 5 Institut Galilée
Sauf dans les cas simples et statiques, il est préférable d’utiliser des définitions inductives et de faire
des raisonnements par induction, quitte à paraı̂tre pesant. Il y a peu de questions en logique de base
que l’on puisse sérieusement traiter autrement, surtout dans le cadre d’une licence d’informatique (on
pourrait admettre plus facilement un certain laxisme devant un public mathématicien!).

Le cadre d’une induction est le suivant :

Soit E un ensemble muni d’une relation d’ordre strict bien fondé, c’est–à–dire, sans suite décroissante
infinie (des algébristes évoqueraient Emil Artin ou Amalie Nœther), que l’on notera ≺.

Voici des exemples :

1) La relation < sur l’ensemble N des entiers naturels, est un ordre strict bien fondé;
2) Toute application h : E → N permet de définir la relation suivante sur E : b ≺ a ssi
h(b) < h(a), qui est un ordre strict bien fondé;
3) L’ensemble T des termes construits avec un ensemble P des symboles d’arité 0 et, pour fixer les
idées, un symbole u d’arité 1 et un symbole d d’arité 2. Alors la relation ≺ définie par transitivité
à partir de :
– t ≺ u t, quel que soit t ∈ T ;
– t1 ≺ d t1 t2 et t2 ≺ d t1 t2 , quels que soient t1 ∈ T et t2 ∈ T ;
est un ordre strict bien fondé sur T ;
4) La relation ”B est un sous–arbre strict de A” est un ordre strict bien fondé sur tout ensemble
d’arbres finis, qui contient tous les sous–arbres de ses éléments.

Le Principe d’induction.
Soit E un ensemble muni d’une relation d’ordre strict bien fondé ≺ et soit P (x) l’énoncé d’une
propriété des éléments de E , alors :
Lorsque pour tout x ∈ E , on peut déduire P (x) de l’hypothèse d’induction
(HI) : pour tout y ∈ E , y ≺ x implique P (y),
on peut en conclure P (x) quel que soit x ∈ E .

On rédige généralement de la façon suivante :

Soit x ∈ E et supposons que l’on ait P (y) pour tout y ≺ x, ... et il faut déduire P (x).
Poser une hypothèse d’induction n’est pas exprimer sa croyance en un miracle, ou espérer un don du
ciel! mais, en termes informatiques, faire des appels récursifs, sur des objets strictement plus petits
que celui auquel on s’intéresse actuellement; ces appels ne manqueront certainement pas d’en faire à
leur tour, jusqu’à ce que ce jeu se termine, puisque l’ordre est bien fondé.
Lorsque x est minimal pour ≺, l’hypothèse d’induction ne dit rien et il faut bien se résoudre à
démontrer P (x) dans ce cas!

*
* *

Dans ce qui suit, des rappels seront faits de temps en temps, mais l’essentiel devra être puisé dans le
cours lui–même!

Institut Galilée 6 MM
CALCUL DES PROPOSITIONS.

Considérons un ensemble E muni des opérations définies par les applications :

neg : E→E
conj : E×E →E
disj : E×E →E
impl : E×E →E
La propriété de lecture unique s’applique de la façon suivante :

Pour toute application f : P → E on peut construire une et une seule application f : F → E vérifiant
les cinq conditions suivantes :

f (p) = f (p)
pour toute variable propositionnelle p, et

f (¬A) = neg(f (A))

f ((A ∧ B)) = conj(f (A), f (B))
f (((A ∨ B)) = disj(f (A), f (B))
f ((A → B)) = impl(f(A), f (B))
pour toute formule A et toute formule B .

Ceci est une construction par induction sur les formules et l’application f ainsi construite s’appelle
l’extension de f aux formules (relativement aux applications neg , conj , disj et impl en cause).
L’existence et l’unicité d’une telle extension s’exprime souvent en disant que F est un objet libre dans
sa catégorie.

En termes informatiques, cette construction correspond exactement à la fonction récursive qui

s’écrit :

fonction f souligne(X : formule) : E ;

p : variable propositionnelle ;
A, B : formule ;
selon la valeur de X faire
p : retourne f(p) ;
¬ A : retourne neg(f souligne(A)) ;
(A ∧ B) : retourne conj(f souligne(A), f souligne(B)) ;
(A ∨ B) : retourne disj(f souligne(A), f souligne(B)) ;
(A → B) : retourne impl(f souligne(A), f souligne(B)) ;
fin
fin
La propriété de lecture unique assure que, pour chaque formule, un et un seul des cinq cas peut se
présenter, et fournit un algorithme permettant, dans les quatre derniers, d’extraire les sous–formules
nécessaires aux appels récursifs.

Exercice 1. Variables propositionnelles apparaissant dans une formule.

Donner une définition, par induction sur les formules, de l’ensemble V (A) des variables proposition-
nelles qui apparaissent dans une formule A.
Il est clair, avec les notations ci–dessus, que f (A) ne dépend que des valeurs que prend f sur les
éléments de V (A).

MM 7 Institut Galilée
Exercice 2. Des formules et des arbres.

∗ Lorsque n 6= 0, où est–il naturel de poser un opérateur n–aire pour montrer qu’il
s’applique à ses arguments et pas à d’autres?
∗ A1 . . . An ∗ Pour n = 2, qui est un cas très courant, la place la plus courante de l’opérateur se
∗ trouve entre ses arguments; mais l’écriture A1 ∗ A2 est bien connue pour entraı̂ner
des ambiguı̈tés! et c’est la raison pour laquelle il est nécessaire de faire usage de
parenthèses lorsque l’on utilise cette notation en infixe.
Dans le cas général, cette position centrale n’existe plus mais quatre positions se présentent, qui sont
toutes excellentes : chacune d’elles, lorsqu’elle est systématiquement utilisée (c’est–à–dire pour tous
les symboles), conduit à une écriture des termes qui n’est pas ambiguë.

– Poser l’opérateur au dessus (resp. en dessous) de ses arguments donne la représentation ar-
borescente avec racine en haut (resp. en bas). Dans ces cas, le dessin de liens entre l’opérateur
et ses arguments, n’est pas indispensable mais facilite grandement la lecture.
a) Donner une construction, par induction sur les formules, de l’arbre (avec, par exemple, la racine
en haut) a(X) associé à une formule X .
b) Après avoir caractérisé les arbres obtenus par la construction précédente, donner une définition,
par induction sur les arbres, de la formule f (A) associée à un arbre A convenable.

– Poser l’opérateur devant (resp. derrière) ses arguments donne l’écriture polonaise préfixe (resp.
suffixe) : les qualités de l’écriture polonaise sont l’objet d’exercices classiques mais difficiles;
c) Donner une définition, par induction sur les formules, de la formule polonaise (par exemple
préfixe) p(X) associé à une formule X .
La caractérisation des formules polonaises est un peu délicate et ne sera pas tentée ici!

Exercice 3.
a) Donner une définition, par induction sur les formules, des applications à valeurs entières suiv-
antes :

l(X) = la longueur de la formule X (compter tous les caractères, parenthèses comprises);

n(X) = le nombre d’occurrences de symboles de négation intervenant dans la formule X ;
b(X) = le nombre d’occurrences de symboles binaires intervenant dans la formule X .
b) En déduire, en raisonnant par induction, que l’on a l(X) = 4b(X) + n(X) + 1 pour toute formule
X.

Autres symboles d’usage courant

• Dans certaines circonstances, il est judicieux d’adopter deux nouveaux symboles logiques primi-
tifs d’arité 0 : ⊤ (le vrai) et ⊥ (le faux). Ce sont des formules (non–atomiques!) qui interviennent dans
la construction générale des formules et pour lesquelles il faut ajouter les clauses δ(⊤) = 1 et δ(⊥) = 0
à la définition de l’extension d’une distribution de valeurs de vérité δ .
Il est aussi possible, mais c’est moins intéressant, de les définir par ⊤ = (p0 ∨ ¬p0 ) et ⊥ = (p0 ∧ ¬p0 ),
où p0 est une variable propositionnelle fixée.
• L’équivalence est le symbole abréviateur ↔ défini par (A ↔ B) = ((A → B) ∧ (B → A)).
L’équivalence, dont l’utilité est indéniable, est trop “composée” pour prétendre à un statut d’opérateur
logique primitif.

Institut Galilée 8 MM
Exercice 4. Tautologies.
Si l’on utilise les applications
neg : {0, 1} → {0, 1} définie par neg(x) = (1 − x)
conj : {0, 1} × {0, 1} → {0, 1} définie par conj(x, y) = xy
disj : {0, 1} × {0, 1} → {0, 1} définie par disj(x, y) = x(1 − y) + y = x + (1 − x)y
impl : {0, 1} × {0, 1} → {0, 1} définie par impl(x, y) = (1 − x) + xy
alors l’extension aux formules de toute distribution de valeurs de vérité δ : P → {0, 1} est celle qui a
été définie dans le cours.
On rappelle qu’une formule A est une tautologie lorsqu’elle est satisfaite par toute distribution de
valeurs de vérité, c’est–à–dire lorsque δ(A) = 1 pour toute δ .
a) Montrer, par un calcul direct utilisant la définition de δ à partir de δ , que les formules choisies
sont des tautologies. Il pourra être utile d’observer que la propriété x ∈ {0, 1} est équivalente à
x(1 − x) = 0, c’est–à–dire à x2 = x.
b) Montrer que les équivalences suivantes sont vraies, quelles que soient les formules A et B et la
distribution de valeurs de vérité δ :
δ((A → B)) = 1 ssi δ(A) ≤ δ(B)
δ((A ↔ B)) = 1 ssi δ(A) = δ(B)
La dernière propriété peut servir à revisiter les formules choisies qui sont des équivalences!
On dit souvent que deux formules A et B sont équivalentes lorsque (A ↔ B) est une tautologie,
c’est–à–dire lorsque δ(A) = δ(B) pour toute δ .
c) Montrer que la définition de δ est en accord avec la logique naı̈ve, c’est–à–dire que les équivalences
suivantes sont vraies, quelles que soient les formules A et B et la distribution de valeurs de vérité δ :
δ(¬A) = 1 ssi non δ(A) = 1 (ce qui peut aussi s’écrire δ(A) = 0 !)
δ((A ∧ B)) = 1 ssi δ(A) = 1 et δ(B) = 1
δ((A ∨ B)) = 1 ssi δ(A) = 1 ou δ(B) = 1
δ((A → B)) = 1 ssi δ(A) = 1 ⇒ δ(B) = 1
Utiliser cette ”traduction” pour montrer que les formules choisies sont des tautologies.
Exercice 5. Substitutions.
L’ensemble F des formules est naturellement muni des opérations :
neg : F → F définie par neg(A) = ¬A
conj : F × F → F définie par conj(A, B) = (A ∧ B)
disj : F × F → F définie par disj(A, B) = (A ∨ B)
impl : F × F → F définie par impl(A, B) = (A → B)
Soit maintenant s : P → F une application et désignons par s son extension aux formules.
a) Vérifier que pour toute formule A, la formule s(A) est obtenue en substituant s(p) à chaque
variable propositionnelle p apparaissant dans A : pour cette raison, on dit souvent qu’une application
du type de s est une substitution.
b) Soit δ une distribution de valeurs de vérité et considérons la nouvelle distribution de valeurs de
vérité δ ′ définie par δ ′ (p) = δ(s(p)).
Montrer, par induction sur les formules, que l’on a δ ′ (A) = δ(s(A)) pour toute formule A (pour
comprendre ce qui se passe, il pourra être intéressant de considérer la représentation arborescente
des formules).
En déduire qu’une substitution transforme une tautologie en une tautologie.

MM 9 Institut Galilée
 Formules choisies
1. (A → A)

2. (A → (A ∧ A)) 5. ((A ∧ ⊤) ↔ A)
3. ((A ∧ B) → A) 6. ((A ∧ (B ∧ C)) ↔ ((A ∧ B) ∧ C))
4. ((A ∧ ⊥) ↔ ⊥) 7. ((A ∧ B) ↔ (B ∧ A))

8. ((A ∨ A) → A) 11. ((A ∨ (B ∨ C)) ↔ ((A ∨ B) ∨ C))

9. (A → (A ∨ B)) 12. ((A ∨ B) ↔ (B ∨ A))
10. ((A ∨ ⊤) ↔ ⊤) 13. ((A ∨ ⊥) ↔ A)

14. (¬¬A ↔ A)

15. (¬(A ∧ B) ↔ (¬A ∨ ¬B)) 18. (¬A ↔ (A → ⊥))

16. (¬(A ∨ B) ↔ (¬A ∧ ¬B)) 19. (A ∨ ¬A)
17. (¬(A → B) ↔ (A ∧ ¬B)) 20. ¬(A ∧ ¬A)

21. ((A → B) ↔ (¬A ∨ B))

22. ((A → B) ↔ (¬B → ¬A))
23. ((A → (B → C)) ↔ ((A ∧ B) → C)

24. ((A ∧ (B ∨ C)) ↔ ((A ∧ B) ∨ (A ∧ C)))

25. ((A ∨ (B ∧ C)) ↔ ((A ∨ B) ∧ (A ∨ C)))
26. ((A → (B ∧ C)) ↔ ((A → B) ∧ (A → C)))
27. ((A → (B ∨ C)) ↔ ((A → B) ∨ (A → C)))
28. ((A → (B → C)) ↔ ((A → B) → (A → C)))

29. (((A ∧ B) → C) ↔ ((A → C) ∨ (B → C)))

30. (((A ∨ B) → C) ↔ ((A → C) ∧ (B → C)))

REMARQUE. Si A est une formule et p une variable propositionnelle, on dira souvent ”Soit A[p] une
formule dans laquelle p apparaı̂t éventuellement”. Cette expression ne dit rien sur A ! mais insiste sur
l’intérêt que l’on porte à p et introduit une notation suggestive : si X est une formule, on peut en effet
considérer la substitution définie par

X si q = p,
s(q) =
q sinon.

On note alors A[X] au lieu de s(A). Il est évidemment possible d’adapter cette notation au cas d’une
suite finie de variables.
Problème 6. Fonctions booléennes et formes normales disjonctives
Une fontion booléenne d’arité n est une application f : {0, 1}n → {0, 1} : une telle fonction
s’applique donc aux suites (x1 , . . . , xn ) formées de n valeurs 0 ou 1 et pour chacune de ces suites,
f (x1 , . . . , xn ) prend la valeur 0 ou la valeur 1.
Le but de cet exercice est de montrer qu’une fonction booléenne est la ”table de vérité” d’une formule :
comme conséquence on obtiendra le calcul simple d’une forme normale disjonctive d’une formule
dont on connaı̂t la table de vérité.
a) Commençons par un peu d’algèbre (booléenne, comme il se doit).
Une fonction booléenne f étant donnée, il y a deux cas à considérer :

Institut Galilée 10 MM
 • si l’arité de f est 0, on a ou bien f () = 0 ou bien f () = 1 ;
• sinon, pour f : {0, 1}n+1 → {0, 1}, on définit les deux fonctions booléennes f0 et f1 : {0, 1}n →
{0, 1} par :
f0 (x1 , . . . , xn ) = f (x1 , . . . , xn , 0)
f1 (x1 , . . . , xn ) = f (x1 , . . . , xn , 1)
Vérifier que l’on a
f (x1 , . . . , xn , xn+1 ) = f0 (x1 , . . . , xn ) xn+1 + f1 (x1 , . . . , xn ) xn+1
(où, pour tout x ∈ {0, 1}, x désigne l’expression (1 − x), que l’on a vraiment intérêt à laisser telle
quelle) pour toute suite (x1 , . . . , xn , xn+1 ) ∈ {0, 1}n+1.
Appelons monôme booléen un produit y1 . . . yn dans
lequel chaque i, yi est ou bien xi ou bien xi (un tel
produit vaut 1 lorsque n = 0). x1 x2 x3 f (x1 , x2 , x3 )
Montrer que toute fonction booléenne est égale à une 0 0 0 1
somme de monômes booléens (éventuellement 0) : on
pourra commencer par étudier la fonction dont la table
1 0 0 0
est dressée ci–contre. 0 1 0 0
b) Maintenant, on associe une formule f˜ du calcul 1 1 0 1
des propositions à chaque fonction booléenne f , par
0 0 1 1
récurrence sur l’arité de f , de la façon suivante :
• si cette arité est 0 alors, on pose 1 0 1 0
f˜ = ⊥ lorsque f () = 0 et f˜ = ⊤ lorsque f () = 1 ; 0 1 1 0
n+1
• sinon, pour f : {0, 1} → {0, 1} on pose 1 1 1 0
f˜ = ((f˜0 ∧ ¬pn+1 ) ∨ (f˜1 ∧ pn+1 )).
(On a évidemment adopté ⊤ et ⊥ comme symboles primitifs.) Montrer que pour toute distribution de
valeurs de vérité δ et toute fonction booléenne f d’arité n, on a δ(f˜) = f (δ(p1 ), . . . , δ(pn )).

c) Soit A une formule dont on connaı̂t la table de vérité. Appliquer ce qui précède pour calculer une
forme normale disjonctive équivalente à A.
Rappels :
• Un littéral est une formule p ou ¬p où p est une variable propositionnelle.
• Une conjonction de littéraux est une conjonction l1 ∧. . .∧ln (où on néglige d’écrire les parenthèses)
où chaque li est un littéral (cette conjonction vaut ⊤ lorsque n = 0).
• Une forme normale disjonctive est une disjonction c1 ∨ . . . ∨ cn (où on néglige d’écrire les
parenthèses) où chaque ci est une conjonction de littéraux (cette disjonction vaut ⊥ lorsque n = 0).

Problème 7. Lemme d’interpolation.

Soient p et q deux variables propositionnelles.

a) Soit A[p] une formule dans laquelle p apparaı̂t éventuellement et considérons les deux formules
A0 = A[¬q] et A1 = A[q] obtenues par des substitutions.
Montrer que (A[p] → (A0 ∨ A1 )) est une tautologie.

b) Soit de plus B une formule dans laquelle p n’apparaı̂t pas et telle que (A[p] → B) soit une
tautologie.
Montrer que ((A0 ∨ A1 ) → B) est une tautologie.
Indication. Si δ est une distribution de valeurs de vérité qui satisfait, par exemple, A1 , considérer la
distribution de valeurs de vérité δ ′ qui coı̈ncide avec δ sauf éventuellement en p, où l’on a δ ′ (p) = δ(q).

MM 11 Institut Galilée
c) Pour énoncer le lemme , il est commode d’adopter l’usage des symboles logiques primitifs ⊤ et ⊥.
Montrer le lemme d’interpolation que voici :
Soient A et B des formules telles que (A → B) est une tautologie alors, il existe une formule C (dite
”interpolante entre A et B ”) qui vérifie les propriétés suivantes :
– (A → C) est une tautologie;
– (C → B) est une tautologie;
– toute variable propositionnelle apparaissant dans C apparaı̂t aussi dans A et dans B .
Lorsque A et B ont une variable commune, on peut faire un raisonnement par récurrence sur le
nombre de variables propositionnelles apparaissant dans A mais pas dans B , en appliquant le résultat
des questions précédentes.
Problème 8. Théorème de compacité.
Pour tout ensemble A de formules du calcul propositionnel, on pose les définitions suivantes :
• une distribution de valeurs de vérité δ satisfait A ssi δ(A) = 1 pour toute A ∈ A ;
• A est satisfaisable ssi il existe une distribution de valeurs de vérité δ qui satisfait A ;
• A est finiment satisfaisable ssi toute partie finie B ⊆ A est satisfaisable (ceci signifie bien que,
pour toute partie finie B ⊆ A, il y a une distribution de valeurs de vérité δB , qui dépend de B et qui
satisfait B ).
Le but de cet exercice est la démonstration du théorème de compacité dont voici l’énoncé :
Pour tout ensemble A de formules du calcul propositionnel, les deux propriétés suivantes sont
équivalentes :
1) A est satisfaisable,
2) A est finiment satisfaisable.

Il est clair que 1) implique 2); de même, 2) implique trivialement 1) lorsque A est fini (puisqu’alors,
toute partie de A est finie). Il reste à démontrer que 2) implique 1) lorsque l’on ne suppose pas que A
est fini.
Soit donc A un ensemble finiment satisfaisable.
a) Soit p une variable propositionnelle quelconque.
Montrer que l’un des deux ensembles A ∪ {p} ou A ∪ {¬p} est finiment satisfaisable.
Indication : En supposant que A ∪ {p} n’est pas finiment satisfaisable (c’est–à–dire, qu’il existe une
partie finie B ⊆ A ∪ {p} qui n’est pas satisfaisable) montrer que A ∪ {¬p} est finiment satisfaisable.
b) Soit P = {p1 , . . . , pn , . . .} une énumération de l’ensemble des variables propositionnelles.
On considère la suite (An )n∈N d’ensembles définie par la récurrence :
A0 = A

An ∪ {pn+1 } si An ∪ {pn+1 } est finiment satisfaisable,
An+1 =
An ∪ {¬pn+1 } sinon.
Montrer que chacun des An est finiment satisfaisable.
c) On définit, par récurrence, les ensembles ln de littéraux suivants :
l0 = ∅

ln ∪ {pn+1 } si pn+1 ∈ An+1 ,
ln+1 =
ln ∪ {¬pn+1 } sinon.
Montrer que ln ⊆ An pour tout n.

Institut Galilée 12 MM
d) On définit, par récurrence, la distribution de valeurs de vérité λ :
1 si pn ∈ An ,
n
λ(pn ) =
0 sinon.
Montrer que λ(A) = 1 pour toute A ∈ A et donc que A est satisfaisable.
On pourra considérer un entier n assez grand pour que toutes les variables apparaissant dans A soient
parmi {p1 , . . . , pn } et se souvenir que ln ∪ {A} ⊆ An .

MM 13 Institut Galilée
 SYSTÈME LK (Calcul propositionnel classique).

Identité

p⊢p

Coupure
Γ ⊢ ∆; A A, Λ ⊢ Π
Γ, Λ ⊢ ∆; Π

Règles structurelles

Γ⊢∆ Γ⊢∆
(E d ) (E g )
Γ ⊢ σ(∆) σ(Γ) ⊢ ∆
pour toute permutation σ pour toute permutation σ
Γ ⊢ ∆; A; A A, A, Γ ⊢ ∆
(C d ) (C g )
Γ ⊢ ∆; A A, Γ ⊢ ∆
Γ⊢∆ Γ⊢∆
(A d ) (A g )
Γ ⊢ ∆; A A, Γ ⊢ ∆

Règles logiques

A, Γ ⊢ ∆ Γ ⊢ ∆; A
(¬ d ) (¬ g )
Γ ⊢ ∆; ¬A ¬A, Γ ⊢ ∆
Γ ⊢ ∆; A Λ ⊢ Π; B A, B, Γ ⊢ ∆
(∧ d ) (∧ g )
Γ, Λ ⊢ ∆; Π; (A ∧ B) (A ∧ B), Γ ⊢ ∆
Γ ⊢ ∆; A; B A, Γ ⊢ ∆ B, Λ ⊢ Π
(∨ d ) (∨ g )
Γ ⊢ ∆; (A ∨ B) (A ∨ B), Γ, Λ ⊢ ∆; Π
A, Γ ⊢ ∆; B Γ ⊢ ∆, A B, Λ ⊢ Π
(→ d ) (→ g )
Γ ⊢ ∆; (A → B) (A → B), Γ, Λ ⊢ ∆; Π

Institut Galilée 14 MM
CALCUL DES SÉQUENTS PROPOSITIONNEL : LK.

Sauf mention explicite du contraire, ”prouvable” signifie ”prouvable dans LK”.

Les ”axiomes” sont figurés ici par une règle sans prémisse, une preuve dans LK se présente sous la
forme d’un arbre dont toutes les feuilles sont vides. Rappelons qu’on dit d’une formule X que c’est
un théorème ou plus simplement qu’elle est valide, lorsque ⊢ X est prouvable.
La propriété fondamentale est le Théorème d’élimination des coupures pour LK
Tout séquent prouvable admet une preuve n’utilisant aucune coupure.
Les coupures dont il est question dans cet énoncé sont dites logiques.
On peut considérer des arbres dont les embranchements sont bien des applications de règles de LK,
mais dont les feuilles ne sont pas toutes vides : soit Σ un ensemble de séquents alors, un arbre dont
les feuilles non vides sont des éléments de Σ s’appellera une déduction à partir de Σ. Le théorème
d’élimination des coupures s’applique encore à ce cas mais, il ne dit rien sur les coupures propres (à Σ),
c’est–à–dire, celles dont la formule coupée provient sans modification d’une formule d’un élément de
Σ, dans l’une au moins des prémisses : Tout séquent déductible d’un ensemble Σ admet une déduction
dont les seules coupures sont propres.

Exercice 9. Les axiomes d’identité et les substitutions.

Les axiomes d’identité sont posés pour les seules variables propositionnelles : montrer, par induction
sur les formules, que le séquent X ⊢ X est prouvable. En déduire qu’une substitution transforme une
formule valide en une formule valide.
Dans la pratique, on considère souvent tout séquent X ⊢ X comme étant un axiome d’identité!

Exercice 10.
Construire une preuve du séquent ⊢ X pour chacune des formules choisies X .

Exercice 11. Les séquents et les formules.

a) Montrer que les règles logiques unaires (c’est–à–dire à une seule prémisse) sont inversibles. Plus
précisément, par exemple pour le connecteur ∧, montrer que l’on peut déduire A, B, Γ ⊢ ∆ à partir
de (A ∧ B), Γ ⊢ ∆.
b) Soit S un séquent distinct du séquent vide ( ⊢ ) et soit Φ(S) l’ensemble des formules X telles que
l’on peut déduire ⊢ X de S en n’appliquant que des règles logiques unaires et des échanges.
Montrer que, réciproquement, on peut déduire S de ⊢ X , pour toute X ∈ Φ(S).

Bien que ça ne soit pas très ”académique”, il est commode de penser à un
, ⊢ ; séquent S comme à une représentation un peu assouplie de l’une quelconque
∧ → ∨ des formules X ∈ Φ(S). La petite table ci–contre résume ces correspon-
dances, si on se souvient de plus qu’une négation ¬ signale le passage d’un
membre à l’autre du séquent. Notons au passage que l’utilisation du point virgule comme séparateur
dans le membre de droite des séquents, qui n’est pas traditionnelle, permet d’écrire la table ci–contre
et surtout, peut décourager les meilleurs esprits à faire des usages frauduleux de la coupure (que l’on
n’a pas à publier ici).

Exercice 12. Inversiblité des règles logiques binaires.

Les règles logiques binaires (c’est–à–dire à deux prémisses) ne sont pas inversibles telles quelles car il
est généralement impossible de répartir les contextes! Fort judicieusement, les règles structurelles sont
là pour les modifier de telle façon que ce problème ne se pose plus. Plus précisément :
a) Montrer que l’on peut déduire Γ ⊢ ∆; A et Γ ⊢ ∆; B à partir de Γ ⊢ ∆; (A ∧ B), et
réciproquement (les contextes Γ et ∆ sont les mêmes dans ces trois séquents).

MM 15 Institut Galilée
Une conséquence simple de ce résultat est que l’ensemble des deux séquents ⊢ X et ⊢ Y , et le
séquent ⊢ (X ∧ Y ) peuvent se déduire l’un de l’autre.
b) Enoncer et démontrer les résultats analogues pour les connecteurs ∨ et →.
Exercice 13. Satisfaction des séquents.
On dit qu’une distribution de valeurs de vérité δ satisfait le séquent Γ ⊢ ∆ ssi lorsque δ satisfait toutes
les formules de Γ, alors δ satisfait aussi au moins une formule de ∆. Par exemple, un séquent de la
forme X ⊢ X est satisfait par toute distribution de valeurs de vérité, mais le séquent vide ⊢ ne l’est
par aucune.
a) Montrer que lorsque δ satisfait la ou les prémisses d’une règle du système LK alors elle satisfait
aussi sa conclusion (on n’oubliera pas le cas de la coupure).
REMARQUE. Ceci implique évidemment que si δ satisfait un ensemble Σ de séquents, alors elle
satisfait aussi tout séquent que l’on peut en déduire.
b) Transposer et démontrer les résultats d’inversibilité des règles logiques, en termes de satisfaction
d’ensembles de séquents.
Un système de décomposition pour LK

Γ′ , A, Γ′′ ⊢ ∆′ ; A; ∆′′

Γ ⊢ ∆′ ; ¬A; ∆′′ Γ′ , ¬A, Γ′′ ⊢ ∆

A, Γ ⊢ ∆′ ; ∆′′ Γ′ , Γ′′ ⊢ ∆; A

Γ ⊢ ∆′ ; (A∧B); ∆′′ Γ′ , (A∧B), Γ′′ ⊢ ∆

Γ ⊢ ∆′ ; A; ∆′′ Γ ⊢ ∆′ ; B; ∆′′ Γ′ , A, B, Γ′′ ⊢ ∆

Γ ⊢ ∆′ ; (A∨B); ∆′′ Γ′ , (A∨B), Γ′′ ⊢ ∆

Γ ⊢ ∆′ ; A; B; ∆′′ Γ′ , A, Γ′′ ⊢ ∆ Γ′ , B, Γ′′ ⊢ ∆

Γ ⊢ ∆′ ; (A→B); ∆′′ Γ′ , (A→B), Γ′′ ⊢ ∆

A, Γ ⊢ ∆′ ; B; ∆′′ Γ′ , Γ′′ ⊢ ∆; A Γ′ , B, Γ′′ ⊢ ∆

Le système de décomposition pour LK représente de façon graphique les résultats d’inversibilité des
règles démontrés dans les exercices précédents. L’application de l’une des règles fait disparaı̂tre
– ou bien un séquent (la première règle);
– ou bien un opérateur logique.

Institut Galilée 16 MM
Si donc on applique ces règles tant qu’il est possible, on transforme un séquent S en un ensemble,
que l’on notera Dec(S), de séquents atomiques, c’est–à–dire, constitués uniquement de variables
propositionnelles (il est clair que Dec(S) n’est pas défini de façon univoque car il peut dépendre de
l’ordre dans lequel on a appliqué les règles de décomposition).
Dans la pratique, on ajoute les règles suivantes, que l’on peut considérer, si l’on veut, comme des con-
tractions. Par contre, les règles de réduction sont écrites de façon à éviter l’application de tout échange,
afin d’écarter le risque fatal de rentrer dans une suite sans fin d’applications de cette opération.

”Contractions”

Γ ⊢ ∆; A; ∆′ ; A; ∆′′ Γ, A, Γ′ , A, Γ′′ ⊢ ∆

Γ ⊢ ∆; A; ∆′ ; ∆′′ Γ, Γ′ , A, Γ′′ ⊢ ∆

Problème 14. Formes normales conjonctives et méthode de résolution.

a) Montrer comment calculer, à partir de Dec( ⊢ X), une forme normale conjonctive (duale d’une
forme normale disjonctive) équivalente à la formule X .
La pratique montre rapidement que ce calcul d’une forme normale conjonctive de X est plus aisé que
le calcul ”classique” et même, que Dec( ⊢ X) est bien plus maniable que cette forme normale!
b) Montrer qu’un séquent S est prouvable ssi Dec(S) = ∅.
REMARQUE. Ce résultat donne un algorithme de prouvabilité du calcul propositionnel, mais cet
algorithme est d’allure exponentielle, car un arbre de décomposition admet des embranchements
binaires. En fait, le problème est connu pour être NP–complet.
c) Montrer, en appliquant le théorème de complétude, que si l’on peut déduire le séquent vide ⊢ à
partir de Dec(X ⊢ ) alors la formule X est valide.
Cette façon, assez indirecte, de montrer qu’une formule est valide est connue sous le nom de
résolution : elle sera surtout utile dans le cas du calcul des prédicats, pour lequel elle a donné lieu
à de nombreux travaux dans les milieux informatiques.
REMARQUE. D’après ce qui a été dit, au début de cette section, au sujet du théorème d’élimination
des coupures, une déduction sans coupure logique du séquent vide ⊢ à partir de Dec(X ⊢ ) peut
contenir des coupures propres à cet ensemble.
En partant de l’idée que, lors d’une telle déduction, toute formule doit disparaı̂tre, il est facile de voir
que les seules règles utiles sont :
– des coupures;
– des contractions;
et, pour mettre les formules dans la position nécessaire à l’application de ces règles, des échanges.
d) Montrer par résolution que les formules choisies sont valides.

Exercice 15.
Soit X une formule.
a) Montrer, par induction sur les déductions, que si l’on peut déduire le séquent Γ ⊢ ∆ de ⊢ X alors
X, Γ ⊢ ∆ est prouvable.
b) Donner une justification de la méthode de résolution n’utilisant que la notion de prouvabilité (alors
que la justification précédente utilise aussi la notion de satisfaisabilité).

MM 17 Institut Galilée
Problème 16. Théorème de complétude.
Le but de ce problème est de redémontrer le Théorème de complétude pour le calcul des propositions :
Si A est une tautologie, alors ⊢ A est prouvable dans LK.
Posons d’abord une définition : soient A une formule et δ une distribution de valeurs de vérité, alors,
la formule Aδ est définie par :
si δ(A) = 1,
Aδ = A
n
¬A sinon.

a) Montrer, par induction sur la formule A, que le séquent pδ1 , . . . , pδm ⊢ Aδ est prouvable dans LK,
quelle que soit δ , lorsque les variables propositionnelles apparaissant dans A sont parmi p1 , . . . , pm .
Indication. On simplifiera sensiblement la démonstration en montrant que, pour tout opérateur
binaire ∗ ∈ {∧, ∨, →}, le séquent Aδ , B δ ⊢ (A ∗ B)δ est prouvable dans LK.
b) Soit A une tautologie dont les variables propositionnelles sont parmi p1 , . . . , pm .
Montrer que le séquent pδ1 , . . . , pδi ⊢ A est prouvable dans LK pour tout entier naturel i ≤ m, quelle
que soit δ . En déduire le théorème de complétude.

Le vrai et le faux
Lorsque l’on veut adopter ⊤ et ⊥ comme symboles logiques primitifs, il faut compléter LK par les
règles :

(⊤ d )
⊢⊤
(⊥ g )
⊥⊢

Problème 17. Lemme d’interpolation.

La question de l’inversion de la règle de coupure ne se pose pas car, lorsque l’on ne connaı̂t que la
conclusion d’une telle règle, on ignore tout d’une éventuelle formule de coupure A ... Cependant,
on peut montrer que tout séquent prouvable admet une preuve se terminant par une coupure, sur
la formule de laquelle on a un certain contrôle!
Pour énoncer le résultat proprement, on adopte ⊤ et ⊥ comme symboles logiques primitifs, avec les
règles ci–dessus.
a) Plus précisément, montrer que pour tout séquent prouvable Γ1 , Γ2 ⊢ ∆1 ; ∆2 il existe une formule
C vérifiant les propriétés suivantes :
– Γ1 ⊢ ∆1 ; C est prouvable;
– C, Γ2 ⊢ ∆2 est prouvable;
– toute variable propositionnelle apparaissant dans C apparaı̂t aussi dans Γ1 ⊢ ∆1 et dans
Γ2 ⊢ ∆2 .
La démonstration se fait par induction sur les preuves sans coupure : le nombre de cas à considérer est
assez important!

b) En déduire le lemme d’interpolation qui a déjà été démontré dans un exercice précédent par
d’autres moyens.

Institut Galilée 18 MM
Logique intuitionniste et système LJ.
A côté de la logique classique, objet principal du cours, se trouve la logique intuitionniste qui, elle,
n’exclut pas le tiers, c’est–à–dire dans laquelle la formule (A ∨ ¬A) n’est généralement pas prouvable.
La restriction essentielle qui distingue les séquents du système intuitionniste LJ de ceux du système LK
porte sur la forme des séquents Γ ⊢ A où le second membre A est réduit à une formule et une seule.
Les formules du calcul des propositions intuitionniste sont construites, à partir d’un ensemble de
variables propositionnelles et de la constante 0, par application des symboles binaires ∧, ∨ et →.
La négation intuitionniste est un symbole abréviateur défini par ¬A = (A → 0). L’introduction de
ce symbole permet de considérer une formule classique comme étant aussi une formule intuition-
niste : une formule intervenant dans les deux systèmes sera nécessairement classique mais, il y a
évidemment des formules intuitionnistes qui ne sont pas classiques!
L’introduction de 0 a pour rôle essentiel de simplifier l’écriture de la règle (∨ g) pour la disjonction à
gauche : on aura intérêt à regarder attentivement les règles relatives à la disjonction!
On admettra le Théorème d’élimination des coupures pour LJ (mais il est intéressant de regarder
comment se transposent les cas–clefs dont il a été question dans le cours au sujet de LK) :
Tout séquent prouvable dans LJ y admet une preuve n’utilisant aucune coupure.

Problème 18. Calcul des propositions intuitionniste.

a) Construire une preuve dans LJ de chacun des séquents suivants :
X ⊢ ¬¬X
¬¬¬X ⊢ ¬X
¬¬(X ∧ Y ) ⊢ (¬¬X ∧ ¬¬Y )
¬¬(X → Y ) ⊢ (¬¬X → ¬¬Y )
b) Les axiomes de l’identité sont posés pour les seules variables propositionnelles : montrer, par
induction sur les formules, que le séquent X ⊢ X est prouvable dans LJ quelle que soit X .
c) Montrer, par induction sur les preuves, la propriété suivante pour toute Γ constituée de formules
classiques et toute formule classique A :
si Γ ⊢ A (resp. Γ ⊢ 0) est prouvable dans LJ alors Γ ⊢ A (resp. Γ ⊢ ) est prouvable dans LK.
d) La réciproque du résultat précédent n’est pas vraie! Par exemple, le séquent ¬¬X ⊢ X n’est pas
prouvable pour toute formule X (faire une tentative de preuve en prenant une variable proposition-
nelle). Voici la propriété essentielle de la logique intuitionniste (constructivité de la disjonction intu-
itionniste) :
Montrer que si ⊢ (X ∨ Y ) est prouvable dans LJ alors l’un des deux séquents ⊢ X ou ⊢ Y l’est aussi.
En déduire par exemple que ⊢ (X ∨ (X → Y )) et ⊢ (X ∨ ¬X) ne sont généralement pas prouvables
dans LJ (alors que de tels séquents le sont toujours dans LK).
e) Etudier la prouvabilité dans LJ des implications constituant les formules choisies 15 à 23 (sauf
évidemment 18!).
Problème 19. Traduction par double négation (Gödel).
Une formule A est dite spéciale ssi le séquent ¬¬A ⊢ A est prouvable dans LJ. Par exemple, toute
formule de la forme ¬X est spéciale, d’après un résultat précédent.
a) Montrer que, lorsque A et B sont spéciales, les séquents suivants sont prouvables dans LJ :
(¬¬A ∧ ¬¬B) ⊢ (A ∧ B)
(¬¬X → ¬¬B) ⊢ (X → B) (pour X quelconque)
b) On associe à toute formule classique A la formule sA (la notation traditionnelle A¬¬ n’est faite pour
simplifier ni l’écriture ni la lecture!), définie par l’induction suivante :

MM 19 Institut Galilée
 SYSTÈME LJ (Calcul propositionnel intuitionniste).

Les séquents ont la forme Γ ⊢ A où A est une seule formule.

Identité

p⊢p

Coupure
Γ ⊢ A A, Λ ⊢ B
Γ, Λ ⊢ B

Règles structurelles

Γ⊢B
(A g )
A, Γ ⊢ B
A, A, Γ ⊢ B
(C g )
A, Γ ⊢ B
Γ⊢C
(E g )
σ(Γ) ⊢ C
pour toute permutation σ

Règles logiques

(0 g )
0⊢A
Γ⊢A Λ⊢B A, B, Γ ⊢ C
(∧ d ) (∧ g )
Γ, Λ ⊢ (A ∧ B) (A ∧ B), Γ ⊢ C
Γ⊢A
(∨B d )
Γ ⊢ (A ∨ B) A, Γ ⊢ C B, Λ ⊢ C
(∨ g )
Γ⊢B (A ∨ B), Γ, Λ ⊢ C
(A∨ d )
Γ ⊢ (A ∨ B)
A, Γ ⊢ B Γ ⊢ A B, Λ ⊢ C
(→ d ) (→ g )
Γ ⊢ (A → B) (A → B), Γ, Λ ⊢ C

On définit la négation par ¬A = (A → 0).

Institut Galilée 20 MM
 s
p = ¬¬p pour toute variable propositionnelle p
s
¬A = ¬ sA
s
(A ∧ B) = (sA ∧ s B)
s
(A ∨ B) = ¬¬(sA ∨ s B)
s
(A → B) = (sA → s B)
Montrer que sA est spéciale pour toute formule classique A.

c) Montrer que lorsque le séquent Γ ⊢ ∆ est prouvable dans LK alors ¬ s∆, Γ ⊢ 0 est prouvable dans
LJ. (Pour ∆ = B1 ; . . . ; Bn , on a posé ¬ s∆ = ¬ s B1 , . . . , ¬ s Bn .)

d) Montrer que ⊢ A est prouvable dans LK ssi ⊢ sA est prouvable dans LJ, quelle que soit la formule
classique A.

MM 21 Institut Galilée