Logique du second ordre - Second-order logic

En logique et en mathématiques, la logique du second ordre est une extension de la logique du premier ordre , qui est elle-même une extension de la logique propositionnelle . La logique du second ordre est à son tour étendue par la logique d'ordre supérieur et la théorie des types .

La logique du premier ordre ne quantifie que les variables qui s'échelonnent sur les individus (éléments du domaine du discours ) ; la logique du second ordre quantifie également les relations. Par exemple, la phrase du second ordre dit que pour chaque formule P , et chaque individu x , soit Px est vrai ou non ( Px ) est vrai (c'est la loi du tiers exclu ). La logique du second ordre inclut également la quantification sur des ensembles , des fonctions et d'autres variables (voir la section ci - dessous ). Tant la logique du premier ordre que la logique du second ordre utilisent l'idée d'un domaine de discours (souvent appelé simplement le « domaine » ou l'« univers »). Le domaine est un ensemble sur lequel des éléments individuels peuvent être quantifiés. ${\displaystyle \forall P\,\forall x(Px\lor \neg Px)}$

Exemples

Graffiti à Neukölln (Berlin) montrant la phrase de second ordre la plus simple admettant des modèles non triviaux, "∃φ φ".

La logique du premier ordre peut quantifier sur des individus, mais pas sur des propriétés. C'est-à-dire que nous pouvons prendre une phrase atomique comme Cube( b ) et obtenir une phrase quantifiée en remplaçant le nom par une variable et en attachant un quantificateur :

∃ x Cube ( x )

Mais on ne peut pas faire de même avec le prédicat. C'est-à-dire l'expression suivante :

PP( b )

n'est pas une phrase de logique du premier ordre. Mais c'est une phrase légitime de la logique du second ordre.

En conséquence, la logique du second ordre a beaucoup plus de « pouvoir expressif » que la logique du premier ordre. Par exemple, il n'y a aucun moyen en logique du premier ordre de dire que a et b ont une propriété en commun ; mais dans la logique du second ordre cela s'exprimerait comme

P (P( a ) P( b )).

Supposons que nous voudrions dire que a et b ont la même forme. Le mieux que nous puissions faire dans la logique du premier ordre est quelque chose comme ceci :

(Cube( a ) ∧ Cube( b )) ∨ (Tet( a ) ∧ Tet( b )) ∨ (Dodec( a ) ∧ Dodec( b ))

Si les seules formes sont le cube, le tétraèdre et le dodécaèdre, pour que a et b aient la même forme, il faut qu'ils soient soit les deux cubes, soit les deux tétraèdres, soit les deux dodécaèdres. Mais cette phrase logique du premier ordre ne semble pas signifier tout à fait la même chose que la phrase anglaise qu'elle traduit - par exemple, elle ne dit rien sur le fait que c'est la forme que a et b ont en commun.

En logique du second ordre, en revanche, nous pourrions ajouter un prédicat Shape qui s'applique précisément aux propriétés correspondant aux prédicats Cube, Tet et Dodec. C'est-à-dire,

Forme(Cube) ∧ Forme(Tet) ∧ Forme(Dodec)

On pourrait donc écrire :

∃P (Forme(P) P(a) ∧ P( b ))

Et cela est vrai exactement lorsque a et b sont tous deux des cubes, tous les deux des tétraèdres, ou tous les deux des dodécaèdres. Ainsi, dans la logique du second ordre, nous pouvons exprimer l'idée de la même forme en utilisant l'identité et le prédicat du second ordre Shape ; on peut se passer du prédicat spécial SameShape.

De même, nous pouvons exprimer l'affirmation selon laquelle aucun objet n'a toutes les formes d'une manière qui fait ressortir le quantificateur dans chaque forme :

¬∃ x ∀P(Forme(P) → P( x ))

En logique du premier ordre, on dit qu'un bloc est l'un des éléments suivants : un cube, un tétraèdre ou un dodécaèdre :

¬∃ x (Cube( x ) ∧ Tet( x ) ∧ Dodec( x ))

Syntaxe et fragments

