La logique définit les règles formelles que doit respecter tout raisonnement correct. La notion de preuve est essentielle en mathématiques et plus généralement dans toutes les activités scientifiques. Il ne s’agit pas juste de déterminer ce qui est vrai ou faux mais d’être capable de donner des explications qui justifient que le résultat annoncé est valide. Il y a donc des règles du jeu à suivre qui doivent être assez simples pour que chacun puisse se convaincre qu’il n’y a pas tricherie.
L’objectif de cette partie du cours est de mieux comprendre la structure des énoncés mathématiques et des preuves afin de mieux les maitriser et de faire moins d’erreurs dans leur utilisation générale.
La première étape consiste à introduire des notations rigoureuses et standardisées pour représenter des énoncés. On parle de langage formel. Les informaticiens sont particulièrement sensibles à cet aspect car c’est une étape essentielle pour que les ordinateurs puissent manipuler de manière pertinente de tels objets.
Une formule décrit une propriété (vraie ou fausse) d’objets (par exemple des entiers, mais aussi des ensembles, des fonctions …). Pour décrire les objets, on dispose de constantes comme 0, 1, ∅…, d’opérations +, ×, ∪,…Une opération s’applique à des objets pour former de nouveaux objets. Par exemple 3+2 est un objet qui est obtenu en appliquant l’opération + aux deux constantes 3 et 2. Chaque opération s’applique à un nombre fixe d’objets, par exemple 3+2 représente un objet mais 3+ ne représente rien.
On utilise également des variables qui sont des symboles permettant de représenter des objets arbitraires comme par exemple dans l’objet x+1.
Les formules atomiques incluent ⊤ (la propriété vraie) et ⊥ (la propriété fausse). On peut aussi introduire des symboles de prédicat comme l’égalité = ou la comparaison ≤. Un symbole de prédicat associé à un ou plusieurs objets est une formule atomique.
Les formules composées se construisent à l’aide de connecteurs logiques. On distingue la partie dite propositionnelle :
Et les quantificateurs du premier ordre :
On peut introduire plusieurs variables dans un quantificateur, par exemple : ∀ x y, P représente la formule ∀ x, ∀ y, P.
Comme pour les formules arithmétiques, il y a des règles de précédence pour les connecteurs logiques qui évitent l’utilisation des parenthèses. La précédence de ¬ est la plus forte, vient ensuite la conjonction ∧ puis la disjonction ∨ et finalement l’implication ⇒. Ces connecteurs associent à droite.
Dans ce cours, les quantificateurs ∀ et ∃ ont une précédence plus faible que les autres opérateurs. Leur portée s’étend donc aussi loin que possible.
Pour définir quand une formule est vraie, il faut se placer dans un modèle qui explicite de quels objets on parle et également pour chaque symbole de prédicat, nous dit pour quels objets il est vérifié.
Par exemple 2 ≤ 4 est vrai mais 0=1 est faux.
Certaines propriétés peuvent être vraies dans un modèle et fausses dans un autre, par exemple ∀ x, x < 2 ⇒ x ≤ 1 est vrai si on considère les entiers mais faux si on s’intéresse aux rationnels.
Une fois que l’on connait quelles formules atomiques sont vérifiées, on peut définir quand une formule composée est vraie en fonction de la véracité des formules qui la composent. On utilise la valeur V pour une formule vraie et la valeur F pour une formule fausse.
|
Pour savoir si une formule propositionnelle est vraie, il “suffit” de la décomposer pour se ramener à la vérité des formules atomiques qui la composent.
Dans le cas où certains symboles de prédicats ne sont pas définis, ils sont vus comme des inconnus. On pourra s’intéresser à savoir si une formule est vraie pour toutes les interprétations possibles de ces prédicats (pour tous les modèles). Si c’est le cas on dira que la formule est valide ou encore que c’est une tautologie. Si la formule est vraie pour certaines interprétations, on dit que la formule est satisfiable, si elle est fausse dans toutes les interprétations alors elle est dite insatisfiable.
On peut faire le parallèle avec des identités remarquables en mathématiques (x+y)2=x2+2xy+y2 est toujours vrai, x+y=3 est vrai pour certaines valeurs de x et de y, x+1=0 est toujours faux (sur les entiers naturels). Connaitre des formes standard de propriétés logiques toujours vraies ou toujours fausses permet de raisonner plus rapidement sans refaire de calculs.
Une formule logique peut contenir des variables qui représentent des objets arbitraires.
Une formule P avec variables représente un ensemble de formules closes obtenues en remplaçant les variables par des objets du modèle.
Par exemple x ≤ y est une formule avec deux variables x et y. Se poser la question de savoir si cette formule est vraie nécessite d’expliciter comment on traite les inconnues x et y.
Les variables représentent des objets arbitraires. On peut donc les remplacer dans une formule par d’autres objets (qui peuvent eux-mêmes contenir des variables). On notera P[x← t] la formule obtenue en remplaçant x par t dans P.
On ne peut pas dire a priori si une formule avec variable est vraie ou fausse. Il faut au préalable expliciter comment les variables sont interprétées. On pourra s’intéresser à s’il existe des objets pour lesquels la formule est vraie ou à une propriété plus forte qui dit que la formule est vraie quelle que soit la manière dont on remplace les variables.
Dans les formules ∀ x, P et ∃ x, P, la
variable x est dite liée, en effet les occurrences de
x sont reliées au quantificateur correspondant et on peut
changer le nom de manière cohérente dans P et le
quantificateur sans changer le sens de la formule:
∀ x, ∃ y, x < y exprime la même propriété que
∀ t, ∃ u, t < u. Une variable x qui
apparait dans une formule P mais qui n’est pas dans une
sous-expression de la forme ∀ x, Q ou ∃ x,
Q est dite libre. Par exemple dans la formule
∃ y, x < y, la variable x est libre et y
est liée.
une variable peut à la fois apparaître en position libre et en position liée, ou bien apparaître liée dans plusieurs quantificateurs comme y dans la formule 0<x× y ∨ (∃ y, x < y) ∧ (∃ y, y+y < x). Cependant ces trois positions ne représentent pas la même chose car on peut toujours choisir un nom nouveau pour les variables liées. La formule pourra s’écrire: 0<x× y ∨ (∃ y1, x < y1) ∧ (∃ y2, y2+y2 < x).
La vérité d’une formule avec des quantificateurs du premier ordre dépend en général de l’exploration de la vérité d’un ensemble infini de formules (obtenues en remplaçant les variables par des objets arbitraires).
Plutôt que de calculer des valeurs de vérité (ce qui peut être très fastidueux), on peut formaliser des étapes de raisonnement qui nous permettent d’aller plus vite.
Par exemple un principe bien connu est le “modus ponens” : si on a établi d’un côté que P⇒ Q est vrai et de l’autre que P est vrai alors on peut en déduire que Q est vrai.
L’activité de preuve ne consiste pas juste à déterminer si un énoncé est vrai ou non, mais s’intéresse plutôt à des étapes de raisonnement qui à partir d’un certain nombre d’hypothèses (des énoncés qui sont supposés vrais), déduisent une conclusion (un autre énoncé) que l’on cherche à établir.
On peut ainsi avoir des principes de preuve plus élaborés. Par exemple si à partir d’une hypothèse ¬ H on est capable d’établir la propriété P mais aussi d’établir la proprété contraire ¬ P alors c’est qu’il y a une contradiction et donc que l’hypothèse ¬ H est fausse, cela permet de justifier que H est vrai (on a raisonné par l’absurde). Un autre exemple est si d’une hypothèse H on est capable d’établir la propriété P et à partir de l’hypothèse contraire ¬ H on est aussi capable d’établir la propriété P c’est que P est vrai sans aucune hypothèse (il s’agit d’un raisonnement par cas).
Pour établir la validité des formules, on va donc utiliser des systèmes de déduction qui permettent de déduire qu’une formule (la conclusion) est une conséquence logique d’un ensemble de formules (les hypothèses).
On écrit cette relation Γ ⊢ P avec Γ un ensemble de formules (que l’on pourra aussi écrire H1,…,Hn en explicitant les formules) et P une formule. On appelle cet objet un séquent. Les formules de Γ sont appelées les hypothèses et la formule P est la conclusion du séquent.
L’interprétation de cette relation est que si on a pu dériver Γ ⊢ P et que les formules dans Γ sont vraies alors la formule P est vraie.
Il existe plusieurs systèmes de preuve, nous utiliserons un système appelé calcul des séquents (avec une seule formule conclusion). Ce système organise les étapes de déduction en deux catégories en fonction du connecteur principal d’une formule P. Les étapes d’introduction (à droite du signe ⊢) qui expliquent comment on peut établir une dérivation de Γ ⊢ P et des règles d’élimination d’hypothèses (à gauche du signe ⊢) qui expliquent comment on peut exploiter une hypothèse P.
Une démonstration dans ce système se construit sous la forme d’un arbre dont la racine est le séquent à prouver et dont chaque nœud correspond à une des règles de la logique. Les feuilles seront formées des règles qui n’ont pas de conditions.
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Un schéma de preuve très utile s’appelle la coupure. Il s’agit pour prouver une propriété B, d’introduire une propriété A comme une nouvelle hypothèse qui va aider à prouver B et que l’on va prouver par ailleurs. C’est exactement la procédure suivie lorsque l’on introduit un lemme intermédiaire. Ce principe appelé coupure s’énonce ainsi sous forme de règle d’inférence.
|
|
|
|
|
|
|
A partir des règles de base données précédemment, on peut déduire des règles avancées qui permettent de faire des preuves plus courtes.
On remarque que si une formule F est une conséquence d’hypothèses Γ alors a fortiori F est une conséquence d’un ensemble d’hypothèses Γ′ qui contient les hypothèses de Γ. C’est vrai pour la règle hypothèse, puis c’est préservé par toutes les règles.
Ce principe s’énonce ainsi : si Γ ⊢ A et Γ ⊆ Γ′ alors Γ′ ⊢ A. On peut aussi l’écrire sous forme de règle d’inférence :
|
On peut donc oublier des hypothèses inutiles lorsque l’on construit une preuve de bas en haut.
La règle de modus ponens mentionnée précédemment peut se déduire des règles précédentes.
Un système de déduction doit également comporter des règles pour prouver les formules atomiques.
Une théorie importante est celle de l’égalité. Les règles pour l’égalité sont :
|
|
On retrouve ici aussi une règles d’introduction et une règle d’élimination d’hypothèse. La deuxième règle traduit le fait que si l’égalité t=u est vérifiée alors on peut remplacer t par u dans une formule quelconque sans en changer la vérité.
|
| ∀ x y, x+1=y+1 ⇒ x=y ∀ x, 0≠x+1 ∀ y, 0+y=y ∀ x y, (x+1)+y=(x+y)+1 |
| ∀ x y, x+y=y+x ∀ x y z, x+(y+z)=(x+y)+z |
|
|
Il y a plusieurs manières d’interpréter une formule logique suivant le domaine dans lequel on se place. Par exemple la formule ∀ x, ∃ y, y < x est vraie si on se place sur les entiers relatifs avec l’interprétation usuelle de la relation < mais fausse si on se place sur les entiers naturels, elle peut redevenir vrai pour une autre interprétation de la relation <.
Un séquent Γ ⊢ A est valide si toute interprétation qui rend vrai les formules de Γ rend aussi vraie la formule A.
Un système de démonstration est correct s’il ne permet de dériver que des séquents valides. Il est complet s’il permet de dériver tous les séquents valides.
Le calcul des séquents proposé est correct, il suffit de vérifier individuellement chacune des règles proposées.
Le calcul est aussi complet, dans le sens que si une formule est vraie pour toute interprétation possible des symboles de fonction et de prédicat alors il sera possible de la prouver dans le calcul des séquents donnés.
Mais en général, on s’intéresse à démontrer si une formule est vraie dans les entiers (ou les réels, ou tout autre structure).
L’ensemble d’axiomes proposé précédemment pour raisonner sur les entiers naturels ne donne pas un système complet. Par exemple la propriété ∀ x,x≠x+1 qui est vraie n’est pas démontrable. En effet on peut construire un modèle avec les entiers usuels plus un objet infini ∞ tel que ∞+1=∞. Toutes les règles logiques données pour les entiers sont vérifiées mais pas ∀ x,x≠x+1.
Il nous manque en particulier le principe de raisonnement par récurrence qui pourra s’écrire:
|
qui exprime qu’un entier est de la forme 0+1+⋯ +1.
Cependant l’ajout de la récurrence ne suffit pas à faire un système complet, c’est ce qu’établit le théorème d’incomplétude de Gödel : dans un système logique qui est cohérent (ne peut pas tout montrer) et assez puissant pour contenir l’arithmétique, alors il existe des formules vraies qui ne sont pas prouvables.
Des outils informatiques permettent de faire des preuves sur ordinateur.
Certains outils font de la démonstration automatique, ils prennent en entrée un problème (par exemple sous la forme Γ ⊢ A) et se placent dans une certaine logique. Ils établissent si oui ou non le problème donné est valide (ou satisfiable) dans la logique.
Dans la pluspart des logiques un peu expressives, le problème est indécidable, c’est-à-dire qu’il n’existe pas de programme informatique qui répond exactement à la question. On peut avoir des programmes qui répondent partiellement, c’est-à-dire que dans certains cas, ils ne pourront pas dire si le problème est valide ou non.
Si on se place dans le fragment propositionnel (pas de quantificateurs) alors on peut savoir si une formule est satisfiable, valide ou non. Les SAT-solvers sont des outils qui permettent de traiter des problèmes propositionnels. L’idée est d’avoir des variables pour des propositions atomiques qui peuvent valoir vrai ou faux, puis de décrire un problème sous la forme de contraintes sur ces variables exprimées comme des formules propositionnelles. L’outil détermine s’il existe une manière d’affecter une valeur vrai ou faux à chaque variable propositionnelle qui rende le problème vrai.
Les SAT-solvers utilisent des algorithmes sophistiqués pour pouvoir traiter des formules avec un très grand nombre de variables propositionnelles.
Sur le problème du Sudoku, on voit qu’utiliser des formules du premier ordre avec des variables pour représenter les positions et les chiffres permet de factoriser la description. Au lieu des variables propositionnelles, on introduira un symbole de prédicat pos(i,j,k) qui sera vrai lorsque le chiffre k est à la position (i,j). D’autres fragments de logique sont décidables comme l’arithmétique linéaire (l’addition mais pas la multiplication). Cependant les procédures pour résoudre de tels problèmes ont une forte complexité.
Des outils comme les SAT-solvers sont utilisés pour vérifier des programmes, ou bien pour résoudre des problèmes de planification qui seront modélisés de manière logique.
Si établir la vérité d’un problème Γ ⊢ A est complexe, il est par contre élémentaire de vérifier qu’une démonstration de ce même problème suit les règles de déduction de la logique. C’est ce que font les assistants de preuve. Ils proposent des environnements qui permettent de construire interactivement des preuves. L’utilisateur indique les étapes de démonstration et l’ordinateur maintient l’état du problème : ce qui a été démontré, ce qu’il reste à résoudre. On peut ainsi construire de grosse preuves en garantissant la correction du résultat. L’environnement peut également aider à construire des preuves complexes en introduisant des étapes de preuve qui correspondent à un enchainement de règles logiques élémentaires.
Dans les travaux pratiques de ce cours nous utiliserons l’assistant de preuve Coq. Cet outil est utilisé à la fois pour garantir la correction de programmes (sécurité de la plateforme JavaCard, preuve de compilateurs, algorithmes de calculs sur les flottants, cryptographie …), mais aussi pour des preuves mathématiques avancées (théorème des 4 couleurs, conjecture de Kepler, classification des groupes finis …).