Logique formelle/Calcul des prédicats
Apparence
Le calcul des prédicats est aussi appelé logique du premier ordre et permet de faire de la logique sur des fonctions, des relations et de quantifier des relations sur les variables. Plus formellement, on commence par définir le langage sur lequel porte cette logique, c'est-à-dire :
- un ensemble de connecteurs, qui sont ceux de la logique des propositions auquel on ajoute "quel que soit" et "il existe"
- un ensemble au plus dénombrable de variables V
- un ensemble de constantes C
- un ensemble de relations R. Chaque relation aura pour vocation d’être vraie ou fausse (suivant les valeurs de ses arguments). Elle a une arité, soit un nombre d'arguments.
- un ensemble de fonctions F, chaque fonction a également une arité.
Par exemple, le langage associé à la logique sur les nombres entiers est constitué:
- d'un ensemble de variables, disons x,...,x_n,....
- d'un ensemble de variables, C est composé de 0,
- F sera l’ensemble dont la seule fonction est la fonction successeur d'arité 1, c'est-à-dire que si x est une variable ou une constante, on peut former s(x)
- R comprendra l'égalité, d'arité 2. Au lieu de noter =(x,y), on prend souvent x = y
Pour l'instant, il n'y a pas de notion de modèle ou d'entier, on définit juste les constituants du langage. Pour le définir, il faudra parler de terme, qui illustre ce qu'on peut faire avec les fonctions, les constantes et les variables. Ensuite seulement, nous construirons le langage.
- Une variable ou une constante est un terme
- Si f est une fonction d'arité k et si a1, ... ak sont des termes, alors f(a1, ..., ak) est un terme
- Un terme clos est un terme sans variable
- Un terme est un élément du langage
- Si R est une relation d'arité k et si a1, ..., ak sont des termes, alors R(a1,...ak) est un élément du langage
- Si A est un élément du langage, "non A" aussi
- Si A et B sont des éléments du langage, il en est de même de "A et B", "A ou B", "A implique B", "A équivaut à B"
- Si A est un élément du langage et x une variable, alors "il existe x tel qu'A" et "pour tout x on a A" aussi