Introduction à la logique

Logique des propositions

En logique formelle, la logique des propositions est la première étape dans la définition de la logique et du raisonnement. Dans la logique propositionnelle, on étudie les relations entre des énoncés, que l’on va appeler propositions ou encore des formules. Elle définit les règles de déduction qui relient les propositions entre elles, sans en examiner le contenu. Ces relations peuvent être exprimées par l’intermédiaire de connecteurs logiques qui permettent, par composition, de construire des formules syntaxiquement correctes.

Dans le cadre de la logique des propositions, le calcul propositionnel (ou un système déductif) est un ensemble de règles permettant en un nombre fini d’étapes et selon des règles explicites de déterminer si une proposition est vraie. Un tel procédé s’appelle une démonstration. Nous verrons également que nous pouvons établir des raisonnements plus large sur l’équivalence de formules.

Syntaxe

La logique des propositions traite des expressions construites à l’aide d’un vocabulaire 𝓥 constitué de propositions (ou atomes) 𝓟 et d’opérateurs (ou connecteurs) 𝓒 :

𝓟 = {p, q, …}
𝓒 = {¬, ∧, ∨, →, ↔}
𝓥 = 𝓟 ⋃ 𝓒 ⋃ {(, )}

Les symboles de 𝓟 (p, q, etc.) dénotent des affirmations telles que « le moteur est en marche », « la vanne de sécurité est ouverte », « la cuve de liquide radioactif fuit », etc. On remplace ces affirmations par des symboles neutres pour s’affranchir du sens particulier de ces phrases et pour ne se concentrer que sur la cohérence, la validité du raisonnement, et non sur le sens des propositions elles-mêmes.

Nous proposons ici un ensemble de connecteurs parmi d’autres existants, plus ou moins riches — e.g. {¬, ∨}, {¬, ∧}, {¬, ∧, ∨}, etc.

Expression: Une expression est une concaténation de termes de 𝓥.

On note 𝓥* l’ensemble de toutes les expressions que l’on peut former avec le vocabulaire 𝓥.