La syntaxe de la logique du second ordre indique quelles expressions sont des formules bien formées . En plus de la syntaxe de la logique du premier ordre , la logique du second ordre comprend de nombreuses nouvelles sortes (parfois appelées types ) de variables. Ceux-ci sont:

• Une sorte de variables qui s'étendent sur des ensembles d'individus. Si S est une variable de ce genre et t est un premier ordre terme , alors l'expression t ∈ S (également écrit S ( t ), ou St pour enregistrer entre parenthèses) est une formule atomique . Les ensembles d'individus peuvent également être considérés comme des relations unaires sur le domaine.
• Pour chaque entier naturel k, il existe une sorte de variables qui s'étendent sur toutes les relations k -aires sur les individus. Si R est une telle variable relationnelle k -aire et t ₁ ,..., t _k sont des termes du premier ordre alors l'expression R ( t ₁ ,..., t _k ) est une formule atomique.
• Pour chaque entier naturel k, il existe une sorte de variables qui s'étendent sur toutes les fonctions prenant k éléments du domaine et renvoyant un seul élément du domaine. Si f est une telle variable de fonction k -aire et t ₁ ,..., t _k sont des termes du premier ordre alors l'expression f ( t ₁ ,..., t _k ) est un terme du premier ordre.

Chacune des variables qui viennent d'être définies peut être quantifiée universellement et/ou existentiellement, pour construire des formules. Ainsi, il existe de nombreux types de quantificateurs, deux pour chaque type de variables. Une phrase en logique du second ordre, comme en logique du premier ordre, est une formule bien formée sans variables libres (d'aucune sorte).

Il est possible de renoncer à l'introduction de variables de fonction dans la définition donnée ci-dessus (et certains auteurs le font) car une variable de fonction n -aire peut être représentée par une variable de relation d'arité n +1 et une formule appropriée pour l'unicité du " résultat" dans l' argument n +1 de la relation. (Shapiro 2000, p. 63)

La logique monadique du second ordre (MSO) est une restriction de la logique du second ordre dans laquelle seule la quantification sur des relations unaires (c'est-à-dire des ensembles) est autorisée. La quantification sur des fonctions, en raison de l'équivalence des relations décrites ci-dessus, n'est donc pas non plus autorisée. La logique du second ordre sans ces restrictions est parfois appelée logique du second ordre complète pour la distinguer de la version monadique. La logique monadique du second ordre est particulièrement utilisée dans le contexte du théorème de Courcelle , un méta-théorème algorithmique de la théorie des graphes .

Tout comme dans la logique du premier ordre, la logique du second ordre peut inclure des symboles non logiques dans un langage particulier du second ordre. Ceux-ci sont limités, cependant, en ce que tous les termes qu'ils forment doivent être soit des termes de premier ordre (qui peuvent être substitués à une variable de premier ordre) soit des termes de second ordre (qui peuvent être substitués à une variable de second ordre d'une variable de premier ordre). tri approprié).

