Logique du premier ordre - First-order logic

Logique du premier ordre -également connu sous le nom logique des prédicats , logique quantificationnelle et de premier ordre calcul des prédicats -est une collection de systèmes formels utilisés dans les mathématiques , la philosophie , la linguistique et la science informatique . La logique du premier ordre utilise des variables quantifiées sur des objets non logiques, et permet l'utilisation de phrases qui contiennent des variables, de sorte que plutôt que des propositions telles que "Socrate est un homme", on peut avoir des expressions sous la forme "il existe x tels que x est Socrate et x est un homme", où "il existe " est un quantificateur, tandis que x est une variable. Cela la distingue de la logique propositionnelle , qui n'utilise pas de quantificateurs ou de relations ; en ce sens, la logique propositionnelle est le fondement de la logique du premier ordre.

Une théorie sur un sujet est généralement une logique du premier ordre avec un domaine spécifié de discours (sur lequel s'étendent les variables quantifiées), un nombre fini de fonctions de ce domaine à lui-même, un nombre fini de prédicats définis sur ce domaine et un ensemble d'axiomes croyait tenir à leur sujet. Parfois, la "théorie" est comprise dans un sens plus formel, qui n'est qu'un ensemble de phrases dans la logique du premier ordre.

L'adjectif « premier ordre » distingue la logique du premier ordre de la logique d'ordre supérieur , dans laquelle il existe des prédicats ayant des prédicats ou des fonctions comme arguments, ou dans lesquels des quantificateurs de prédicats ou des quantificateurs de fonctions ou les deux sont autorisés. Dans les théories du premier ordre, les prédicats sont souvent associés à des ensembles. Dans les théories d'ordre supérieur interprétées, les prédicats peuvent être interprétés comme des ensembles d'ensembles.

Il existe de nombreux systèmes déductifs pour la logique du premier ordre qui sont à la fois solides (c'est-à-dire que toutes les déclarations prouvables sont vraies dans tous les modèles) et complets (c'est-à-dire que toutes les déclarations qui sont vraies dans tous les modèles sont prouvables). Bien que la relation de conséquence logique ne soit que semi - décidable , de nombreux progrès ont été réalisés dans la démonstration automatique de théorèmes en logique du premier ordre. La logique du premier ordre satisfait également plusieurs théorèmes métalogiques qui la rendent propice à l'analyse en théorie de la preuve , tels que le théorème de Löwenheim-Skolem et le théorème de compacité .

La logique du premier ordre est la norme pour la formalisation des mathématiques en axiomes et est étudiée dans les fondements des mathématiques . L'arithmétique de Peano et la théorie des ensembles de Zermelo-Fraenkel sont des axiomatisations de la théorie des nombres et de la théorie des ensembles , respectivement, en logique du premier ordre. Aucune théorie du premier ordre, cependant, n'a la force de décrire de manière unique une structure avec un domaine infini, comme les nombres naturels ou la ligne réelle . Les systèmes d' axiomes qui décrivent complètement ces deux structures (c'est-à-dire les systèmes d'axiomes catégoriques ) peuvent être obtenus dans des logiques plus fortes telles que la logique du second ordre .

Les fondements de la logique du premier ordre ont été développés indépendamment par Gottlob Frege et Charles Sanders Peirce . Pour une histoire de la logique du premier ordre et comment elle en est venue à dominer la logique formelle, voir José Ferreirós (2001).

introduction

Alors que la logique propositionnelle traite des propositions déclaratives simples, la logique du premier ordre couvre en outre les prédicats et la quantification .

Un prédicat prend une ou plusieurs entités dans le domaine du discours comme entrée tandis que les sorties sont soit True soit False . Considérez les deux phrases « Socrate est un philosophe » et « Platon est un philosophe ». Dans la 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 p et q . Le prédicat « est un philosophe » apparaît dans les deux phrases, qui ont une structure commune de « a est un philosophe ». La variable a est instanciée comme "Socrate" dans la première phrase, et est instanciée comme "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 fait 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 avec « a est un philosophe » comme hypothèse, et « a est un savant » comme conclusion. 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 dans la formule précédente peut être quantifiée universellement, par exemple, avec la phrase du premier ordre "Pour chaque 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 érudit" vaut pour tous les choix de a .

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

Les prédicats « est philosophe » et « est érudit » 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 maître de Platon », le prédicat « est le maître de » prend deux variables.

Une interprétation (ou modèle) d'une formule du premier ordre spécifie la signification de chaque prédicat et les entités qui peuvent instancier les variables. Ces entités forment le domaine du discours ou de l'univers, qui doit généralement être un ensemble non vide. Par exemple, dans une interprétation avec le domaine du discours composé de tous les êtres humains et le prédicat « est un philosophe » compris comme « était l'auteur de la République », la phrase « Il existe une telle que un est un philosophe » est vu comme étant vrai, comme en témoigne Platon.

Syntaxe

Il y a deux parties clés de la logique du premier ordre. La syntaxe détermine quelles séquences finies de symboles sont des expressions bien formées dans la logique du premier ordre, tandis que la sémantique détermine les significations derrière ces expressions.

Alphabet

Contrairement aux langues naturelles, telles que l'anglais, la langue de la logique du premier ordre est complètement formelle, de sorte qu'il peut être déterminé mécaniquement si une expression donnée est bien formée. Il existe deux principaux types d'expressions bien formées : les termes , qui représentent intuitivement des objets, et les formules , qui expriment intuitivement des prédicats qui peuvent être vrais ou faux. Les termes et formules de la logique du premier ordre sont des chaînes de symboles , où tous les symboles forment ensemble l' alphabet de la langue. Comme pour tous les langages formels , la nature des symboles eux-mêmes sort du cadre de la logique formelle ; ils sont souvent considérés simplement comme des lettres et des symboles de ponctuation.

Il est courant de diviser les symboles de l'alphabet en symboles logiques , qui ont toujours la même signification, et en symboles non logiques , dont la signification varie selon l'interprétation. Par exemple, le symbole logique représente toujours "et" ; il n'est jamais interprété comme "ou", qui est représenté par le symbole logique . D'un autre côté, un symbole de prédicat non logique tel que Phil ( x ) pourrait être interprété comme signifiant « x est un philosophe », « x est un homme nommé Philippe », ou tout autre prédicat unaire selon l'interprétation à portée de main.

Symboles logiques

Il existe plusieurs symboles logiques dans l'alphabet, qui varient selon l'auteur, mais comprennent généralement :

  • Les quantificateurs symboles: pour la quantification universelle, et pour la quantification existentielle
  • Les connecteurs logiques : pour conjonction , pour disjonction , pour implication , pour biconditionnel , ¬ pour négation. Occasionnellement, d'autres symboles de connexion logiques sont inclus. Certains auteurs utilisent C pq , au lieu de , et E pq , au lieu de , en particulier dans des contextes où → est utilisé à d'autres fins. De plus, le fer à cheval peut remplacer ; la triple barre peut remplacer ; un tilde ( ~ ), N p , ou F p , peut remplacer ¬ ; une double barre , ou A pq peut remplacer ; et esperluette & K pq , ou le point milieu, , peut remplacer , surtout si ces symboles ne sont pas disponibles pour des raisons techniques. (Les symboles susmentionnés C pq , E pq , N p , A pq et K pq sont utilisés dans la notation polonaise .)
  • Parenthèses, crochets et autres symboles de ponctuation. Le choix de ces symboles varie selon le contexte.
  • Un ensemble infini de variables , souvent désignées par des lettres minuscules à la fin de l' alphabet x , y , z , ... . Les indices sont souvent utilisés pour distinguer les variables : x 0 , x 1 , x 2 , ... .
  • Un symbole d'égalité (parfois, symbole d'identité ) = (voir § Égalité et ses axiomes ci-dessous).

Tous ces symboles ne sont pas nécessaires – un seul des quantificateurs, négation et conjonction, variables, crochets et égalité suffit. Il existe de nombreuses variantes mineures qui peuvent définir des symboles logiques supplémentaires :

  • Dans certaines occasions, les constantes de vérité T, V pq ou , pour "vrai" et F, O pq , ou , pour "faux" sont inclus. Sans ces opérateurs logiques de valence 0, ces deux constantes ne peuvent être exprimées qu'à l'aide de quantificateurs.
  • Dans d'autres cas, des connecteurs logiques supplémentaires sont inclus, tels que le trait de Sheffer , D pq (NAND) et exclusif ou , J pq .

Symboles non logiques

