Arithmétique de second ordre
En logique mathématique, l'arithmétique de second ordre est une collection de systèmes axiomatiques qui formalisent les entiers naturels et leurs sous-ensembles. C'est une alternative à la théorie des ensembles axiomatiques comme fondement d'une grande partie des mathématiques. Elle a été introduite par David Hilbert et Paul Bernays dans leur livre Grundlagen der Mathematik. L'axiomatisation standard de l'arithmétique de second ordre est notée Z2.
L'arithmétique de second ordre inclut son arithmétique de Peano de premier ordre équivalente, mais est significativement plus forte (plus générale) que celle-ci. Contrairement à l'arithmétique de Peano, l'arithmétique de second ordre permet la quantification sur des ensembles d'entiers naturels ainsi que sur des nombres eux-mêmes. Parce que les nombres réels peuvent être représentés comme des ensembles (infinis) d'entiers naturels de manières connues, et parce que l'arithmétique de second ordre permet la quantification sur ces ensembles, il est possible de formaliser les nombres réels dans l'arithmétique de second ordre. Pour cette raison, l'arithmétique de second ordre est parfois appelée « analyse » (Sieg 2013, p.291).
L'arithmétique de second ordre peut aussi être considérée comme une version faible de la théorie des ensembles dans laquelle chaque élément est soit un entier naturel, soit un ensemble d'entiers naturels. Bien qu'elle soit beaucoup plus faible (moins générale) que la théorie des ensembles de Zermelo-Fraenkel, l'arithmétique de second ordre peut prouver l'essentiel des résultats des mathématiques classiques exprimables dans son langage.
Un sous-système d'arithmétique de second ordre est une théorie dans le langage de l'arithmétique de second ordre dont chaque axiome est un théorème de l'arithmétique de second ordre complet (Z2). Ces sous-systèmes sont essentiels pour les mathématiques à rebours, un programme de recherche qui étudie combien de mathématiques classiques peuvent être dérivées dans certains sous-systèmes faibles de force variable. Une grande partie des mathématiques basiques peut être formalisée dans ces sous-systèmes faibles, dont certains sont définis ci-dessous. Les mathématiques à rebours clarifient aussi l'étendue et la manière dont les mathématiques classiques sont non constructives.
Définition
Syntaxe
Le langage de l'arithmétique de second ordre est ordonné en deux parties. La première sorte de termes, et en particulier les variables, généralement désignées par des lettres minuscules, se compose d'individus, dont l'interprétation est comme des nombres naturels. L'autre sorte de variables, appelées « variables d'ensemble », « variables de classe » ou même « prédicats » sont habituellement désignées par des majuscules. Ils se réfèrent aux classes/prédicats/propriétés des individus, et peuvent donc être considérés comme des ensembles de nombres naturels. Les individus et les variables fixes peuvent être quantifiés universellement ou existentiellement. Une formule sans variables d'ensemble liées (c'est-à-dire sans quantificateurs par rapport aux variables définies) est appelée arithmétique. Une formule arithmétique peut avoir des variables d'ensemble libres et des variables individuelles liées.
.
Par exemple, , est une formule bien formée arithmétique, elle a une variable d'ensemble libre X et une variable d'individu n liée. Tandis que est une 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
Modèle:Section vide ou incomplète
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 ensembles quantifiés peuvent être tous les sous-ensembles du domaine des variables d'individus, de nombres. Si l'arithmétique du second ordre est formalisée en utilisant la sémantique de la logique du premier ordre alors tout modèle comprend un domaine pour les variables d'ensembles, et ce domaine peut être un sous-ensemble strict de l'ensemble des parties du domaine des variables de nombres. (Shapiro 1991, Modèle:P.–75).
Axiomes
Les axiomes suivants sont connus sous le nom d'axiomes de base, ou parfois 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 l'induction. Le domaine du discours pour les variables quantifiées est les entiers naturels, notés N, y compris le membre, appelé « zéro ».
Les fonctions primitives sont la fonction successeur unaire, notée par le préfixe Et deux opérations binaires, l'addition et la multiplication, notées « + » et « » respectivement. Il existe également une relation binaire primitive notée « < ».
Axiomes régissant la fonction successeur et zéro:
- 1. (« Le successeur d'un entier naturel n'est jamais nul »)
- 2. (« La fonction successeur est injective »)
- 3. (« Chaque entier naturel est zéro ou un successeur »)
![{\displaystyle \forall m[Sm=0\rightarrow \bot ].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b0a8f3ffca8c5cc849df18690f46bf1e8d2bab3b)
![{\displaystyle \forall m\forall n[Sm=Sn\rightarrow m=n].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/df7fdd8e9d172deeab2412d40a53bc1091cd7839)
![{\displaystyle \forall n[0=n\lor \exists m[Sm=n]].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/17a818e8072d48fb1e448d64e9d227434cb3e9ba)
Addition définie récursivement:
- 4. Échec de l’analyse (⧼mw_math_mathml⧽ : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \forall m [m+0=m].}
- 5.
![{\displaystyle \forall m\forall n[m+Sn=S(m+n)].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e474ea6efcfdc12cdcab571a6cdf942c61b4852a)
Multiplication définie récursivement:
- 6.
- 7.
![{\displaystyle \forall m[m\cdot 0=0].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/caef550c2bcd17efe0cc5f98fff865def039f2e0)
![{\displaystyle \forall m\forall n[m\cdot Sn=(m\cdot n)+m].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/065e803bdf6d53602cffad597a7d1385762ee4ed)
Axiomes régissant la relation d'ordre « < »:
- 8. (« Aucun entier naturel n'est inférieur à zéro »)
- 9.
- 10. (« Tout entier naturel est égal ou supérieur à zéro »)
- 11.
![{\displaystyle \forall m[m<0\rightarrow \bot ].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4d037a9e910a8abefe6e02931e8f7a0a56214e74)
![{\displaystyle \forall n\forall m[m<Sn\leftrightarrow (m<n\lor m=n)].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/207a5708c22334f5f5f0a08f69521964025cb0ac)
![{\displaystyle \forall n[0=n\lor 0<n].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/30c04b939d04aad652f928d0bc933a7cd4f5a4e5)
![{\displaystyle \forall m\forall n[(Sm<n\lor Sm=n)\leftrightarrow m<n].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/03b25b287ebba2d74f3889b3038f48e8907e6867)
Ces axiomes sont tous des énoncés de premier ordre. 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, forment la définition de Peano-Dedekind de N.
Propriétés
Références
- Burgess, J. P. (2005), Fixing Frege, Princeton University Press.
- Buss, S. R. (1998), Handbook of proof theory, Elsevier. Modèle:ISBN
- Friedman, H. (1976), "Systems of second order arithmetic with restricted induction, " I, II (Abstracts). Journal of Symbolic Logic, v. 41, Modèle:P.– 559. JStor
- Girard, L. and Taylor (1987), Proofs and Types, Cambridge University Press.
- Hilbert, D. and Bernays, P. (1934), Grundlagen der Mathematik, Springer-Verlag. MR 0237246
- Sieg, W. (2013), Hilbert's Programs and Beyond, Oxford University Press.
- Shapiro, S. (1991), Foundations without foundationalism, Oxford University Press. Modèle:ISBN
- Simpson, S. G. (2009), Subsystems of second order arithmetic, 2nd edition, Perspectives in Logic, Cambridge University Press. Modèle:ISBN MR 2517689
- Takeuti, G. (1975) Proof theory Modèle:ISBN
- Woodin, W. H. (2001), "The Continuum Hypothesis, Part I", Notices of the American Mathematical Society, v. 48 n. 6.