Voir la source de Calcul des prédicats

En [[logique mathématique]], le '''calcul des prédicats du premier ordre''', '''logique du premier ordre''', '''calcul des relations''', '''logique quantificationnelle'''{{Référence nécessaire|date=23 juillet 2023}}, ou tout simplement '''calcul des prédicats''', est un [[système formel]] utilisé pour raisonner et décrire des énoncés en [[mathématiques]], [[informatique]], [[intelligence artificielle]]<ref>{{Ouvrage|langue=English|prénom1=RUSSELL /|nom1=NORVIG|titre=Artificial Intelligence: A Modern Approach, Global Edition|passage=Chapitre 8 - First order logic|éditeur=Pearson|date=2014-01-01|isbn=978-1-292-15396-4|lire en ligne=https://www.amazon.com/Artificial-Intelligence-Modern-Approach-Global/dp/1292153962|consulté le=2023-07-24}}</ref>, [[philosophie]] et [[linguistique]]. Il a été proposé par [[Gottlob Frege]]<ref>{{Lien web|titre=Biographie de Gottlob Frege|url=https://www.bibmath.net/bios/index.php?action=affiche&quoi=frege|site=www.bibmath.net}}</ref> comme une formalisation du langage des [[mathématiques]] entre la fin du {{s-|XIX}} et le début du {{s-|XX}}. La logique du premier ordre comporte deux parties : 

* la ''[[Syntaxe (logique)|syntaxe]]'' définit le [[vocabulaire]] symbolique de base ainsi que les règles permettant de construire des énoncés ;
* la ''[[Sémantique axiomatique|sémantique]]'' interprète ces énoncés comme exprimant des relations entre les éléments d'un domaine, également appelé ''modèle''.
 
Sur le plan syntaxique, les langages du premier ordre opposent deux grandes classes linguistiques : 

* les constituants servant à identifier ou nommer des éléments du domaine : ''variables'', ''symboles de constantes'', ''termes'' ;
* les constituants servant à exprimer des propriétés ou des relations entre ces éléments : ''prédicats'' et ''formules''.
 
Un [[Prédicat (linguistique)|prédicat]] est une expression linguistique qui peut être reliée à un ou plusieurs éléments du domaine pour former une phrase. Par exemple, dans la phrase « Mars est une planète », l'expression « est une planète » est un prédicat qui est relié au nom (symbole de constante) « Mars » pour former une phrase. Et dans la phrase « Jupiter est plus grand que Mars », l'expression « est plus grand que » est un prédicat qui se relie aux deux noms, « Jupiter » et « Mars », pour former une phrase.

Lorsqu'un prédicat est lié à une expression, on dit qu'il exprime une propriété (telle que la propriété d'être une planète), et lorsqu'il est lié à deux ou plusieurs expressions, on dit qu'il exprime une relation (telle que la relation d'être plus grand). Ainsi on peut raisonner sur des énoncés comme « il existe un <math>x</math> tel que pour tout <math>y</math>, <math>x</math> est ami avec <math>y</math> », ce qui est exprimé symboliquement par la formule :
<center><math>\exists x \forall y~ \mathrm{amis}(x, y)</math>.</center>

Il convient de noter cependant que la logique du premier ordre ne contient aucune relation spécifique (comme telle [[relation d'ordre]], d'inclusion ou d'égalité) ; en fait, il ne s'agit que d'étudier la façon dont on doit parler et raisonner avec les expressions du [[langage mathématique]].

Les traits caractéristiques de la logique du premier ordre sont :
* l'utilisation de [[Variable (mathématiques)|''variables'']] comme <math>x</math>, <math>y</math>{{Etc.}} pour dénoter des éléments du domaine d'interprétation ;
* l'utilisation de [[Prédicat (logique mathématique)|''prédicats'']] (ou ''relations'') sur les éléments ;
* l'utilisation d'[[Connecteur logique|opérations logiques]] (''et, ou, implique''{{Etc.}}) ;
* l'utilisation de [[Quantification (logique)|''quantifications'']], par exemple, l'une universelle (« Quel que soit », « pour tout » noté [[∀]]) et l'autre existentielle (« il existe au moins un… tel que », noté [[∃]]).

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 l'affirmation que deux éléments sont les mêmes, 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.

On parle de logique du premier ordre par opposition aux [[Logique d'ordre supérieur|logiques d'ordre supérieur]], où l'on peut aussi appliquer les quantificateurs et les prédicats aux prédicats ou aux fonctions, en plus des variables. En outre, cet article ne traite que de la logique du premier ordre [[Logique classique|classique]], mais on notera qu'il existe aussi une [[Logique intuitionniste#Le calcul des prédicats intuitionniste|logique du premier ordre intuitionniste]].

== Introduction ==
Alors que la [[Calcul des propositions|logique propositionnelle]] traite des propositions déclaratives simples, la logique du premier ordre couvre en plus les prédicats et la quantification.

Un prédicat prend en entrée une ou plusieurs entités du domaine du discours et en sortie, il est soit Vrai, soit Faux. Considérons les deux phrases « Socrate est un philosophe » et « [[Platon]] est un philosophe ». En logique propositionnelle, ces phrases sont considérées comme non liées et peuvent être désignées, par exemple, par des variables telles que {{nobr|p et q}}. Le prédicat « est un philosophe » apparaît dans les deux phrases, dont la structure commune est « a est un philosophe ». La variable a est instanciée en tant que « Socrate » dans la première phrase, et est instanciée en tant que « Platon » dans la deuxième phrase. Alors que la logique du premier ordre permet l'utilisation de prédicats, tels que « est un philosophe » dans cet exemple, la logique propositionnelle ne le permet pas.

Les relations entre les prédicats peuvent être énoncées à l'aide de connecteurs logiques. Considérons, par exemple, la formule du premier ordre « si a est un philosophe, alors a est un savant ». Cette formule est un énoncé conditionnel dont l'hypothèse est « a est un philosophe » et la conclusion « a est un savant ». La vérité de cette formule dépend de l'objet désigné par a, et des interprétations des prédicats « est un philosophe » et « est un savant ».

Les quantificateurs peuvent être appliqués aux variables d'une formule. La variable a de la formule précédente peut être quantifiée universellement, par exemple avec la phrase du premier ordre « Pour tout a, si a est un philosophe, alors a est un savant ». Le quantificateur universel « pour chaque » dans cette phrase exprime l'idée que l'affirmation « si a est un philosophe, alors a est un savant » est valable pour tous les choix de a.

La négation de la phrase « Pour tout a, si a est un philosophe, alors a est un savant » est logiquement équivalente à la phrase « Il existe a tel que a est un philosophe et a n'est pas un savant ». Le quantificateur existentiel « il existe » exprime l'idée que l'affirmation « a est un philosophe et a n'est pas un savant » est valable pour un certain choix de a.

Les prédicats « est un philosophe » et « est un savant » prennent chacun une seule variable. En général, les prédicats peuvent prendre plusieurs variables. Dans la phrase du premier ordre « Socrate est le professeur de Platon », le prédicat « est le professeur de » prend deux variables.

== Histoire ==
[[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<ref>{{Lien web|auteur1=Emmanuel Kant|titre=Préface de la Critique de la raison pure|url=https://fr.wikisource.org/wiki/Critique_de_la_raison_pure_(trad._Barni)/Tome_I/Pr%C3%A9face_de_la_2e_%C3%A9dition|site=fr.wikisource.org|date=1787}}.</ref>). Les logiciens<ref>{{Lien web|titre=logicien — Wiktionnaire|url=https://fr.wiktionary.org/wiki/logicien|site=fr.wiktionary.org|consulté le=2020-05-25}}.</ref> du {{s-|XIX}} 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 démontré 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 ([[Axiome logique|axiomes logiques]], [[Schéma d'axiomes|schémas d'axiomes]] logiques et [[Déduction logique|règles de déduction]]<ref>{{Lien web|titre=Logique (mathématiques)/Déduction naturelle — Wikiversité|url=https://fr.wikiversity.org/wiki/Logique_(math%C3%A9matiques)/D%C3%A9duction_naturelle|site=fr.wikiversity.org|consulté le=2020-05-25}}.</ref>) 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]], [[Assistant de preuve|mécanisation du raisonnement]]…

== Syntaxe ==
[[Fichier:Logiquepremierordre syntaxe.svg|vignette|Exemple d'une formule de la logique du premier ordre. Le schéma montre les quantificateurs, les occurrences des symboles de fonctions et des symboles de prédicats.|292x292px]]
Contrairement à un [[langage naturel]], comme le [[français]], la logique du premier ordre est un [[langage formel]]. Cette section donne une brève présentation de la syntaxe du langage formel du calcul des prédicats. Pour cela, on a besoin d'un ''alphabet'', c'est-à-dire un ensemble de symboles utilisées pour écrire les ''énoncés'' (ou ''formules''). On se donne un ensemble des symboles appelés ''[[Variable (mathématiques)|variables]]'', toujours infini : <math>x</math>, <math>y</math>, <math>z</math>{{etc.}}

=== Signature ===
On se donne une signature<ref>{{Ouvrage|langue=fr|titre=Logique : fondements et applications|passage=p. 122, Définition 7.1|date=2023-07-23|lire en ligne=https://www.dunod.com/sciences-techniques/logique-fondements-et-applications-cours-et-exercices-corriges|consulté le=2023-07-23}}</ref>, c'est-à-dire :
* un ensemble de symboles de fonctions : <math>f</math>, <math>g</math>, <math>h</math>{{etc.}} ;
* un ensemble de symboles de ''prédicats'' : <math>P</math>, <math>Q</math>, <math>R</math>{{etc.}}

Chaque symbole de fonction et chaque symbole de prédicat a une ''[[arité]]'' : il s'agit du nombre d'arguments ou d'objets auxquels il est appliqué. Par exemple, le prédicat <math>B</math> pour « est bleu(e) » a une arité égale à 1 (on dit qu'il est unaire ou [[wikt:monadique|monadique]]), tandis que le prédicat <math>amis</math> pour « être amis » a une arité de deux (on dit qu'il est binaire ou dyadique). Il peut y avoir des symboles de fonction ou de prédicat d'arité 0. Un symbole de fonction d'arité 0 s'appelle une ''constante.'' Les constantes se notent généralement <math>a</math>, <math>b</math>, <math>c</math>{{etc.}}

==== Exemples ====

* Si l'on veut parler de personnes, Bob est un symbole de constante, mère(.) est un symbole de fonction d'{{nobr|arité 1}}, amis(., .) est un symbole de prédicats d'{{nobr|arité 2}}.
* Si l'on veut parler d'entiers naturels, « 0, 1 » sont des symboles de constantes. Les symboles {{nobr|+ et ×}} sont des symboles de fonctions d'{{nobr|arité 2}}. Les symboles {{nobr|{{=}} et ≤}} sont des symboles de prédicats d'{{nobr|arité 2}}.

=== Termes ===
{{Article détaillé|Terme (logique)}}
Les termes sont définis par induction :

* un symbole de variable est un terme ;
* un symbole de constante est un terme ;
* si <math>f</math> est un symbole de fonctions d'arité ''n'', et que ''t''{{ind|1}}, …, ''t{{ind|n}}'' sont des termes alors <math>f(t_1, \dots, t_n)</math> est un terme.

==== Exemples ====

* Bob, mère(Bob), mère(mère(Bob)), mère(x) sont des termes
* {{nobr|0 + 1, x + 3 × y × y}} sont des termes.

=== Formule ===
Les ''formules'' du calcul des prédicats du premier ordre sont définies par induction :
* <math>P(t_1, \dots, t_n)</math> si <math>P</math> un symbole de prédicat d'arité ''n'' et ''t''{{ind|1}}, …, ''t{{ind|n}}'' sont des [[Terme (logique)|termes]]
* ¬''e'' si e est une formule ;
* (''e''{{ind|1}}∧''e''{{ind|2}}) si ''e''{{ind|1}} et ''e''{{ind|2}} sont des formules ;
* (''e''{{ind|1}}∨''e''{{ind|2}}) si ''e''{{ind|1}} et ''e''{{ind|2}} sont des formules ;
* (''e''{{ind|1}}→''e''{{ind|2}}) si ''e''{{ind|1}} et ''e''{{ind|2}} sont des formules ;
* <math>\forall x \; e</math> si ''e'' est une formule ;
* <math>\exists x \; e</math> si ''e'' est une formule.
Une formule de la forme <math>P(t_1, \dots, t_n)</math> s'appelle un ''atome'' ou une ''formule atomique''. Les symboles <math>\lnot</math> (''non''), <math>\land</math> (''et''), <math>\lor</math> (''ou'') et <math>\to</math> (''implique''), qui sont des ''connecteurs'' que possède aussi le [[calcul des propositions]]. Les symboles <math>\forall</math> (''quel que soit'') et <math>\exists</math> (''il existe''), appelés ''quantificateurs''. On pourrait se contenter d'un seul quantificateur <math>\forall</math> et de deux connecteurs logiques <math>\lnot</math> et <math>\land</math> en définissant les autres connecteurs et quantificateur à partir de ceux-ci. Par exemple <math>\exists x \; P(x)</math> est défini comme <math>\lnot (\forall x \; \lnot P(x))</math>. Les symboles de parenthèses « ) » et « ( » sont comparables aux symboles de ponctuations dans une langue naturelle. 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 {{nobr|0 et 1}}, pour symboles de fonctions binaires {{nobr|+ et .}}, et pour symboles de prédicats binaires les symboles {{nobr|{{=}} et <}}, alors le langage utilisé peut être interprété comme étant celui de l'arithmétique. {{nobr|''x'' et ''y''}} désignant des variables, {{nobr|''x'' + 1}} est un [[Terme (logique)|terme]], {{nobr|0 + 1 + 1}} est un [[Terme (logique)|terme]] clos, {{nobr|''x'' < ''y'' + 1}} est une formule, {{nobr|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 « {{exp|-1}} », un symbole de [[relation binaire]] « = », alors le langage utilisé peut être interprété comme étant celui de la [[théorie des groupes]]. Si {{nobr|''x'' et ''y''}} désignent des variables, {{nobr|''x'' * ''y''}} est un terme, {{nobr|''e'' * ''e''}} est un terme clos, {{nobr|''x'' {{=}} ''y'' * ''y''}} est une formule, {{nobr|''e'' {{=}} ''e'' * ''e''{{exp|-1}}}} et ({{nobr|''e''{{exp|-1}} * ''e''){{exp|-1}} {{=}} (''e''{{exp|-1}}){{exp|-1}}}} sont des formules closes.

=== Prédicats, formules closes, formules polies, variables libres, variables liées ===
Lorsqu’une variable <math>x</math> appartient à une sous-formule précédée d’un quantificateur, <math>\forall x </math> ou <math>\exists x </math>, 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, <math>\exists x (x < y)</math> est identique à <math>\exists z (z < y)</math> mais pas à <math>\exists x (x < z)</math> et encore moins à <math>\exists y (y < y)</math>.

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, <math>\forall x \exists y (x < y)</math> est une formule close du langage de l'arithmétique. <math>\forall x (x < z)</math> 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}}

== Sémantique ==

[[Fichier:Logiquepremierordre modele exemple.png|vignette|Voici un modèle pour la logique du premier ordre. Le domaine a trois éléments : un bonhomme de neige, un oiseau et une cerise. Le modèle permet d'interpréter un prédicat binaire <math>\mathrm{aime}</math> : le bonhomme de neige aime l'oiseau, l'oiseau aime tout le monde (y compris lui-même) et la cerise n'aime personne.]]
La théorie de la vérité des formules du calcul des prédicats a été appelée par [[Alfred Tarski|Tarski]] sa sémantique{{Référence nécessaire|date=25 mai 2016}}.

Une ''interprétation'' d'un langage du premier ordre dans un domaine d'interprétation, appelé aussi ''modèle'' du langage, décrit les valeurs prises par les constituants du premier ordre (variables, symboles de constantes, termes) et les relations associées aux prédicats. Chaque énoncé se voit attribuer une [[valeur de vérité]]. L'étude des interprétations des langages formels est appelée ''sémantique formelle'' ou ''théorie des modèles''. Ce qui suit est une description de la sémantique standard ou tarskienne pour la logique du premier ordre. Il existe d'autres types de sémantique, notamment la [[sémantique des jeux]], qui ne sont pas détaillés dans cet article.

{{Article détaillé|Théorie des modèles}}

=== Modèle ===
Un modèle M d'un langage du premier ordre est une structure : c'est un ensemble d'éléments (appelé domaine) dans lequel on donne un sens aux symboles du langage. Généralement, si le langage possède un prédicat binaire pour le symbole d'égalité « = », alors son interprétation dans la structure est l'égalité.

=== Conditions de vérité ===
Un modèle donne une valeur de vérité (''vrai'' ou ''faux'') à toute formule close du langage. Les [[Condition de vérité|conditions de vérité]] sont définies par [[induction structurelle]] sur les formules.
Par exemple, dans le modèle ci-contre : 
* <math>\exists x \forall y~ \mathrm{aime}(x,y)</math> est vraie dans le modèle M car il existe un élément (l'oiseau) qui aime tout le monde ;
* <math>\exists x \forall y~ \lnot \mathrm{aime}(x,y)</math> est vraie dans le modèle M car il existe un élément (la cerise) qui n'aime personne.

=== Formule satisfaisable ===
Une formule est '''satisfaisable''' s'il existe un modèle M qui la rend vraie. Par exemple <math>\exists x \forall y~ \mathrm{aime}(x,y)</math> est satisfaisable.

=== Formule valide ===
On dit qu'une formule F du langage est une formule '''valide''' si cette formule est vraie dans tout modèle du langage, ce qu'on note <math>\vDash F</math>. Par exemple, la formule <math>\exists x \forall y~ \mathrm{aime}(x,y) \to \forall y \exists x~ \mathrm{aime}(x,y)</math> est une formule valide. Dans un modèle M, si <math>\exists x \forall y~ \mathrm{aime}(x,y)</math> est vraie alors, il existe un élément <math>x</math> dans le domaine qui aime tout le monde. Mais alors tout le monde est aimé et donc la formule <math>\forall y \exists x~ \mathrm{aime}(x,y)</math> est vraie dans le modèle M.
L'implication étant vraie dans tout modèle M, la formule est valide.

Par contre, la formule <math>\forall y \exists x~ \mathrm{aime}(x,y) \to \exists x \forall y~ \mathrm{aime}(x,y)</math> n'est pas valide. En effet, dans un modèle avec deux éléments {''a'', ''b''} et où <math>\mathrm{aime}</math> est interprété par a n'aime que a et b n'aime que b, la formule <math>\forall y \exists x \; ~ \mathrm{aime}(x,y)</math> est vraie alors que <math>\exists x \forall y \; ~ \mathrm{aime}(x,y)</math> est fausse. L'implication est donc fausse dans le modèle et la formule n'est pas valide.

=== Conséquence sémantique ===
On dit que F est conséquence sémantique d'une théorie T si, tout modèle qui satisfait toutes les formules de T satisfait aussi F.

== Système de déduction ==
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 ;
* le [[calcul des séquents]] ;
* la [[Règle de résolution|résolution]] ;
* les [[axiome logique|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 [[Alfred North Whitehead|Whitehead]] et [[Bertrand Russell|Russell]], a une grande importance à la fois [[Logique mathématique|métamathématique]] et historique. L'un des systèmes d'axiomes le plus court est constitué du triplet suivant :
*;Les axiomes du [[calcul des propositions]]
*:<math>f \to (g \to f)</math>			
*:<math>(f \to (g \to h)) \to ((f \to g) \to (f \to h))</math>
*:<math>(\lnot f \to g) \to ((\lnot f \to \lnot g) \to f)</math>
*:les axiomes relatifs au quantificateur <math>\forall</math>
*:<math>\forall x( f \to g(x)) \to (f \to \forall x g(x))</math> où ''x'' n'est pas libre dans ''f''
*:<math>\forall x f(x) \to f(a)</math> où ''x'' n'a pas d'occurrence libre dans une partie bien formée de ''f'' de la forme <math>\forall a, h</math> (ceci pour éviter une substitution embarrassante si par exemple, ''f''(''x'') est de la forme <math>\exists a, a < x</math>).
*;La règle du [[modus ponens]] 
*: si on a prouvé <math>f \to g</math> et <math>f</math>, alors on a prouvé <math>g</math>
*;La règle de généralisation 
*: si on a prouvé <math>f(x)</math>, alors on a prouvé <math>\forall x f(x)</math> (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 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 appelé ''théorème''. On dit aussi qu'elle est ''prouvable'', ce qu'on note <math>\vdash F</math>.

== Propriétés ==

=== Complétude ===
{{Article détaillé|Théorème de complétude de Gödel}}

Le [[Théorème de complétude de Gödel|théorème de complétude]] dit que F est valide est équivalent à F est prouvable. Mieux, on parle de complétude forte : si F est conséquence sémantique d'une théorie T alors F est prouvable à partir de T.

=== Indécidabilité ===
Tous les systèmes logiques ne sont pas décidables, autrement dit bien qu'ils soient parfaitement définis, il n'existe pas toujours un [[algorithme]] pour dire si une formule est oui ou non un théorème. D'ailleurs historiquement la [[théorie de la calculabilité]] s'est construite pour démontrer précisément leur indécidabilité. Avant de développer ces résultats, voici résumé ce qu'on sait sur la décidabilité et l'indécidabilité des systèmes logiques.

* ''Calcul propositionnel :'' décidable et complet. Pour la décidabilité, il y a donc une procédure effective pour décider si une formule du calcul propositionnel est satisfaisable, c'est-à-dire que l'on peut affecter aux variables propositionnelles des valeurs de vérité qui la rendent vraie, mais le problème, nommé [[problème SAT]], est [[Problème NP-complet|NP-complet]], c'est-à-dire que tous les algorithmes déterministes connus de recherche d'une solution sont en temps exponentiel par rapport au nombre de variables (voir l'article [[Problème SAT]]).
* ''Calcul des prédicats du premier ordre monadique'', c'est-à-dire réduit aux relations unaires et sans fonctions : décidable et complet, par réduction au calcul propositionnel.
* ''Calcul des prédicats du premier ordre :'' réductible au calcul des prédicats dyadique, soit avec au plus des prédicats binaires (comme il en est en théorie des ensembles n'ayant que l'appartenance et l'égalité comme symboles primitifs) : semi-décidable et [[Théorème de complétude de Gödel|complet]].
*''[[Logique d'ordre supérieur#Logique du second ordre|Calcul des prédicats de deuxième ordre]]'' : [''quid'' sur sa décidabilité], et {{refsou|théorème de complétude partiel sur une sous-classe de formules|date=28 mai 2018}}.
* ''[[Logique d'ordre supérieur|Calcul des prédicats d'ordre supérieur]]'' :  {{...}}

Le calcul des prédicats est semi-décidable, dans le sens où une machine peut énumérer les théorèmes les uns après les autres. Mais, contrairement au [[calcul des propositions]], il n'est pas en général [[Décidabilité|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).

Des fragments syntaxiques sont décidables comme la [[logique monadique du premier ordre]] ou la [[classe de Bernays-Schönfinkel]].

=== Compacité ===
Voir [[théorème de compacité]].

=== Expressivité ===
Une application intéressante du théorème de compacité est qu'il n'existe pas de formules qui exprime « le domaine est infini ».

=== Théorème de Löwenheim-Skolem ===
Voir [[théorème de Löwenheim-Skolem]].
{{Article détaillé|théorème de Löwenheim-Skolem}}

=== Incomplétude ===
En un sens différent, les [[théorie axiomatique|théories]] « raisonnables »<ref group=note>Récursivement axiomatisables et cohérentes.</ref> qui permettent de formaliser suffisamment l'arithmétique intuitive, comme l'[[Axiomes de Peano|arithmétique de Peano]], ou la [[théorie des ensembles]] ne sont pas [[complétude|complètes]] : il existe un énoncé non démontrable dont la négation est également non démontrable (voir [[théorèmes d'incomplétude de Gödel]]).

== Fragments décidables ==
Le problème de satisfiabilité d'une formule de la logique du premier ordre est indécidable. Mais en se restreignant à certaines classes de formules, le problème de satisfiabilité devient décidable. Le tableau suivant énumère quelques fragments décidables<ref>{{Ouvrage|langue=en|auteur1=|titre=The Classical Decision Problem {{!}} Egon Börger {{!}} Springer|passage=Th. 6.02 p. 240|éditeur=|date=|isbn=|lire en ligne=https://www.springer.com/gp/book/9783540423249|consulté le=2018-04-13}}</ref>.

{| class="wikitable"
|+
!Fragments
|-
|Fragment monadique et symboles de fonction d'arité 1
|-
|Fragment à deux variables seulement
|-
|[[Classe de Bernays-Schönfinkel]], Classe <math>\exists^*\forall^*</math> sans symboles de fonction et égalité
|-
|Classe <math>\exists^*\forall^2\exists^*</math> sans symboles de fonction
|-
|Classe <math>\exists^*\forall\exists^*</math> avec symboles de fonction
|-
|Classe <math>\exists^*</math> avec symboles de fonction et égalité
|-
|Fragment monadique avec symboles de fonction d'arité et égalité
|-
|Classe <math>\exists^*\forall\exists^*</math> avec symboles de fonction d'arité un, et égalité
|}

== Variantes ==
Le [[calcul des propositions]] est un fragment syntaxique de la logique du premier ordre où il n'y a pas de variables et où tous les prédicats sont d'arité 0{{Référence nécessaire|date=25 mai 2016}}.

La [[logique modale]] propositionnelle et la [[logique de description]] sont des fragments syntaxiques de la logique du premier ordre{{Référence nécessaire|date=25 mai 2016}}. D'ailleurs, toute formule du premier ordre qui est invariante par [[bisimulation]] est équivalente à une formule de la logique modale : c'est le théorème de Van Benthem{{Référence nécessaire|date=25 mai 2016}}. La logique du premier ordre a aussi été étendu à la logique modale du premier ordre{{Référence nécessaire|date=25 mai 2016}}. La logique de la dépendance (''{{Langue|en|dependence logic}}'') est une généralisation de la logique du premier ordre où les dépendances entre variables sont explicitement décrites dans le langage{{Référence nécessaire|date=25 mai 2016}}.

== Notes et références ==
=== Notes ===
{{références|groupe="note"}}

=== Références ===
{{Références}}

== Annexes ==

=== Articles connexes ===

* [[Calcul des propositions]]
* [[Théorie des modèles]]
* [[Skolémisation]]
* [[Notation (mathématiques)|Langage formel mathématique]]
* [[Théorème de Lindström]]
* Langage informatique [[Prolog]]
* [[Déduction naturelle]]
* [[Signature (logique)]]
* [[Structure (logique mathématique)]]
* [[Théorème d'interpolation de Craig]]
* [[Théorème de Trakhtenbrot]]

== 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'', [[Éditions Dunod|Dunod]], 2001 {{ISBN|2-10-006796-6}}
* Pierre Lebarbenchon, Sophie Pinchinat, François Schwarzentruber, Logique : fondements et applications. Dunod 2022 {{ISBN|978-2100821587}}

{{Palette|Logique|Règles de transformation|Informatique théorique}}
{{Portail|logique|Informatique théorique}}

[[Catégorie:Logique]]
[[Catégorie:Logique mathématique]]
[[Catégorie:Modèle conceptuel]]