Les symboles non logiques représentent des prédicats (relations), des fonctions et des constantes sur le domaine du discours. Auparavant, il était de pratique courante d'utiliser un ensemble fixe et infini de symboles non logiques à toutes fins utiles. Une pratique plus récente consiste à utiliser des symboles non logiques différents selon l'application envisagée. Par conséquent, il est devenu nécessaire de nommer l'ensemble de tous les symboles non logiques utilisés dans une application particulière. Ce choix se fait via une signature .

L'approche traditionnelle consiste à n'avoir qu'un seul ensemble infini de symboles non logiques (une signature) pour toutes les applications. Par conséquent, dans l'approche traditionnelle, il n'y a qu'un seul langage de logique du premier ordre. Cette approche est encore courante, en particulier dans les livres à orientation philosophique.

  1. Pour tout entier n  ≥ 0, il y a une collection de n - aire ou n - lieu , symboles de prédicats . Parce qu'ils représentent des relations entre n éléments, ils sont également appelés symboles de relation . Pour chaque arité n , nous en avons une quantité infinie :
    P n 0 , P n 1 , P n 2 , P n 3 , ...
  2. Pour tout entier n  0, il existe une infinité de symboles de fonction n -aire :
    f n 0 , f n 1 , f n 2 , f n 3 , ...

Dans la logique mathématique contemporaine, la signature varie selon l'application. Les signatures typiques en mathématiques sont {1, ×} ou simplement {×} pour les groupes , ou {0, 1, +, ×, <} pour les champs ordonnés . Il n'y a aucune restriction sur le nombre de symboles non logiques. La signature peut être vide , finie ou infinie, voire indénombrable . D'innombrables signatures se produisent par exemple dans les preuves modernes du théorème de Löwenheim-Skolem .