pq(, p→, ¬∧ sont des expressions de 𝓥*.

On construit, sur 𝓥, le langage propositionnel 𝓛₀ ⊂ 𝓥* (ou ensemble de formules) comme étant le plus petit sous-ensemble de 𝓥* obtenu par les lois suivantes :

tout atome appartient à 𝓛₀ ;
si φ ∈ 𝓛₀ et ψ ∈ 𝓛₀ alors ¬φ, (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ) ∈ 𝓛₀ ;
il n’existe pas d’autres façons d’obtenir un élément de 𝓛₀.

Seules les expressions formées à partir des règles indiquées sont dites « bien formées ».

Formule: On appelle formule ou ebf (expression bien formée) tout élément de 𝓛₀.

p, (p → q), (p → ((q → r) ∨ t) sont des expressions de 𝓛₀.

Sémantique

La sémantique détermine les règles d’interprétations des propositions, et permet ainsi d’attacher des valeurs de vérité à des formules.

Interprétation: On appelle interprétation toute application I : 𝓟 ⟶ {⊤, ⊥}. ⊤ (ou Vrai ou 1) et ⊥ (ou Faux ou 0) sont appelées valeurs de vérité.

Une interprétation est une correspondance entre des éléments de 𝓛₀ et une image du monde extérieur ; cette correspondance peut être étendue à toutes les formules de 𝓛₀ en reprenant les lois de construction de 𝓛₀. Soit une formule η ∈ 𝓛₀, l’interprétation étendue d’une formule η, notée I[η], est obtenue récursivement de la façon suivante :

si η est un atome, alors I[η] est obtenue directement par I
si η est obtenue par la loi (ii), plusieurs cas sont possibles :
- η = ¬φ alors I[η] = ⊤ ssi I[φ] = ⊥
- η = (φ ∧ ψ) alors I[η] = ⊤ ssi I[φ] = I[ψ] = ⊤
- η = (φ ∨ ψ) alors I[η] = ⊤ ssi I[φ] = ⊤ ou I[ψ] = ⊤
- η = (φ → ψ) alors I[η] = ⊤ ssi I[φ] = ⊥ ou I[ψ] = ⊤
- η = (φ ↔ ψ) alors I[η] = ⊤ ssi I[φ] = I[ψ]

Cependant, par souci de simplicité, nous utiliserons également la notation I pour désigner l’interprétation étendue I.

Les tables suivantes indiquent, pour chaque connecteur, la valeur résultante :

∧	⊤	⊥
⊤	⊤	⊥
⊥	⊥	⊥

∨	⊤	⊥
⊤	⊤	⊤
⊥	⊤	⊥

→	⊤	⊥
⊤	⊤	⊥
⊥	⊤	⊤

↔	⊤	⊥
⊤	⊤	⊥
⊥	⊥	⊤

	¬
⊤	⊥
⊥	⊤

Lorsqu’on attribue des valeurs de vérité à chacune des propositions élémentaires intervenant dans une proposition de telle sorte que la proposition est vraie pour cette interprétation, on dit que l’on définit un modèle de la proposition.

Soit η = (a → (b ∨ c)), soit I telle que I(a) = I(b) = ⊤, I(c) = ⊥, alors :

I(η) = I(a → (b ∨ c))
= (I(a) → (I(b) ∨ I(c))
= (⊤ → (⊤ ∨ ⊥))
= (⊤ → ⊤)
= ⊤

Voici quelques définitions et notations essentielles, reposant sur la notion de sémantique et d’interprétation en logique des propositions. Il s’agit ici de qualifier les différentes formules selon leur interprétation.

Tautologie: On appelle tautologie toute formule φ telle que I[φ] = ⊤ pour toute interprétation I. On écrit alors : ⊨ φ

Contradiction: On appelle contradiction toute formule φ telle que I[φ] = ⊥ pour toute interprétation I.

Satisfiabilité: Une formule φ est dite satisfiable s’il existe au moins une interprétation I telle que I[φ] = ⊤.

Conséquence logique: On note φ ⊨ ψ (ψ conséquence logique de φ) si pour toute interprétation I telle que I[φ] = ⊤ alors I[ψ] = ⊤.

Équivalence logique: On note φ ≡ ψ (ψ équivalent logiquement à φ) ssi φ ⊨ ψ et ψ ⊨ φ.

Quelques équivalences

Pour toutes formules φ et ψ de 𝓛₀, on a les résultats suivants :

¬¬φ ≡ φ(1.2.1)
¬(φ ∧ ψ) ≡ (¬φ ∨ ¬ψ)(1.2.2)
¬(φ ∨ ψ) ≡ (¬φ ∧ ¬ψ)(1.2.3)
ρ ∧ (φ ∨ ψ) ≡ ((ρ ∧ φ) ∨ (ρ ∧ ψ))(1.2.4)
ρ ∨ (φ ∧ ψ) ≡ ((ρ ∨ φ) ∧ (ρ ∨ ψ))(1.2.5)
(φ ∧ ψ) ≡ (ψ ∧ φ)(1.2.6)
(φ ∨ ψ) ≡ (ψ ∨ φ)(1.2.7)
(φ → ψ) ≡ (¬φ ∨ ψ)(1.2.8)

Pour démontrer ces équivalences, il est possible d’utiliser la méthode des tables de vérité.

Forme normale conjonctive

Il peut être certaines fois nécessaire de s’intéresser à des formules ayant des formes particulières (standardisée), notamment dans le cadre de la déduction automatique et de la programmation logique, où ces formules devront être interprétable par un ordinateur.

Forme normale conjonctive: φ ∈ 𝓛₀ est sous forme normale conjonctive (ou FNC) ssi φ = (C₁ ∧ … ∧ C_n), avec C_i = (L_i1 ∨ … ∨ L_ip) et L_ij = a, a ∈ 𝓟 ou L_ij = ¬a, a ∈ 𝓟. Les L_ij sont appelés des littéraux.

D’autres formes normales existent, notamment la forme normale disjonctive (FND).

: Pour toute formule φ ∈ 𝓛₀, il existe une formule φ_c sous forme normale conjonctive telle que φ ≡ φ_c

Calcul propositionnel : méthode des tables de vérité

Cette méthode permet d’obtenir facilement des démonstrations dans 𝓛₀. En effet, une interprétation I associe à chaque élément la valeur ⊤ ou ⊥ ; une propriété faisant intervenir n éléments offre 2ⁿ interprétations envisageables. On obtient alors une démonstration par exhaustivité. Une telle démarche peut être utilisée pour montrer qu’une formule est une tautologie (la formule doit prendre la valeur ⊤ pour toutes les interprétations) ou pour montrer une équivalence logique.

Par exemple, l’équivalence logique (1.2.4) peut être établie de la façon suivante :

ρ	φ	ψ	(φ ∨ ψ)	(ρ ∧ (φ ∨ ψ))	(ρ ∧ φ)	(ρ ∧ ψ)	((ρ ∧ φ) ∨ (ρ ∧ ψ))
⊤	⊤	⊤	⊤	⊤	⊤	⊤	⊤
⊤	⊤	⊥	⊤	⊤	⊤	⊥	⊤
⊤	⊥	⊤	⊤	⊤	⊥	⊤	⊤
⊤	⊥	⊥	⊥	⊥	⊥	⊥	⊥
⊥	⊤	⊤	⊤	⊥	⊥	⊥	⊥
⊥	⊤	⊥	⊤	⊥	⊥	⊥	⊥
⊥	⊥	⊤	⊤	⊥	⊥	⊥	⊥
⊥	⊥	⊥	⊥	⊥	⊥	⊥	⊥

Les deux membres de l’expression (1.2.4) prennent les mêmes valeurs de vérité, il y a donc équivalence logique (colonnes grisées).

Malheureusement, cette méthode est systématique et trés coûteuse. Une alternative à cette méthode est la formalisation (ou déduction axiomatique).

Calcul propositionnel : déduction axiomatique (système formel)

Un système formel est défini par un tuple 〈𝓥, 𝓔, 𝓐, 𝓡〉, tel que :

𝓥 est un ensemble de symboles
𝓔 est un ensemble d’expressions bien formées dans 𝓥*
𝓐 est un ensemble d’axiomes (𝓐 ⊂ 𝓔)
𝓡 est un ensemble de règles de déduction de la forme :
- r_i : f₁, f₂, …, f_n ⊢ g avec f_i, g ∈ 𝓔

Un système formel est un mécanisme abstrait permettant d’engendrer un ensemble d’ebf à partir des axiomes en utilisant les règles.

Déduction ou preuve

Soit un système formel SF, on appelle déduction (ou preuve) de c_p à partir de h₁, h₂, …, h_n dans SF, et on note

h₁, h₂, …, h_n ⊢ c_p

toute suite _c₁, _c₂, …, c_p telle que pour i = 1, …, p

ou bien c_i est un axiome (c_i ∈ 𝓐)
ou bien c_i est une des hypothèses (h_k)
ou bien c_i peut être obtenue par application d’une règle r_i telle que
- c_i₁, c_i₂, …, c_{i_k} ⊢ c_i avec i₁, …, i_k < i

On peut assimiler une déduction à une forme de démonstration de l’expression c_p à l’aide des hypothèses h_i ; un cas particulier apparaît lorsque la démonstration peut être établie sans utilisation d’hypothèses.

Théorème: Étant donné un système formel SF, t est un théorème de SF et on note ⊢ t si t peut être déduit sans hypothèse.

Un système formel pour la logique des propositions

Définissons un système formel, avec son axiomatique et ses règles propres, dans le cadre de la logique des propositions, afin d’obtenir un système de preuve. Ce système est un exemple parmi d’autres.

Système formel pour 𝓛₀

Soit SF₀ le système formel suivant (où A, B et C désignent des variables pouvant être remplacées par toute expression de 𝓛₀) :

𝓥 = {a, b, c, …, ¬, →, (, )}
𝓔 est l’ensemble d’expressions bien formées dans 𝓥*
𝓐 = {A₁, A₂, A₃} avec :
- A₁ : (A → (B → A))
- A₂ : ((A → (B → C)) → ((A → B) → (A → C)))
- A₃ : ((¬A → ¬B) → (B → A))
𝓡 = {R_MP} contient une unique règle (le modus ponens) :
- R_MP : A, (A → B) ⊢ B

Montrons que ⊢ a → a. (a → a) est un théorème si on peut construire une déduction c₁, …, c_p, avec c_p = (a → a).

c₁ = ((a → ((b → a) → a)) → ((a → (b → a)) → (a → a)))Axiome A₂ avec A = a, B = (b → a), C = a
c₂ = (a → ((b → a) → a))Axiome A₁ en posant A = a, B = (b → a)
c₃ = ((a → (b → a)) → (a → a))Règle R_MP sur c₂ et c₁
c₄ = (a → (b → a))Axiome A₁ en posant A = a, B = b
c₅ = (a → a)Règle R_MP sur c₄ et c₃

Voici quelques résultats clés en logique des propositions.

Théorème de la déduction

Pour tout φ₁, …, φ_n, ψ ∈ 𝓛₀ :

φ₁, …, φ_n–1 ⊢ (φ_n → ψ) ssi φ₁, …, φ_n ⊢ ψ

Il y a équivalence entre être une tautologie et être prouvable, comme l’énoncent les théorèmes suivants.

Théorème de la correction en calcul propositionnel: Dans SF₀, pour tout φ ∈ 𝓛₀, ⊨ φ si ⊢ φ.

Théorème de la complétude en calcul propositionnel: Dans SF₀, pour tout φ ∈ 𝓛₀, ⊢ φ si ⊨ φ.

Ces résultats expriment que l’ensemble des tautologies correspond à l’ensemble des théorèmes établis dans le cadre du système formel SF₀. Ce système formel permet de construire des déductions de façon syntaxique — i.e. sans faire référence à la notion de ⊤ ou ⊥ — qui correspondent à des expressions prenant la valeur ⊤ (tautologies). SF₀ est une caractérisation syntaxique des tautologies de 𝓛₀.

Calcul propositionnel : méthode des tableaux

Le système formel étudié dans la section précédente permet d’obtenir des déductions dont le résultat est l’ensemble des tautologies de la logique des propositions. La méthode des tableaux (ou des arbres de vérité) est une autre façon de construire des déductions ; sa manipulation plus intuitive permet d’obtenir plus facilement des déductions. Par contre son aspect graphique en limite l’usage à des expressions simples.

Arbre de déduction: On appelle arbre de déduction, tout arbre dont les sommets sont des ebf de 𝓛₀ et dont toutes les branches sont fermées.

Branche fermée: Une branche (d’un arbre de déduction) est fermée si elle contient φ et ¬φ (φ étant un atome ou ebf de 𝓛₀).

Principe et règles

Une déduction de φ à partir de h₁, h₂, …, h_n notée h₁, h₂, …, h_n ⊢ φ peut être obtenue en montrant que l’arbre de racine : h₁, h₂, …, h_n, ¬φ est fermé. La fermeture de l’arbre (au début réduit à sa racine) est obtenue pas à pas par l’application des règles suivantes :

Montrons que l’expression (a → (b → a)) est un théorème — i.e. ⊢ (a → (b → a)).

L’unique branche de l’arbre est fermée grâce à la présence de a et ¬a.

Cette méthode est directement transcriptible en un algorithme de déduction et de raisonnement automatique.

Exercices

En utilisant les atomes S (le soleil brille), P (il pleut), B (il bruine), A (il y a un arc en ciel), O (il a un vent d’Ouest), E (il y a du vent d’Est), traduire dans la logique des propositions 𝓛₀ les énoncés suivants :

S’il pleut et que le soleil brille en même temps, alors il y a un arc en ciel,
Si le vent d’ouest amène la pluie, on n’a jamais vu qu’un vent d’est soit porteur de pluie,
La bruine est une forme de pluie.

Représenter dans le formalisme de la logique des propositions les théorèmes de géométrie suivants :

Si un triangle est équilatéral alors il est isocèle.
Un triangle rectangle n’est jamais équilatéral.
Un carré est à la fois un parallélogramme et un rectangle.
Un losange n’est ni un quadrilatère rectangle ni un triangle.
Deux droites coplanaires sont soit sécantes, soit parallèles.
Deux droites ne peuvent être à la fois sécantes et parallèles.

Formaliser dans 𝓛₀ les propositions suivantes :

Si Alice et Julie viennent à Paris, Zoé viendra aussi ;
Si Julie vient à Paris, Alice aussi ;
Julie ou Zoé, l’une des deux au moins, viendra à Paris.

Alice viendra-t-elle à Paris ? Et Julie ? Et Zoé ?

Montrer que ((p → r) ∧ (q ↔ s) ∧ (r ↔ q) ∧ p) ⊨ s.

Montrer que :

((¬q ∨ ¬s) ∧ (p → s) ∧ (¬p → (r → (q ∧ s))) ∧ ((q ∧ ¬s) → (¬r → (q ∧ p)))) ⊨ ¬q.

Construire dans SF₀ la preuve de ⊢ ((a → b) → ((b → c) → (a → c))).

Construire dans SF₀ la preuve de ⊢ (¬a → (a → b)).

Lors de ses aventures au pays des merveilles rapportées par Lewis Carroll, Alice est souvent accompagnée par le chat de Cheshire. Ce félin énigmatique s’exprime sous la forme d’affirmations logiques qui sont toujours vraies. Alice se trouve dans un corridor dont toutes les portes à sa taille sont fermées. La seule porte ouverte est nettement trop petite pour qu’elle puisse l’emprunter. Une étagère est fixée au-dessus de cette porte. Le chat dit alors à Alice : « L’un des flacons posés sur cette étagère contient un liquide qui te permettra de prendre une taille plus adéquate. Mais attention, les autres flacons peuvent contenir un poison fatal. » Trois flacons sont effectivement posés sur l’étagère. Le premier est rouge, le second jaune, le troisième bleu. Une étiquette est collée sur chaque flacon. Alice lit l’inscription figurant sur chaque étiquette :

Flacon rouge : le flacon jaune contient un poison ; le bleu n’en contient pas ;
Flacon jaune : si le flacon rouge contient un poison, alors le bleu aussi ;
Flacon bleu : je ne contiens pas de poison, mais au moins l’un des deux autres si.

Nous noterons R, J et B les variables propositionnelles correspondant au fait que les flacons rouge, jaune et bleu contiennent un poison. Nous noterons I_R, I_J et I_B les propositions correspondant aux inscriptions sur les flacons rouge, jaune et bleu.

On résoudra les questions suivantes d’abord en utilisant une table de vérité, puis en utilisant des simplifications et règles d’équivalence des formules.

Exprimez les formules I_R, I_J et I_B sous la forme de formules dépendant de R, J et B.
Les inscriptions sur les trois flacons sont-elles compatibles ?
Dans le cas où aucun des trois flacons ne contient un poison, est-ce qu’une ou plusieurs inscriptions sont fausses ?
Si les trois inscriptions sont vraies, est-ce qu’un ou plusieurs flacons contiennent un poison ?
Si seuls les flacons ne contenant pas un poison ont une inscription vraie, est-ce qu’un ou plusieurs flacons ne contiennent pas un poison ?

Logique des prédicats (du premier ordre)

Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage des mathématiques proposée par les logiciens de la fin du XIX^e siècle et du début du XX^e siècle.

Le calcul des propositions (vu en section précédente) est la partie du calcul des prédicats qui concerne ce qui ne contient pas les notions de variables, de fonctions et de prédicats et donc pas les quantificateurs ∀ et ∃. Il sert à formaliser essentiellement les déductions du calcul des prédicats.

Syntaxe

Comme pour la logique des propositions, nous allons définir l’ensemble des formules de la logique des prédicats, noté 𝓛₁ à partir d’un vocabulaire, noté 𝓥, composé de symboles de variables (𝓥ar), de symboles de fonctions (𝓕onc), de symboles de prédicats (𝓟red), de symboles de constantes (𝓒onst), de symboles de connecteurs (𝓒onnect), de symboles de quantificateurs (𝓠uant) et de parenthèses :

𝓥ar = {x, y, z, …}
𝓕onc = {f, g, h, …}
𝓟red = {P, Q, R, …}
𝓒onst = {c₁, c₂, …}
𝓒onnect = {¬, ∧, ∨, →, ↔}
𝓠uant = {∀, ∃}
𝓥 = 𝓥ar ⋃ 𝓕onc ⋃ 𝓟red ⋃ 𝓒onst ⋃ 𝓒onnect ⋃ 𝓠uant ⋃ {(, )}

Chaque symbole de fonction de 𝓕onc ou de prédicat de 𝓟red a une arité qui détermine le nombre d’arguments ou d’objets auxquels il est appliqué. Par exemple, le prédicat H pour « est un homme » a une arité d’un (on dit qu’il est unaire), tandis que le prédicat P pour « est le père de » a une arité de deux (on dit qu’il est binaire).

Nous construisons alors l’ensemble des termes 𝓣 comme suit :

si c ∈ 𝓒onst, alors c ∈ 𝓣 ;
si x ∈ 𝓥ar alors x ∈ 𝓣 ;
si t₁, …, t_n ∈ 𝓣 et f ∈ 𝓕onc d’arité n alors f(t₁, …, t_n) ∈ 𝓣 ;
il n’existe pas d’autre méthode pour obtenir des éléments de 𝓣.

Nous construisons également l’ensemble des atomes 𝓐 comme suit :

si t₁, …, t_n ∈ 𝓣, P ∈ 𝓟red d’arité n alors P(t₁, …, t_n) ∈ 𝓐;
il n’existe pas d’autre méthode pour obtenir des éléments de 𝓐.

On construit alors, comme pour la logique des propositions, le langage des prédicats 𝓛₁ (ou ensemble de formules) comme étant le plus petit ensemble obtenu par les lois suivantes :

𝓐 ⊂ 𝓛₁
si α₁, α₂ ∈ 𝓛₁ alors
¬α₁ ∈ 𝓛₁
(α₁ ∧ α₂) ∈ 𝓛₁
(α₁ ∨ α₂) ∈ 𝓛₁
(α₁ → α₂) ∈ 𝓛₁
(α₁ ↔ α₂) ∈ 𝓛₁
∀x α₁ ∈ 𝓛₁
∃x α₁ ∈ 𝓛₁
il n’existe pas d’autre méthode pour obtenir un élément de 𝓛₁.

Les expressions suivantes sont des éléments de 𝓛₁ :

P(x,f(y))
∀x (P(x,y) ∧ ∃x Q(y))
∀x R(x,y)
∀x ∀y ∀z ((P(x,y) ∧ P(y,z)) → P(x,z))

Portée d’un quantificateur: Soit la formule Qxφ ∈ 𝓛₁, φ désigne la portée du quantificateur Qx, avec Q ∈ 𝓠uant.

Variable libre/liée

Soit une formule φ ∈ 𝓛₁.

x est liée dans φ ssi x apparaît dans la portée d’un quantificateur Qx (Q ∈ 𝓠uant)
x est libre dans φ ssi x apparaît hors de la portée d’un quantificateur Qx (Q ∈ 𝓠uant)

On observera qu’une variable peut être libre et liée à la fois, comme dans la formule suivante

(P(x) → (∀x (R(x)))

Formule close: Une formule φ ∈ 𝓛₁ est close ssi elle ne comporte aucune variable libre.

Sémantique

Nous allons maintenant définir la sémantique de la logique des prédicats.

Interprétation en logique des prédicats

On définit une interprétation I par un ensemble non vide Ω_I appelé univers (ou domaine) de l’interprétation, tel que :

pour chaque symbole de constante c, I[c] = c_I ∈ Ω_I
pour chaque symbole de fonction n-aire f, I[f] : Ω_Iⁿ ⟶ Ω_I
pour chaque symbole de prédicat m-aire P, I[P] : Ω_I^m ⟶ {⊥,⊤}

À l’aide d’une interprétation, on peut définir la valeur de vérité associée à une formule. Cependant, une formule du premier ordre peut contenir des variables libres et selon la valeur que l’on affecte à ces variables, la valeur de vérité de la formule change. Par exemple, le prédicat Inf(x,y), représentant la relation x < y, est parfois vrai et parfois faux selon la valeur associée à x et y.

Pour cela, on associe à une interprétation une valuation ν : 𝓥ar ⟶ Ω_I définie sur les variables et à valeur dans l’univers d’interprétation pour définir la valeur de vérité d’une formule.

Valuation: Une valuation ν : 𝓥ar ⟶ Ω_I est une application de l’ensemble des variables dans Ω_I.

On notera alors I_ν[η] pour indiquer la valeur de vérité de η vis-à-vis de l’interprétation I et de la valuation ν. Nous définissons cela inductivement.

On étend l’interprétation des symboles à l’interprétation des termes de la façon suivante :

si x est une variable, alors I_ν[x] = ν(x) ;
si c est un symbole de constante (resp., f un symbole de fonction, P un symbole de prédicat), alors I_ν[c] = I[c] (resp., I_ν[f] = I[f], I_ν[P] = I[P]) ;
si I_ν[t₁], …, I_ν[t_n] sont des interprétations de termes, alors I_ν[f(t₁, …, t_n)] = I[f](I_ν[t₁], …, I_ν[t_n]).

Alors, la valeur de vérité d’une formule est :

si η = P(t₁, …, t_n) alors I_ν[η] = ⊤ ssi I[P](I_ν[t₁], …, I_ν[t_n]) = ⊤ ;
si η = ¬φ alors I_ν[η] = ⊤ ssi I_ν[φ] = ⊥ ;
si η = (φ ∧ ψ) alors I_ν[η] = ⊤ ssi I_ν[φ] = I_ν[ψ] = ⊤ ;
si η = (φ ∨ ψ) alors I_ν[η] = ⊤ ssi I_ν[φ] = ⊤ ou I_ν[ψ] = ⊤ ;
si η = (φ → ψ) alors I_ν[η] = ⊤ ssi I_ν[φ] = ⊥ ou I_ν[ψ] = ⊤ ;
si η = (φ ↔ ψ) alors I_ν[η] = ⊤ ssi I_ν[φ] = I_ν[ψ].

Jusqu’ici, la sémantique ressemble beaucoup à celle de la logique propositionnelle. Introduisons alors les quantificateurs :

si φ = ∃x ψ, alors I_ν[φ] = ⊤ ssi il existe dans Ω_I un élément e tel que, si on affecte e à la variable x dans la formule ψ, c’est-à-dire, on utilise une valuation η identique à ν sauf pour la variable x, alors I_η[ψ] = ⊤.
si φ = ∀x ψ, alors I_ν[φ] = ⊤ ssi pour tout les éléments e de Ω_I, si on affecte e à la variable x dans la formule ψ, (on utilise une valuation η), alors I_η[ψ] = ⊤.

Illustrons cette notion à l’aide de la formule suivante : φ = ∀x ∃y P(x,y).

Définissons l’interprétation I₁ en posant Ω_I₁ = ℕ et en associant à P(x,y) la relation x < y. Alors la formule s’interprète de la manière suivante : « Pour tout x entier, on peut trouver un entier y tel que y soit supérieur à x ». Cette assertion est manifestement vraie, on notera alors I₁[φ] = ⊤.

Par contre, si nous reprenons cette même formule avec l’interprétation I₂ où Ω_I₂ = ℕ et où la relation x gt; y est associée à P(x,y), l’interprétation devient : « Pour tout x entier, on peut trouver un entier y tel que y est inférieur à x ». Cette assertion est fausse — I₂[φ] = ⊥ (un contre-exemple est obtenu en prenant la valeur 0 pour x).

Ainsi, comme nous l’avons vu pour la logique des propositions, une formule peut prendre la valeur ⊤ ou ⊥ en fonction de son interprétation. Il faut tenir compte de l’existence d’une ou plusieurs variables libres, dans ce cas une interprétation ne permettra d’obtenir une valeur de vérité que si la valeur de la (des) variable(s) libre(s) est précisée.

Soit ψ(x) = ∃y P(x,y). Reprenons l’interprétation I₂ de l’exemple précédent, I₂[ψ(7)] = ⊤, I₂[ψ(0)] = ⊥.

Étant donnée une interprétation I, alors toute formule close de 𝓛₁ prend la valeur ⊤ ou ⊥ pour cette interprétation (aucune valeur de variable libre n’est à préciser).

Validité universelle, adaptée de la définition 4: Soit φ ∈ 𝓛₁ une formule close, elle est dite universellement valide (ou logiquement valide) si elle prend la valeur ⊤ pour toute interprétation I. On écrit alors : ⊨ φ

Les définitions concernant la conséquence logique (Déf. 7) et l’équivalence logique (Déf. 8) restent inchangées. Les exemples précédents montrent qu’à l’inverse de ceux étudiés dans le cadre de la logique des propositions, il n’existe pas de méthode algorithmique comparable à la méthode des tables de vérité pour établir des résultats relatifs à la conséquence ou à l’équivalence logique. En effet, une telle méthode devrait envisager exhaustivement toutes les interprétations possibles d’une formule ; ceci est impossible dans le cas où on fait correspondre à Ω un ensemble infini. Une méthode syntaxique (e.g. utilisation d’un système formel) est donc nécessaire pour établir des résultats du type ⊨ φ ou φ ⊨ ψ.

Calcul des prédicats : déduction axiomatique (système formel)

Dans la logique des propositions, l’ensemble des tautologies correspond aux théorèmes du système formel SF₀ (théorèmes 3 et 4). Il existe un résultat analogue pour la logique des prédicats en utilisant le système formel SF₁, défini comme suit.

Un système formel pour la logique des prédicats

De la même manière que nous l’avons fait pour la logique des propositions, nous définissons un système formel pour la logique des prédicats, en ajoutant deux nouveaux axiomes et une règle.

Système formel pour 𝓛₁

Soit SF₁ le système formel suivant (où A(.), B, C peuvent être remplacées par toute expression de 𝓛₁) :

𝓥 = 𝓥ar ⋃ 𝓕onc ⋃ 𝓟red ⋃ 𝓒onst ⋃ 𝓒onnect ⋃ 𝓠uant ⋃ {(, )}
𝓔 est l’ensemble d’expressions bien formées dans 𝓥*
𝓐 = {A₁, A₂, A₃} ⋃ {A₄, A₅} avec A₁, A₂ et A₃ identiques à SF₀ et :
- A₄ : (∀x A(x) → A(t)) avec t terme libre pour x
- A₅ : ((B → C) → (B → ∀x C))
𝓡 = {R_MP, R_G} avec :
- R_MP : B, (B → C) ⊢ C(modus ponens)
- R_G : B ⊢ ∀x B(généralisation)

Les définitions 10 et 11 restent valables pour SF₁. Les quantifiateurs ∀ et ∃ sont liés par les équivalences :

∃x φ ≡ ¬∀x ¬φ(2.3.1)
∀x φ ≡ ¬∃x ¬φ(2.3.2)
¬∀x φ ≡ ∃x ¬φ(2.3.3)
¬∃x φ ≡ ∀x ¬φ(2.3.4)

Montrons que (∀x∀y P(x,y)) ⊢ (∀z P(z,z)). Il faut construire une déduction c₁, …, c_p avec c_p = ∀z P(z,z).

c₁ = ∀x∀y P(x,y)Hypothèse
c₂ = (∀x∀y P(x,y) → ∀y P(z,y))Axiome A₄ avec A(x) = ∀y P(x,y)
c₃ = ∀y P(z,y)R_MP sur c₁ et c₂
c₄ = (∀y P(z,y) → P(z,z))Axiome A₄ avec A(x) = P(z,x)
c₅ = P(z,z)R_MP sur c₃ et c₄
c₆ = ∀z P(z,z)R_G sur c₅

Attention : la variable x apparaissant à la fois dans la déduction et dans l’axiome, il y a risque de confusion. Ces variables étant muettes, on peut sans risque les renommer.

Quelques équivalences

On peut montrer dans SF₁ les résultats suivants (par la méthode des tableaux, voir plus bas), sachant que les équivalences obtenues pour la logique des propositions restent vraies.

Lois de distribution des quantificateurs :

∀x (φ ∧ ψ) ≡ (∀x φ ∧ ∀x ψ)(2.3.5)
∃x (φ ∨ ψ) ≡ (∃x φ ∨ ∃x ψ)(2.3.6)

Lois de permutation des quantificateurs de même sorte :

∀x∀y φ ≡ ∀y∀x φ(2.3.7)
∃x∃y φ ≡ ∃y∃x φ(2.3.8)

Théorème de la complétude (et de la correction) — Gödel, 1929: Pour tout φ ∈ 𝓛₁, ⊨ φ ssi ⊢ φ.

Ce résultat est analogue à celui obtenu pour la logique des propositions (Théorèmes 3 et 4). SF₁ constitue une caractérisation des formules universellement valides.

Calcul des prédicats : méthode des tableaux

La méthode étudiée précédemment peut être adaptée au cadre de la logique des prédicats. Les définitions 13 et 14 restent valables, par contre il faut ajouter 4 nouvelles règles aux 9 règles déjà définies.

règles de la méthode des tableaux pour la logique du premier ordre

Montrons que H₁, H₂ ⊢ C avec :

(H₁)∀x∀z∃y∀t ((P(x,y) ∧ Q(y,z)) → P(z,t))
(H₂)∃x∀y P(x,y)
(C)∀z∃x∃y (Q(x,y) → P(z,x))

Cela revient à montrer que l’arbre de racine H₁, H₂, ¬C est fermé. L’application des règles R_∃ et R_¬∀ sur C laisse un seul quantificateur existentiel. La racine comprenant alors 3 variables quantifiées existentiellement, trois constantes différentes — au minimum — devront être utilisées.

Comme pour la logique des propositions, cette méthode est directement transcriptible en un algorithme de déduction et de raisonnement automatique.