Calcul des prédicats

Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage des mathématiques proposée par les logiciens de la fin du XIX^e siècle et du début du XX^e siècle.

Le trait caractéristique de la logique du premier ordre est l'introduction d'un ensemble de symboles appelés variables, d'un ensemble d'autres symboles désignant des relations, d'un ensemble de symboles désignant des prédicats, ainsi que des connecteurs logiques et deux quantificateurs $\forall$ (« Quel que soit », « pour tout ») et $\exists$ (« il existe au moins un ... tel que »). Cela permet ainsi de formuler des énoncés tels que, « Tout x est P » et « Il existe un x tel que pour tout y, x entretient une relation R avec y », en symboles, $\forall x (Px)$ et $\exists x \forall y (x R y)$ .

Les formules logiques déduites de ce calcul des prédicats ont pour but de s'appliquer à n'importe quel modèle, c’est-à-dire n'importe quel ensemble dans lequel les variables, les fonctions, les prédicats du calcul représentent respectivement des éléments de l'ensemble, des fonctions de cet ensemble dans lui-même, et des parties de cet ensemble. Les prédicats représentent des qualités, s’ils sont à une place (unaires), ou des relations n-aires, entre n individus de cet ensemble. Ces notions seront précisées dans la suite de cet article.

Le calcul des prédicats du premier ordre égalitaire adjoint au calcul des prédicats un symbole de relation, l'égalité, dont l'interprétation est obligée : c'est l'identité des éléments du modèle, et qui est axiomatisée en conséquence. Suivant le contexte, on peut parler simplement de calcul des prédicats pour le calcul des prédicats égalitaire.

Le calcul des propositions est la partie du calcul des prédicats qui concerne ce qui ne contient pas les notions de variables, de fonctions et de prédicats et donc pas les quantificateurs $\forall$ et $\exists$ . Il sert à formaliser essentiellement les déductions du calcul des prédicats.

On parle de logique du premier ordre par opposition aux logiques d'ordre supérieur, où l'on peut quantifier aussi bien les variables que les prédicats ou les fonctions.

Sommaire

1 Formation d'une formule du calcul des prédicats du premier ordre
2 But du calcul des prédicats
3 Notes
4 Voir également
5 Bibliographie

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

Syntaxe

Cette section donne une brève présentation du langage formel qu'est le calcul des prédicats.

On se donne pour alphabet :

Un ensemble de symboles appelés variables, toujours infini : $x$ , $y$ , $z$ , etc.
un ensemble de symboles appelés constantes, éventuellement vide : $a$ , $b$ , $c$ , etc.
un ensemble de symboles de prédicats : $P$ , $Q$ , $R$ , etc.

Chaque symbole de prédicat a une arité qui détermine le nombre d'arguments ou d'objets auxquels il est appliqué. Par exemple, le prédicat $B$ pour "est bleu(e)" a une arité d'un, tandis que le prédicat $J$ pour "joindre" a une arité de deux.

les symboles $\forall$ (quel que soit) et $\exists$ (il existe), appelés quantificateurs
les symboles $\lnot$ (non), $\land$ (et), $\lor$ (ou) et $\to$ (implique), qui sont des connecteurs que possède aussi le calcul des propositions.
les symboles de ponctuation ")" et "(".

On pourrait se contenter d'un seul quantificateur $\forall$ et de deux connecteurs logiques $\lnot$ et $\land$ en définissant les autres connecteurs et quantificateur à partir de ceux-ci. Par exemple $\exists x \; P$ est défini comme $\lnot (\forall x \; \lnot P)$ .

Les formules du calcul des prédicats du premier ordre sont les suivants, et uniquement les suivants :

$P (a, b, c,..., n)$ si $P$ est n-aire (une telle formule est appelée un atome ou une formule atomique)
¬e si e est une formule.
(e₁∧e₂) si les éléments (e₁ et e₂) sont des formules.
(e₁∨e₂) si les éléments sont des formules.
(e₁→e₂) si les éléments sont des formules.
$\forall x \; e$ si e est une formule.
$\exists x \; e$ si e est une formule.