Dans cette approche, chaque symbole non logique est de l'un des types suivants.

  1. Un symbole de prédicat (ou symbole de relation ) avec une certaine valence (ou arité , nombre d'arguments) supérieure ou égale à 0. Ceux-ci sont souvent désignés par des lettres majuscules telles que P , Q et R .
    • Les relations de valence 0 peuvent être identifiées avec des variables propositionnelles . Par exemple, P , qui peut représenter n'importe quel énoncé.
    • Par exemple, P ( x ) est une variable prédicat de valence 1. Une interprétation possible est " x est un homme ".
    • Q ( x , y ) est une variable prédicat de valence 2. Les interprétations possibles incluent « x est supérieur à y » et « x est le père de y ».
  2. Un symbole de fonction , avec une certaine valence supérieure ou égale à 0. Ceux-ci sont souvent désignés par des lettres romaines minuscules telles que f , g et h .
    • Exemples : f ( x ) peut être interprété comme pour « le père de x ». En arithmétique , il peut signifier "-x". En théorie des ensembles , il peut signifier "l' ensemble de puissance de x". En arithmétique, g ( x , y ) peut signifier " x + y ". En théorie des ensembles, il peut signifier « l'union de x et y ».
    • Les symboles de fonction de valence 0 sont appelés symboles constants et sont souvent désignés par des lettres minuscules au début de l'alphabet telles que a , b et c . Le symbole a peut représenter Socrate. En arithmétique, il peut représenter 0. En théorie des ensembles, une telle constante peut représenter l' ensemble vide .

L'approche traditionnelle peut être récupérée dans l'approche moderne, en spécifiant simplement la signature "personnalisée" pour se composer des séquences traditionnelles de symboles non logiques.

Règles de formation

Les règles de formation définissent les termes et les formules de la logique du premier ordre. Lorsque les termes et les formules sont représentés sous forme de chaînes de symboles, ces règles peuvent être utilisées pour écrire une grammaire formelle pour les termes et les formules. Ces règles sont généralement sans contexte (chaque production a un seul symbole sur le côté gauche), sauf que l'ensemble de symboles peut être infini et qu'il peut y avoir de nombreux symboles de départ, par exemple les variables dans le cas des termes .

termes

L'ensemble des termes est défini inductivement par les règles suivantes :

  1. Variables. Toute variable est un terme.
  2. Les fonctions. Toute expression f ( t 1 ,..., t n ) de n arguments (où chaque argument t i est un terme et f est un symbole de fonction de valence n ) est un terme. En particulier, les symboles désignant des constantes individuelles sont des symboles de fonction nulle et sont donc des termes.

Seules les expressions qui peuvent être obtenues par un nombre fini d'applications des règles 1 et 2 sont des termes. Par exemple, aucune expression impliquant un symbole de prédicat n'est un terme.

Formules

L'ensemble des formules (également appelées formules bien formées ou WFF ) est défini inductivement par les règles suivantes :

  1. Symboles de prédicat. Si P est un symbole de prédicat n -aire et t 1 , ..., t n sont des termes alors P ( t 1 ,..., t n ) est une formule.
  2. Égalité . Si le symbole d'égalité est considéré comme faisant partie de la logique et que t 1 et t 2 sont des termes, alors t 1 = t 2 est une formule.
  3. Négation. Si est une formule, alors est une formule.
  4. Connecteurs binaires. Si et sont des formules, alors ( ) est une formule. Des règles similaires s'appliquent à d'autres connecteurs logiques binaires.
  5. Quantificateurs. Si est une formule et x est une variable, alors (pour tout x, est vérifié) et (il existe x tel que ) sont des formules.

Seules les expressions qui peuvent être obtenues par un nombre fini d'applications des règles 1 à 5 sont des formules. Les formules obtenues à partir des deux premières règles sont dites formules atomiques .

Par exemple,

est une formule, si f est un symbole de fonction unaire, P un symbole de prédicat unaire et Q un symbole de prédicat ternaire. D'autre part, ce n'est pas une formule, bien qu'il s'agisse d'une chaîne de symboles de l'alphabet.

Le rôle des parenthèses dans la définition est de garantir qu'une formule ne peut être obtenue que d'une seule manière, en suivant la définition inductive (c'est-à-dire qu'il existe un arbre d'analyse unique pour chaque formule). Cette propriété est connue sous le nom de lisibilité unique des formules. Il existe de nombreuses conventions pour l'utilisation des parenthèses dans les formules. Par exemple, certains auteurs utilisent des deux-points ou des points au lieu de parenthèses, ou modifient les endroits où les parenthèses sont insérées. La définition particulière de chaque auteur doit être accompagnée d'une preuve de lisibilité unique.

Cette définition d'une formule ne prend pas en charge la définition d'une fonction if-then-else ite(c, a, b), où "c" est une condition exprimée sous forme de formule, qui renverrait "a" si c est vrai et "b" s'il est faux. En effet, les prédicats et les fonctions ne peuvent accepter que des termes en tant que paramètres, mais le premier paramètre est une formule. Certains langages construits sur la logique du premier ordre, tels que SMT-LIB 2.0, ajoutent ceci.

Conventions de notation

Pour plus de commodité, des conventions ont été développées concernant la priorité des opérateurs logiques, pour éviter d'avoir à écrire des parenthèses dans certains cas. Ces règles sont similaires à l' ordre des opérations en arithmétique. Une convention commune est :

  • est évalué en premier
  • et sont évalués ensuite
  • Les quantificateurs sont évalués ensuite
  • est évalué en dernier.

De plus, une ponctuation supplémentaire non requise par la définition peut être insérée pour faciliter la lecture des formules. Ainsi la formule

pourrait être écrit comme

Dans certains domaines, il est courant d'utiliser la notation infixe pour les relations et fonctions binaires, au lieu de la notation préfixe définie ci-dessus. Par exemple, en arithmétique, on écrit typiquement "2 + 2 = 4" au lieu de "=(+(2,2),4)". Il est courant de considérer les formules en notation infixe comme des abréviations pour les formules correspondantes en notation préfixe, cf. aussi structure du terme vs représentation .

Les définitions ci-dessus utilisent la notation infixe pour les connecteurs binaires tels que . Une convention moins courante est la notation polonaise , dans laquelle on écrit , et ainsi de suite devant leurs arguments plutôt qu'entre eux. Cette convention est avantageuse en ce qu'elle permet de supprimer tous les symboles de ponctuation. En tant que telle, la notation polonaise est compacte et élégante, mais rarement utilisée dans la pratique car elle est difficile à lire pour les humains. En notation polonaise, la formule

devient "∀x∀y→Pfx¬→ PxQfyxz".

Variables libres et liées

Dans une formule, une variable peut apparaître libre ou liée (ou les deux). Intuitivement, une occurrence de variable est libre dans une formule si elle n'est pas quantifiée : dans y P ( x , y ) , la seule occurrence de la variable x est libre alors que celle de y est bornée. Les occurrences de variables libres et liées dans une formule sont définies de manière inductive comme suit.

Formules atomiques
Si φ est une formule atomique, alors x apparaît libre dans φ si et seulement si x apparaît dans φ . De plus, il n'y a pas de variables liées dans aucune formule atomique.
Négation
x apparaît libre dans φ si et seulement si x apparaît libre dans φ . x apparaît lié dans ¬ φ si et seulement si x apparaît lié dans φ
Connecteurs binaires
x apparaît libre dans ( φψ ) si et seulement si x apparaît libre dans φ ou ψ . x apparaît lié dans ( φψ ) si et seulement si x apparaît lié dans φ ou ψ . La même règle s'applique à tout autre connecteur binaire à la place de →.
Quantificateurs
x apparaît libre dans y φ , si et seulement si x apparaît libre dans φ et x est un symbole différent de y . De plus, x apparaît lié dans y φ , si et seulement si x est y ou si x apparaît lié dans φ . La même règle s'applique avec à la place de .

Par exemple, dans xy ( P ( x ) → Q ( x , f ( x ), z )) , x et y n'apparaissent que liés, z n'apparaît que libre, et w n'est ni l'un ni l'autre car il n'apparaît pas dans le formule.

Les variables libres et liées d'une formule n'ont pas besoin d'être des ensembles disjoints : dans la formule P ( x ) → ∀ x Q ( x ) , la première occurrence de x , comme argument de P , est libre tandis que la seconde, comme argument de Q , est attaché.

Une formule en logique du premier ordre sans occurrences de variables libres est appelée une phrase du premier ordre . Ce sont les formules qui auront des valeurs de vérité bien définies sous une interprétation. Par exemple, si une formule telle que Phil( x ) est vraie doit dépendre de ce que x représente. Mais la phrase x Phil( x ) sera soit vraie soit fausse dans une interprétation donnée.

Exemple : groupes abéliens ordonnés

En mathématiques, le langage des groupes abéliens ordonnés a un symbole constant 0, un symbole de fonction unaire −, un symbole de fonction binaire + et un symbole de relation binaire . Puis:

  • Les expressions +( x , y ) et +( x , +( y , −( z ))) sont des termes . Ceux-ci sont généralement écrits comme x + y et x + yz .
  • Les expressions +( x , y ) = 0 et ≤(+( x , +( y , −( z ))), +( x , y )) sont des formules atomiques . Ceux - ci sont généralement écrites comme x + y = 0 et x + y - z  ≤  x + y .
  • L'expression est une formule , qui s'écrit généralement sous la forme Cette formule a une variable libre, z .

Les axiomes pour les groupes abéliens ordonnés peuvent être exprimés comme un ensemble de phrases dans la langue. Par exemple, l'axiome indiquant que le groupe est commutatif s'écrit généralement

Sémantique

Une interprétation d'une langue de premier ordre attribue une dénotation à chaque symbole non logique dans cette langue. Il détermine également un domaine de discours qui spécifie la plage des quantificateurs. Le résultat est que chaque terme se voit attribuer un objet qu'il représente, chaque prédicat se voit attribuer une propriété d'objets et chaque phrase se voit attribuer une valeur de vérité. De cette façon, une interprétation donne une signification sémantique aux termes, aux prédicats et aux formules de la langue. L'étude des interprétations des langages formels est appelée sémantique formelle . Ce qui suit est une description de la sémantique standard ou tarskienne pour la logique du premier ordre. (Il est également possible de définir la sémantique du jeu pour la logique du premier ordre , mais en plus d'exiger l' axiome du choix , la sémantique du jeu est en accord avec la sémantique tarskienne pour la logique du premier ordre, donc la sémantique du jeu ne sera pas élaborée ici.)

Le domaine du discours D est un ensemble non vide d'« objets » d'une certaine sorte. Intuitivement, une formule du premier ordre est une déclaration sur ces objets ; par exemple, énonce l'existence d'un objet x tel que le prédicat P est vrai lorsqu'il s'y réfère. Le domaine du discours est l'ensemble des objets considérés. Par exemple, on peut prendre pour l'ensemble des nombres entiers.

L'interprétation d'un symbole de fonction est une fonction. Par exemple, si le domaine du discours est constitué d'entiers, un symbole de fonction f d'arité 2 peut être interprété comme la fonction qui donne la somme de ses arguments. Autrement dit, le symbole f est associé à la fonction qui, dans cette interprétation, est l'addition.

L'interprétation d'un symbole constant est une fonction de l'ensemble à un élément D 0 à D , qui peut être simplement identifié à un objet dans D . Par exemple, une interprétation peut affecter la valeur au symbole constant .

L'interprétation d'un symbole de prédicat n- aire est un ensemble de n - uplets d'éléments du domaine du discours. Cela signifie que, étant donné une interprétation, un symbole de prédicat et n éléments du domaine du discours, on peut dire si le prédicat est vrai de ces éléments selon l'interprétation donnée. Par exemple, une interprétation I(P) d'un symbole de prédicat binaire P peut être l'ensemble de couples d'entiers tels que le premier est inférieur au second. Selon cette interprétation, le prédicat P serait vrai si son premier argument est inférieur au second.

Structures de premier ordre

La manière la plus courante de spécifier une interprétation (en particulier en mathématiques) est de spécifier une structure (également appelée modèle ; voir ci-dessous). La structure est constituée d'un ensemble non vide D qui forme le domaine du discours et d'une interprétation I des termes non logiques de la signature. Cette interprétation est elle-même une fonction :

  • A chaque symbole de fonction f d'arité n est affectée une fonction de à D . En particulier, à chaque symbole constant de la signature est affecté un individu dans le domaine du discours.
  • Chaque symbole de prédicat P d'arité n se voit attribuer une relation sur ou, de manière équivalente, une fonction de à . Ainsi, chaque symbole de prédicat est interprété par une fonction booléenne sur D .

Évaluation des valeurs de vérité

Une formule est évaluée comme vraie ou fausse selon une interprétation et une affectation de variable qui associe un élément du domaine du discours à chaque variable. La raison pour laquelle une affectation de variable est requise est de donner une signification aux formules avec des variables libres, telles que . La valeur de vérité de cette formule change selon que x et y désignent le même individu.

Premièrement, l'affectation de variable peut être étendue à tous les termes de la langue, avec pour résultat que chaque terme correspond à un seul élément du domaine du discours. Les règles suivantes sont utilisées pour effectuer cette affectation :

  1. Variables. Chaque variable x est évaluée à μ ( x )
  2. Les fonctions. Étant donné les termes qui ont été évalués en éléments du domaine du discours, et un symbole de fonction n- aire f , le terme est évalué en .

Ensuite, chaque formule se voit attribuer une valeur de vérité. La définition inductive utilisée pour effectuer cette affectation est appelée le T-schéma .

  1. Formules atomiques (1). Une formule est associée à la valeur vrai ou faux selon que , où sont l'évaluation des termes et est l'interprétation de , qui par hypothèse est un sous-ensemble de .
  2. Formules atomiques (2). Une formule est assignée vraie si et évalue au même objet du domaine du discours (voir la section sur l'égalité ci-dessous).
  3. Connecteurs logiques. Une formule sous la forme , , etc. est évaluée selon la table de vérité pour le connecteur en question, comme dans la logique propositionnelle.
  4. Quantificateurs existentiels. Une formule est vraie selon M et s'il existe une évaluation des variables qui ne diffère que par rapport à l'évaluation de x et telle que est vraie selon l'interprétation M et l'affectation des variables . Cette définition formelle capture l'idée qui est vraie si et seulement s'il existe un moyen de choisir une valeur pour x telle que φ( x ) est satisfaite.
  5. Quantificateurs universels. Une formule est vraie selon M et si φ( x ) est vraie pour chaque paire composée par l'interprétation M et une affectation variable qui diffère seulement de la valeur de x . Cela capture l'idée qui est vraie si chaque choix possible d'une valeur pour x fait que φ( x ) est vrai.

Si une formule ne contient pas de variables libres, de même qu'une phrase, alors l'affectation de variable initiale n'affecte pas sa valeur de vérité. En d'autres termes, une phrase est vraie selon M et si et seulement si elle est vraie selon M et toute autre affectation de variable .

Il existe une deuxième approche commune pour définir les valeurs de vérité qui ne repose pas sur des fonctions d'affectation de variables. Au lieu de cela, étant donné une interprétation M , on ajoute d'abord à la signature une collection de symboles constants, un pour chaque élément du domaine de discours dans M ; disons que pour chaque d dans le domaine le symbole constant c d est fixe. L'interprétation est étendue de sorte que chaque nouveau symbole constant soit affecté à son élément correspondant du domaine. On définit maintenant la vérité pour les formules quantifiées syntaxiquement, comme suit :

  1. Quantificateurs existentiels (alternatifs). Une formule est vraie selon M s'il existe un d dans le domaine du discours tel qu'il soit vrai . Voici le résultat de la substitution de c d pour chaque occurrence libre de x dans φ.
  2. Quantificateurs universels (alternatifs). Une formule est vraie selon M si, pour tout d dans le domaine du discours, est vraie selon M .

Cette approche alternative donne exactement les mêmes valeurs de vérité à toutes les phrases que l'approche via les affectations de variables.

Validité, satisfiabilité et conséquence logique

Si une phrase φ s'évalue à Vrai sous une interprétation donnée M , on dit que M satisfait ; c'est noté . Une phrase est satisfiable s'il existe une interprétation selon laquelle elle est vraie.

La satisfaisabilité des formules avec des variables libres est plus compliquée, car une interprétation à elle seule ne détermine pas la valeur de vérité d'une telle formule. La convention la plus courante est qu'une formule avec des variables libres est dite satisfaite par une interprétation si la formule reste vraie quels que soient les individus du domaine du discours qui sont affectés à ses variables libres. Cela revient à dire qu'une formule est satisfaite si et seulement si sa clôture universelle est satisfaite.

Une formule est logiquement valide (ou simplement valide ) si elle est vraie dans chaque interprétation. Ces formules jouent un rôle similaire aux tautologies en logique propositionnelle.

Une formule φ est une conséquence logique d'une formule ψ si chaque interprétation qui rend ψ vrai rend également φ vrai. Dans ce cas on dit que φ est logiquement impliqué par ψ.

Algébrisations

Une approche alternative de la sémantique de la logique du premier ordre passe par l'algèbre abstraite . Cette approche généralise les algèbres de Lindenbaum-Tarski de la logique propositionnelle. Il existe trois façons d'éliminer les variables quantifiées de la logique du premier ordre qui n'impliquent pas de remplacer les quantificateurs par d'autres opérateurs de termes de liaison de variables :

Ces algèbres sont tous des réseaux qui prolongent correctement l' algèbre booléenne à deux éléments .

Tarski et Givant (1987) ont montré que le fragment de logique du premier ordre qui n'a pas de phrase atomique dans le cadre de plus de trois quantificateurs a le même pouvoir expressif que l' algèbre de relation . Ce fragment est d'un grand intérêt car il suffit pour l'arithmétique de Peano et la plupart des théories axiomatiques des ensembles , y compris la ZFC canonique . Ils prouvent également que la logique du premier ordre avec une paire ordonnée primitive est équivalente à une algèbre relationnelle avec deux fonctions de projection de paires ordonnées .

Théories, modèles et classes élémentaires du premier ordre

Une théorie du premier ordre d'une signature particulière est un ensemble d' axiomes , qui sont des phrases composées de symboles de cette signature. L'ensemble des axiomes est souvent fini ou récursivement énumérable , auquel cas la théorie est dite effective . Certains auteurs exigent que les théories incluent également toutes les conséquences logiques des axiomes. Les axiomes sont considérés comme valables dans la théorie et à partir d'eux, d'autres phrases qui tiennent dans la théorie peuvent être dérivées.

Une structure du premier ordre qui satisfait toutes les phrases d'une théorie donnée est dite un modèle de la théorie. Une classe élémentaire est l'ensemble de toutes les structures satisfaisant une théorie particulière. Ces classes sont un sujet d'étude principal en théorie des modèles .

De nombreuses théories ont une interprétation voulue , un certain modèle qui est gardé à l'esprit lors de l'étude de la théorie. Par exemple, l'interprétation prévue de l'arithmétique de Peano se compose des nombres naturels habituels avec leurs opérations habituelles. Cependant, le théorème de Löwenheim-Skolem montre que la plupart des théories du premier ordre auront également d'autres modèles non standard .

Une théorie est cohérente s'il n'est pas possible de prouver une contradiction à partir des axiomes de la théorie. Une théorie est complète si, pour chaque formule dans sa signature, soit cette formule soit sa négation est une conséquence logique des axiomes de la théorie. Le théorème d'incomplétude de Gödel montre que les théories efficaces du premier ordre qui incluent une partie suffisante de la théorie des nombres naturels ne peuvent jamais être à la fois cohérentes et complètes.

Pour plus d'informations sur ce sujet voir Liste des théories du premier ordre et Théorie (logique mathématique)

Domaines vides

La définition ci-dessus exige que le domaine du discours de toute interprétation ne soit pas vide. Il existe des paramètres, tels que la logique inclusive , où les domaines vides sont autorisés. De plus, si une classe de structures algébriques comprend une structure vide (par exemple, il y a un poset vide ), cette classe ne peut être une classe élémentaire en logique du premier ordre que si les domaines vides sont autorisés ou si la structure vide est supprimée de la classe .

Cependant, les domaines vides présentent plusieurs difficultés :

  • De nombreuses règles d'inférence communes ne sont valables que lorsque le domaine du discours doit être non vide. Un exemple est la règle selon laquelle implique quand x est pas une variable libre . Cette règle, qui est utilisée pour mettre des formules sous forme normale prenex , est valable dans les domaines non vides, mais non valable si le domaine vide est autorisé.
  • La définition de la vérité dans une interprétation qui utilise une fonction d'affectation de variable ne peut pas fonctionner avec des domaines vides, car il n'y a pas de fonctions d'affectation de variable dont la plage est vide. (De même, on ne peut pas attribuer d'interprétations à des symboles constants.) Cette définition de vérité exige que l'on doive sélectionner une fonction d'attribution de variable (μ ci-dessus) avant que des valeurs de vérité pour des formules atomiques puissent être définies. Ensuite, la valeur de vérité d'une phrase est définie comme étant sa valeur de vérité sous n'importe quelle affectation de variable, et il est prouvé que cette valeur de vérité ne dépend pas de l'affectation choisie. Cette technique ne fonctionne pas s'il n'y a aucune fonction d'affectation ; il doit être modifié pour s'adapter aux domaines vides.

Ainsi, lorsque le domaine vide est autorisé, il doit souvent être traité comme un cas particulier. Cependant, la plupart des auteurs excluent simplement le domaine vide par définition.

Systèmes déductifs

Un système déductif est utilisé pour démontrer, sur une base purement syntaxique, qu'une formule est la conséquence logique d'une autre formule. Il existe de nombreux systèmes de ce type pour la logique du premier ordre, notamment les systèmes déductifs de style Hilbert , la déduction naturelle , le calcul des séquences , la méthode des tableaux et la résolution . Ceux-ci partagent la propriété commune qu'une déduction est un objet syntaxique fini ; le format de cet objet, et la façon dont il est construit, varient considérablement. Ces déductions finies elles-mêmes sont souvent appelées dérivations en théorie de la preuve. Elles sont aussi souvent appelées preuves, mais sont complètement formalisées contrairement aux preuves mathématiques en langage naturel .

Un système déductif est valable si une formule qui peut être dérivée dans le système est logiquement valide. Inversement, un système déductif est complet si chaque formule logiquement valide est dérivable. Tous les systèmes abordés dans cet article sont à la fois solides et complets. Ils partagent également la propriété qu'il est possible de vérifier efficacement qu'une déduction prétendument valide est en réalité une déduction ; de tels systèmes de déduction sont dits effectifs .

Une propriété clé des systèmes déductifs est qu'ils sont purement syntaxiques, de sorte que les dérivations peuvent être vérifiées sans tenir compte d'aucune interprétation. Ainsi, un argument solide est correct dans toutes les interprétations possibles de la langue, que cette interprétation concerne les mathématiques, l'économie ou un autre domaine.

En général, la conséquence logique en logique du premier ordre n'est que semi - décidable : si une phrase A implique logiquement une phrase B, alors cela peut être découvert (par exemple, en cherchant une preuve jusqu'à ce qu'elle soit trouvée, en utilisant une preuve efficace, solide et complète système). Cependant, si A n'implique pas logiquement B, cela ne signifie pas que A implique logiquement la négation de B. Il n'y a pas de procédure efficace qui, étant donné les formules A et B, décide toujours correctement si A implique logiquement B.

Règles d'inférence

Une règle d'inférence stipule que, étant donné une formule particulière (ou un ensemble de formules) avec une certaine propriété comme hypothèse, une autre formule spécifique (ou un ensemble de formules) peut être dérivée comme conclusion. La règle est saine (ou préservant la vérité) si elle préserve la validité en ce sens que chaque fois qu'une interprétation satisfait l'hypothèse, cette interprétation satisfait également la conclusion.

Par exemple, une règle d'inférence courante est la règle de substitution . Si t est un terme et est une formule contenant éventuellement la variable x , alors φ[ t / x ] est le résultat du remplacement de toutes les instances libres de x par t dans φ. La règle de substitution stipule que pour tout φ et tout terme t , on peut conclure φ[ t / x ] à partir de φ à condition qu'aucune variable libre de t ne devienne liée pendant le processus de substitution. (Si une variable libre de t devient liée, alors pour substituer t à x, il est d'abord nécessaire de modifier les variables liées de pour qu'elles diffèrent des variables libres de t .)

Pour voir pourquoi la restriction sur les variables liées est nécessaire, considérons la formule logiquement valide φ donnée par , dans la signature de (0,1,+,×,=) de l'arithmétique. Si t est le terme "x + 1", la formule [ t / y ] est , ce qui sera faux dans de nombreuses interprétations. Le problème est que la variable libre x de t est devenue liée lors de la substitution. Le remplacement prévu peut être obtenu en renommant la variable liée x de φ en quelque chose d'autre, disons z , de sorte que la formule après substitution soit , ce qui est à nouveau logiquement valide.

La règle de substitution démontre plusieurs aspects communs des règles d'inférence. C'est entièrement syntaxique ; on peut dire s'il a été correctement appliqué sans faire appel à aucune interprétation. Il a des limites (définies syntaxiquement) sur le moment où il peut être appliqué, qui doivent être respectées pour préserver l'exactitude des dérivations. De plus, comme c'est souvent le cas, ces limitations sont nécessaires en raison des interactions entre les variables libres et liées qui se produisent lors des manipulations syntaxiques des formules impliquées dans la règle d'inférence.

Systèmes à la Hilbert et déduction naturelle

Une déduction dans un système déductif de style Hilbert est une liste de formules, dont chacune est un axiome logique , une hypothèse qui a été supposée pour la dérivation à portée de main, ou découle de formules précédentes via une règle d'inférence. Les axiomes logiques consistent en plusieurs schémas d'axiomes de formules logiquement valides ; ceux-ci englobent une quantité importante de logique propositionnelle. Les règles d'inférence permettent la manipulation de quantificateurs. Les systèmes typiques de style Hilbert ont un petit nombre de règles d'inférence, ainsi que plusieurs schémas infinis d'axiomes logiques. Il est courant de n'avoir que le modus ponens et la généralisation universelle comme règles d'inférence.

Les systèmes de déduction naturelle ressemblent aux systèmes de style Hilbert en ce qu'une déduction est une liste finie de formules. Cependant, les systèmes de déduction naturelle n'ont pas d'axiomes logiques ; ils compensent en ajoutant des règles d'inférence supplémentaires qui peuvent être utilisées pour manipuler les connecteurs logiques dans les formules de la preuve.

Calcul séquentiel

Le calcul des séquences a été développé pour étudier les propriétés des systèmes de déduction naturelle. Au lieu de travailler avec une formule à la fois, il utilise des séquences , qui sont des expressions de la forme

où A 1 , ..., A n , B 1 , ..., B k sont des formules et le symbole du tourniquet est utilisé comme signe de ponctuation pour séparer les deux moitiés. Intuitivement, un séquent exprime l'idée qui implique .

Méthode Tableaux

Une preuve en tableaux pour la formule propositionnelle ((a ∨ ¬b) ∧ b) → a.

Contrairement aux méthodes qui viennent d'être décrites, les dérivations dans la méthode des tableaux ne sont pas des listes de formules. Au lieu de cela, une dérivation est un arbre de formules. Pour montrer qu'une formule A est prouvable, la méthode des tableaux tente de démontrer que la négation de A est insatisfiable. L'arbre de la dérivation a à sa racine ; les branches de l'arbre d'une manière qui reflète la structure de la formule. Par exemple, montrer que c'est insatisfiable nécessite de montrer que C et D sont chacun insatisfiables ; cela correspond à un point de branchement dans l'arbre avec le parent et les enfants C et D.

Résolution

La règle de résolution est une règle d'inférence unique qui, avec l' unification , est solide et complète pour la logique du premier ordre. Comme avec la méthode des tableaux, une formule est prouvée en montrant que la négation de la formule est insatisfiable. La résolution est couramment utilisée dans la démonstration automatisée de théorèmes.

La méthode de résolution ne fonctionne qu'avec des formules qui sont des disjonctions de formules atomiques ; les formules arbitraires doivent d'abord être converties sous cette forme par skolémisation . La règle de résolution stipule qu'à partir des hypothèses et , la conclusion peut être obtenue.

Identités prouvables

De nombreuses identités peuvent être prouvées, qui établissent des équivalences entre des formules particulières. Ces identités permettent de réorganiser les formules en déplaçant les quantificateurs sur d'autres connecteurs et sont utiles pour mettre des formules sous forme normale prenex . Certaines identités prouvables incluent :

(où ne doit pas apparaître libre dans )
(où ne doit pas apparaître libre dans )

L'égalité et ses axiomes

Il existe plusieurs conventions différentes pour utiliser l'égalité (ou l'identité) dans la logique du premier ordre. La convention la plus courante, connue sous le nom de logique du premier ordre avec égalité , inclut le symbole d'égalité en tant que symbole logique primitif qui est toujours interprété comme la relation d'égalité réelle entre les membres du domaine du discours, de sorte que les « deux » membres donnés sont les même membre. Cette approche ajoute également certains axiomes sur l'égalité au système déductif employé. Ces axiomes d'égalité sont :

  1. Réflexivité . Pour chaque variable x , x = x .
  2. Remplacement des fonctions. Pour toutes les variables x et y , et tout symbole de fonction f ,
    x = yf (..., x ,...) = f (..., y ,...).
  3. Substitution des formules . Pour toutes variables x et y et toute formule φ( x ), si φ' est obtenu en remplaçant n'importe quel nombre d'occurrences libres de x dans φ par y , tel que celles-ci restent des occurrences libres de y , alors
    x = y → (φ → φ').

Ce sont des schémas d'axiomes , dont chacun spécifie un ensemble infini d'axiomes. Le troisième schéma est connu sous le nom de loi de Leibniz , "le principe de substituabilité", "l'indiscernabilité des identiques", ou "la propriété de remplacement". Le deuxième schéma, impliquant le symbole de fonction f , est (équivalent à) un cas particulier du troisième schéma, utilisant la formule

x = y → ( f (..., x ,...) = z → f (..., y ,...) = z).

De nombreuses autres propriétés d'égalité sont des conséquences des axiomes ci-dessus, par exemple :

  1. Symétrie. Si x = y alors y = x .
  2. Transitivité. Si x = y et y = z alors x = z .

Logique du premier ordre sans égalité

Une autre approche considère la relation d'égalité comme un symbole non logique. Cette convention est connue sous le nom de logique du premier ordre sans égalité . Si une relation d'égalité est incluse dans la signature, les axiomes d'égalité doivent maintenant être ajoutés aux théories considérées, si désiré, au lieu d'être considérés comme des règles de logique. La principale différence entre cette méthode et la logique du premier ordre avec égalité est qu'une interprétation peut désormais interpréter deux individus distincts comme « égal » (bien que, selon la loi de Leibniz, ceux-ci satisferont exactement les mêmes formules quelle que soit l'interprétation). C'est-à-dire que la relation d'égalité peut maintenant être interprétée par une relation d'équivalence arbitraire sur le domaine du discours qui est congruente par rapport aux fonctions et aux relations de l'interprétation.

Lorsque cette seconde convention est suivie, le terme modèle normal est utilisé pour désigner une interprétation où aucun individu distinct a et b ne satisfait a = b . Dans la logique du premier ordre avec égalité, seuls les modèles normaux sont considérés, et il n'y a donc pas de terme pour un modèle autre qu'un modèle normal. Lorsque la logique du premier ordre sans égalité est étudiée, il est nécessaire de modifier les énoncés de résultats tels que le théorème de Löwenheim-Skolem afin que seuls les modèles normaux soient considérés.

La logique du premier ordre sans égalité est souvent employée dans le contexte de l' arithmétique du second ordre et d'autres théories arithmétiques d'ordre supérieur, où la relation d'égalité entre les ensembles de nombres naturels est généralement omise.

Définir l'égalité dans une théorie

Si une théorie a une formule binaire A ( x , y ) qui satisfait la réflexivité et la loi de Leibniz, la théorie est dite avoir l'égalité, ou être une théorie avec égalité. La théorie peut ne pas avoir toutes les instances des schémas ci-dessus comme axiomes, mais plutôt comme théorèmes dérivables. Par exemple, dans les théories sans symboles de fonction et un nombre fini de relations, il est possible de définir l' égalité en termes de relations, en définissant les deux termes s et t égaux si une relation est inchangée en changeant s en t dans toute argumentation.

Certaines théories autorisent d'autres définitions ad hoc de l'égalité :

  • Dans la théorie des ordres partiels avec un symbole de relation ≤, on pourrait définir s = t être une abréviation pour stts .
  • En théorie des ensembles avec une relation ∈, on peut définir s = t comme une abréviation de x ( sxtx ) ∧ ∀ x ( xsxt ) . Cette définition de l'égalité satisfait alors automatiquement les axiomes de l'égalité. Dans ce cas, il faut remplacer l' axiome habituel d'extensionnalité , qui peut être énoncé comme , par une formulation alternative , qui dit que si les ensembles x et y ont les mêmes éléments, alors ils appartiennent également aux mêmes ensembles.

Propriétés métalogiques

Une motivation pour l'utilisation de la logique du premier ordre, plutôt que de la logique d'ordre supérieur , est que la logique du premier ordre a de nombreuses propriétés métalogiques que les logiques plus fortes n'ont pas. Ces résultats concernent les propriétés générales de la logique du premier ordre elle-même, plutôt que les propriétés des théories individuelles. Ils fournissent des outils fondamentaux pour la construction de modèles de théories du premier ordre.

Intégralité et indécidabilité

Le théorème de complétude de Gödel , prouvé par Kurt Gödel en 1929, établit qu'il existe des systèmes déductifs solides, complets et efficaces pour la logique du premier ordre, et ainsi la relation de conséquence logique du premier ordre est capturée par la prouvabilité finie. Naïvement, l'affirmation qu'une formule φ implique logiquement une formule ψ dépend de chaque modèle de φ ; ces modèles seront en général de cardinalité arbitrairement grande, et donc la conséquence logique ne peut pas être vérifiée efficacement en vérifiant chaque modèle. Cependant, il est possible d'énumérer toutes les dérivations finies et de rechercher une dérivation de ψ à partir de φ. Si ψ est logiquement impliqué par φ, une telle dérivation sera finalement trouvée. Ainsi la conséquence logique du premier ordre est semi - décidable : il est possible de faire une énumération effective de toutes les paires de phrases (φ,ψ) telles que ψ est une conséquence logique de φ.

Contrairement à la logique propositionnelle, la logique du premier ordre est indécidable (bien que semi-décidable), à ​​condition que le langage ait au moins un prédicat d'arité au moins 2 (autre que l'égalité). Cela signifie qu'il n'y a pas de procédure de décision qui détermine si des formules arbitraires sont logiquement valides. Ce résultat a été établi indépendamment par Alonzo Church et Alan Turing en 1936 et 1937, respectivement, donnant une réponse négative au problème d'Entscheidungs posé par David Hilbert et Wilhelm Ackermann en 1928. Leurs preuves démontrent un lien entre l'insolvabilité du problème de décision pour le premier- la logique d'ordre et l'insolvabilité du problème d'arrêt .

