La logique s’intéresse à la notion de vérité et de raisonnement. Un raisonnement est un discours qui permet d’établir la vérité d’un fait. Dans ce cours, nous nous intéressons à la logique mathématique qui s’appuie sur un langage formel et un ensemble de règles fixé. Le raisonnement ne sera donc pas un discours en langue naturel mais une suite bien précise de constructions qui obéissent à des règles du jeu définies.
Dans ce chapitre nous introduisons le langage de la logique du premier ordre, appelée aussi calcul des prédicats.
On utilisera un langage formel pour écrire les propositions afin d’éviter les ambiguïtés du langage naturel ou des notations imprécises. Dans le langage naturel, le même mot peut refléter des situations logiques différentes. On le voit dans les énoncés ci-dessous avec différents sens pour le connecteur ou qui a souvent dans le langage courant un sens exhaustif (l’un des deux mais pas les deux), ou encore dans la dernière phrase dans laquelle le concept d’être une étoile représente deux réalités différents (entre l’astre et la vedette).
Un langage formel présente également moins de redondance que le langage naturel dans lequel la même situation logique peut s’exprimer de plusieurs manières différentes. Les langages formels sont donc plus simples à étudier et à représenter en machine.
Une formule décrit une propriété (vraie ou fausse) qui en général va parler d’objets (on dit aussi des termes), par exemple des entiers, des figures géométriques, mais aussi des ensembles, des fonctions, des objets dans une base de données ….
Pour décrire les objets, on introduira un langage spécifique formé de symboles qui sont juste des suites de caractères spécifiques. Chaque symbole utilisé dans le langage des objets est défini avec une arité qui est un entier naturel représentant le nombre d’arguments qu’il faut associer au symbole pour représenter un nouvel objet.
Lorsqu’un symbole est d’arité 0, on dit que c’est une constante. Cela représente donc un objet sans nécessité d’argument supplémentaire. Ce sont les objets de base.
Par exemple on peut introduire 0, 1, ∅ comme des constantes particulières. Un symbole d’arité 1 est dit symbole unaire. On peut par exemple introduire un symbole unaire sqrt pour représenter l’opération de racine carrée ou bien P pour représenter l’ensemble des parties d’un ensemble. Un symbole d’arité 2 est dit symbole binaire, c’est le cas des symboles pour repésenter les opérations arithmétiques +, × ou bien l’union de deux ensembles.
Le langage des objets utilise également des variables d’objets qui sont aussi des symboles qui représente des objets, mais contrairement aux constantes, ils ne désignent pas un objet particulier, mais sont une manière de nommer un objet arbitraire comme par exemple dans l’expression x+1.
On note T(F,X) l’ensemble des termes sur la signature F et l’ensemble des variables X. On notera T(F) le sous-ensemble de ces termes qui ne contiennent pas de variable, appelés aussi termes clos.
La manière d’écrire le terme peut varier suivant les systèmes mais la structure du terme (variable ou symbole associé à 0, 1 ou plusieurs termes) reste la même.
Les formules atomiques représentent une notion qui peut être vraie ou fausse et que l’on ne peut pas décomposer sur une base logique. Il s’agit plutôt de propriétes que l’on observe plutôt que des formules logiques sur lesquelles on peut raisonner.
Parmi les formules atomiques, on distingue deux objets spéciaux : la formule notée ⊤ (aussi appelé formule vraie, ou tautologie) qui est toujours vraie et la formule ⊥ qui est toujours fausse, aussi appelée contradiction.
Les formules atomiques qui ne sont pas ⊤ ou ⊥ sont construites à partir de symboles de prédicat. Elles servent à représenter des propriétés de base des objets.
Un symbole de prédicat est juste une suite de caractères à laquelle on va pouvoir attribuer ultérieurement un sens. Comme pour les symboles d’objets, on associe à un symbole de prédicat un entier naturel que l’on appelle une arité. Cet entier correspond au nombre d’arguments représentants des objets qu’il faudra associer au symbole pour en faire une formule. On peut faire une analogie entre un symbole de prédicat et une procédure en programmation à laquelle on passe des arguments avant de pouvoir l’exécuter.
On dispose souvent (mais pas tout le temps) d’un symbole de prédicat binaire (arité 2) pour représenter l’égalité. On note de manière infixe t=u, le symbole d’égalité appliqué aux deux termes t et u.
Un symbole de prédicat est juste un nom (syntaxe). La sémantique lui attribue un sens en lui associant une relation mathématique entre les objets modélisés. Il y a parfois un sens implicite (par exemple l’égalité ou l’ordre sur les entiers) mais d’un point de vue logique, de nombreuses interprétations sont possibles.
L’arité d’un symbole de prédicat peut être 0. Le symbole de prédicat représente alors à lui tout seul une formule vraie ou fausse. On parle alors de variable propositionnelle. On verra que c’est un cas important, car avec seulement des variables propositionnelles, la logique (que l’on appelle alors logique propositionnelle) devient décidable. De nombreux problèmes peuvent se modéliser en logique propositionnelle, quitte à introduire des milliers de variables propositionnelles et de formules.
Les symboles se choisissent en fonction du problème à modéliser et il y a souvent plusieurs manières de faire.
Etant donnée une situation à représenter en logique, il peut être demandé de la modéliser et donc de trouver les bons symboles à introduire pour pouvoir représenter le problème. Dans d’autres situations, le langage peut être imposé (comme lorsque on doit utiliser l’interface d’une bibliothèque donnée) et il faudra se limiter aux symboles autorisés.
La notation standard pour un symbole f d’arité au moins 1 (symbole de fonction ou de prédicat) est f(t1,…,tn).
Pour certains symboles binaires (d’arité 2), on utilise parfois plutôt une notation infixe, c’est-à-dire que l’on écrira t ∘ u plutôt que f(t,u). Par exemple : t + u, t × u pour des termes et t = u, t ≤ u pour des formules atomiques …
Les formules complexes se construisent à partir des formules atomiques à l’aide de connecteurs logiques. On distingue la partie dite propositionnelle :
on ajoute les quantificateurs du premier ordre :
La quantification universelle peut se voir comme une conjonction généralisée sur tous les x possibles (il peut y en avoir une infinité, pas forcément dénombrable). La quantification existentielle peut se voir comme une disjonction généralisée, elle aussi possiblement infinie.
On pourrait ajouter dans la définition des formules complexes, l’utilisation du connecteur logique d’équivalence, mais nous utiliserons plutôt la notation A ⇔ B comme un raccourci pour la formule (A ⇒ B) ∧ (B ⇒ A).
On peut introduire plusieurs variables dans un quantificateur, par exemple : ∀ x y, P représente la formule ∀ x, ∀ y, P.
Dans le langage de la logique, on distingue deux catégories syntaxiques, les objets et les formules. En particulier, il y aura des symboles de fonctions (comme 0 ou +) qui permettent de construire des objets et des symboles de prédicat pour construire les formules. La catégorie des termes (ou objets) se construit à partir des données suivantes
et se décrit syntaxiquement par les règles :
|
La catégorie des formules logiques se construit à partir des symboles de prédicats
et se décrit syntaxiquement par les règles :
|
En utilisant un symbole de prédicat unaire N, tel que N(x) représente le fait que x∈ℕ, donner des formules de la logique du premier ordre qui représentent les deux quantifications ensemblistes ∀ x∈ℕ,P et ∃ x∈ℕ,P.
Une formule peut se voir comme un arbre dont les nœuds internes sont les connecteurs logiques (les connecteurs propositionnels sont binaires, sauf la négation qui est unaire) et les quantificateurs ∀ x, ∃ x qui sont des nœuds internes unaires. Les feuilles de l’arbre sont les formules atomiques.
On peut ainsi dessiner sous forme d’arbre la formule (P ⇒ Q ⇒ ∀ x, R) ⇒ P ∧ ∃ x, Q ⇒ R :
Cette représentation arborescente pourra être utilisée si on veut représenter les formules en machine. C’est aussi elle qui va nous servir pour construire des fonctions sur les formules et aussi pour raisonner sur les formules.
La définition des formules complexes correspond à une méthode de construction des formules à partir des formules atomiques. Néanmoins si on écrit simplement P ∧ Q ∨ R il y a une ambiguïté: cette formule peut se construire de deux manières différentes suivant si on utilise d’abord la règle pour la disjonction puis la conjonction ou bien dans l’autre sens. Pour lever cette ambiguïté, on utilise des parenthèses et on pourra écrire P ∧ (Q ∨ R) ou bien (P ∧ Q) ∨ R. Les parenthèses sont importantes car les deux formules ne sont pas vraies en même temps (prendre P faux et Q et R vrai).
Comme pour les formules arithmétiques, il y a des règles de précédence pour les connecteurs logiques qui évitent l’utilisation systématique des parenthèses. La précédence de ¬ est la plus forte, vient ensuite la conjonction ∧ puis la disjonction ∨ et finalement l’implication ⇒.
Dire que ¬ a une précédence plus forte que ∧ signifie que la formule ¬ P ∧ Q doit se parenthéser en (¬ P) ∧ Q et pas en ¬ (P ∧ Q). De même dire que ∧ a une précédence plus forte que ⇒ signifie que P ⇒ Q ∧ R se parenthèse comme P ⇒ (Q ∧ R) et pas (P ⇒ Q) ∧ R. On commence par mettre les parenthèses autour du connecteur dont la précédence est la plus forte.
Les connecteurs ∧, ∨ et ⇒ associent à droite, ce qui signifie que la formule P⇒ Q⇒ R se parenthèse en P⇒ (Q⇒ R) et pas (P⇒ Q)⇒ R.
L’ordre des parenthèses ne change pas le sens des formules pour les connecteurs ∧ et ∨, par contre dans le cas de l’implication, les formules P⇒ (Q⇒ R) et (P⇒ Q)⇒ R ne disent pas du tout la même chose, il faut donc être très attentif à ne pas se tromper.
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.
Dans les formules ∀ x, P et ∃ x, P, la
variable x est dite liée (on dit aussi muette), 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
apparaît 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. Cette formule représente le fait que “Il existe un nombre plus grand que x”.
En langage courant, le plus souvent, on n’introduit pas de nom explicite pour les variables liées, comme dans les exemples suivants :
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).
Les variables libres représentent des paramètres de la formule par exemple dans la formule ∃ y, x=2× y, la variable x est libre, la formule représente la notion “x est pair”, qui dépend de x. Cette formule est vraie ou fausse en fonction de la valeur de la variable x. On peut faire une analogie avec une variable globale d’un programme qui devra avoir une valeur pour permettre une exécution.
Une variable libre peut être remplacée par un terme plus complexe, on parle de substitution, par exemple
Attention au phénomène de capture lorsqu’on substitue une variable par un terme. Supposons que l’on veuille écrire la formule “3× y est pair” :
Il y a deux valeurs de vérité vrai et faux. On les représente par les éléments de l’ensemble B={V,F} des booléens. L’élément V correspond à vrai et F à faux. On utilise parfois les entiers {1,0} à la place, mais il est préférable de ne pas confondre valeur de vérité et valeur entière, d’où le choix de notations spécifiques.
Pour définir quand une formule quelconque est vraie, il faut se placer dans un modèle (on parle aussi d’interprétation) qui explicite de quels objets on parle et également pour chaque symbole de prédicat (propriété atomique), nous dit pour quels objets il est vérifié.
Par exemple, dans le modèle usuel des mathématiques 2 ≤ 4 est vrai mais 0=1 est faux. L’énoncé «Anne est l’amie de Bob» peut être vrai dans certaines situations et faux dans d’autres. L’énoncé «Tout le monde a les yeux bleus» sera vrai ou faux en fonction en fonction de notre interprétation de «tout le monde», suivant si on se restreint a une famille donnée ou bien si on considère l’ensemble de la population française.
Une formule logique complexe contient des connecteurs logiques qui ont un sens précis.
La formule atomique ⊥ est toujours fausse et la formule atomique ⊤ est toujours vraie.
Les tables suivantes rappellent les valeurs de vérité des connecteurs propositionnels en fonction des valeurs de vérité des composants de la formule.
|
|
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.
Si une formule propositionnelle ne contient pas de variables propositionnelles ni de symboles de prédicats, alors on peut calculer sa valeur de vérité en utilisant les tables ci-dessus.
Par exemple ((⊥⇒ ⊥) ⇒ ⊥) ⇒⊥ est une formule propositionnelle qui est toujours vraie.
Les formules sans variables ne sont pas très intéressantes à étudier. On va donc se placer dans le cas d’une formule propositionnelle (pas de quantificateur) qui ne contient comme symbole de prédicat que des variables propositionnelles (symbole d’arité 0, sans argument).
Une variable propositionnelle dans une formule peut prendre soit la valeur vrai, soit la valeur faux. C’est une inconnue du problème. Une formule propositionnelle contient un nombre fini de variables propositionnelles que l’on note X1,…, Xn. Chacune peut prendre comme valeur vrai ou faux. Il y a donc en tout 2n possibilités. Chaque choix correspond à une interprétation. Si on fixe une interprétation, alors on peut calculer la valeur de vérité de la formule en utilisant les tables ci-dessus.
Chaque ligne correspond à une interprétation différente de X1,…, Xn et contient dans la colonne P, la valeur de la formule P dans cette interprétation.
La table de vérité contient a priori 2n lignes (une par interprétation). Cependant la valeur de vérité d’une formule ne dépend parfois que de la valeur d’une ou deux variables propositionnelles, on s’autorisera alors à n’écrire qu’une seule ligne, en laissant les valeurs des autres variables indéterminées (et donc cette ligne représentera plusieurs interprétation qui donnent pour lesquels la valeur de P est la même).
|
|
|
On va 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.
Attention insatisfiable est la négation de satisfiable, mais ne pas être valide (au moins une interprétation rend fausse la formule) ne signifie pas être insatisfiable (toutes les interprétations rendent fausses la formule). Une formule valide (toutes les interprétations rendent vraie la formule) est a fortiori satisfiable (au moins une interprétation rend vraie la formule), une formule non valide (au moins une interprétation rend la formule fausse) peut être satisfiable (une autre interprétation rend vraie la formule) ou insatisfiable (la formule est tout le temps fausse).
Il y a cependant un lien direct entre validité et satisfiabilité grace à l’opération de négation sur les formules. En effet pour toute formule P (propositionnelle ou non), La formule P est valide si et seulement si la formule ¬ P est insatisfiable. Savoir répoudre un des problèmes est donc équivalent à savoir résoudre l’autre.
Le calcul propositionnel permet de modéliser et de résoudre des problèmes. En plus de pouvoir décider si une formule est valide, on peut également répondre à la question pour quelles valeurs des formules atomiques la propriété sera-t-elle vérifiée ? ou bien à la question combien y-a-t-il de solutions différentes ?
Des inscriptions sur les portes guident leur choix:
La porte 1 comporte la mention “Il y a une princesse derrière cette porte et un tigre derrière l’autre”, la porte 2 comporte la mention “Il y a une princesse derrière une des portes et un tigre derrière l’autre”, on sait de plus qu’une seule de ces inscriptions est vraie.
On introduit les variables propositionnelles P1 (resp. P2) pour représenter la présence d’une princesse derrière la porte 1 (resp. la porte 2).
Le sens commun de la formule ∀ x,P est que P doit être vrai pour tous les x mais cela ne peut avoir un sens que si on explique ce que représente x.
Avant de pouvoir dire quelle est la valeur de vérité de ∀ x,P, il faut donc préciser notre interprétation des symboles. S’il y a des quantificateurs, c’est qu’il y a des objets et donc il faut préciser de quels objets on parle. On se donne donc un ensemble, appelé domaine de l’interprétation (on dira aussi plus simplement domaine) qui représente l’univers auquel appartiennent nos objets. Cet ensemble doit être non vide. On fait correspondre à chaque constante, un élément de notre domaine. Deux constantes qui ont des noms différents dans la logique peuvent parfaitement correspondre à la même valeur dans le domaine. A chaque symbole de fonction de la logique, va correspondre une fonction sur le domaine. Pour faire un parallèle avec la programmation, les symboles utilisés de la logique correspondent à l’interface d’un module à partir duquel on peut construire de nouveaux programmes alors que l’interprétation va correspondre à l’implémentation du module qui va vous permettre d’exécuter vos programmes. Le comportement de ces programmes peut complètement changer en fonction de l’implémentation du module.
Une formule atomique P(t1,…,tn) représente une vérité qui dépend évidemment de la valeur des arguments t1,…,tn. On peut choisir l’interprétation de P parmi toutes les relations n-aires sur le domaine de l’interprétation.
Si on a un prédicat unaire comme yeux-bleus l’interprétation revient à choisir le sous-ensemble des individus qui ont les yeux bleus. Si on a une relation binaire comme ami ou ≤, l’interprétation peut se représenter comme un graphe orienté dont les sommets sont les éléments du domaine et dans lequel une arête de s à t sera présente lorsque la relation est vraie entre s et t.
Même si la formule ne contient qu’un symbole de prédicat, si le domaine est infini, le nombre d’interprétations possibles est lui-même infini et donc on ne peut plus faire une table de vérité qui énumère toutes les interprétations.
Par contre si on exhibe une interprétation qui rend vraie la formule, on sait qu’elle est satisfiable et si on trouver un contre-exemple (une interprétation qui rend fausse la formule) alors on sait qu’elle n’est pas valide.
Nous verrons dans les chapitres 2 et 4 des méthodes pour simplifier la recherche.
La vérité d’une formule sans variable libre mais 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 interprétant les variables par des objets arbitraires).
Une formule est un élement de syntaxe qui utilise des symboles qui peuvent avoir de nombreuses interprétations différentes.
Si au contraire on part d’un univers et qu’on s’intéresse à certaines opérations et certaines propriétés dans cet univers, on peut essayer de modéliser cet univers en introduisant un ensemble de symboles et un ensemble d’énoncés A tel que notre univers corresponde à un modèle qui rend vraies toutes les formules de A.
On pourra alors travailler au niveau de la logique à partir de cet ensemble d’axiomes et en déduire des propriétés de l’univers qui nous intéresse.
Les mathématiciens se sont intéressés depuis l’antiquité à trouver des présentations axiomatiques de théories. Par exemple Euclide a formalisé un ensemble d’axiomes pour la géométrie. La théorie des groupes est une généralisation du modèle des entiers relatifs : on se donne une constante 0, une opération binaire +, une opération unaire − et un prédicat binaire d’égalité. On suppose que ces opérateurs vérifient un certain nombre de propriétés logiques
et on en déduit divers conséquences qui seront vraies pour les entiers relatifs mais aussi pour toutes les autres structures de groupe.
Un modèle d’une théorie est donné par une interprétation de la signature (c’est-à-dire un ensemble domaine et des fonctions et relations sur ce domaine) telle que dans cette interprétation, tous les axiomes ont pour valeur vraie.
Une théorie peut être définie par un ensemble infini d’axiomes.
Soit une théorie définie par un ensemble A d’axiomes. Au lieu de s’intéresser à la validité d’une formule, on va se poser la question est-ce que la formule est vraie dans tous les modèle de la théorie ? ou encore est-ce qu’on peut par un raisonnement qui suppose vrais tous les axiomes de la théorie, déduire cette propriété.
La théorie A est complète si pour toute formule P on peut prouver P ou bien on peut prouver ¬ P à partir des axiomes A. Attention, on peut aussi avoir des théories incohérentes telles que on peut prouver ⊥ à partir des axiomes et donc a fortiori n’importe quelle formule P. Une théorie incohérente n’aura pas de modèle. La plupart des théories ne sont pas complètes. Le théorème d’incomplétude de Gödel nous dit que toute théorie qui contient l’arithmétique est forcément incomplète et que quelque soit les axiomes que l’on ajoute la théorie restera incomplète à moins de devenir incohérente.
Une théorie est décidable, si on sait, pour toute formule P, décider si P est ou non prouvable à partir des axiomes. La théorie vide n’est pas décidable. La théorie de l’arithmétique linéaire (sans multiplication) est décidable ainsi que la théorie des réels.
Une théorie importante est celle de l’égalité. Les axiomes nécessaires sont les suivants.
| ∀ x1… xn y1… yn, x1=y1∧…∧ xn=yn ⇒ f(x1,…, xn)=f(y1,…, yn) |
| ∀ x1… xn y1… yn, x1=y1∧…∧ xn=yn ⇒ P(x1,…, xn)⇒ P(y1,…, yn) |
Les axiomes sont données par l’ensemble P0 suivant qui constitue l’arithmétique élémentaire
La théorie formée de ces 7 axiomes est notée PA0. Cette théorie n’est pas suffisante pour prouver une propriété comme la symétrie de l’addition.
Pour obtenir l’arithmétique de Peano, on lui ajoute une infinité d’axiomes pour le schéma de preuve par récurrence. Pour chaque formule P ayant comme variables libres x1,…,xn,x, on aura comme axiome la formule
| ∀ x1… xn,P[x← O] ⇒ (∀ x, P⇒ P[x← S(x)]) ⇒ ∀ x,P |
A tout entier n∈ℕ, on associe un terme de l’arithmétique de Peano Sn(0) que l’on notera ñ.
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. Ils 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.
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).
On a vu que les formules pouvaient se représenter comme des arbres. On introduit dans cette section une méthode générale de définition récursive sur la structure des formules qui nous permet de définir des opérations ou propriétes mathématiques sur les formules ou bien de les manipuler par ordinateur.
Les formules atomiques pouvant faire référence à des termes, nous donnons également les éléments pour définir des fonctions de manière récursive sur les termes et raisonner par récurrence structurelle.
On peut définir une fonction G de l’ensemble des formules logiques dans un ensemble D quelconque en se donnant un ensemble d’équations que doit satisfaire cette fonction. Les équations sont de la forme G(t)=u avec u un élément de l’ensemble D. Il faut une équation pour chacune des constructions possibles de formule: formules atomiques (en particulier ⊤, ⊥), formules composées d’un connecteur propositionnel ¬ A, A∧ B, A∨ B, A⇒ B ou d’un quantificateur ∀ x, A, ∃ x, A.
Dans le cas des connecteurs propositionnels et des quantificateurs, le membre droit u peut utiliser la valeur de G sur des sous-formules de t (comme G(A) et G(B)). On parle de définition récursive.
On peut par exemple définir une fonction nbsymbp qui compte le nombre de connecteurs propositionnels dans une formule :
|
|
Dans les définitions ci-dessus p, A ou B ne sont pas des symboles logiques mais des variables mathématiques qui nous servent à définir la fonction (comme la variable x dans une définition f(x)=x+1), elles représentent n’importe quelle formule complexe.
Ce qui est important dans cette définition est qu’elle est complète car elle couvre tous les cas de formules, que pour chaque formule il n’y a qu’une seule équation qui s’applique et donc que la définition est non-ambigüe et finalement on dit qu’elle est bien fondée car les références à la fonction f dans les membres droits des équations se font sur des formules strictement plus petites que le membre gauche.
Ces équations définissent également un moyen de calcul de la valeur de G pour une formule donnée. Par exemple dans le cas de la formule A =def (∀ x, P ⇒ Q) ⇒ ¬ Q ⇒ ¬ ∃ x, P on aura nbsymbp(A)=5.
Le calcul propositionnel est le sous-ensemble du calcul des prédicats qui ne contient que des symboles de prédicat d’arité 0, qui sont appelés des variables propositionnelles et pas de quantificateur ni de termes. On peut de la même manière faire une définition récursive sur la structure d’une formule propositionnelle en décomposant le cas des formules atomiques en trois cas ⊥, ⊤ et les variables propositionnelles et en éliminant les deux cas des quantificateurs.
Une fois que l’on se donne une interprétation I qui à chaque variable propositionelle associe sa valeur de vérité, on peut définir une fonction val(I,P)∈B qui calcule la valeur de vérité d’une formule propositionnelle quelconque P par les équations suivantes
|
Pour établir un résultat pour toutes les formules, on peut utiliser un raisonnement par récurrence sur la structure de la formule. Soit une propriété φ(P) qui dépend d’une formule P.
Ce principe de preuve est très utile lorsque l’on veut montrer des propriétés qui parlent de fonctions sur les formules qui sont elles-mêmes définies récursivement.
|
|
Pour faire cette preuve, on commence par expliciter la propriété φ(P) que l’on cherche à montrer par récurrence structurelle sur P. Dans notre cas, il s’agit de nbatom(P)≤ 1+nbsymbp(P). On doit examiner chacun des cas possibles pour la formule P:
| nbatom(¬ A)=nbatom(A)≤ 1+nbsymbp(A)=nbsymbp(¬ A)≤ 1+nbsymbp(¬ A) |
On suppose (hypothèses de récurrence) que φ(A) et φ(B) sont vérifiés et donc que nbatom(A)≤ 1+nbsymbp(A) et nbatom(B)≤ 1+nbsymbp(B).
Il faut montrer que φ(A∘ B) est également vérifié. Par définition de nbatom et nbsymbp, on a nbatom(A∘ B)=nbatom(A)+nbatom(B) et nbsymbp(A∘ B)=1+nbsymbp(A)+nbsymbp(B).
En utilisant les hypothèses de récurrence on a donc
|
et donc on a bien montré que φ(A∘ B) était vérifiée.
On suppose (hypothèse de récurrence) que φ(A) est vérifié et donc que nbatom(A)≤ 1+nbsymbp(A).
Il faut montrer que φ(∀ x, A) et φ(∃ x, A) sont également vérifiés. On traite seulement le cas ∀ x, A car celui de ∃ x, A est identique.
Par définition de nbatom et nbsymbp, on a nbatom(∀ x, A)=nbatom(A) et nbsymbp(∀ x, A)=nbsymbp(A). En utilisant l’hypothèse de récurrence on a donc
| nbatom(∀ x, A)=nbatom(A)≤ 1+nbsymbp(A)=1+nbsymbp(∀ x, A) |
et donc on a bien montré que φ(∀ x, A) était vérifiée.
La même preuve nous donne que φ(∃ x, A) est vérifié.
On a bien examiné tous les cas possibles et prouvé par récurrence sur la structure de la formule P, que pour toute formule logique P, on a nbatom(P)≤ 1+nbsymbp(P).
En logique du premier ordre, les formules font référence à des objets qui sont représentés syntaxiquement par des termes qui apparaissent en argument des symboles de prédicat au niveau des formules atomiques.
Soit F une signature, c’est-à-dire un ensemble de symboles de fonctions définis avec leur arité et X un ensemble de variables. On note Fn l’ensemble des symboles de F d’arité n et T(F,X) l’ensemble des termes bien formés construits à partir de cette signature et de ces variables.
De la même manière que l’on fait une définition récursive sur les formules, on peut construire une fonction G de manière récursive sur les termes, en se donnant un ensemble d’équations. Il y aura une équation dans le cas où le terme est une variable x et une équation pour chaque symbole d’objet. Si on a un symbole f d’arité n alors il y aura une équation G(f(t1,…,tn))=u avec la possibilité pour u de faire référence aux résultats de la fonction G sur les sous termes et donc de mentionner non seulement les termes t1,…,tn mais aussi les valeurs G(t1),…,G(tn).
On définit une fonction clos qui étant donné un terme t teste s’il est clos, c’est-à-dire s’il ne contient aucune variable, en utilisant les équations suivantes :
|
|
On suppose que l’on veut définir une application G qui prend en argument un terme et renvoie un élément de D, on a donc G∈T(F,X) → D. Pour cela on va se donner les objets suivants :
| × |
| → A | ||||||||||||||||||||||||||||||||||||
Il existe une unique application G dans T(F,X) → D qui vérifie :
|
Le fait que l’on puisse définir une telle application est une conséquence de notre choix de l’égalité syntaxique sur les termes. On rappelle que dans l’égalité syntaxique, deux termes qui débutent par des symboles différents sont différents.
En effet ce schéma permet de définir une application G telle que G(c)=1 pour les constantes et G(t)=2 pour tous les termes qui commencent par un symbole de fonction. Si on avait plus(0,0)=0 alors on en déduirait G(plus(0,0))=G(0) et donc 2=1.
Nous avons déjà introduit la notion de remplacement d’une variable par un terme. Ici on généralise cette opération par le remplacement en parallèle de plusieurs variables par des termes. Pour cela, on se donne une application σ∈X→T(F,X), appelée substitution qui associe un terme à chaque variable. On notera {x1←u1;…;xn←un} la substitution σ telle que σ(x)=ui si x=xi et σ(x)=x sinon.
On définit pour chaque terme t, le résultat de la substitution dans t de toute variable x par σ(x) que l’on note t[σ].
Si σ est de la forme {x1←u1;…;xn←un}, alors le terme t[σ] sera noté t[x1←u1;…;xn←un].
La définition de t[σ] se fait de manière récursive sur t:
On peut montrer que le résultat de t[σ] ne dépend que de la valeur de la substitution σ sur les variables de t. De manière plus précise cela revient à montrer que si on a deux substitutions σ1 et σ2 ainsi qu’un terme t, si pour toute variable x∈vars(t) on a σ1(x)=σ2(x) alors t[σ1]=t[σ2]. La preuve se fait aisément par récurrence structurelle sur le terme t suivant le schéma ci-dessous.
On a également un schéma de preuve par récurrence sur les termes de T(F,X) qui s’exprime de la manière suivante. Soit φ(t) une propriété mathématique qui dépend d’un terme t ∈ T(F,X). On suppose :
alors our tout terme t ∈ T(F,X) la propriété φ(t) est vérifiée.
Preuve: La preuve se fait par récurrence sur la structure du terme t.
|
On en déduit que ht(t) ≤ size(t) est vérifié pour tout les termes du langage. □
On a défini formellement la fonction de substitution d’une variable par un terme dans un autre terme. On peut faire de même avec la définition de la substitution d’une variable par un terme dans une formule quelconque. On construit la fonction à l’aide d’équations récursives sur le structure de la formule.
La définition de la substitution d’une variable x par un terme t dans une formule P doit prendre en compte le problème de la capture possible d’une des variables libres du terme t par un des quantificateurs interne de P.
Cette définition est donc partielle dans le cas des formules avec quantificateurs si une variable liée dans la formule est aussi libre dans le terme que l’on veut substituer. Cependant en procédant à un renommage des variables liées dans les quantificateurs, on peut toujours se ramener à une situation dans laquelle la substitution sera possible.
Montrer par récurrence sur la structure de la formule, que la règle de substitution dans un contexte arbitraire est valide :
| t=u ⇒ P[x← t] ⇒ P[x← u] |
.
| t=u ⇒ v[x← t]=v[x← u] |