Worldlex Wiki Une théorie portant sur un sujet donné, comme la théorie des ensembles , une théorie des groupes ou une théorie formelle de l' arithmétique , est généralement une logique du premier ordre munie d'un domaine de discours spécifié (sur lequel les variables quantifiées prennent des valeurs), d'un nombre fini de fonctions de ce domaine vers lui-même, d'un nombre fini de prédicats définis sur ce domaine et d'un ensemble d'axiomes supposés valides à leur sujet. Le terme « théorie » est parfois compris, dans un sens plus formel, comme un simple ensemble d'énoncés de la logique du premier ordre.
Le terme « premier ordre » distingue la logique du premier ordre de la logique d'ordre supérieur , dans laquelle les prédicats ont d'autres prédicats ou des fonctions comme arguments, ou dans laquelle la quantification sur les prédicats, les fonctions, ou les deux, est autorisée. 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 corrects (toutes les propositions démontrables sont vraies dans tous les modèles) et complets (toutes les propositions vraies dans tous les modèles sont démontrables). Bien que la relation de conséquence logique ne soit que semi-décidable , des progrès considérables ont été réalisés dans la démonstration automatique de théorèmes en logique du premier ordre. Cette dernière satisfait également plusieurs théorèmes métalogiques qui la rendent analysable en théorie de la démonstration , 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 le cadre des 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. Cependant, aucune théorie du premier ordre n'est suffisamment puissante pour décrire de manière unique une structure à domaine infini, comme l'ensemble des nombres naturels ou la droite réelle . Les systèmes d'axiomes qui décrivent pleinement 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 .
Historiquement parlant, les fondements de la logique du premier ordre ont été développés indépendamment par Gottlob Frege et Charles Sanders Peirce dans les années 1880. Cependant, la distinction entre la logique du premier ordre et la logique d'ordre supérieur n'a été bien comprise qu'avec l'arrivée d'idées et de résultats métalogiques , tels que le théorème de complétude de Gödel en 1929. Dans les années 1940, la logique du premier ordre était devenue le langage dominant des fondements mathématiques.
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 est évalué à vrai ou faux pour une ou plusieurs entités du domaine de discours .Considérons les deux phrases « Socrate est un philosophe » et « Platon est un philosophe ». En logique propositionnelle , ces phrases sont considérées comme les individus d'étude et peuvent être désignées, par exemple, par des variables telles que p et q . Elles ne sont pas considérées comme une application d'un prédicat.
La vérité d'une formule telle que « x est un philosophe » dépend de l'objet désigné par x et de l'interprétation du prédicat « est un philosophe ». Par conséquent, « x est un philosophe » seul n'a pas de valeur de vérité définie (vrai ou faux) et s'apparente à un fragment de phrase. Les relations entre prédicats peuvent être exprimées à l'aide de connecteurs logiques . Par exemple, la formule du premier ordre « si x est un philosophe, alors x est un érudit » est une proposition conditionnelle dont l'hypothèse est « x est un philosophe » et la conclusion « x est un érudit », ce qui nécessite également la spécification de x pour avoir une valeur de vérité définie.
On peut appliquer des quantificateurs aux variables d'une formule. La variable x de la formule précédente peut être quantifiée universellement, par exemple, avec la proposition du premier ordre « Pour tout x , si x est un philosophe, alors x est un érudit ». Le quantificateur universel « pour tout » dans cette proposition exprime l'idée que l'affirmation « si x est un philosophe, alors x est un érudit » est vraie pour toutes les valeurs de x .
La négation de la phrase « Pour tout x , si x est un philosophe, alors x est un érudit » est logiquement équivalente à la phrase « Il existe x tel que x soit un philosophe et x ne soit pas un érudit ». Le quantificateur existentiel « il existe » exprime l'idée que l'affirmation « x est un philosophe et x n'est pas un érudit » est vraie pour un certain choix de x .
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 un modèle) d'une formule du premier ordre précise la signification de chaque prédicat et les entités pouvant instancier les variables. Ces entités constituent le domaine du discours , ou univers, qui est généralement un ensemble non vide. Par exemple, considérons la phrase « Il existe x tel que x est philosophe ». Cette phrase est considérée comme vraie dans une interprétation où le domaine du discours comprend tous les êtres humains et où le prédicat « est philosophe » est compris comme « était l'auteur de la République ». Elle est donc vraie dans le cas de Platon.
La logique du premier ordre comporte deux éléments clés : la syntaxe, qui détermine quelles séquences finies de symboles constituent des expressions bien formées, et la sémantique, qui détermine la signification de ces expressions.
Syntaxe
Alphabet
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
Symboles logiques
Symboles non logiques
Les symboles non logiques représentent des prédicats (relations), des fonctions et des constantes. Auparavant, on utilisait couramment un ensemble fixe et infini de symboles non logiques pour tous les usages.
- Pour tout entier n ≥ 0, il existe une collection de symboles de prédicat n - aires , ou à n places . Comme ils représentent des relations entre n éléments, on les appelle aussi symboles de relation . Pour chaque arité n , il en existe une infinité.
- P n 0 , P n 1 , P n 2 , P n 3 , ...
- Pour tout entier n ≥ 0, il existe une infinité de symboles de fonction n -aires :
- f n 0 , f n 1 , f n 2 , f n 3 , ...
Lorsque l'arité d'un symbole de prédicat ou d'un symbole de fonction est claire d'après le contexte, l'exposant n est souvent omis.
Dans cette approche traditionnelle, il n'existe qu'un seul langage de logique du premier ordre. Cette approche reste courante, notamment dans les ouvrages à orientation philosophique.
Une pratique plus récente consiste à utiliser différents symboles non logiques selon l'application envisagée. Il est donc devenu nécessaire de nommer l'ensemble de tous les symboles non logiques utilisés dans une application particulière. Ce choix est effectué par le biais d'une signature .
En mathématiques, les signatures typiques sont {1, ×} ou simplement {×} pour les groupes , ou {0, 1, +, ×, <} pour les corps ordonnés . Le nombre de symboles non logiques n'est pas limité. La signature peut être vide , finie, infinie, voire non dénombrable . On trouve par exemple des signatures non dénombrables dans les démonstrations modernes du théorème de Löwenheim-Skolem .
Bien que les signatures puissent parfois indiquer comment interpréter des symboles non logiques, l'interprétation de ces symboles est distincte (et pas nécessairement figée). Les signatures concernent la syntaxe plutôt que la sémantique.
Dans cette approche, chaque symbole non logique est de l'un des types suivants :
- Un symbole de prédicat (ou symbole de relation ) dont la valence (ou l'arité , le nombre d'arguments) est supérieure ou égale à 0. Ces symboles sont souvent représentés par des lettres majuscules telles que P , Q et R. Exemples :
- Dans P ( x ), P est un symbole prédicat de valence 1. Une interprétation possible est « x est un homme ».
- Dans Q ( x , y ), Q est un symbole prédicat de valence 2. Les interprétations possibles incluent « x est supérieur à y » et « x est le père de y ».
- Les relations de valence 0 peuvent être assimilées à des variables propositionnelles , qui peuvent représenter n'importe quel énoncé. Une interprétation possible de R est : « Socrate est un homme ».
- Un symbole de fonction , dont la valence est supérieure ou égale à 0. Ces symboles sont souvent représentés par des lettres romaines minuscules telles que f , g et h . Exemples :
- f ( x ) peut s'interpréter comme « le père de x ». En arithmétique , il peut représenter « -x ». En théorie des ensembles, il peut représenter « l' ensemble des parties de x ».
- En arithmétique, g ( x , y ) peut représenter « x + y ». En théorie des ensembles, il peut représenter « 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 en début d'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, il peut représenter l' ensemble vide .
L'approche traditionnelle peut être retrouvée dans l'approche moderne, en spécifiant simplement que la signature « personnalisée » soit composée des séquences traditionnelles de symboles non logiques.
Règles de formation
Termes
L'ensemble des termes est défini inductivement par les règles suivantes :
- Variables . Tout symbole de variable est un terme.
- Fonctions . Si f est un symbole de fonction n- aire et si t₁ , ..., tₙ sont des termes, alors f ( t₁ , ..., tₙ ) est un terme. En particulier, les symboles désignant des constantes individuelles sont des symboles de fonction nuls et sont donc des termes .
Seules les expressions pouvant être obtenues par un nombre fini d'applications des règles 1 et 2 sont des termes. Par exemple, aucune expression contenant un symbole 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 :
- 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.
- Égalité . Si le symbole d'égalité est considéré comme faisant partie de la logique, et si t 1 et t 2 sont des termes, alors t 1 = t 2 est une formule.
- Négation . Si
- Connecteurs binaires . des formules, alors (
- Quantificateurs . Si
Seules les expressions qui peuvent être obtenues par un nombre fini d'applications des règles 1 à 4 sont des formules. Les formules obtenues à partir de la première règle sont appelées 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. Cependant,
Le rôle des parenthèses dans une définition est de garantir que toute 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 syntaxique unique pour chaque formule). Cette propriété est appelée lisibilité unique des formules. Il existe de nombreuses conventions quant à l'utilisation des parenthèses dans les formules. Par exemple, certains auteurs utilisent des deux-points ou des points à la place des parenthèses, ou modifient leur emplacement. Chaque définition proposée par un auteur doit être accompagnée d'une preuve de lisibilité unique.
Conventions de notation
Par commodité, des conventions ont été établies concernant la priorité des opérateurs logiques, afin d'éviter l'utilisation de parenthèses dans certains cas. Ces règles sont similaires à l' ordre des opérations arithmétiques. Une convention courante est la suivante :
- Les quantificateurs sont ensuite évalués
De plus, on peut insérer des signes de ponctuation supplémentaires non requis par la définition afin de faciliter la lecture des formules. Ainsi, la formule est la suivante :
pourrait s'écrire ainsi :
Variables libres et liées
Sémantique
Une interprétation d'un langage du premier ordre attribue une dénotation à chaque symbole non logique (symbole de prédicat, symbole de fonction ou symbole de constante) de ce langage. Elle détermine également un domaine de discours qui spécifie l'étendue des quantificateurs. Il en résulte que chaque terme se voit attribuer un objet qu'il représente, chaque prédicat une propriété des objets et chaque proposition une valeur de vérité. Ainsi, une interprétation confère une signification sémantique aux termes, prédicats et formules du langage. 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 de la logique du premier ordre. (Il est également possible de définir une sémantique des jeux pour la logique du premier ordre , mais, outre l'exigence de l' axiome du choix , la sémantique des jeux coïncide avec la sémantique tarskienne de la logique du premier ordre ; elle ne sera donc pas développée ici.)
Structures du premier ordre
Évaluation des valeurs de vérité
Validité, satisfaisabilité et conséquence logique
Algébrisations
Une autre approche 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 manières d'éliminer les variables quantifiées de la logique du premier ordre sans remplacer les quantificateurs par d'autres opérateurs de liaison de variables :
- Algèbre cylindrique , par Alfred Tarski , et al.;
- Algèbre polyadique , par Paul Halmos ;
- Logique des foncteurs de prédicats , principalement par Willard Quine .
Ces algèbres sont toutes des treillis qui étendent correctement l' algèbre booléenne à deux éléments .
Tarski and Givant (1987) showed that the fragment of first-order logic that has no atomic sentence lying in the scope of more than three quantifiers has the same expressive power as relation algebra. This fragment is of great interest because it suffices for Peano arithmetic and most axiomatic set theory, including the canonical Zermelo–Fraenkel set theory (ZFC). They also prove that first-order logic with a primitive ordered pair is equivalent to a relation algebra with two ordered pair projection functions.
First-order theories, models, and elementary classes
A first-order theory of a particular signature is a set of axioms, which are sentences consisting of symbols from that signature. The set of axioms is often finite or recursively enumerable, in which case the theory is called effective. Some authors require theories to also include all logical consequences of the axioms. The axioms are considered to hold within the theory and from them other sentences that hold within the theory can be derived.
A first-order structure that satisfies all sentences in a given theory is said to be a model of the theory. An elementary class is the set of all structures satisfying a particular theory. These classes are a main subject of study in model theory.
Many theories have an intended interpretation, a certain model that is kept in mind when studying the theory. For example, the intended interpretation of Peano arithmetic consists of the usual natural numbers with their usual operations. However, the Löwenheim–Skolem theorem shows that most first-order theories will also have other, nonstandard models.
A theory is consistent (within a deductive system) if it is not possible to prove a contradiction from the axioms of the theory. A theory is complete if, for every formula in its signature, either that formula or its negation is a logical consequence of the axioms of the theory. Gödel's incompleteness theorem shows that effective first-order theories that include a sufficient portion of the arithmetic of the natural numbers can never be both consistent and complete.
Empty domains
Il existe cependant plusieurs difficultés liées aux domaines vides :
- De nombreuses règles d'inférence courantes ne sont valides que lorsque le domaine du discours doit être non vide. Un exemple en est la règle stipulant que
- La définition de la vérité dans une interprétation utilisant une fonction d'affectation de variable est inapplicable aux domaines vides, car aucune fonction d'affectation de variable n'a pour image une image vide. (De même, on ne peut affecter d'interprétations à des symboles constants.) Cette définition de la vérité exige le choix d'une fonction d'affectation de variable (μ ci-dessus) avant de pouvoir définir des valeurs de vérité, même pour les formules atomiques. La valeur de vérité d'une proposition est alors définie comme sa valeur de vérité pour toute affectation de variable, et il est démontré que cette valeur de vérité est indépendante de l'affectation choisie. Cette technique est inopérante en l'absence de toute fonction d'affectation ; elle doit être adaptée pour prendre en compte les domaines vides.
Ainsi, lorsque le domaine vide est autorisé, il doit souvent être traité comme un cas particulier. La plupart des auteurs, cependant, l'excluent tout simplement par définition.
Systèmes déductifs
Un système déductif est correct si toute formule pouvant être dérivée dans ce système est logiquement valide. Réciproquement, un système déductif est complet si toute formule logiquement valide est dérivable. Tous les systèmes présentés dans cet article sont à la fois corrects et complets. Ils partagent également la propriété qu'il est possible de vérifier efficacement qu'une déduction supposément valide est bien une déduction ; de tels systèmes déductifs sont dits effectifs .
Une propriété essentielle des systèmes déductifs est leur nature purement syntaxique : les dérivations peuvent ainsi être vérifiées sans aucune interprétation. Par conséquent, un raisonnement valide est correct quelle que soit l’interprétation du langage, qu’elle concerne les mathématiques, l’économie ou tout autre domaine.
En général, la conséquence logique en logique du premier ordre n'est que semi-décidable : si une proposition A implique logiquement une proposition B, cela peut être démontré (par exemple, en cherchant une preuve jusqu'à en trouver une, à l'aide d'un système de preuve efficace, rigoureux et complet). Cependant, si A n'implique pas logiquement B, cela ne signifie pas que A implique logiquement la négation de B. Il n'existe aucune procédure efficace qui, étant donné les formules A et B, permette de déterminer systématiquement et correctement si A implique logiquement B.
Règles d'inférence
Par exemple, une règle d'inférence courante est la règle de substitution . Si t est un terme et φ une formule pouvant contenir la variable x , alors φ[ t / x ] est le résultat du remplacement de toutes les occurrences libres de x par t dans φ. La règle de substitution stipule que pour tout φ et tout terme t , on peut déduire φ[ t / x ] de φ à condition qu'aucune variable libre de t ne soit liée lors de la substitution. (Si une variable libre de t est liée, il faut d'abord modifier les variables liées de φ pour qu'elles diffèrent des variables libres de t avant de substituer t à x .)
Pour comprendre pourquoi la restriction sur les variables liées est nécessaire, considérons la formule logiquement valide φ donnée par
La règle de substitution illustre plusieurs aspects communs aux règles d'inférence. Elle est purement syntaxique ; on peut vérifier sa validité sans recourir à aucune interprétation. Elle présente des limitations (définies syntaxiquement) quant à son application, limitations qu'il convient de respecter pour garantir la validité des dérivations. De plus, comme c'est souvent le cas, ces limitations sont nécessaires en raison des interactions entre variables libres et liées qui se produisent lors des manipulations syntaxiques des formules intervenant dans la règle d'inférence.
Systèmes de type Hilbert et déduction naturelle
Dans un système déductif de type hilbertien, une déduction est une liste de formules, chacune étant un axiome logique , c'est-à-dire une hypothèse posée pour la déduction en cours ou découlant de formules précédentes par une règle d'inférence. Les axiomes logiques se composent de plusieurs schémas d'axiomes de formules logiquement valides ; ceux-ci couvrent une part importante de la logique propositionnelle. Les règles d'inférence permettent la manipulation des quantificateurs. Les systèmes de type hilbertien typiques possèdent un nombre restreint 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 type Hilbert en ce qu'une déduction est une liste finie de formules. Cependant, les systèmes de déduction naturelle ne possèdent pas d'axiomes logiques ; ils compensent cette absence en ajoutant des règles d'inférence supplémentaires permettant de manipuler les connecteurs logiques dans les formules de la démonstration.
calcul séquentiel
Méthode des tableaux
Résolution
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 en cette forme par skolemisation . La règle de résolution stipule que, à partir des hypothèses
Identités vérifiables
De nombreuses identités peuvent être démontrées, établissant des équivalences entre certaines formules. Ces identités permettent de réorganiser les formules en déplaçant les quantificateurs par rapport à d'autres connecteurs et sont utiles pour mettre les formules sous forme normale pré-ex . Voici quelques exemples d'identités démontrables :
L'égalité et ses axiomes
- φ(z) : f (..., x , ...) = f (..., z , ...)
Alors
- x = y → ( f (..., x , ...) = f (..., x , ...) → f (..., x , ...) = f (..., y , ...)).
Puisque x = y est donné, et que f (..., x , ...) = f (..., x , ...) est vrai par réflexivité, nous avons f (..., x , ...) = f (..., y , ...)
De nombreuses autres propriétés de l'égalité découlent des axiomes ci-dessus, par exemple :
- Symétrie . Si x = y, alors y = x .
- 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 désormais être ajoutés aux théories considérées, si nécessaire, au lieu d'être considérés comme des règles logiques. La principale différence entre cette méthode et la logique du premier ordre avec égalité est qu'une interprétation peut désormais considérer deux individus distincts comme « égaux » (bien que, selon la loi de Leibniz, ces individus satisfassent exactement aux mêmes formules quelle que soit l'interprétation). Autrement dit, la relation d'égalité peut maintenant être interprétée par une relation d'équivalence arbitraire sur le domaine du discours, congruente quant aux fonctions et aux relations de l'interprétation.
Lorsque cette seconde convention est respectée, le terme « modèle normal » désigne une interprétation où aucun individu distinct a et b ne vérifie a = b . En logique du premier ordre avec égalité, seuls les modèles normaux sont considérés ; il n’existe donc pas de terme pour désigner un autre modèle. Lorsqu’on étudie la logique du premier ordre sans égalité, il est nécessaire de modifier l’énoncé de résultats tels que le théorème de Löwenheim-Skolem afin de ne considérer que les modèles normaux.
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 le cadre d'une théorie
Si une théorie possède une formule binaire A ( x , y ) qui satisfait la réflexivité et la loi de Leibniz, on dit qu'elle possède l'égalité, ou qu'il s'agit d'une théorie avec égalité. Cette théorie peut ne pas posséder tous les exemples des schémas précédents comme axiomes, mais plutôt comme théorèmes dérivables. Par exemple, dans les théories sans symboles de fonction et avec un nombre fini de relations, il est possible de définir l'égalité en termes de relations, en définissant deux termes s et t comme égaux si une relation quelconque reste inchangée lorsqu'on remplace s par t dans un argument quelconque.
Certaines théories autorisent d'autres définitions ad hoc de l'égalité :
- Dans la théorie des ordres partiels avec un seul symbole de relation ≤, on pourrait définir s = t comme une abréviation de s ≤ t
- En théorie des ensembles avec une seule relation ∈, on peut définir s = t comme une abréviation de . Cette définition de l'égalité satisfait alors automatiquement les axiomes d'égalité. Dans ce cas, il convient de remplacer l' axiome d'extensionalité usuel , qui peut s'énoncer comme
Propriétés métalogiques
L'utilisation de la logique du premier ordre, plutôt que des logiques d'ordre supérieur , se justifie notamment par le fait que la logique du premier ordre possède de nombreuses propriétés métalogiques absentes des logiques plus fortes. Ces résultats concernent les propriétés générales de la logique du premier ordre elle-même, et non celles de théories individuelles. Ils fournissent des outils fondamentaux pour la construction de modèles de théories du premier ordre.
Complétude et indécidabilité
Le théorème de complétude de Gödel , démontré par Kurt Gödel en 1929, établit l'existence de systèmes déductifs corrects, complets et efficaces pour la logique du premier ordre, et donc la relation de conséquence logique du premier ordre est démontrée par une prouvabilité finie. De manière naïve, l'affirmation qu'une formule φ implique logiquement une formule ψ dépend de chaque modèle de φ ; or, ces modèles sont généralement de cardinalité arbitrairement grande, et la conséquence logique ne peut donc être vérifiée efficacement en examinant 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ée par φ, une telle dérivation sera finalement trouvée. Ainsi, la conséquence logique du premier ordre est semi-décidable : il est possible d'énumérer efficacement toutes les paires d'énoncés (φ, ψ) telles que ψ soit une conséquence logique de φ.
Contrairement à la logique propositionnelle , la logique du premier ordre est indécidable (bien que semi-décidable), pourvu que le langage possède au moins un prédicat d'arité supérieure ou égale à 2 (autre que l'égalité). Cela signifie qu'il n'existe aucune procédure de décision permettant de déterminer la validité logique de formules arbitraires. Ce résultat a été établi indépendamment par Alonzo Church et Alan Turing , respectivement en 1936 et 1937, apportant une réponse négative au problème de la décision (Entscheidungsproblem) posé par David Hilbert et Wilhelm Ackermann en 1928. Leurs démonstrations établissent un lien entre l'insolubilité du problème de la décision pour la logique du premier ordre et l'insolubilité du problème de l'arrêt .
fragments décidables
Il existe des systèmes plus faibles que la logique du premier ordre complète pour lesquels la relation de conséquence logique est décidable. Parmi ceux-ci figurent la logique propositionnelle et la logique des prédicats monadiques , qui est une logique du premier ordre restreinte aux symboles de prédicat unaires et dépourvue de symboles 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. Les sous-ensembles décidables de la logique du premier ordre sont également étudiés dans le cadre des logiques de description . Voir (Pratt-Hartmann, 2023) pour une monographie.
Exemples de fragments décidables :
- C2 , FOL avec deux variables et les quantificateurs de comptage
- Fragment monadique du premier ordre (MFO, ou fragment de Löwenheim) : FOL sans égalité, sans symboles de fonction et avec uniquement des symboles de prédicat unaires.
- Fragment de Löb–Gurevich : FOL sans égalité, avec uniquement des symboles de fonction unaires et avec uniquement des symboles de prédicat unaires.
- Fragment de Rabin : FOL avec égalité, avec exactement un symbole de fonction unaire et avec uniquement des symboles de prédicat unaires.
- Fragment de Bernays–Schönfinkel–Ramsey : toutes les phrases relationnelles du premier ordre sous forme normale pré-ex avec
Théorème de Löwenheim-Skolem
Le théorème de Löwenheim-Skolem démontre que si une théorie du premier ordre de cardinalité λ admet un modèle infini, alors elle admet des modèles de toute cardinalité infinie supérieure ou égale à λ. Ce résultat, parmi les plus anciens de la théorie des modèles , implique qu'il est impossible de caractériser la dénombrabilité ou l'indénombrabilité dans un langage du premier ordre à signature dénombrable. Autrement dit, il n'existe pas de formule du premier ordre φ( x ) telle qu'une structure M quelconque satisfasse φ 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 être catégoriquement axiomatisées en logique du premier ordre. Par exemple, il n'existe aucune théorie du premier ordre dont le seul modèle soit la droite réelle : toute théorie du premier ordre admettant un modèle infini possède également un modèle de cardinalité supérieure à celle du continu. Puisque la droite réelle est infinie, toute théorie satisfaite par la droite réelle l'est également par certains modèles non standard . L'application du théorème de Löwenheim-Skolem aux théories ensemblistes du premier ordre engendre des conséquences contre-intuitives connues sous le nom de paradoxe de Skolem .
théorème de compacité
Le théorème de compacité stipule qu'un ensemble de propositions du premier ordre possède un modèle si et seulement si tout sous-ensemble fini de cet ensemble possède un modèle. Ceci implique que si une formule est une conséquence logique d'un ensemble infini d'axiomes du premier ordre, alors elle est une conséquence logique d'un nombre fini de ces axiomes. Ce théorème a été démontré initialement par Kurt Gödel comme conséquence du théorème de complétude, mais de nombreuses démonstrations supplémentaires ont été obtenues depuis. Il constitue un outil fondamental en théorie des modèles, fournissant une méthode essentielle pour la construction de modèles.
Le théorème de compacité restreint la définition des classes élémentaires parmi les ensembles de structures du premier ordre. Par exemple, il implique que toute théorie admettant des modèles finis arbitrairement grands possède un modèle infini. Ainsi, la classe de tous les graphes finis n'est pas une classe élémentaire (ceci est également valable pour de nombreuses autres structures algébriques).
Il existe également des limitations plus subtiles de la logique du premier ordre, impliquées par le théorème de compacité. Par exemple, en informatique, de nombreuses situations peuvent être modélisées par un graphe orienté d'états (nœuds) et de connexions (arêtes orientées). La validation d'un tel système peut nécessiter de démontrer qu'aucun état « mauvais » n'est accessible depuis un état « bon ». On cherche donc à déterminer si les états bon et mauvais appartiennent à des composantes connexes différentes du graphe. Or, le théorème de compacité permet de montrer que les graphes connexes ne constituent pas une classe élémentaire en logique du premier ordre, et qu'il n'existe pas de formule φ( x , y ) de la logique du premier ordre, dans la logique des graphes , qui exprime l'idée qu'il existe un chemin de x à y . La connexité peut toutefois être exprimée en logique du second ordre , mais pas uniquement à l'aide de quantificateurs existentiels.
Théorème de Lindström
- Un système logique satisfaisant la définition de Lindström, contenant une logique du premier ordre et satisfaisant à 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, possédant une relation de conséquence logique semi-décidable et satisfaisant le théorème de Löwenheim-Skolem, doit être équivalent à la logique du premier ordre.
Limites
Bien que la logique du premier ordre suffise à formaliser une grande partie des mathématiques et soit couramment utilisée en informatique et dans d'autres domaines, elle présente certaines limitations. Celles-ci concernent notamment son expressivité et les fragments de langages naturels qu'elle peut décrire.
Expressivité
Le théorème de Löwenheim-Skolem démontre que si une théorie du premier ordre possède un modèle infini, alors elle possède des modèles infinis de toute cardinalité. En particulier, aucune théorie du premier ordre possédant un modèle infini ne peut être catégorique . Ainsi, il n'existe aucune théorie du premier ordre dont le seul modèle ait pour domaine l'ensemble des nombres naturels, ni dont le seul modèle ait pour domaine l'ensemble des nombres réels. De nombreuses extensions de la logique du premier ordre, notamment les logiques infinitaires et les logiques d'ordre supérieur, sont plus expressives en ce sens qu'elles permettent des axiomatisations catégoriques des nombres naturels ou des nombres réels le théorème de Lindström , le théorème de compacité et le théorème de Löwenheim-Skolem descendant ne sont valides dans aucune logique d'ordre supérieur au premier.
Formalisation des langues naturelles
Néanmoins, certaines caractéristiques complexes du langage naturel ne peuvent être exprimées par la logique du premier ordre. « Tout système logique approprié à l’analyse du langage naturel nécessite une structure beaucoup plus riche que la logique des prédicats du premier ordre. »
| Taper | Exemple | Commentaire |
|---|---|---|