Il existe des systèmes plus faibles que la logique complète du premier ordre pour lesquels la relation de conséquence logique est décidable. Il s'agit notamment de la logique propositionnelle et de la logique des prédicats monadiques , qui est une logique du premier ordre limitée aux symboles de prédicats unaires et à aucun symbole de fonction. D'autres logiques sans symboles de fonction qui sont décidables sont le fragment gardé de la logique du premier ordre, ainsi que la logique à deux variables . La classe de formules du premier ordre de Bernays-Schönfinkel est également décidable. Des sous-ensembles décidables de la logique du premier ordre sont également étudiés dans le cadre des logiques de description .

Le théorème de Löwenheim-Skolem

Le théorème de Löwenheim-Skolem montre que si une théorie du premier ordre de cardinalité a un modèle infini, alors elle a des modèles de chaque cardinalité infinie supérieure ou égale à λ. L' un des premiers résultats dans la théorie des modèles , cela implique qu'il est impossible de caractériser dénombrabilité ou uncountability dans une langue de premier ordre avec une signature dénombrable. C'est-à-dire qu'il n'y a pas de formule du premier ordre φ( x ) telle qu'une structure arbitraire M satisfait φ si et seulement si le domaine de discours de M est dénombrable (ou, dans le second cas, indénombrable).