On appelle énoncé une formule dont toutes les variables sont liées par un quantificateur (donc qui n'a pas de variable libre).

Exemples

Exemple 1

Si on se donne pour constantes les deux symboles 0 et 1, pour symboles de fonctions binaires + et ., et pour symboles de prédicats binaires les symboles = et <, alors le langage utilisé peut être interprété comme étant celui de l'arithmétique. x et y désignant des variables, x+1 est un terme, 0+1+1 est un terme clos, x<y+1 est une formule, 0+1+1<0+1+1+1 est une formule close.

Exemple 2

Si on se donne un ensemble de variables quelconque, une constante notée e, un symbole de fonction binaire noté *, un symbole de fonction unaire notée ^-1, un symbole de relation binaire =, alors le langage utilisé peut être interprété comme étant celui de la théorie des groupes. Si x et y désignent des variables, x*y est un terme, e*e est un terme clos, x=y*y est une formule, e=e*e^-1 est une formule close.

Prédicats, formules closes, formules polies, variables libres, variables liées

Lorsqu’une variable $x$ appartient à une sous-formule précédée d’un quantificateur, $\forall x$ ou $\exists x$ , elle est dite liée par ce quantificateur. Si une variable n’est liée par aucun quantificateur, elle est libre.

La distinction entre variable libre et variable liée est importante. Une variable liée ne possède pas d'identité propre et peut être remplacée par n'importe quel autre nom de variable qui n'apparaît pas dans la formule. Ainsi, $\exists x (x < y)$ est identique à $\exists z (z < y)$ mais pas à $\exists x (x < z)$ et encore moins à $\exists y (y < y)$ .

Une formule close est une formule dont toutes les variables sont liées. Un prédicat est une formule qui contient une ou plusieurs variables libres. On peut considérer les prédicats comme des concepts. Ainsi, $\forall x \exists y (x < y)$ est une formule close du langage de l'arithmétique. $\forall x (x < z)$ est un prédicat portant sur la variable z.

Une formule est dite polie lorsque d'une part aucune variable n'y a à la fois d'occurrences libres et d'occurrences liées et que d'autre part aucune variable liée n'est soumise à plus d'une mutification (on dit qu'un signe est mutificateur lorsqu'il permet de confirmer l'hypothèse d'une variable liée).

Article détaillé : Variable libre.

But du calcul des prédicats

Comme le calcul des propositions, le calcul des prédicats se donne pour but de définir quels sont les énoncés qui sont valides et quels sont ceux qui ne le sont pas. Et comme pour le calcul des propositions, il existe deux façons d'aborder cette question, l'aspect sémantique et l'aspect syntaxique. Un théorème de complétude montre l'équivalence entre ces deux aspects.

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

La théorie de la vérité des formules du calcul des prédicats a été appelée par Tarski sa sémantique. Elle est présentée dans l'article Théorie des modèles. Un modèle d'un langage du premier ordre est un ensemble dans lequel on donne un sens aux symboles du langage. On peut alors attribuer une valeur de vérité (vrai ou faux) aux formules du langage dans ce modèle. On dit qu'une formule F du langage est un théorème si cette formule est vraie dans tout modèle du langage, ce qu'on note $\vDash F$ . Par exemple, si P désigne un prédicat binaire, la formule $\exists x \forall y P(x,y) \to \forall y \exists x P(x,y)$ est un théorème. En effet, tout modèle M sera un ensemble non vide dans lequel le prédicat P sera représenté par un ensemble A de M × M. Les variables x et y se verront affectées comme valeur des éléments de M, et dire que P(x, y) est vrai signifiera que (x, y) est élément de A. Il y a alors deux cas.

Ou bien il existe un élément a de M tel que $\{(a,y), y \in M\} \subset A$ et, dans ce cas, les deux propositions $\exists x \forall y \; (x,y) \in A$ et $\forall y \exists x \; (x,y)\in A$ sont vraies (il suffit de prendre x = a), et l'implication est vraie.

Ou bien un tel a n'existe pas et la proposition $\exists x \forall y \; (x,y) \in A$ est fausse. Mais alors, quelle que soit la valeur de vérité de $\forall y \exists x \; (x,y)\in A$ , l'implication sera vraie.

L'implication étant vraie dans tout modèle, la formule est valide.

Par contre, la formule $\forall y \exists x P(x,y) \to \exists x \forall y P(x,y)$ n'est pas valide. Il suffit pour cela de prendre pour modèle un ensemble à deux éléments {a, b} et de modéliser P par l'égalité. Dans cette structure, la phrase $\forall y \exists x \; (x=y)$ est vraie alors que $\exists x \forall y \; (x=y)$ est fausse. L'implication est donc fausse et la formule est invalide.

Axiomes du calcul des prédicats

Dans le calcul des prédicats, on peut également déduire des formules au moyen de déductions relevant d'un calcul. Une déduction consiste à partir d’hypothèses, ou d’axiomes, à progresser par étapes logiques jusqu’à une conclusion selon des règles prédéfinies. Il existe plusieurs présentations possibles de ces axiomes et de ces règles.

La déduction naturelle. Les principes logiques y sont présentés d’une façon aussi proche que possible des raisonnements naturels. Elle consiste en une liste de treize règles. Elles pourraient être réduites à un plus petit nombre, mais l'évidence des principes serait moins naturelle.
Les axiomes logiques. Plusieurs systèmes d’axiomes équivalents peuvent être proposés. Cette approche, adoptée par presque tous les logiciens depuis les Principia Mathematica de Whitehead et Russell, a une grande importance à la fois métamathématique et historique. L'un des systèmes d'axiomes le plus court consiste en :

les axiomes du calcul des propositions

$f \to (g \to f)$

$(f \to (g \to h)) \to ((f \to g) \to (f \to h))$

$(\lnot f \to g) \to ((\lnot f \to \lnot g) \to f)$

les axiomes relatifs au quantificateur $\forall$

$\forall x( f \to g(x)) \to (f \to \forall x g(x))$ où x n'est pas libre dans f

$\forall x f(x) \to f(a)$ où x n'a pas d'occurrence libre dans une partie bien formée de f de la forme $\forall a, h$ (ceci pour éviter une substitution embarrassante si par exemple, f(x) est de la forme $\forall a, a < x$ ).

La règle du modus ponens : si on a prouvé $f \to g$ et

f

, alors on a prouvé

g

La règle de généralisation : si on a prouvé

f (x)

, alors on a prouvé $\forall x f(x)$ (puisque le x de la première preuve joue un rôle arbitraire).

Mais si la recherche de systèmes d'axiomes minimaux met en évidence les principes élémentaires sur lesquels peuvent s'appuyer tous les raisonnements, elle ne montre pas le caractère d’évidence naturelle des principes logiques plus généraux.

La logique du dialogue apporte également un autre éclairage sur la nature des lois logiques.
Voir aussi correspondance de Curry-Howard.

Quelle que soit la présentation abordée, les axiomes et règles peuvent être codés de façon à ce qu'une machine puisse vérifier la validité ou non d'une déduction conduisant à une formule F. Si la déduction est correcte, la formule F est dite prouvable, ce qu'on note $\vdash F$ .

Se pose alors la question suivante : y a-t-il équivalence entre la présentation sémantique et la présentation syntaxique ? $\vDash F$ est-il équivalent à $\vdash F$ ? Autrement dit :

Toute formule prouvable est-elle un théorème ? Si la validité de F est attestée par un calcul syntaxique, F est-elle valide dans tout modèle du langage utilisé ?

Réciproquement, si F est un théorème, valide dans tout modèle, peut-on montrer sa validité à la suite d'un calcul syntaxique ?

C'est à cette question que répond le théorème de complétude qui suit.

Complétude et indécidabilité

Emmanuel Kant croyait à tort que la logique de son temps, celle d’Aristote, était une science complète et définitivement achevée (préface de la seconde édition de la critique de la raison pure, 1787). Les logiciens du XIX^e siècle se sont rendu compte que la théorie d’Aristote ne dit rien ou presque sur la logique des relations. Gottlob Frege et beaucoup d'autres ont comblé cette lacune en définissant le calcul des prédicats au premier ordre.

Kurt Gödel a prouvé en 1929 (dans sa thèse de doctorat) que le calcul des prédicats est complet, au sens où on peut donner un nombre fini de principes (axiomes logiques, schémas d'axiomes logiques et règles de déduction) qui suffisent pour déduire de façon mécanique toutes les lois logiques (voir le théorème de complétude de Gödel). Il y a équivalence entre la présentation sémantique et la présentation syntaxique du calcul des prédicats. Tout énoncé universellement valide (c'est-à-dire vrai dans tout modèle du langage utilisé) est un théorème (c'est-à-dire qu'il peut être déduit d'un calcul, un système de règles logiques et d'axiomes, de façon équivalente un système à la Hilbert, la déduction naturelle, ou le calcul des séquents), et réciproquement. La logique du premier ordre est donc achevée au sens où le problème de la correction logique des démonstrations y est résolu. Elle continue cependant à faire l’objet d’importantes recherches : théorie des modèles, théorie de la démonstration, mécanisation du raisonnement...

En un sens différent, les théories « raisonnables^[1] » qui permettent de formaliser suffisamment l'arithmétique intuitive, comme l'arithmétique de Peano, ou la théorie des ensembles ne sont pas complètes : certains énoncés « vrais » ne sont pas démontrables (voir théorème d'incomplétude de Gödel).

Le calcul des prédicats est semi-décidable, dans le sens où une machine peut dresser, les uns après les autres, la liste de ses théorèmes. Mais, contrairement au calcul des propositions, il n'est pas en général décidable dans le sens où, il n'existe pas de moyen « mécanique », qui, si on se donne une formule F, permette de décider si F est un théorème ou non. La semi-décidabilité ne permet pas de conclure : la confrontation de F avec la liste des théorèmes se terminera si F est effectivement un théorème, mais dans l'attente de la terminaison, a priori on ne sait pas si le calcul des théorèmes n'a pas été mené assez loin pour identifier F comme théorème ou si ce calcul ne se terminera pas parce que F n'est pas un théorème.

Cela dépend cependant du langage utilisé, en particulier du choix des symboles primitifs (la signature). Le calcul des prédicats égalitaire monadique (n'ayant que des symboles de prédicats unaires et pas de symbole de fonction) est décidable. Le calcul des prédicats égalitaire pour un langage comportant au moins un symbole de prédicat binaire est indécidable (algorithmiquement).

Notes

↑ récursivement axiomatisables et cohérentes

Voir également

Bibliographie

Stephen Kleene, logique mathématique, Armand Colin, 1971 ou Gabay 1987, (ISBN 2-87647-005-5)
R. David, K. Nour et C. Raffalli, Introduction à la logique. Théorie de la démonstration. Cours et exercices corrigés, Dunod, 2001, (ISBN 2-10-006796-6)

v · d · m

Informatique théorique

Théorie du calcul

Calculabilité	Décidabilité et indécidabilité • Ensemble récursif • Problème de l'arrêt • Ensemble récursivement énumérable
Modèle de calcul	Automate fini •Transducteur fini •Automate sur les mots infinis •Automate à pile •Automate linéairement borné • Automate cellulaire • Machine de Turing • Thèse de Church
Modes de calcul	Concurrence • Parallèlisme • Théorie de l'ordonnancement
Mesure et échelle de complexité	Réduction polynomiale • Problème NP-complet

Logique, syntaxe et sémantique

Logique mathématique	Assistant de preuve • Calcul des prédicats • Correspondance de Curry-Howard • Fonction récursive • Lambda-calcul • Théorème d'incomplétude de Gödel • Théorie des types
Grammaire formelle et systèmes de réécriture	Compilation • Expression rationnelle • Grammaire formelle • Transduction rationnelle • Langage rationnel • Langage algébrique • Langage contextuel • Théorie des langages
Sémantique	Sémantique des langages de programmation • Sémantique dénotationnelle • Sémantique axiomatique • Sémantique opérationnelle
Spécifier, vérifier et concevoir des programmes	Interprétation abstraite • Méthodes formelles • Model checking

Algorithmique, complexité et mathématiques discrètes

Algorithmique	Algorithme génétique • Algorithme glouton • Algorithme probabiliste • Complexité algorithmique • Diviser pour régner • Heuristique • Programmation dynamique
Problèmes et algorithmes numériques	Algorithme du simplexe • Géométrie algorithmique • Algorithme d'Euclide • Test de primalité
Problèmes et algorithmes non-numériques	Algorithmes de la théorie des graphes • Arbre (structure de données) • Liste (informatique) • Table de hachage • Tas (informatique)
Théorie des graphes	Coloration de graphe • Problèmes de cheminement
Recherche opérationnelle	Optimisation • Optimisation combinatoire • Théorie de l'ordonnancement
Données et codage	Combinatoire des mots •Codage • Codage de l'information • Compression de données • Cryptage • Cryptanalyse • Cryptographie • Théorie de l'information

Catégories :

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Calcul des prédicats de Wikipédia en français (auteurs)

Игры ⚽ Нужно сделать НИР?

Regardez d'autres dictionnaires:

Calcul Des Prédicats — Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage des mathématiques proposée par les logiciens de la fin du XIXe siècle et … Wikipédia en Français
Calcul des predicats — Calcul des prédicats Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage des mathématiques proposée par les logiciens de la fin… … Wikipédia en Français
Calcul des prédicats — ● Calcul des prédicats partie de la logique qui traite des propriétés générales des propositions analysées en prédicats … Encyclopédie Universelle
Calcul des prédicats du premier ordre — Calcul des prédicats Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage des mathématiques proposée par les logiciens de la fin… … Wikipédia en Français
Calcul des relations — Calcul des prédicats Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage des mathématiques proposée par les logiciens de la fin… … Wikipédia en Français
Calcul Des Propositions — Pour les articles homonymes, voir Déduction. Le calcul des propositions ou calcul propositionnel est une théorie logique qui définit les lois formelles du raisonnement. C est la version moderne de la logique stoïcienne. C est aussi la première… … Wikipédia en Français
PRÉDICATS (CALCUL DES) — PRÉDICATS CALCUL DES Dans la logique aristotélicienne, la distinction du sujet et du prédicat est à la fois d’ordre linguistique (grammatical), d’ordre ontologique (la substance et ce qu’on peut dire d’elle) et d’ordre logique. Le prédicat est… … Encyclopédie Universelle
Calcul Des Constructions — Le calcul des constructions (CoC de l anglais calculus of constructions) est un lambda calcul typé d ordre supérieur dans lequel les types sont des valeurs de première classe. Il est par conséquent possible, dans le CoC, de définir des fonctions… … Wikipédia en Français
Calcul des Constructions — Le calcul des constructions (CoC de l anglais calculus of constructions) est un lambda calcul typé d ordre supérieur dans lequel les types sont des valeurs de première classe. Il est par conséquent possible, dans le CoC, de définir des fonctions… … Wikipédia en Français
Calcul Des Séquents — En logique mathématique et plus précisément en théorie de la démonstration, le calcul des séquents est un système de déduction créé par Gerhard Gentzen[1][2]. Le nom de ce formalisme fait référence à un style particulier de déduction qui manipule … Wikipédia en Français

Dictionnaires et Encyclopédies sur 'Academic'

Calcul des prédicats

Sommaire