Page d'accueil	encyclopedie-enligne.com en page d'accueil
Liste Articles: [0-A] [A-C] [C-F] [F-J] [J-M] [M-P] [P-S] [S-Z] \| Liste Catégories \| Une page au hasard \| Pages liées

Calcul des prédicats

Cet article est considéré comme une ébauche à compléter, vous pouvez partager vos connaissances en le modifiant .

Le calcul des prédicats du premier ordre ou logique du premier ordre, ou tout simplement calcul des prédicats est une logique formelle qui étend la logique propositionnelle. L'originalité de cette logique est l'introduction d'un ensemble de symboles appelés variables, d'un autre ensemble de symboles représentant des prédicats, ainsi que de deux symboles $\forall$ et $\exists$ appelés quantificateurs, permettant ainsi d'exprimer des propriétés telles que : «Pour tout X, P(X).».

Ici les variables représentent des valeurs d'un certain ensemble d'objets de base donné (par exemple, les entiers naturels), les quantifications de variables se rapportent donc uniquement à cet ensemble, et les prédicats représentent des relations n-aires sur cet ensemble.

On parle de logique du premier ordre par opposition aux logiques d'ordre supérieur, où l'on peut quantifier aussi bien les objets de l'ensemble de base que des prédicats ou des fonctions sur l'ensemble de base. Il s'ensuit que les prédicats représentent ainsi des relations entre tous ces objets.

Sommaire

1 Formation d'une formule du calcul des prédicats du premier ordre

2 Formules closes, variables libres, variables liées

3 Sémantique du calcul des prédicats du premier ordre

4 Résultats de complétude et d'incomplétude

Formation d'une formule du calcul des prédicats du premier ordre

On se donne :

V un ensemble de symboles appelés variables
Une signature Σ qui est l'union de deux ensembles :
- , un ensemble de symboles de prédicats
- , un ensemble de symboles de fonctions
chaque symbole de la signature se voit affecté une arité (un entier naturel)
les symboles $\forall$ et $\exists$ , appelés quantificateurs
les symboles ¬, $\wedge$ , $\or$ et $\implies$ , qui sont les connecteurs logiques du calcul des propositions (on peut en ajouter d'autres, on peut aussi en enlever pour se contenter de ¬ et $\wedge$ , ou d'un autre système minimal)

On pourrait de contenter d'un seul quantificateur $\forall$ et de deux connecteurs logiques ¬ et $\wedge$ sans perdre en expressivité.

On appellera termes les formules composées ainsi :

$x \in V$ est un terme,
si f est un symbole de fonction n-aire et $t_1,t_2,\dots,t_n$ sont des termes, alors $f\; t_1 t_2 \dots t_n$ est un terme.

Appelons T l'ensemble des termes.

Les formules du calcul des prédicats du premier ordre sont les suivantes, et uniquement les suivantes (appelons F l'ensemble des formules):

$p\; t_1 t_2 \dots t_n$ si $(t_1,t_2,\dots,t_n)\in T^n$ , $p\in \Sigma_P$ et p est n-aire (une telle formule est appelée un atome)
$f_1\wedge f_2$ si $f_1,f_2\in F$
$f_1\or f_2$ si $f_1,f_2\in F$
$f_1\implies f_2$ si $f_1,f_2\in F$
$\neg f$ si $f\in F$
$\forall x f$ si $f\in F$ et $x\in V$
$\exists x f$ si $f\in F$ et $x\in V$

Ce système très formel peut s'instancier, par exemple en l'arithmétique en prenant pour fonctions 0-aires les nombres (entiers par exemple) pour fonctions binaires les symboles des opérations « + » et « * » et comme prédicats binaires, les symboles « = » et « < ».

Formules closes, variables libres, variables liées

Sémantique du calcul des prédicats du premier ordre

Résultats de complétude et d'incomplétude

Catégories: Logique | Wikipédia:ébauche

This site support the Wikimedia Foundation. This Article originally from Wikipedia. All text is available under the terms of the