Le théorème de Löwenheim-Skolem implique que les structures infinies ne peuvent pas être catégoriquement axiomatisées en logique du premier ordre. Par exemple, il n'y a pas de théorie du premier ordre dont le seul modèle est la droite réelle : toute théorie du premier ordre avec un modèle infini a aussi un modèle de cardinalité plus grand que le continu. Puisque la ligne réelle est infinie, toute théorie satisfaite par la ligne réelle est également satisfaite par certains modèles non standard . Lorsque le théorème de Löwenheim-Skolem est appliqué aux théories des ensembles du premier ordre, les conséquences non intuitives sont connues sous le nom de paradoxe de Skolem .

Le théorème de compacité

Le théorème de compacité stipule qu'un ensemble de phrases du premier ordre a un modèle si et seulement si chaque sous-ensemble fini de celui-ci a un modèle. Cela implique que si une formule est une conséquence logique d'un ensemble infini d'axiomes du premier ordre, alors c'est une conséquence logique d'un nombre fini de ces axiomes. Ce théorème a été prouvé en premier par Kurt Gödel en conséquence du théorème de complétude, mais de nombreuses preuves supplémentaires ont été obtenues au fil du temps. C'est un outil central dans la théorie des modèles, fournissant une méthode fondamentale pour la construction de modèles.

