Arithmétique du second ordre - Second-order arithmetic

En logique mathématique , l' arithmétique du second ordre est un ensemble de systèmes axiomatiques qui formalisent les nombres naturels et leurs sous-ensembles. C'est une alternative à la théorie des ensembles axiomatique comme fondement de la plupart des mathématiques, mais pas toutes.

Un précurseur de l'arithmétique du second ordre qui implique des paramètres du troisième ordre a été introduit par David Hilbert et Paul Bernays dans leur livre Grundlagen der Mathematik . L'axiomatisation standard de l'arithmétique du second ordre est notée Z 2 .

L'arithmétique du second ordre inclut, mais est significativement plus forte que, son homologue du premier ordre l'arithmétique de Peano . Contrairement à l'arithmétique de Peano, l'arithmétique du second ordre permet la quantification sur des ensembles de nombres naturels ainsi que sur les nombres eux-mêmes. Parce que les nombres réels peuvent être représentés comme des ensembles ( infinis ) de nombres naturels de manières bien connues, et parce que l'arithmétique du second ordre permet la quantification sur de tels ensembles, il est possible de formaliser les nombres réels en arithmétique du second ordre. Pour cette raison, l'arithmétique du second ordre est parfois appelée « analyse » (Sieg 2013, p. 291).

L'arithmétique du second ordre peut également être considérée comme une version faible de la théorie des ensembles dans laquelle chaque élément est soit un nombre naturel, soit un ensemble de nombres naturels. Bien qu'elle soit beaucoup plus faible que la théorie des ensembles de Zermelo-Fraenkel , l'arithmétique du second ordre peut prouver essentiellement tous les résultats des mathématiques classiques exprimables dans son langage.

Un sous-système de l'arithmétique du second ordre est une théorie dans le langage de l'arithmétique du second ordre dont chaque axiome est un théorème de l'arithmétique complète du second ordre (Z 2 ). De tels sous-systèmes sont essentiels pour inverser les mathématiques , un programme de recherche étudiant la quantité de mathématiques classiques pouvant être dérivée de certains sous-systèmes faibles de force variable. Une grande partie des mathématiques fondamentales peut être formalisée dans ces sous-systèmes faibles, dont certains sont définis ci-dessous. Les mathématiques inversées clarifient également l'étendue et la manière dont les mathématiques classiques sont non constructives .

Définition

Syntaxe

