Arithmétique du second ordre

Le langage de l'arithmétique du second ordre traite deux sortes d'objets : les termes d'individus, dont les variables sont généralement désignées par des lettres minuscules et interprétés par des nombres entiers, et les « variables d'ensemble », « variables de classe » ou même « prédicats » (il n'y a généralement pas d'autres termes que les variables au niveau des ensembles) qui sont habituellement désignées par des majuscules et interprétés par des sous-ensembles d'entiers, éventuellement de uples d'entiers, ou de façon équivalentes de prédicat sur les entiers. Les individus et les variables fixes peuvent être quantifiés universellement ou existentiellement. Une formule du langage sans variables d'ensemble liées (c'est-à-dire sans quantifications portant sur les ensembles d'entiers) est appelée arithmétique. Une formule arithmétique peut avoir des variables d'ensemble libres et des variables d'individu liées.

Par exemple, dans le langage de signature ${\displaystyle {\mathcal {L}}=\{0,S,+,\cdot ,=,<,\in \}}$, ${\displaystyle \forall n(n\in X\rightarrow Sn\in X)}$, est une formule arithmétique : elle a une variable d'ensemble libre X et une variable d'individu n liée, tandis que${\displaystyle \exists X\forall n(n\in X\leftrightarrow n<SSSSSS0\cdot SSSSSSS0)}$ est une formule qui n'est pas arithmétique, ayant une variable d'ensemble liée X.

Il existe deux sémantiques courantes de la logique du second ordre, et donc de l'arithmétique du second ordre. La première en apparence la plus intuitive est dite « sémantique standard », ou « sémantique des modèles pleins ». Le domaine d'interprétation des variables d'ensembles est celui de toutes les parties du domaine d'interprétation des individus, à priori l'ensemble des entiers naturels. La quantification universelle du second ordre portera alors sur tous les sous-ensembles d'entiers naturels. Il ne peut exister de théorème de complétude pour cette sémantique. Dit autrement il n'y a pas d'axiomatisation satisfaisante pour une telle sémantique.

Une sémantique plus générale autorise des modèles où les variables d'ensembles sont interprétées sur un ensemble quelconque de parties du domaine d'interprétation des individus, pourvu qu'il satisfasse le schéma d'axiomes de compréhension. Un exemple est celui des modèles pleins, mais il existe aussi des modèles où le domaine d'interprétation des variables d'ensemble est un sous-ensemble strict du domaine d'interprétation des variables (Shapiro 1991, p. 74-75), il peut par exemple être dénombrable. Leon Henkin (en) a démontré le théorème de complétude pour cette sémantique.

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${\displaystyle \ 0}$, appelé « zéro ».

Les fonctions primitives sont la fonction successeur unaire, notée par le préfixe${\displaystyle \ S,}$ Et deux opérations binaires, l'addition et la multiplication, notées « + » et « ${\displaystyle \cdot }$ » respectivement. Il existe également une relation binaire primitive notée « < ».

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

1. ${\displaystyle \forall m[Sm=0\rightarrow \bot ].}$ (« Le successeur d'un entier naturel n'est jamais nul »)

2. ${\displaystyle \forall m\forall n[Sm=Sn\rightarrow m=n].}$ (« La fonction successeur est injective »)

3. ${\displaystyle \forall n[0=n\lor \exists m[Sm=n]].}$ (« Chaque entier naturel est zéro ou un successeur »)

Addition définie récursivement:

4. ${\displaystyle \forall m[m+0=m].}$

5. ${\displaystyle \forall m\forall n[m+Sn=S(m+n)].}$

Multiplication définie récursivement:

6. ${\displaystyle \forall m[m\cdot 0=0].}$

7. ${\displaystyle \forall m\forall n[m\cdot Sn=(m\cdot n)+m].}$

Axiomes régissant la relation d'ordre « < »:

8. ${\displaystyle \forall m[m<0\rightarrow \bot ].}$ (« Aucun entier naturel n'est inférieur à zéro »)

9. ${\displaystyle \forall n\forall m[m<Sn\leftrightarrow (m<n\lor m=n)].}$

10. ${\displaystyle \forall n[0=n\lor 0<n].}$ (« Tout entier naturel est égal ou supérieur à zéro »)

11. ${\displaystyle \forall m\forall n[(Sm<n\lor Sm=n)\leftrightarrow m<n].}$

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.