Le théorème de compacité a un effet limitatif sur les collections de structures du premier ordre qui sont des classes élémentaires. Par exemple, le théorème de compacité implique que toute théorie qui a des modèles finis arbitrairement grands a un modèle infini. Ainsi la classe de tous les graphes finis n'est pas une classe élémentaire (il en va de même pour beaucoup d'autres structures algébriques).

Il existe également des limitations plus subtiles de la logique du premier ordre qui sont impliquées par le théorème de compacité. Par exemple, en informatique, de nombreuses situations peuvent être modélisées sous la forme d'un graphe orienté d'états (nœuds) et de connexions (arêtes dirigées). La validation d'un tel système peut nécessiter de montrer qu'aucun "mauvais" état ne peut être atteint à partir d'un quelconque "bon" état. Ainsi on cherche à déterminer si les bons et mauvais états sont dans des composantes connexes différentes du graphe. Cependant, le théorème de compacité peut être utilisé pour montrer que les graphes connectés ne sont pas une classe élémentaire en logique du premier ordre, et il n'y a pas de formule φ( x , y ) de la logique du premier ordre, dans la logique des graphes , qui exprime le idée qu'il existe un chemin de x à y . Cependant, la connexité peut être exprimée en logique du second ordre , mais pas seulement avec des quantificateurs d'ensembles existentiels, car elle bénéficie également de la compacité.

Le théorème de Lindström

Per Lindström a montré que les propriétés métalogiques dont nous venons de parler caractérisent en fait la logique du premier ordre dans le sens où aucune logique plus forte ne peut également avoir ces propriétés (Ebbinghaus et Flum 1994, chapitre XIII). Lindström a défini une classe de systèmes logiques abstraits et une définition rigoureuse de la force relative d'un membre de cette classe. Il a établi deux théorèmes pour les systèmes de ce type :

  • Un système logique satisfaisant la définition de Lindström qui contient la logique du premier ordre et satisfait à la fois le théorème de Löwenheim-Skolem et le théorème de compacité doit être équivalent à la logique du premier ordre.
  • Un système logique satisfaisant la définition de Lindström qui a une relation de conséquence logique semi-décidable et satisfait le théorème de Löwenheim-Skolem doit être équivalent à la logique du premier ordre.

Limites

Bien que la logique du premier ordre soit suffisante pour formaliser une grande partie des mathématiques et soit couramment utilisée en informatique et dans d'autres domaines, elle présente certaines limites. Il s'agit notamment des limitations de son expressivité et des limitations des fragments de langues naturelles qu'il peut décrire.

Par exemple, la logique du premier ordre est indécidable, ce qui signifie qu'un algorithme de décision solide, complet et final pour la prouvabilité est impossible. Cela a conduit à l'étude de fragments décidables intéressants, tels que C 2 : logique du premier ordre à deux variables et les quantificateurs de comptage et .