Le langage de l'arithmétique du second ordre est à deux tris . Le premier type de termes et en particulier les variables , généralement désignés par des lettres minuscules, se compose d' individus , dont l'interprétation prévue est comme des nombres naturels. Les autres types de variables, appelées diversement « variables d'ensemble », « variables de classe » ou même « prédicats » sont généralement désignées par des lettres majuscules. Ils font référence à des classes/prédicats/propriétés d'individus et peuvent donc être considérés comme des ensembles de nombres naturels. Les individus et les variables d'ensemble peuvent être quantifiés de manière universelle ou existentielle. Une formule sans variables définies liées (c'est-à-dire sans quantificateurs sur les variables définies) est appelée arithmétique . Une formule arithmétique peut avoir des variables libres et des variables individuelles liées.

Les termes individuels sont formés à partir de la constante 0, de la fonction unaire S (la fonction successeur ) et des opérations binaires + et (addition et multiplication). La fonction successeur ajoute 1 à son entrée. Les relations = (égalité) et < (comparaison des nombres naturels) mettent en relation deux individus, tandis que la relation (appartenance) met en relation un individu et un ensemble (ou classe). Ainsi en notation le langage de l'arithmétique du second ordre est donné par la signature .

Par exemple, , est une formule bien formée d'arithmétique du second ordre qui est arithmétique, a une variable d'ensemble libre X et une variable individuelle liée n (mais pas de variables d'ensemble liées, comme cela est requis d'une formule arithmétique) - alors qu'est un formule bien formée qui n'est pas arithmétique, ayant une variable d'ensemble liée X et une variable individuelle liée n .

Sémantique

Plusieurs interprétations différentes des quantificateurs sont possibles. Si l'arithmétique du second ordre est étudiée en utilisant la sémantique complète de la logique du second ordre, alors les quantificateurs d'ensembles s'étendent sur tous les sous-ensembles de la plage des variables numériques. Si l'arithmétique du second ordre est formalisée à l'aide de la sémantique de la logique du premier ordre (sémantique de Henkin), alors tout modèle comprend un domaine sur lequel les variables de l'ensemble doivent s'étendre, et ce domaine peut être un sous-ensemble approprié de l'ensemble des puissances complètes du domaine du nombre. variables (Shapiro 1991, p. 74-75).

Axiomes

De base

Les axiomes suivants sont connus comme les axiomes de base , ou parfois les axiomes de Robinson. La théorie du premier ordre résultante , connue sous le nom d' arithmétique de Robinson , est essentiellement l'arithmétique de Peano sans induction. Le domaine de discours pour les variables quantifiées est celui des nombres naturels , désignés collectivement par N , et incluant le membre distingué , appelé « zéro ».

Les fonctions primitives sont la fonction successeur unaire , désignée par préfixe , et deux opérations binaires , addition et multiplication , désignées par infixe "+" et " ", respectivement. Il existe également une relation binaire primitive appelée ordre , notée par l'infixe "<".

Axiomes régissant la fonction successeur et zéro :

1. (« le successeur d'un nombre naturel n'est jamais zéro »)
2. (« la fonction successeur est injective »)
3. (« chaque nombre naturel est zéro ou un successeur »)

Addition définie récursivement :

4.
5.

Multiplication définie récursivement :

6.
7.

Axiomes régissant la relation d'ordre "<":

8. (« aucun nombre naturel n'est inférieur à zéro »)
9.
10. (« chaque nombre naturel est égal à zéro ou supérieur à zéro »)
11.

Ces axiomes sont tous des énoncés du premier ordre . C'est-à-dire que toutes les variables s'étendent sur les nombres naturels et non sur des ensembles de ceux-ci, un fait encore plus fort que leur étant arithmétique. De plus, il n'y a qu'un quantificateur existentiel , dans l'axiome 3. Les axiomes 1 et 2, ainsi qu'un schéma d'axiome d'induction constituent la définition habituelle de Peano-Dedekind de N . Ajouter à ces axiomes toute sorte de schéma d'induction d' axiomes rend redondants les axiomes 3, 10 et 11.

Schéma d'induction et de compréhension

Si φ( n ) est une formule d'arithmétique du second ordre avec une variable de nombre libre n et éventuellement d'autres variables de nombre libre ou d'ensemble (notées m et X ), l' axiome d'induction pour φ est l'axiome :

Le schéma d'induction ( complet ) du second ordre comprend toutes les instances de cet axiome, sur toutes les formules du second ordre.

Un exemple particulièrement important du schéma d'induction est lorsque φ est la formule " " exprimant le fait que n est un membre de X ( X étant une variable d'ensemble libre): dans ce cas, l'axiome d'induction pour φ est

Cette phrase est appelée l' axiome d'induction du second ordre .

Si φ( n ) est une formule avec une variable libre n et éventuellement d'autres variables libres, mais pas la variable Z , l' axiome de compréhension pour φ est la formule

Cet axiome permet de former l'ensemble des entiers naturels vérifiant ( n ). Il existe une restriction technique selon laquelle la formule ne peut pas contenir la variable Z , car sinon la formule conduirait à l'axiome de compréhension

,

ce qui est incohérent. Cette convention est assumée dans la suite de cet article.

Le système complet

La théorie formelle de l' arithmétique du second ordre (dans le langage de l'arithmétique du second ordre) comprend les axiomes de base, l'axiome de compréhension pour chaque formule (arithmétique ou autre) et l'axiome d'induction du second ordre. Cette théorie est parfois appelée arithmétique complète du second ordre pour la distinguer de ses sous-systèmes, définis ci-dessous. Parce que la sémantique complète du second ordre implique que chaque ensemble possible existe, les axiomes de compréhension peuvent être considérés comme faisant partie du système déductif lorsque ces sémantiques sont utilisées (Shapiro 1991, p. 66).

Des modèles

Cette section décrit l'arithmétique du second ordre avec la sémantique du premier ordre. Ainsi un modèle du langage de l'arithmétique du second ordre se compose d'un ensemble M (qui forme l'étendue des variables individuelles) avec une constante 0 (un élément de M ), une fonction S de M à M , deux opérations binaires + et · sur M , une relation binaire < sur M , et une collection D de sous-ensembles de M , qui est la plage des variables d'ensemble. L'omission de D produit un modèle du langage de l'arithmétique du premier ordre.

Lorsque D est le jeu de puissance complet de M , le modèle est appelé modèle complet . L'utilisation de la sémantique complète du second ordre revient à limiter les modèles de l'arithmétique du second ordre aux modèles complets. En fait, les axiomes de l'arithmétique du second ordre n'ont qu'un seul modèle complet. Cela découle du fait que les axiomes de l'arithmétique de Peano avec l'axiome d'induction du second ordre n'ont qu'un seul modèle sous sémantique du second ordre.

