Logique
Mathématique

Fondements formels du raisonnement — propositions, prédicats, preuves, complétude

VRAI| FAUX| ∧ ∨ ¬ ⇒ ⇔| ∀ ∃| ▮
[01]

Fondements de la logique

La logique mathématique est la branche des mathématiques qui étudie les systèmes formels de raisonnement. Elle fournit les fondements sur lesquels repose l’ensemble des mathématiques : définition rigoureuse de la preuve, des axiomes et des théorèmes.

P

Logique propositionnelle

Étudie les relations entre propositions vraies/fausses par des connecteurs logiques. Base de l’électronique numérique.

∀

Logique des prédicats

Étend la logique propositionnelle avec variables, quantificateurs ∀ (pour tout) et ∃ (il existe). Langage naturel des mathématiques.

M

Théorie des modèles

Étudie les structures qui satisfont des systèmes d’axiomes. Lien entre syntaxe (formules) et sémantique (modèles).

⊢

Théorie de la preuve

Étudie les démonstrations formelles : séquents, déduction naturelle, calcul des séquents (Gentzen).

λ

Théorie de la calculabilité

Qu’est-ce qui est calculable ? Machines de Turing, fonctions récursives, indécidabilité (Turing, Church, Gödel).

K

Logique modale

Étudie les notions de nécessité (□) et possibilité (◇). Applications en informatique (vérification de modèles, épistémologie).

[02]

Logique propositionnelle

La logique propositionnelle travaille avec des propositions atomiques (P, Q, R…) qui sont vraies (1) ou fausses (0), et des connecteurs logiques pour les combiner.

¬
Négation
NOT P — vrai si P est faux
∧
Conjonction
P AND Q — vrai si P et Q sont vrais
∨
Disjonction
P OR Q — vrai si P ou Q est vrai
⇒
Implication
P ⇒ Q — faux seulement si P vrai et Q faux
⇔
Équivalence
P ⇔ Q — vrai si P et Q ont même valeur
⊻
XOR (exclusif)
P XOR Q — vrai si exactement un est vrai

Lois fondamentales

¬(¬P) ⇔ PDouble négation
P ∧ (Q ∨ R) ⇔ (P ∧ Q) ∨ (P ∧ R)Distributivité
¬(P ∧ Q) ⇔ ¬P ∨ ¬QDe Morgan 1
¬(P ∨ Q) ⇔ ¬P ∧ ¬QDe Morgan 2
P ⇒ Q ⇔ ¬P ∨ QImpl. comme disj.
P ⇒ Q ⇔ ¬Q ⇒ ¬PContraposée
[03]

Logique des prédicats du 1er ordre

La logique du premier ordre (LP1) ajoute aux connecteurs propositionnels des variables, des prédicats et des quantificateurs. C’est le langage naturel des axiomes mathématiques.

∀
Quantificateur universel
∀x ∈ ℝ, x² ≥ 0

Pour tout x réel, le carré de x est positif ou nul.

∃
Quantificateur existentiel
∃x ∈ ℚ, x² = 2

Il n’existe pas de rationnel dont le carré vaut 2. (Faux dans ℚ, vrai dans ℝ.)

∃!
Unicité
∃! x ∈ ℝ, x + 3 = 7

Il existe un unique réel x tel que x+3=7. (∃! est un sucre syntaxique pour ∃∧∀.)

Négation des quantificateurs (De Morgan généralisé)

¬(∀x, P(x))≡∃x, ¬P(x)
¬(∃x, P(x))≡∀x, ¬P(x)
[04]

Tables de vérité

Une table de vérité énumère toutes les combinaisons de valeurs de vérité pour évaluer une formule. Elle permet de vérifier les tautologies (toujours vraies) et les contradictions (toujours fausses).

P ⇒ Q (implication)
PQP⇒Q
VVV
VFF
FVV
FFV
(P⇒Q) ∧ (Q⇒P)
PQP⇔Q
VVV
VFF
FVF
FFV
P ∨ ¬P (tautologie)
P¬PP∨¬P
VFV
FVV

Satisfiabilité (SAT)

Une formule est satisfiable s’il existe une valuation la rendant vraie. Décider la satisfiabilité d’une formule propositionnelle (SAT) est le premier problème NP-complet démontré (Cook, 1971). Les solveurs SAT modernes (à millions de variables) sont essentiels en vérification formelle et IA.

[05]

Déduction et systèmes de preuve

Un système de preuve formel définit des règles pour dériver des théorèmes à partir d’axiomes. Les règles d’inférence les plus courantes :

Modus Ponens
P    P⇒Q
Q