Expressivité

Le théorème de Löwenheim-Skolem montre que si une théorie du premier ordre a un modèle infini, alors elle a des modèles infinis de chaque cardinal. En particulier, aucune théorie du premier ordre avec un modèle infini ne peut être catégorique . Ainsi il n'y a pas de théorie du premier ordre dont le seul modèle a l'ensemble des nombres naturels comme domaine, ou dont le seul modèle a l'ensemble des nombres réels comme domaine. De nombreuses extensions de la logique du premier ordre, y compris les logiques infinités et les logiques d'ordre supérieur, sont plus expressives dans le sens où elles permettent des axiomatisations catégoriques des nombres naturels ou des nombres réels. Cette expressivité a cependant un coût métalogique : selon le théorème de Lindström , le théorème de compacité et le théorème descendant de Löwenheim-Skolem ne peuvent tenir dans aucune logique plus forte que le premier ordre.

Formaliser les langues naturelles

La logique du premier ordre est capable de formaliser de nombreuses constructions de quantificateurs simples en langage naturel, telles que « chaque personne qui vit à Perth vit en Australie ». Mais il existe de nombreuses caractéristiques plus compliquées du langage naturel qui ne peuvent pas être exprimées dans la logique du premier ordre (à tri unique). « Tout système logique approprié comme instrument pour l'analyse du langage naturel a besoin d'une structure beaucoup plus riche que la logique des prédicats du premier ordre ».

Taper Exemple Commenter
Quantification sur les propriétés Si Jean est satisfait de lui-même, alors il y a au moins une chose qu'il a en commun avec Pierre. L'exemple nécessite un quantificateur sur les prédicats, qui ne peut pas être implémenté dans une logique du premier ordre à tri simple : Zj → ∃X(Xj∧Xp) .
Quantification sur les propriétés Le Père Noël a tous les attributs d'un sadique. L'exemple nécessite des quantificateurs sur des prédicats, qui ne peuvent pas être implémentés dans une logique du premier ordre à tri simple : ∀X(∀x(Sx → Xx) → Xs) .
Adverbe de prédicat John marche vite. L'exemple ne peut pas être analysé comme Wj Qj ;
Les adverbes de prédicat ne sont pas le même genre de chose que les prédicats de second ordre tels que la couleur.
Adjectif relatif Jumbo est un petit éléphant. L'exemple ne peut pas être analysé comme Sj Ej ;
les adjectifs de prédicat ne sont pas le même genre de chose que les prédicats de second ordre tels que la couleur.
Modificateur adverbial de prédicat John marche très vite. -
Modificateur d'adjectif relatif Jumbo est terriblement petit. Une expression telle que "terriblement", lorsqu'elle est appliquée à un adjectif relatif tel que "petit", résulte en un nouvel adjectif relatif composite "terriblement petit".
Prépositions Mary est assise à côté de John. La préposition « à côté de » lorsqu'elle est appliquée à « Jean » donne le prédicat adverbial « à côté de Jean ».

Restrictions, extensions et variations

Il existe de nombreuses variantes de la logique du premier ordre. Certains d'entre eux sont inessentiels dans le sens où ils changent simplement la notation sans affecter la sémantique. D'autres modifient le pouvoir expressif de manière plus significative, en étendant la sémantique grâce à des quantificateurs supplémentaires ou à d'autres nouveaux symboles logiques. Par exemple, les logiques infinités permettent des formules de taille infinie, et les logiques modales ajoutent des symboles pour la possibilité et la nécessité.

Langues restreintes

La logique du premier ordre peut être étudiée dans les langues avec moins de symboles logiques que ceux décrits ci-dessus.

  • Parce que peut être exprimé comme , et peut être exprimé comme , l'un des deux quantificateurs et peut être supprimé.
  • Puisque peut être exprimé comme et peut être exprimé comme , soit ou peut être supprimé. En d'autres termes, il suffit d'avoir et , ou et , comme seuls connecteurs logiques.
  • De même, il suffit d'avoir uniquement et comme connecteurs logiques, ou de n'avoir que l' opérateur de trait de Sheffer (NAND) ou de flèche de Peirce (NOR).
  • Il est possible d'éviter totalement les symboles de fonction et les symboles constants, en les réécrivant via des symboles de prédicat de manière appropriée. Par exemple, au lieu d'utiliser un symbole constant, on peut utiliser un prédicat (interprété comme ) et remplacer chaque prédicat tel que par . Une fonction telle que sera également remplacée par un prédicat interprété comme . Ce changement nécessite d'ajouter des axiomes supplémentaires à la théorie à portée de main, de sorte que les interprétations des symboles de prédicat utilisés aient la sémantique correcte.

De telles restrictions sont utiles en tant que technique pour réduire le nombre de règles d'inférence ou de schémas d'axiome dans les systèmes déductifs, ce qui conduit à des preuves plus courtes de résultats métalogiques. Le coût des restrictions est qu'il devient plus difficile d'exprimer des déclarations en langage naturel dans le système formel en question, car les connecteurs logiques utilisés dans les déclarations en langage naturel doivent être remplacés par leurs définitions (plus longues) en termes de collection restreinte de connecteurs logiques. De même, les dérivations dans les systèmes limités peuvent être plus longues que les dérivations dans les systèmes qui incluent des connecteurs supplémentaires. Il y a donc un compromis entre la facilité de travailler au sein du système formel et la facilité de prouver des résultats sur le système formel.

Il est également possible de restreindre les arités des symboles de fonction et des symboles de prédicat, dans des théories suffisamment expressives. On peut en principe se passer entièrement des fonctions d'arité supérieure à 2 et des prédicats d'arité supérieure à 1 dans les théories qui incluent une fonction d'appariement . C'est une fonction d'arité 2 qui prend des paires d'éléments du domaine et renvoie une paire ordonnée les contenant. Il suffit également d'avoir deux symboles de prédicat d'arité 2 qui définissent des fonctions de projection d'une paire ordonnée à ses composants. Dans les deux cas, il est nécessaire que les axiomes naturels pour une fonction d'appariement et ses projections soient satisfaits.

Logique à plusieurs tris

Les interprétations ordinaires du premier ordre ont un seul domaine de discours sur lequel s'étendent tous les quantificateurs. La logique du premier ordre à plusieurs tris permet aux variables d'avoir différentes sortes , qui ont des domaines différents. Ceci est également appelé logique du premier ordre typée , et les sortes sont appelées types (comme dans le type de données ), mais ce n'est pas la même chose que la théorie des types du premier ordre . La logique du premier ordre à plusieurs tris est souvent utilisée dans l'étude de l' arithmétique du second ordre .

Lorsqu'il n'y a qu'un nombre fini de sortes dans une théorie, la logique du premier ordre à plusieurs tris peut être réduite à une logique du premier ordre à un seul tri. On introduit dans la théorie des tris simples un symbole de prédicat unaire pour chaque sorte dans la théorie des tris multiples, et ajoute un axiome disant que ces prédicats unaires partitionnent le domaine du discours. Par exemple, s'il y a deux sortes, on ajoute des symboles de prédicat et et l'axiome

.

Alors les éléments satisfaisants sont pensés comme des éléments de la première sorte, et les éléments satisfaisants comme des éléments de la seconde sorte. On peut quantifier sur chaque sorte en utilisant le symbole de prédicat correspondant pour limiter la plage de quantification. Par exemple, pour dire qu'il existe un élément de la première sorte satisfaisant la formule φ( x ), on écrit

.

Quantificateurs supplémentaires

Des quantificateurs supplémentaires peuvent être ajoutés à la logique du premier ordre.

  • Parfois, il est utile de dire que " P ( x ) est valable pour exactement un x ", ce qui peut être exprimé par ∃ ! x P ( x ) . Cette notation, appelée quantification d'unicité , peut être prise pour abréger une formule telle que x ( P ( x ) ∧∀ y ( P ( y ) → ( x = y ))) .
  • La logique du premier ordre avec des quantificateurs supplémentaires a de nouveaux quantificateurs Qx ,..., avec des significations telles que "il y a beaucoup de x tels que ...". Voir aussi les quantificateurs de branchement et les quantificateurs pluriels de George Boolos et d'autres.
  • Les quantificateurs bornés sont souvent utilisés dans l'étude de la théorie des ensembles ou de l'arithmétique.

Logiques infinités