Une formule en logique du second ordre est dite du premier ordre (et parfois notée ou ) si ses quantificateurs (qui peuvent être universels ou existentiels) ne s'étendent que sur des variables du premier ordre, bien qu'elle puisse avoir des variables libres du second ordre. Une formule (existentielle de second ordre) est une formule qui possède en plus des quantificateurs existentiels sur des variables de second ordre, c'est -à- dire où est une formule de premier ordre. Le fragment de logique du second ordre constitué uniquement de formules existentielles du second ordre est appelé logique existentielle du second ordre et abrégé en ESO, en , ou même en ∃SO. Le fragment de formules est défini duellement, il est appelé logique universelle du second ordre. Des fragments plus expressifs sont définis pour tout k > 0 par récursivité mutuelle : a la forme , où est une formule, et similaire, a la forme , où est une formule. (Voir hiérarchie analytique pour la construction analogue de l' arithmétique du second ordre .) ${\displaystyle \Sigma _{0}^{1}}$${\displaystyle \Pi _{0}^{1}}$${\displaystyle \Sigma _{1}^{1}}$${\displaystyle \exists R_{0}\ldots \exists R_{m}\phi }$${\style d'affichage \phi }$${\displaystyle \Sigma _{1}^{1}}$${\displaystyle \Pi _{1}^{1}}$${\displaystyle \Sigma _{k+1}^{1}}$${\displaystyle \exists R_{0}\ldots \exists R_{m}\phi }$${\style d'affichage \phi }$${\displaystyle \Pi _{k}^{1}}$${\displaystyle \Pi _{k+1}^{1}}$${\displaystyle \forall R_{0}\ldots \forall R_{m}\phi }$${\style d'affichage \phi }$${\displaystyle \Sigma _{k}^{1}}$

Sémantique

La sémantique de la logique du second ordre établit le sens de chaque phrase. Contrairement à la logique du premier ordre, qui n'a qu'une seule sémantique standard, il existe deux sémantiques différentes qui sont couramment utilisées pour la logique du second ordre : la sémantique standard et la sémantique Henkin . Dans chacune de ces sémantiques, les interprétations des quantificateurs du premier ordre et des connecteurs logiques sont les mêmes que dans la logique du premier ordre. Seules les gammes de quantificateurs sur les variables de second ordre diffèrent dans les deux types de sémantique (Väänänen 2001) .

En sémantique standard, également appelée sémantique complète, les quantificateurs s'étendent sur tous les ensembles ou fonctions de la sorte appropriée. Ainsi, une fois le domaine des variables de premier ordre établi, la signification des quantificateurs restants est fixée. Ce sont ces sémantiques qui donnent à la logique du second ordre son pouvoir expressif, et elles seront assumées pour la suite de cet article.

Dans la sémantique Henkin, chaque sorte de variable de second ordre a un domaine particulier à parcourir, qui peut être un sous-ensemble approprié de tous les ensembles ou fonctions de cette sorte. Leon Henkin (1950) a défini cette sémantique et a prouvé que le théorème de complétude et le théorème de compacité de Gödel , qui sont valables pour la logique du premier ordre, se prolongent dans la logique du second ordre avec la sémantique de Henkin. En effet, la sémantique Henkin est presque identique à la sémantique du premier ordre à plusieurs tris, où des sortes supplémentaires de variables sont ajoutées pour simuler les nouvelles variables de la logique du second ordre. La logique du second ordre avec la sémantique de Henkin n'est pas plus expressive que la logique du premier ordre. La sémantique Henkin est couramment utilisée dans l'étude de l' arithmétique du second ordre .

Jouko Väänänen ( 2001 ) a soutenu que le choix entre les modèles Henkin et les modèles complets pour la logique du second ordre est analogue au choix entre ZFC et V comme base de la théorie des ensembles : "Comme avec la logique du second ordre, nous ne pouvons pas vraiment choisir si nous axiomatiser les mathématiques en utilisant V ou ZFC. Le résultat est le même dans les deux cas, car ZFC est la meilleure tentative à ce jour d'utiliser V comme axiomatisation des mathématiques.

Puissance expressive

La logique du second ordre est plus expressive que la logique du premier ordre. Par exemple, si le domaine est l'ensemble de tous les nombres réels , on peut affirmer en logique du premier ordre l'existence d'un inverse additif de chaque nombre réel en écrivant ∀ x ∃ y ( x + y = 0) mais il faut un second- logique d'ordre pour affirmer la propriété de limite supérieure pour les ensembles de nombres réels, qui stipule que chaque ensemble de nombres réels borné et non vide a un supremum . Si le domaine est l'ensemble de tous les nombres réels, la phrase de second ordre suivante (répartie sur deux lignes) exprime la propriété de borne supérieure :

(∀ A) ([ (∃ w ) ( w ∈ A) ∧ (∃ z )(∀ u )( u ∈ A → u ≤ z ) ]

: → (∃ x ) (∀ y ) ([(∀ w ) ( w ∈ A → w ≤ x )] ∧ [(∀ u ) ( u ∈ A → u ≤ y )] → x ≤ y ) )

Cette formule est une formalisation directe de « tout non vide , délimitée ensemble A a une borne supérieure . » On peut montrer que tout corps ordonné qui satisfait cette propriété est isomorphe au corps des nombres réels. D'autre part, l'ensemble des phrases du premier ordre valides dans les réels a des modèles arbitrairement grands en raison du théorème de compacité. Ainsi, la propriété de la limite supérieure ne peut être exprimée par aucun ensemble de phrases en logique du premier ordre. (En fait, chaque champ clos réel satisfait les mêmes phrases de premier ordre dans la signature que les nombres réels.) ${\displaystyle \langle +,\cdot ,\leq \rangle }$

En logique du second ordre, il est possible d'écrire des phrases formelles qui disent « le domaine est fini » ou « le domaine est de cardinalité dénombrable ». Pour dire que le domaine est fini, utilisez la phrase qui dit que toute fonction surjective du domaine à elle-même est injective . Pour dire que le domaine a une cardinalité dénombrable, utilisez la phrase qui dit qu'il y a une bijection entre tous les deux sous-ensembles infinis du domaine. Il résulte du théorème de compacité et du théorème ascendant de Löwenheim-Skolem qu'il n'est pas possible de caractériser la finitude ou la dénombrement, respectivement, en logique du premier ordre.

Certains fragments de logique du second ordre comme l'ESO sont également plus expressifs que la logique du premier ordre même s'ils sont strictement moins expressifs que la logique complète du second ordre. L'ESO bénéficie également de l'équivalence de traduction avec certaines extensions de la logique du premier ordre qui permettent un ordre non linéaire des dépendances des quantificateurs, comme la logique du premier ordre étendue avec les quantificateurs Henkin , la logique favorable à l' indépendance de Hintikka et Sandu et la logique de dépendance de Väänänen .

Systèmes déductifs

Un système déductif pour une logique est un ensemble de règles d'inférence et d'axiomes logiques qui déterminent quelles séquences de formules constituent des preuves valides. Plusieurs systèmes déductifs peuvent être utilisés pour la logique du second ordre, bien qu'aucun ne puisse être complet pour la sémantique standard (voir ci-dessous). Chacun de ces systèmes est sain , ce qui signifie que toute phrase qu'ils peuvent être utilisés pour prouver est logiquement valide dans la sémantique appropriée.

Le système déductif le plus faible qui peut être utilisé consiste en un système déductif standard pour la logique du premier ordre (comme la déduction naturelle ) augmenté de règles de substitution pour les termes du second ordre. Ce système déductif est couramment utilisé dans l'étude de l' arithmétique du second ordre .

Les systèmes déductifs considérés par Shapiro (1991) et Henkin (1950) ajoutent au schéma déductif du premier ordre augmenté à la fois des axiomes de compréhension et des axiomes de choix. Ces axiomes sont valables pour la sémantique standard du second ordre. Ils sont valables pour la sémantique de Henkin restreinte aux modèles de Henkin satisfaisant les axiomes de compréhension et de choix.

Non-réductibilité à la logique du premier ordre

On pourrait tenter de réduire la théorie du second ordre des nombres réels, avec une sémantique complète du second ordre, à la théorie du premier ordre de la manière suivante. Développez d'abord le domaine de l'ensemble de tous les nombres réels à un domaine à deux tris, le second tri contenant tous les ensembles de nombres réels. Ajoutez un nouveau prédicat binaire au langage : la relation d'appartenance. Ensuite, les phrases qui étaient du second ordre deviennent du premier ordre, avec les quantificateurs anciennement du second ordre s'étendant sur le second tri à la place. Cette réduction peut être tentée dans une théorie à un tri en ajoutant des prédicats unaires qui indiquent si un élément est un nombre ou un ensemble, et en prenant le domaine comme étant l'union de l'ensemble des nombres réels et de l' ensemble de puissance des nombres réels.

Mais notez que le domaine a été affirmé pour inclure tous les ensembles de nombres réels. Cette exigence ne peut pas être réduite à une phrase de premier ordre, comme le montre le théorème de Löwenheim-Skolem . Ce théorème implique qu'il existe un sous- ensemble dénombrable infini des nombres réels, dont nous appellerons les membres nombres internes , et une collection dénombrable infinie d'ensembles de nombres internes, dont nous appellerons les membres "ensembles internes", tels que le domaine constitué de les nombres internes et les ensembles internes satisfont exactement les mêmes phrases du premier ordre que celles satisfaites par le domaine des nombres réels et des ensembles de nombres réels. En particulier, il satisfait une sorte d'axiome de moindre borne supérieure qui dit, en effet :

La dénombrement de l'ensemble de tous les nombres internes (en conjonction avec le fait que ceux-ci forment un ensemble densément ordonné) implique que cet ensemble ne satisfait pas l'axiome complet de la limite supérieure. La dénombrement de l'ensemble de tous les ensembles internes implique qu'il ne s'agit pas de l'ensemble de tous les sous-ensembles de l'ensemble de tous les nombres internes (puisque le théorème de Cantor implique que l'ensemble de tous les sous-ensembles d'un ensemble dénombrable est un ensemble infiniment indénombrable). Cette construction est étroitement liée au paradoxe de Skolem .

Ainsi, la théorie du premier ordre des nombres réels et des ensembles de nombres réels a de nombreux modèles, dont certains sont dénombrables. La théorie du second ordre des nombres réels n'a cependant qu'un seul modèle. Cela découle du théorème classique qu'il n'y a qu'un seul champ ordonné complet d' Archimède , ainsi que du fait que tous les axiomes d'un champ ordonné complet d'Archimède sont exprimables en logique du second ordre. Cela montre que la théorie du second ordre des nombres réels ne peut pas être réduite à une théorie du premier ordre, en ce sens que la théorie du second ordre des nombres réels n'a qu'un seul modèle mais que la théorie du premier ordre correspondante a de nombreux modèles.

Il existe des exemples plus extrêmes montrant que la logique du second ordre avec une sémantique standard est plus expressive que la logique du premier ordre. Il existe une théorie finie du second ordre dont le seul modèle est celui des nombres réels si l' hypothèse du continu est vérifiée et qui n'a pas de modèle si l'hypothèse du continu n'est pas vérifiée (cf. Shapiro 2000, p. 105). Cette théorie consiste en une théorie finie caractérisant les nombres réels comme un champ ordonné d'Archimède complet plus un axiome disant que le domaine est de la première cardinalité indénombrable. Cet exemple illustre que la question de savoir si une phrase dans la logique du second ordre est cohérente est extrêmement subtile.

Les limitations supplémentaires de la logique du second ordre sont décrites dans la section suivante.

Résultats métalogiques

C'est un corollaire du théorème d'incomplétude de Gödel qu'il n'y a pas de système déductif (c'est-à-dire pas de notion de prouvabilité ) pour les formules du second ordre qui satisfasse simultanément ces trois attributs souhaités :

• ( Solidité ) Chaque phrase prouvable du second ordre est universellement valide, c'est-à-dire vraie dans tous les domaines selon la sémantique standard.
• ( Complétude ) Toute formule du second ordre universellement valide, selon la sémantique standard, est prouvable.
• ( Efficacité ) Il existe un algorithme de vérification de preuve qui peut décider correctement si une séquence donnée de symboles est une preuve ou non.

Ce corollaire est parfois exprimé en disant que la logique du second ordre n'admet pas de théorie de la preuve complète . À cet égard, la logique du second ordre avec une sémantique standard diffère de la logique du premier ordre ; Quine (1970, pp. 90-91 ) a souligné l'absence d'un système de preuve complet comme une raison de penser à la logique du second ordre comme n'étant pas logique , à proprement parler.

Comme mentionné ci-dessus, Henkin a prouvé que le système déductif standard pour la logique du premier ordre est solide, complet et efficace pour la logique du second ordre avec la sémantique Henkin , et que le système déductif avec les principes de compréhension et de choix est solide, complet et efficace pour Henkin sémantique utilisant uniquement des modèles qui satisfont à ces principes.

Le théorème de compacité et le théorème de Löwenheim-Skolem ne sont pas valables pour les modèles complets de la logique du second ordre. Ils sont toutefois valables pour les modèles Henkin.

Histoire et valeur contestée

La logique des prédicats a été introduite dans la communauté mathématique par CS Peirce , qui a inventé le terme logique du second ordre et dont la notation est la plus similaire à la forme moderne (Putnam 1982). Cependant, aujourd'hui, la plupart des étudiants en logique connaissent mieux les travaux de Frege , qui a publié ses travaux plusieurs années avant Peirce mais dont les travaux sont restés moins connus jusqu'à ce que Bertrand Russell et Alfred North Whitehead les rendent célèbres. Frege a utilisé différentes variables pour distinguer la quantification sur les objets de la quantification sur les propriétés et les ensembles ; mais il ne se considérait pas comme faisant deux sortes de logiques différentes. Après la découverte du paradoxe de Russell, on s'est rendu compte que quelque chose n'allait pas avec son système. Finalement, les logiciens ont découvert que restreindre la logique de Frege de diverses manières - à ce qu'on appelle maintenant la logique du premier ordre - éliminait ce problème : les ensembles et les propriétés ne peuvent pas être quantifiés dans la seule logique du premier ordre. La hiérarchie désormais standardisée des ordres de logiques date de cette époque.

Il a été constaté que la théorie des ensembles pouvait être formulée comme un système axiomatisé au sein de l'appareil de la logique du premier ordre (au prix de plusieurs types de complétude , mais rien d'aussi mauvais que le paradoxe de Russell), et cela a été fait (voir l' ensemble de Zermelo-Fraenkel théorie ), car les ensembles sont vitaux pour les mathématiques . L'arithmétique , la méréologie et une variété d'autres théories logiques puissantes pourraient être formulées axiomatiquement sans faire appel à un appareil plus logique que la quantification du premier ordre, et ceci, avec l' adhésion de Gödel et Skolem à la logique du premier ordre, a conduit à une baisse du travail dans la logique du deuxième ordre (ou de tout ordre supérieur).

Ce rejet a été activement avancé par certains logiciens, notamment WV Quine . Quine a avancé l'idée que dans les phrases en langage à prédicat comme Fx, le « x » doit être considéré comme une variable ou un nom désignant un objet et peut donc être quantifié, comme dans « Pour toutes choses, c'est le cas que . . . ." mais le " F " doit être considéré comme l' abréviation d'une phrase incomplète, pas le nom d'un objet (pas même d'un objet abstrait comme une propriété). Par exemple, cela pourrait signifier « . . . est un chien ». Mais cela n'a aucun sens de penser que nous pouvons quantifier quelque chose comme ça. (Une telle position est tout à fait cohérente avec les propres arguments de Frege sur la distinction concept-objet ). Donc, utiliser un prédicat comme variable, c'est lui faire occuper la place d'un nom, que seules des variables individuelles devraient occuper. Ce raisonnement a été rejeté par George Boolos .

Ces dernières années, la logique du second ordre a fait une sorte de reprise, soutenue par l'interprétation de Boolos de la quantification du second ordre comme une quantification plurielle sur le même domaine d'objets que la quantification du premier ordre (Boolos 1984). Boolos souligne en outre la prétendue non- classification de phrases telles que "Certains critiques ne s'admirent que les uns les autres" et "Certains des hommes de Fiancheto sont entrés dans l'entrepôt sans être accompagnés par quelqu'un d'autre", ce qui, selon lui, ne peut être exprimé que par toute la force du second ordre. quantification. Cependant, la quantification généralisée et la quantification partiellement ordonnée (ou ramifiée) peuvent suffire à exprimer une certaine classe de phrases prétendument non ordonnables en premier et celles-ci ne font pas appel à la quantification de second ordre.

Relation avec la complexité de calcul

Le pouvoir expressif de diverses formes de logique du second ordre sur des structures finies est intimement lié à la théorie de la complexité computationnelle . Le domaine de la complexité descriptive étudie quelles classes de complexité informatique peuvent être caractérisées par la puissance de la logique nécessaire pour exprimer des langages (ensembles de chaînes finies) en eux. Une chaîne w  =  w ₁ ··· w _n dans un alphabet fini A peut être représentée par une structure finie de domaine D  = {1,..., n }, des prédicats unaires P _a pour chaque a  ∈  A , satisfaits par ceux des indices i tels que w _i  =  a , et des prédicats supplémentaires qui servent à identifier de manière unique quel indice est lequel (typiquement, on prend le graphe de la fonction successeur sur D ou la relation d'ordre <, éventuellement avec d'autres prédicats arithmétiques). Inversement, les tables de Cayley de toute structure finie (sur une signature finie ) peuvent être codées par une chaîne finie.

Cette identification conduit aux caractérisations suivantes des variantes de la logique du second ordre sur les structures finies :

• REG (l'ensemble des langages réguliers ) est définissable par des formules monadiques du second ordre (théorème de Büchi, 1960)
• NP est l'ensemble des langages définissables par des formules existentielles du second ordre ( théorème de Fagin , 1974).
• co-NP est l'ensemble des langages définissables par des formules universelles du second ordre.
• PH est l'ensemble des langages définissables par des formules du second ordre.
• PSPACE est l'ensemble des langages définissables par des formules du second ordre avec un opérateur de fermeture transitif ajouté .
• EXPTIME est l'ensemble des langages définissables par des formules du second ordre avec un opérateur de point le moins fixe ajouté .

Les relations entre ces classes ont un impact direct sur l'expressivité relative des logiques sur les structures finies ; par exemple, si PH  =  PSPACE , l'ajout d'un opérateur de fermeture transitif à la logique du second ordre ne le rendrait pas plus expressif sur des structures finies.

Voir également

• Logique du premier ordre
• Logique d'ordre supérieur
• Numéro de Löwenheim
• Langue oméga
• Logique propositionnelle de second ordre
• Logique monadique du second ordre

Remarques

Les références

• Andrews, Peter (2002). Une introduction à la logique mathématique et à la théorie des types : À la vérité par la preuve (2e éd.). Éditeurs académiques Kluwer.
• Boolos, Georges (1984). "Être, c'est être une valeur d'une variable (ou être des valeurs de certaines variables)". Revue de Philosophie . 81 (8) : 430-50. doi : 10.2307/2026308 . JSTOR  2026308 .. Réimprimé dans Boolos, Logic, Logic and Logic , 1998.
• Henkin, L. (1950). « La complétude dans la théorie des types ». Journal de logique symbolique . 15 (2) : 81-91. doi : 10.2307/2266967 . JSTOR  2266967 .
• Hinman, P. (2005). Fondements de la logique mathématique . AK Peters. ISBN 1-56881-262-0.
• Putnam, Hilary (1982). "Peirce le Logicien" . Historia Mathématique . 9 (3) : 290-301. doi : 10.1016/0315-0860(82)90123-9 .. Réimprimé dans Putnam, Hilary (1990), Realism with a Human Face , Harvard University Press , pp. 252-260 .
• WV Quine (1970). Philosophie de la logique . Salle des apprentis .
• Rossberg, M. (2004). « Logique de premier ordre, logique de deuxième ordre et complétude » (PDF) . Dans V. Hendricks ; et al. (éd.). La logique du premier ordre revisitée . Berlin : Logos-Verlag.
• Shapiro, S. (2000) [1991].Fondations sans fondationnalisme : un cas pour la logique de second ordre. Oxford : Clarendon Press. ISBN 0-19-825029-0.
• Väänänen, J. (2001). « Logique de second ordre et fondements des mathématiques » (PDF) . Bulletin de Logique Symbolique . 7 (4) : 504-520. CiteSeerX  10.1.1.25.5579 . doi : 10.2307/2687796 . JSTOR  2687796 .

Lectures complémentaires

• Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid ; Martin, Marx ; Spencer, Joël ; Vardi, Moshé Y. ; Venema, Yde ; Weinstein, Scott (2007). Théorie des modèles finis et ses applications . Textes en informatique théorique. Une série EATCS. Berlin : Springer-Verlag . ISBN 978-3-540-00428-8. Zbl  1133.03001 .

• Väänänen, Jouko. Edward N. Zalta (éd.). Logique de second ordre et d'ordre supérieur . L'Encyclopédie de philosophie de Stanford (édition d'automne 2021).