Si P est vrai et P implique Q, alors Q est vrai. Règle fondamentale.

Modus Tollens
¬Q    P⇒Q
¬P

Si Q est faux et P implique Q, alors P est faux (contraposée appliquée).

Syllogisme
P⇒Q    Q⇒R
P⇒R

La transitivité de l’implication. Base du raisonnement en chaîne.

Instanciation ∀
∀x P(x)
P(a)

Si P est vrai pour tout x, il est vrai pour tout terme particulier a.

Généralisation ∀
P(x) (x libre)
∀x P(x)

Si P(x) est démontré pour x quelconque (libre), on peut universaliser.

Résolution
P∨Q    ¬P∨R
Q∨R

Principe unificateur de la logique clausale, utilisé dans Prolog et les prouveurs automatiques.

Théorème de complétude de Gödel (1929)

Tout énoncé vrai (sémantiquement valide) dans la logique du premier ordre est démontrable (syntaxiquement). Autrement dit : la logique du premier ordre est complète. À ne pas confondre avec les théorèmes d’incomplétude de 1931.

[06]

Théorèmes d’incomplétude de Gödel

En 1931, Kurt Gödel publie les résultats les plus profonds de la logique du XXe siècle : tout système axiomatique suffisamment puissant porte en lui sa propre limite.

1er théorème

Incomplétude

Tout système axiomatique consistant (sans contradiction) capable d’exprimer l’arithmétique de Peano contient des énoncés vrais mais indémontrables dans ce système.

« Cette phrase est indémontrable. » — Le numéro de Gödel en est la version formelle.
2e théorème

Incohérence relative

Aucun système axiomatique consistant capable d’exprimer l’arithmétique ne peut prouver sa propre consistance à partir de ses propres axiomes.

Le programme de Hilbert — fonder les mathématiques sur des axiomes finis et vérifier leur cohérence — est impossible.

Gödel a utilisé l’arithmétisation de la syntaxe : à chaque formule logique est assigné un entier unique (numéro de Gödel), permettant à l’arithmétique de parler d’elle-même.

[07]

Théorie des ensembles & axiomes ZFC

Les mathématiques modernes sont généralement fondées sur la théorie des ensembles de Zermelo-Fraenkel avec axiome du choix (ZFC), formulée entièrement en logique du premier ordre.

A1
Extensionalité : deux ensembles sont égaux s’ils ont les mêmes éléments. ∀x(x∈A ⇔ x∈B) ⇒ A=B.
A2
Paire : pour tout a et b, il existe l’ensemble {a, b}.
A3
Réunion : pour tout ensemble E, il existe l’union de tous ses éléments.
A4
Parties : pour tout ensemble E, il existe l’ensemble de toutes ses parties ℘(E).
A5
Infini : il existe un ensemble infini (contenant ø et fermé par successeur).
A6
Séparation : pour tout ensemble E et propriété P, {x∈E | P(x)} existe.
A7
Remplacement : l’image d’un ensemble par une fonction est un ensemble.
A8
Régularité : tout ensemble non vide possède un élément minimal (pas d’ensemble s’appartenant lui-même).
AC
Axiome du choix : pour toute famille d’ensembles non vides, il existe une fonction de choix. Indépendant de ZF (Gödel 1938, Cohen 1963).

Le paradoxe de Russell (1901) avait montré que la théorie naïve des ensembles était incohérente : l’ensemble R = {x | x ∉ x} mène à la contradiction. ZFC évite ce paradoxe par l’axiome de séparation (on ne peut former que des sous-ensembles d’ensembles existants).

[08]

Calculabilité & indécidabilité

La théorie de la calculabilité (également appelée récursivité) étudie quels problèmes sont calculables (décidables par un algorithme) et lesquels ne le sont pas.

✅ Décidables

  • Trier une liste
  • Tester la primalité
  • SAT (NP, mais décidable)
  • Les problèmes en P et NP

❌ Indécidables

  • Problème de l’arrêt (Halting Problem, Turing 1936)
  • Correspondance de Post
  • 10e problème de Hilbert (Matiyasevich 1970)
  • Vérité arithmétique (Tarski 1936)

Le problème de l’arrêt (Turing, 1936)

Existe-t-il un algorithme universel HALT(P, E) qui, étant donné un programme P et une entrée E, détermine si P s’arrête ? Turing démontre que non, par un argument diagonal : si HALT existait, construire le programme D(P) = « si HALT(P,P) alors boucler, sinon s’arrêter » mène à une contradiction en appliquant D à lui-même. Ce résultat fonde la théorie de la complexité et de la vérification formelle.