La logique de l'infini permet des phrases infiniment longues. Par exemple, on peut autoriser une conjonction ou une disjonction d'une infinité de formules, ou une quantification sur une infinité de variables. Des phrases infiniment longues apparaissent dans les domaines des mathématiques, y compris la topologie et la théorie des modèles .

La logique infinité généralise la logique du premier ordre pour autoriser des formules de longueur infinie. La manière la plus courante par laquelle les formules peuvent devenir infinies est à travers des conjonctions et des disjonctions infinies. Cependant, il est également possible d'admettre des signatures généralisées dans lesquelles les symboles de fonction et de relation sont autorisés à avoir des arités infinies, ou dans lesquelles les quantificateurs peuvent lier une infinité de variables. Parce qu'une formule infinie ne peut pas être représentée par une chaîne finie, il est nécessaire de choisir une autre représentation des formules ; la représentation habituelle dans ce contexte est un arbre. Ainsi, les formules sont, essentiellement, identifiées avec leurs arbres d'analyse, plutôt qu'avec les chaînes analysées.

Les logiques infinités les plus couramment étudiées sont notées L αβ , où α et sont chacun soit des nombres cardinaux, soit le symbole ∞. Dans cette notation, la logique du premier ordre ordinaire est L ωω . Dans la logique L ∞ω , les conjonctions ou disjonctions arbitraires sont autorisées lors de la construction de formules, et il existe une offre illimitée de variables. Plus généralement, la logique qui permet des conjonctions ou des disjonctions avec moins de κ constituants est connue sous le nom de L κω . Par exemple, L w 1 ω permet dénombrables conjonctions et disjonctions.

L'ensemble des variables libres dans une formule de L κω peut avoir n'importe quelle cardinalité strictement inférieure à κ, mais seulement un nombre fini d'entre elles peuvent être dans la portée d'un quantificateur lorsqu'une formule apparaît comme une sous-formule d'une autre. Dans d'autres logiques infinités, une sous-formule peut être dans la portée d'une infinité de quantificateurs. Par exemple, en L κ∞ , un seul quantificateur universel ou existentiel peut se lier arbitrairement plusieurs variables simultanément. De même, la logique L κλ permet la quantification simultanée sur moins que les variables X, ainsi que des conjonctions et des disjonctions de taille inférieure à κ.

Logiques non classiques et modales

  • La logique intuitionniste du premier ordre utilise le calcul propositionnel intuitionniste plutôt que classique ; par exemple, ¬¬φ n'a pas besoin d'être équivalent à φ.
  • La logique modale du premier ordre permet de décrire d'autres mondes possibles ainsi que ce monde contingentement vrai que nous habitons. Dans certaines versions, l'ensemble des mondes possibles varie en fonction du monde possible dans lequel on habite. La logique modale a des opérateurs modaux supplémentaires avec des significations qui peuvent être caractérisées de manière informelle comme, par exemple "il est nécessaire que " (vrai dans tous les mondes possibles) et "il est possible que " (vrai dans un monde possible). Avec la logique standard du premier ordre, nous avons un seul domaine et chaque prédicat se voit attribuer une extension. Avec la logique modale du premier ordre, nous avons une fonction de domaine qui attribue à chaque monde possible son propre domaine, de sorte que chaque prédicat n'obtienne une extension que par rapport à ces mondes possibles. Cela nous permet de modéliser des cas où, par exemple, Alex est un philosophe, mais aurait pu être un mathématicien, et pourrait ne pas avoir existé du tout. Dans le premier monde possible, P ( a ) est vrai, dans le second P ( a ) est faux, et dans le troisième monde possible, il n'y a pas du tout de a dans le domaine.
  • Les logiques floues du premier ordre sont des extensions du premier ordre des logiques floues propositionnelles plutôt que du calcul propositionnel classique.

Logique de point fixe

La logique des points fixes étend la logique du premier ordre en ajoutant la fermeture sous les points les moins fixes des opérateurs positifs.

Logiques d'ordre supérieur

Le trait caractéristique de la logique du premier ordre est que les individus peuvent être quantifiés, mais pas les prédicats. Ainsi

est une formule légale de premier ordre, mais

n'est pas, dans la plupart des formalisations de la logique du premier ordre. La logique du second ordre étend la logique du premier ordre en ajoutant ce dernier type de quantification. D'autres logiques d'ordre supérieur permettent une quantification sur des types encore plus élevés que ne le permet la logique de second ordre. Ces types supérieurs incluent les relations entre les relations, les fonctions des relations aux relations entre les relations et d'autres objets de type supérieur. Ainsi, le "premier" dans la logique du premier ordre décrit le type d'objets qui peuvent être quantifiés.

Contrairement à la logique du premier ordre, pour laquelle une seule sémantique est étudiée, il existe plusieurs sémantiques possibles pour la logique du second ordre. La sémantique la plus couramment utilisée pour la logique du second ordre et d'ordre supérieur est connue sous le nom de sémantique complète . La combinaison de quantificateurs supplémentaires et de la sémantique complète de ces quantificateurs rend la logique d'ordre supérieur plus forte que la logique de premier ordre. En particulier, la relation de conséquence logique (sémantique) pour la logique de second ordre et d'ordre supérieur n'est pas semi-décidable ; il n'y a pas de système de déduction efficace pour la logique du second ordre qui soit solide et complet sous une sémantique complète.

La logique du second ordre avec une sémantique complète est plus expressive que la logique du premier ordre. Par exemple, il est possible de créer des systèmes d'axiomes en logique du second ordre qui caractérisent de manière unique les nombres naturels et la droite réelle. Le coût de cette expressivité est que les logiques de second ordre et d'ordre supérieur ont moins de propriétés métalogiques attractives que la logique de premier ordre. Par exemple, le théorème de Löwenheim-Skolem et le théorème de compacité de la logique du premier ordre deviennent faux lorsqu'ils sont généralisés aux logiques d'ordre supérieur avec une sémantique complète.

Démonstration automatisée de théorèmes et méthodes formelles

La preuve automatisée de théorèmes fait référence au développement de programmes informatiques qui recherchent et trouvent des dérivations (preuves formelles) de théorèmes mathématiques. Trouver des dérivations est une tâche difficile car l' espace de recherche peut être très grand ; une recherche exhaustive de toutes les dérivations possibles est théoriquement possible mais informatiquement infaisable pour de nombreux systèmes d'intérêt en mathématiques. Ainsi, des fonctions heuristiques compliquées sont développées pour tenter de trouver une dérivation en moins de temps qu'une recherche aveugle.

Le domaine connexe de la vérification automatisée des preuves utilise des programmes informatiques pour vérifier que les preuves créées par l'homme sont correctes. Contrairement aux démonstrateurs de théorèmes automatisés complexes, les systèmes de vérification peuvent être suffisamment petits pour que leur exactitude puisse être vérifiée à la fois manuellement et par une vérification logicielle automatisée. Cette validation du vérificateur de preuve est nécessaire pour s'assurer que toute dérivation étiquetée comme « correcte » est réellement correcte.

Certains vérificateurs de preuves, tels que Metamath , insistent pour avoir une dérivation complète en entrée. D'autres, comme Mizar et Isabelle , prennent un croquis de preuve bien formaté (qui peut être encore très long et détaillé) et complètent les pièces manquantes en effectuant de simples recherches de preuves ou en appliquant des procédures de décision connues : la dérivation qui en résulte est ensuite vérifiée par un petit noyau "noyau". Beaucoup de ces systèmes sont principalement destinés à une utilisation interactive par les mathématiciens humains : ils sont connus sous le nom d' assistants de preuve . Ils peuvent également utiliser des logiques formelles plus fortes que la logique du premier ordre, comme la théorie des types. Parce qu'une dérivation complète de tout résultat non trivial dans un système déductif du premier ordre sera extrêmement longue à écrire pour un humain, les résultats sont souvent formalisés comme une série de lemmes, pour lesquels les dérivations peuvent être construites séparément.

Les démonstrateurs de théorèmes automatisés sont également utilisés pour mettre en œuvre la vérification formelle en informatique. Dans ce cadre, les démonstrateurs de théorèmes sont utilisés pour vérifier l'exactitude des programmes et du matériel tels que les processeurs par rapport à une spécification formelle . Parce qu'une telle analyse est chronophage et donc coûteuse, elle est généralement réservée aux projets dans lesquels un dysfonctionnement aurait de graves conséquences humaines ou financières.

Pour le problème de la vérification de modèle , des algorithmes efficaces sont connus pour décider si une structure finie d'entrée satisfait une formule du premier ordre, en plus des limites de complexité de calcul : voir Vérification de modèle § Logique du premier ordre .

Voir également

Remarques

Les références

Liens externes