Lorsque M est l'ensemble habituel des nombres naturels avec ses opérations habituelles, est appelé un ω-modèle . Dans ce cas, le modèle peut être identifié à D , sa collection d'ensembles de naturels, car cet ensemble est suffisant pour déterminer complètement un -modèle.

Le modèle complet unique , qui est l'ensemble habituel des nombres naturels avec sa structure habituelle et tous ses sous-ensembles, est appelé le modèle prévu ou standard de l'arithmétique du second ordre.

Fonctions définissables

Les fonctions du premier ordre qui sont prouvées totales en arithmétique du second ordre sont précisément les mêmes que celles représentables dans le système F (Girard et Taylor 1987, pp. 122-123). De manière presque équivalente, le système F est la théorie des fonctionnelles correspondant à l'arithmétique du second ordre d'une manière parallèle à la façon dont le système T de Gödel correspond à l'arithmétique du premier ordre dans l' interprétation de Dialectica .

Sous-systèmes

Il existe de nombreux sous-systèmes nommés d'arithmétique du second ordre.

Un indice 0 dans le nom d'un sous-système indique qu'il n'inclut qu'une partie restreinte du schéma d'induction complet du second ordre (Friedman 1976). Une telle restriction réduit considérablement la force de preuve-théorique du système. Par exemple, le système ACA 0 décrit ci-dessous est équicohérent avec l'arithmétique de Peano . La théorie correspondante ACA, composée de ACA 0 plus le schéma d'induction complet du second ordre, est plus forte que l'arithmétique de Peano.

Compréhension arithmétique

De nombreux sous-systèmes bien étudiés sont liés aux propriétés de fermeture des modèles. Par exemple, on peut montrer que chaque -modèle de l'arithmétique complète du second ordre est fermé sous le saut de Turing , mais que tout ω-modèle fermé sous le saut de Turing n'est pas un modèle de l'arithmétique complète du second ordre. Le sous-système ACA 0 comprend juste assez d'axiomes pour saisir la notion de fermeture sous saut de Turing.

ACA 0 est défini comme la théorie constituée des axiomes de base, le schéma d' axiome de compréhension arithmétique (en d'autres termes l'axiome de compréhension pour chaque formule arithmétique ) et l'axiome d'induction ordinaire du second ordre. Cela équivaudrait à inclure tout le schéma d'axiome d'induction arithmétique, en d'autres termes d'inclure l'axiome d'induction pour chaque formule arithmétique .

On peut montrer qu'une collection S de sous-ensembles de ω détermine un ω-modèle d'ACA 0 si et seulement si S est fermé par saut de Turing, réductibilité de Turing et jointure de Turing (Simpson 2009, pp. 311-313).

L'indice 0 dans ACA 0 indique que toutes les instances du schéma d'axiome d'induction ne sont pas incluses dans ce sous-système. Cela ne fait aucune différence pour les modèles , qui satisfont automatiquement chaque instance de l'axiome d'induction. Il est cependant important dans l'étude des modèles non-ω. Le système composé d'ACA 0 plus induction pour toutes les formules est parfois appelé ACA sans indice.

Le système ACA 0 est une extension conservatrice de l' arithmétique du premier ordre (ou des axiomes de Peano du premier ordre), définis comme les axiomes de base, plus le schéma d'axiome d'induction du premier ordre (pour toutes les formules n'impliquant aucune variable de classe, liée ou sinon), dans le langage de l'arithmétique du premier ordre (qui n'autorise pas du tout les variables de classe). En particulier, il a le même ordinal de la théorie de la preuve ε 0 que l'arithmétique du premier ordre, en raison du schéma d'induction limité.

La hiérarchie arithmétique des formules

Une formule est appelée arithmétique bornée , ou 0 0 , lorsque tous ses quantificateurs sont de la forme ∀ n < t ou ∃ n < t (où n est la variable individuelle à quantifier et t est un terme individuel), où

signifie

et

signifie

.

Une formule est appelée Σ 0 1 (ou parfois Σ 1 ), respectivement Π 0 1 (ou parfois Π 1 ) lorsqu'elle est de la forme ∃ m (φ), respectivement ∀ m (φ) où φ est une formule arithmétique bornée et m est une variable individuelle (c'est-à-dire libre dans ). Plus généralement, une formule est appelée Σ 0 n , respectivement Π 0 n lorsqu'elle est obtenue en ajoutant des quantificateurs individuels existentiels, respectivement universels, à une formule Π 0 n −1 , respectivement Σ 0 n −1 (et Σ 0 0 et Π 0 0 sont tous équivalents à Δ 0 0 ). Par construction, toutes ces formules sont arithmétiques (aucune variable de classe n'est jamais liée) et, en fait, en mettant la formule sous la forme Skolem prenex on peut voir que chaque formule arithmétique est équivalente à une formule Σ 0 n ou Π 0 n pour tout assez grand n .

Compréhension récursive

Le sous-système RCA 0 est un système plus faible que l'ACA 0 et est souvent utilisé comme système de base en mathématiques inversées . Il comprend : les axiomes de base, le schéma d'induction 0 1 et le schéma de compréhension Δ 0 1 . Le premier terme est clair : le schéma d'induction Σ 0 1 est l'axiome d'induction pour toute formule Σ 0 1 φ. Le terme « compréhension Δ 0 1 » est plus complexe, car il n'existe pas de formule Δ 0 1 . Le schéma de compréhension Δ 0 1 affirme à la place l'axiome de compréhension pour chaque formule Σ 0 1 qui est équivalente à une formule Π 0 1 . Ce schéma comprend, pour toute formule Σ 0 1 φ et toute formule Π 0 1 ψ, l'axiome :

L'ensemble des conséquences du premier ordre de RCA 0 est le même que celui du sous-système IΣ 1 de l'arithmétique de Peano dans lequel l'induction est restreinte aux formules Σ 0 1 . À son tour, IΣ 1 est conservateur par rapport à l'arithmétique récursive primitive (PRA) pour les phrases. De plus, l'ordinal de la théorie de la preuve de est ω ω , le même que celui de PRA.

On peut voir qu'une collection S de sous-ensembles de ω détermine un ω-modèle de RCA 0 si et seulement si S est fermé par réductibilité de Turing et jointure de Turing. En particulier, la collection de tous les sous-ensembles calculables de ω donne un ω-modèle de RCA 0 . C'est la motivation derrière le nom de ce système - si un ensemble peut être prouvé à l'aide de RCA 0 , alors l'ensemble est récursif (c'est-à-dire calculable).

Systèmes plus faibles

Parfois, un système encore plus faible que RCA 0 est souhaité. Un tel système est défini comme suit : il faut d'abord augmenter le langage de l'arithmétique avec une fonction exponentielle (dans les systèmes plus forts, l'exponentielle peut être définie en termes d'addition et de multiplication par l'astuce habituelle, mais lorsque le système devient trop faible ce n'est pas plus possible) et les axiomes de base par les axiomes évidents définissant l'exponentiation inductivement à partir de la multiplication ; alors le système se compose des axiomes de base (enrichis), plus Δ 0 1 compréhension, plus Δ 0 0 induction.

Des systèmes plus forts

Sur ACA 0 , chaque formule d'arithmétique du second ordre est équivalente à une formule Σ 1 n ou Π 1 n pour tout n assez grand . Le système Π 1 1 -compréhension est le système constitué des axiomes de base, plus l'axiome d'induction ordinaire du second ordre et l'axiome de compréhension pour chaque formule Π 1 1 φ. Ceci équivaut à 1 1 -compréhension (en revanche, Δ 1 1 -compréhension, définie de manière analogue à Δ 0 1 -compréhension, est plus faible).

Détermination projective

La détermination projective est l'affirmation selon laquelle chaque jeu d'information parfait à deux joueurs avec des mouvements étant des nombres entiers, une longueur de jeu et un ensemble de gains projectifs est déterminé, c'est-à-dire que l'un des joueurs a une stratégie gagnante. (Le premier joueur gagne le jeu si le jeu appartient à l'ensemble des gains ; sinon, le deuxième joueur gagne.) Un ensemble est projectif ssi (comme prédicat) il est exprimable par une formule dans le langage de l'arithmétique du second les nombres réels comme paramètres, donc la détermination projective est exprimable comme un schéma dans le langage de Z 2 .

De nombreuses propositions naturelles exprimables dans le langage de l'arithmétique du second ordre sont indépendantes de Z 2 et même de ZFC mais sont prouvables à partir de la détermination projective. Les exemples incluent coanalytique propriété sous - ensemble parfait , mesurabilité et la propriété de Baire pour les ensembles, l' uniformisation , etc. Plus d' une faible théorie de base (tels que RCA 0 ), déterminabilité projective implique la compréhension et fournit une théorie essentiellement complète de l' arithmétique du second ordre - des déclarations naturelles dans le langage de Z 2 qui sont indépendants de Z 2 avec une détermination projective sont difficiles à trouver (Woodin 2001).

ZFC + {il y a n cardinaux de Woodin : n est un nombre naturel} est conservateur sur Z 2 avec détermination projective, c'est-à-dire qu'un énoncé dans le langage de l'arithmétique du second ordre est prouvable dans Z 2 avec détermination projective ssi sa traduction dans le langage de la théorie des ensembles est prouvable dans ZFC + {il y a n cardinaux de Woodin : n ∈N}.

Codage des mathématiques

L'arithmétique du second ordre formalise directement les nombres naturels et les ensembles de nombres naturels. Cependant, il est capable de formaliser indirectement d'autres objets mathématiques via des techniques de codage, un fait qui a été remarqué pour la première fois par Weyl (Simpson 2009, p. 16). Les entiers, les nombres rationnels et les nombres réels peuvent tous être formalisés dans le sous-système RCA 0 , avec des espaces métriques séparables complets et des fonctions continues entre eux (Simpson 2009, chapitre II).

Le programme de recherche de Reverse Mathematics utilise ces formalisations des mathématiques en arithmétique du second ordre pour étudier les axiomes d'existence d'ensembles nécessaires pour prouver des théorèmes mathématiques (Simpson 2009, p. 32). Par exemple, le théorème des valeurs intermédiaires pour les fonctions des réels aux réels est démontrable dans RCA 0 (Simpson 2009, p. 87), tandis que le théorème de Bolzano Weierstrass est équivalent à ACA 0 sur RCA 0 (Simpson 2009, p. 34 ).

Le codage susmentionné fonctionne bien pour les fonctions continues et totales, comme indiqué dans (Kohlenbach 2002, section 4), en supposant une théorie de base d'ordre supérieur plus le lemme de Koenig faible . Comme on peut s'y attendre, dans le cas de la topologie ou de la théorie de la mesure, le codage n'est pas sans problèmes, comme exploré par exemple dans (Hunter, 2008) ou (Normann-Sanders, 2019). Cependant, même le codage des fonctions intégrables de Riemann pose des problèmes : comme le montre (Normann-Sanders, 2020), les axiomes (de compréhension) minimaux nécessaires pour prouver le théorème de convergence d'Arzelà pour l'intégrale de Riemann sont *très* différents selon que l'on utilise ou non la seconde- codes de commande ou fonctions de troisième ordre.

Voir également

Les références

  • Burgess, JP (2005), Fixing Frege , Princeton University Press.
  • Buss, SR (1998), Manuel de théorie de la preuve , Elsevier. ISBN  0-444-89840-9
  • Friedman, H. (1976), "Systèmes d'arithmétique du second ordre avec induction restreinte," I, II (Résumés). Journal of Symbolic Logic , v. 41, pp. 557-559. JStor
  • Girard, L. et Taylor (1987), Preuves et types , Cambridge University Press.
  • Hilbert, D. et Bernays, P. (1934), Grundlagen der Mathematik , Springer-Verlag. MR 0237246
  • Hunter, James, Topologie inverse d'ordre supérieur , thèse, Université de Madison-Wisconsin [1] .
  • Kohlenbach, U. , Utilisations fondamentales et mathématiques des types supérieurs , Réflexions sur les fondements des mathématiques, Lect. Journal des notes, vol. 15, ASL, 2002, p. 92–116.
  • Dag Normann et Sam Sanders, Représentations en théorie de la mesure , arXiv : 1902.02756 , (2019).
  • Dag Normann et Sam Sanders, On the uncountability of $\mathbb{R}$ , arxiv : [2] , (2020), pp. 37.
  • Sieg, W. (2013), Hilbert's Programs and Beyond , Oxford University Press.
  • Shapiro, S. (1991), Fondations sans fondationnalisme , Oxford University Press. ISBN  0-19-825029-0
  • Simpson, SG (2009), Sous - systèmes d'arithmétique du second ordre , 2e édition, Perspectives in Logic, Cambridge University Press. ISBN  978-0-521-88439-6 MR 2517689
  • Takeuti, G. (1975) Théorie de la preuve ISBN  0-444-10492-5
  • Woodin, WH (2001), "The Continuum Hypothesis, Part I", Notices of the American Mathematical Society , v. 48 n. 6.