<figure><img src="image_1.png" /></figure>

# Suite de choix et extension nonstandard
de la théorie des types

Une théorie des types nonstandard

Wallet Guy

Laboratoire Mathématiques, Image et Applications
Université de La Rochelle
17042 La Rochelle
France
guyima@univ-lr.fr

RÉSUMÉ. Partant de son travail Mathematics of Infinity [6], Martin-Löf a développé l'idée d'un lien conceptuel profond entre les notions de suite de choix et d'objet mathématique nonstandard. Précisément, il a défini une extension nonstandard de la théorie des types en ajoutant une série d'axiomes nonstandard conçue comme une sorte de suite de choix. Enfin, dans sa communication [8], il a présenté les grandes lignes d'une théorie des types nonstandard plus générale et munie d'un fort contenu computationnel. Le présent travail est une tentative de donner un développement complet d'une théorie de ce genre. Cependant, dans le but de garder un fort contrôle sur la théorie résultante et notablement pour éviter quelques problèmes en rapport avec l'égalité définitionnelle, le champ des axiomes nonstandard est moins général que ceux proposés dans [8]. L'étude présente est poussée jusqu'à l'introduction d'une notion de proposition externe qui joue le même rôle que les propriétés externes si utiles dans l'analyse nonstandard usuelle. Du fait que ce texte débute par une introduction à la théorie des types de Martin-Löf, il peut intéresser les mathématiciens non familiers avec ce sujet.

**ABSTRACT.** Starting from his work Mathematics of Infinity [6], Martin-Löf has developed the idea of a deep conceptual link between the notions of choice sequence and nonstandard mathematical object. Specifically, he defines a nonstandard extension of type theory by adding a series of nonstandard axioms intended as a kind of choice sequence. At last, in his communication [8], he has sketched the outlines of a more general nonstandard type theory with a strong computational content. The present work is an attempt to give a full development of a theory of this kind. However, in order to keep a strong control on the resulting theory and notably to avoid some problems related to the definitional equality, the range of the nonstandard axioms is less general than those proposed in [8]. The present study is conducted until the introduction of a notion of external propositions which play the role of external properties so useful in usual nonstandard analysis. Since this text begins with an introduction to Martin-Löf type theory, it may be interesting for a mathematician not familiar with the subject.

**MOTS-CLÉS** : Suite de choix, théorie des types, analyse nonstandard constructive.

**KEYWORDS** : Choice sequence, type theory, constructive nonstandard analysis.
Un texte développant les principes logico-fondationnels d'une théorie des types non-standard peut paraître bien éloigné du sujet dans des actes d'un colloque dédié aux perturbations singulières et à la dynamique des populations. Par chance, cette appréciation ne tient pas compte du fait que ce colloque s'est tenu en l'honneur d'Éric Benoît. En effet, non seulement Éric utilise fréquemment l'analyse nonstandard - particulièrement dans la forme IST (Internal Set Theory) d'E. Nelson [9] - dans ses travaux mathématiques quels qu'ils soient, mais de plus, il le fait généralement avec une efficacité et une élégance remarquables. On peut donc voir dans ce travail un écho à l'un des aspects de la pratique des mathématiques d'Éric. Incidemment, cet essai est aussi un signe de reconnaissance que je lui adresse pour les années passées à participer à la mise en place de l'université de La Rochelle et de ses composantes mathématiques en enseignement et en recherche.

# 1. Introduction

Bien que ce ne soit pas son but principal, cet article peut être vu comme une introduction informelle à la théorie des types de Martin-Löf. Cette introduction est relativement adaptée au public des mathématiciens et informaticiens non rompus aux développements récents situés à la frontière de la logique et de l'informatique. On sait que la popularité croissante des assistants de preuves comme Coq ou Agda commence à développer l'intérêt pour cette théorie qui a servi de cadre pour la conception de ces outils informatiques.

De fait, le fil directeur de cette étude est celui de la définition d'une extension non-standard de la théorie des types. Ce thème constitue un excellent champ d'expérimentation pour les différents mécanismes de la théorie des types initiale. Cette extension présente elle-même un fort intérêt car elle propose ni plus ni moins que l'édification d'une forme d'analyse nonstandard radicalement constructive très proche de l'univers de l'informatique. Néanmoins, il convient de noter que ce travail est consacré aux questions concernant la fondation de ce système nonstandard et il n'a aucunement pour objectif d'appliquer cette théorie à de vraies questions d'analyse mathématique.

Cet essai se situe dans un des courants de recherche qui, depuis la fin des années 80, a eu pour objet de développer une approche constructive de l'analyse nonstandard. À l'origine on trouve le lumineux travail de Martin-Löf Mathematics of Infinity [6] qui, sur la base d'une certaine notion de suite de choix, décrit une extension nonstandard de la théorie des types ainsi que son modèle privilégié. Dans une série d'exposés donnés peu de temps après [7], Martin-Löf a développé sa conception d'un lien conceptuel entre les notions de suite de choix, d'objet nonstandard et de logique modale. Suite à ce travail pionnier, de nombreuses recherches[1, 3, 12, 15] sur le thème de l'analyse nonstandard constructive ont proposé des versions de plus en plus riches, souvent liées à la théorie des catégories, mais développées dans un cadre moins contraignant que celui de la théorie des types. En 1999, Martin-Löf a fait une communication [8] exposant les principes d'une théorie des types nonstandard plus générale et dotée d'un contenu computationnel plus fort que celle exposée dans son article initial [6]. Malheureusement, cet exposé n'a pas donné lieu à
une publication et ce travail n’est connu que sous la forme de brèves notes manuscrites forcément incomplètes et parfois problématiques. D’ailleurs, il semble que récemment Martin-Löf ait apporté des modifications à cette théorie afin d’en corriger certains aspects mais il n’a pas eu l’occasion de communiquer sur cette question.

Le présent travail développe une version d’analyse nonstandard conçue dans l’esprit de Martin-Löf, c’est-à-dire obtenue en rajoutant à la théorie des types une série d’axiomes apparentée à une suite de choix. Ces axiomes sont en gros ceux qui étaient proposés dans l’article initial de Martin-Löf [6] mais le développement théorique qui utilise ces axiomes se fait en empruntant en partie le point de vue exposé dans la dernière communication de Martin-Löf sur le sujet [8]. Cette stratégie permet d’éviter certains aspects problématiques de la suite de choix sous-jacente à cette dernière étude tout en en conservant d’autres aspects très intéressants, moyennant quelques substantielles adaptations. L’un des buts est de tester les qualités de la théorie des types nonstandard que l’on obtient à partir de la forme certes contraignante mais bien contrôlée de la forme de suite de choix résultant des axiomes en question. L’idée est de développer cette théorie jusqu’à l’introduction de ce que je nomme les propositions externes. Construites sur une idée de Martin-Löf, ces dernières sont explicitement conçues pour jouer le rôle des propriétés dites externes qui, pour l’essentiel, font la fécondité de de l’analyse nonstandard usuelle. Les qualités démontrées de ces propositions externes pourront servir de critère pour juger de l’efficience de cette forme de théorie nonstandard et éventuellement suggérer des améliorations comme cela est fait à la fin de ce travail.

Outre l'introduction, cet article comporte 6 parties. La première est consacrée à une présentation de la théorie des types de Martin-Löf, la seconde à la notion de suite de choix et à l'extension nonstandard de la théorie des types, la troisième à la notion de voisinage, à l'opération d'élimination de la suite de choix et au théorème de transfert, la quatrième à une étude fine des relations d'égalité entre des termes de la suite de choix, la cinquième à une forme de standardisation, et la sixième conclut ce travail avec la notion de proposition externe. Les trois premières parties et partiellement la quatrième devraient bien convenir à un lecteur non familier de la théorie des types.

Quelques remerciements maintenant. Evidemment, ce travail doit énormément à Per Martin-Löf : sans lui, le sujet traité ici n'existerait tout simplement pas. Je le remercie particulièrement pour le temps qu'il m'a accordé lors de deux longues discussions en 2011. Merci également à Thierry Coquand pour les quelques explications fort éclairantes qu'il m'a apportées. Enfin, je dois aussi remercier Pascal Boldini qui, à l'occasion d'un séminaire introductif sur le point de vue de Martin-Löf en matière d'analyse nonstandard, m'avait confié une copie des notes manuscrites [7] et [8] sans lesquelles je n'aurais jamais eu l'idée de ce travail.

Enfin, je signale qu'une collaboration en cours avec des collègues informaticiens, Nicolas Magaud<fnref n="1" /> et Laurent Fuchs<fnref n="2" />, a pour objet de voir dans quelle mesure cette forme

<footnote n="1">1. Laboratoire ICube de l'Université de Strasbourg.</footnote>

<footnote n="2">2. Laboratoire XLIM-SIC de l'Université de Poitiers.</footnote>
de théorie des types nonstandard peut être transposée dans le cadre informatique de l'as-
sistant de preuve Coq.

2. La théorie des types de Martin-Löf

2.1. Discussion préliminaire

Notée $\mathcal{T}$ dans la suite, la théorie des types de Martin-Löf<fnref n="3" /> est apparue au début des années 70. Depuis cette date, elle n'a pas cessé d'évoluer tout en gardant ses traits essentiels. A l'origine, Martin-Löf a présenté sa théorie comme une formalisation des mathématiques constructives, par exemple de l'analyse de Bishop [1], de même que la théorie des ensembles de Zermelo-Fraenkel avec l'axiome du choix (ZFC) constitue un fondement formel pour les développements mathématiques classiques. Il est apparu au fil du temps que $\mathcal{T}$ était porteuse d'une richesse expressive étonnante allant bien au delà de sa vocation initiale. La dernière preuve en est l'ensemble des travaux sur la théorie homotopique des types [18] découlant d'un lien surprenant mis à jour entre $\mathcal{T}$ et la théorie abstraite de l'homotopie à la Grothendieck ; cela a conduit à la proposition d'une nouvelle forme de fondement pour les mathématiques classiques et constructives, les Fondations Universalistes des Mathématiques [18]. Cependant, il est nécessaire de préciser que le présent article ne dépend pas quant au fond de ces développements théoriques. La prise en compte de ces travaux a seulement entraîné une inflexion dans la terminologie visant à éviter une ambiguïté relative à la notion d'ensemble<fnref n="4" /> : dans la suite, on utilisera seulement le terme de type et non pas celui d'ensemble.

C'est à la frontière de la logique et de l'informatique (théorique et pratique) que $\mathcal{T}$ a vu le jour. De fait, elle a intégré de nombreux traits et innovations spécifiques à ce dernier champ, ce qui contribue manifestement à ses grandes qualités. Mais cela a pour conséquence que $\mathcal{T}$ se présente sous une forme et avec un mode de fonctionnement radicalement différents de ceux auxquels sont habitués la majorité des mathématiciens et même de nombreux informaticiens et logiciens. Il en découle une difficulté certaine pour appréhender et comprendre en profondeur les ressorts de cette théorie lorsque l'on ne possède pas la culture du milieu logico-informatique dont elle est issue. En conséquence, il ne semble pas raisonnable de vouloir présenter exhaustivement $\mathcal{T}$ en quelques pages dans un article prétendant s'adresser aux mathématiciens en général. Dans cette étude, il est proposé une approche progressive de quelques-uns des traits importants de $\mathcal{T}$. Cette approche est volontairement non exhaustive et elle évite certains volets formels comme les énoncés des règles dites d'élimination. Toutefois, elle est en principe suffisante pour

<footnote n="3">3. La théorie des types de Martin-Löf est aussi appelée théorie constructive des types ou théorie intuitionniste des types.</footnote>

<footnote n="4">4. La notion d'ensemble au sens de Martin-Löf ne correspond pas à celle qui est proposée dans la théorie homotopique des types.</footnote>
comprendre la suite de l'article. Le lecteur intéressé pourra toujours se reporter ultérieu-
rement à la littérature pour approfondir le sujet (voir [11, 14] et le chapitre 1 de [18]).
Enfin, l'approche de $\mathcal{T}$ développée dans cette partie 2 se poursuivra en fait dans toute la
suite de cet article puisque, comme on le verra, tout développement dans la théorie des
types nonstandard se ramène d'une certaine manière à un développement dans $\mathcal{T}$.

Dans un premier temps, il est demandé au lecteur d'admettre sans plus de détails que, comme on l'a dit, $\mathcal{T}$ est une théorie formalisant le vaste champ des mathématiques constructives. Cela implique qu'il est possible en principe d'y définir et de travailler avec des fonctions, les nombres usuels, le nombre $\pi$, ... Dans la suite de cette section 2, nous allons présenter trois thèmes qui sont importants dans $\mathcal{T}$ et pour lesquels cette théorie est radicalement différente des autres formalisations plus anciennes comme ZFC : les notions de type et de jugement, la place de la logique, et enfin le traitement de l'égalité. Il faut ajouter que ces trois points jouent un rôle particulièrement important dans la définition et le fonctionnement de l'extension nonstandard.

## 2.2. Les types et les jugements

2.2.1. Généralités sur les types

Dans $\mathcal{T}$, la notion de base est celle de type. L'assertion *A est un type* est notée formellement (*A type*). La signification de cette assertion suppose que les points suivants sont vérifiés.

1) On a défini les conditions permettant d'affirmer que quelque chose est un objet de type A. Ces conditions donnent une définition inductive des objets de type A, définition qui se fait au moyen de constructeurs qui sont intrinsèquement attachés à A.

2) On a défini les conditions permettant d'affirmer que deux objets de type *A* sont égaux,
L'assertion *a est un objet de type A* est notée (*a* : *A*) et l'assertion *a et b sont égaux en tant qu'objets de type A* est notée (*a* = *b* : *A*).

Le prototype des types dans $\mathcal{T}$ est le type $\mathbb{N}$ des entiers naturels. Ce type est défini par la donnée de deux constructeurs $0$ et $S$ et des règles inductives suivantes :

1) $0 : \mathbb{N}$

2) Du jugement $x : \mathbb{N}$ on déduit le jugement $S(x) : \mathbb{N}$
Les objets de type $\mathbb{N}$ donnés par les deux règles précédentes sont dits canoniques. Plus
généralement, un objet de $\mathbb{N}$ est un procédé de calcul qui produit un objet canonique.

De manière générale, les objets canoniques d'un type *A* sont ceux qui sont obtenus
directement par les constructeurs de *A* ; les objets non canoniques de type *A* sont ceux
qui, par un procédé de calcul se ramène à des objets canoniques.

On définit des opérations qui permettent de construire de nouveaux types à partir
d'autres types donnés. Par exemple, si *A* et *B* sont des types, on définit $A \to B$ comme
le type des fonctions de *A* dans *B*.
### 2.2.2. Les jugements

La théorie $\mathcal{T}$ est un système formel qui permet de dériver (de démontrer) des propriétés mathématiques appelées des jugements<fnref n="5" />. Voici trois premiers exemples de jugements :

$$(\mathbb{N} \text{ type}), (0 : \mathbb{N}), (1 : \mathbb{N})$$

où 1 est défini comme $S(0)$.

Un jugement est un morceau de connaissance, un savoir acquis. Il en découle que cela n'a aucun sens de le nier, ou de l'utiliser dans une construction logique hypothétique. Par exemple, l'énoncé $\neg(0 : \mathbb{N})$ n'a aucun sens dans $\mathcal{T}$. En effet, $(0 : \mathbb{N})$ est un jugement, une connaissance préalablement établie au moment où l'on définit l'ensemble $\mathbb{N}$. A partir du moment où cette connaissance est assurée, il devient incohérent de prétendre la nier.

### 2.2.3. Jugements, types et objets dépendants

L'une des originalités de $\mathcal{T}$ est d'introduire à la base de cette théorie la notion de jugement dépendant : c'est un jugement qui est obtenu sous certaines conditions. Ces conditions sont formalisées par la notion de contexte. La forme générale d'un contexte est donnée par une suite ordonnée de jugements, présentée entre crochets dans cet article, de la forme

$$[x_1 : A_1, x_2 : A_2, \dots, x_n : A_n] \qquad (1)$$

où l'on suppose préalablement que l'on dispose des jugements suivants<fnref n="6" /> :

$A_1$: type

$A_2$: type $[x_1 : A_1]$ (où $A_2$ peut dépendre de la variable $x_1$)

...

$A_n$: type $[x_1 : A_1, \dots, x_{n-1} : A_{n-1}]$

(où $A_n$ peut dépendre des variables $x_1, \dots, x_{n-1}$)

La forme générale d'un jugement $J$ dépendant du contexte (1) est

$$J [x_1 : A_1, \dots, x_n : A_n]$$

ce qui signifie que l'on dispose du jugement $J$ sous la condition que les variables $x_1, \dots, x_n$ respectent le contexte en question (ce qui présuppose que $J$ peut dépendre de ces variables). Un type $A$ est dépendant si le jugement ($A$ type) est dépendant. De même, un

<footnote n="5">5. Les descriptions classiques des systèmes formels utilisent plutôt le terme de théorème. Ce dernier possède deux usages dans les mathématiques usuelles : d'une part, on dit que toute propriété démontrée est un théorème, d'autre part il est d'usage de réserver le nom de théorème à des résultats estimés suffisamment importants. Au contraire, toute assertion dérivée dans $\mathcal{T}$ est appelée un jugement.</footnote>

<footnote n="6">6. A partir du deuxième, ces jugements sont eux-mêmes dépendants. De fait, la notion de jugement dépendant se définit de manière inductive relativement au nombre de variables.</footnote>
objet *b* d'un type *B* est dépendant si le jugement (*b* : *B*) est dépendant. L'explicitation dans *T* de cette notion de dépendance est d'une certaine importance du fait que, dans la pratique des mathématiques, une grande partie des entités sur lesquelles on raisonne sont dépendantes.

## 2.3. La place de la logique dans $\mathcal{T}$

Le genre de choses que l'on peut nier et que l'on peut combiner avec les constantes logiques ne sont pas les jugements mais ce sont les propositions<fnref n="7" />. Par exemple ($\exists x : N$) ($0 = S(x)$) est une proposition, de même que sa négation ($\neg(\exists x : N)$) ($0 = S(x)$).

Dans les mathématiques classiques, les entités qui correspondent aux propositions sont les formules mais ces dernières ne sont que des objets syntaxiques, c'est-à-dire des assemblages de symboles construits selon certaines règles et non pas des objets mathématiques. Au contraire, dans $\mathcal{T}$, les propositions sont de vrais objets mathématiques. Précisément, les propositions sont des types particuliers ; l'assertion selon laquelle un type *A* dans $\mathcal{T}$ est une proposition constitue un jugement noté (*A* prop).

De prime abord, l'identification des propositions à des types paraît complètement injustifiée. Comment peut-on imaginer que des entités aussi différentes que d'une part un type et d'autre part une proposition puissent être considérés comme appartenant au même genre de choses ? En effet, un type peut être grossièrement assimilé à un ensemble et depuis Cantor, ces derniers sont les objets mathématiques par excellence, alors que depuis Frege, Russell et Wittgenstein une proposition est vue comme un énoncé logique. La justification de cette identification dépend de la logique intuitionniste dont l'un des principes de base est qu'une proposition est vraie lorsqu'une preuve peut en être donnée. Précisément, l'identification en question s'appuie sur les remarques suivantes :

- L'interprétation BHK<fnref n="8" /> de la logique intuitionnisme établit que les preuves d'une proposition peuvent être ramenées à une forme canonique particulière. Par exemple, une preuve d'une proposition $P \implies Q$ peut être ramenée à une fonction qui transforme toute preuve de *P* en une preuve de *Q* : de même, une preuve de $P \land Q$ peut être ramenée à un couple (*p*, *q*) où *p* est une preuve de *P* et *q* une preuve de *Q*.

- Une proposition est définie par la forme canonique de ces preuves de la même manière qu'un type est défini par ses éléments canoniques.

- D'après l'interprétation BHK, les opérations logiques utilisées pour construire les propositions s'interprètent exactement comme les opérations usuelles de construction de types.

A partir de là, il est naturel d'identifier une proposition *A* avec le type, noté aussi *A*, dont les objets sont les preuves de cette proposition ; dans ce cas, les preuves de *A* sont aussi appelées les objets-preuves de *A* (ou les témoins de *A*). Par exemple, la proposition

<footnote n="7">7. Depuis les mathématiques grecques, le terme de proposition est synonyme d'une forme légèrement affaiblie de théorème. Dans cet article, on se plie à l'usage des logiciens qui réservent le mot proposition pour qualifier une assertion susceptible d'être mis à l'épreuve de la vérité.</footnote>

<footnote n="8">8. Brouwer-Heyting-Kolmogorov.</footnote>
absurde $\perp$ est représentée par le type vide $\emptyset$; si $A$ est une proposition, alors la négation $\neg A$ de $A$ est la proposition $(A \Rightarrow \perp)$ qui n'est rien d'autre que le type $(A \to \emptyset)$; si $A$ et $B$ sont des propositions, alors la proposition $(A \Rightarrow B)$ s'identifie au type $A \to B$ des fonctions de $A$ dans $B$ et la proposition $(A \wedge B)$ s'identifie au produit $A \times B$, et ainsi de suite.

Cette identification entre propositions et types est appelée le *principe des propositions comme types*. Ce principe présente une économie conceptuelle intéressante : la théorie $\mathcal{T}$ n'a plus aucun besoin d'une logique extérieure à elle-même, sa notion de type fournissant toutes les propositions voulues, avec l'avantage que les propositions et leurs objets-preuves sont maintenant des objets mathématiques susceptibles d'entrer dans les raisonnements.

Voici un exemple simple pour montrer comment cette identification fonctionne. On considère la proposition $(A \Rightarrow \neg(\neg A))$ où $A$ est une proposition donnée. Elle se développe en $(A \Rightarrow ((A \Rightarrow \perp) \Rightarrow \perp))$ et elle s'identifie au type $(A \to ((A \to \emptyset) \to \emptyset))$ qui manifestement possède l'objet<fnref n="9" /> $(\lambda x)((\lambda f)f(x))$. Cet objet-preuve atteste que $(A \Rightarrow \neg(\neg A))$ est vraie. Il est bien connu que l'implication réciproque ne peut être prouvée en logique intuitionniste.

L'affirmation qu'une proposition $B$ est vraie, notée $(B \text{ true})$, est une forme faible de jugement car elle occulte une information importante. La forme complète, sans perte d'information, d'un tel jugement est $(b : B)$ où $b$ est un objet-preuve explicitement construit. Par exemple, la forme complète du jugement $((A \Rightarrow \neg(\neg A)) \text{ true})$ est le jugement $((\lambda x)((\lambda f)f(x)) : (A \Rightarrow \neg(\neg A)))$.

Enfin, pour revenir à une proposition mentionnée au début de la partie 2.3, on peut montrer que

$$ \neg(\exists x : \mathbb{N}) (0 = S(x)) \qquad (2) $$

est vraie<fnref n="10" />. Non triviale, la démonstration n'en sera pas donnée ici d'autant plus qu'elle n'est pas utilisée dans le présent texte. Néanmoins, la compréhension de la signification de l'énoncé de cette proposition nécessite de clarifier ce qu'est l'égalité dans $\mathcal{T}$, ce qui va être fait dans la partie 2.4.

## 2.4. Le traitement de l'égalité dans $\mathcal{T}$

Le traitement de l'égalité dans $\mathcal{T}$ est totalement surprenant pour le lecteur qui le découvre. En effet, dans $\mathcal{T}$, l'égalité, ce concept semble-t-il naturel et sans mystère, se scinde en deux notions différentes - l'égalité définitionnelle et l'égalité propositionnelle - muni de statuts et de modes de fonctionnement très différents<fnref n="11" />. De prime abord, cette distinc-

<footnote n="9">9. Cet objet est écrit en utilisant la notation usuelle du lambda calcul. Il est curieux que cette forme de notation très commode ne soit pratiquement pas utilisée en mathématiques. Avec une notation plus commune en mathématiques, ce même élément s'écrit $x \mapsto (f \mapsto f(x))$.</footnote>

<footnote n="10">10. Cette affirmation est classiquement l'un des axiomes de Peano.</footnote>

<footnote n="11">11. Il semble que la distinction entre deux sortes d'égalité est aussi présente dans des travaux de de Bruijn.</footnote>
tion peut sembler n'être qu'une contrainte formelle de plus dont l'effet principal serait de rendre délicate, lourde voire impossible, la transcription dans $\mathcal{T}$ du moindre raisonnement mathématique utilisant l'égalité. Cette première impression est partiellement trompeuse puisque cette distinction se révèle être la source d'une richesse expressive étonnante. Par exemple, l'extension nonstandard de $\mathcal{T}$ étudiée plus loin dans ce texte, est dans sa définition même fortement dépendante de cette distinction. De même pour la très récente théorie homotopique des types qui est basée sur l'analogie entre les propriétés de l'égalité propositionnelle et celles de l'homotopie.

### 2.4.1. L'égalité définitionnelle

L'égalité définitionnelle ou égalité par définition est la forme d'égalité qui est en elle-même un jugement. C'est un jugement qui affirme l'égalité de deux objets de même type

$$a = b : A$$

Un cas simple mais significatif d'égalité définitionnelle est lorsque l'on introduit un nom pour un objet préalablement construit. Par exemple, on peut décider d'attribuer le nom $f$ à la fonction $(\lambda x)x^2 : \mathbb{N} \to \mathbb{N}$ :

$$f = (\lambda x)x^2 : \mathbb{N} \to \mathbb{N} \qquad (3)$$

C'est une égalité définitionnelle qui va générer une nouvelle égalité définitionnelle chaque fois que dans un terme faisant intervenir le nom $f$, on substitut $(\lambda x)x^2$ à chaque occurrence du nom $f$. Ainsi

$$f(2) = 2^2 : \mathbb{N}$$

En ce sens, tout texte de mathématiques est habituellement truffé d'égalités définitionnelles ; jusqu'à Martin-Löf<fnref n="12" />, personne n'avait vraiment accordé une grande importance à ces égalités qui n'étaient perçues que comme des conventions linguistique de confort sans aucune profondeur conceptuelle.

Autre exemple significatif : l'addition sur $\mathbb{N}$ est définie par induction de sorte que, par définition, on a les deux jugements dépendants du contexte $x : \mathbb{N}$, $y : \mathbb{N}$

$$\begin{cases} x + 0 = x & : \mathbb{N} \\ x + S(y) = S(x + y) & : \mathbb{N} \end{cases}$$

qui sont donc des égalités définitionnelles<fnref n="13" />. Cet exemple illustre une autre source d'égalités définitionnelles qui est l'ensemble des règles de calcul qui traduisent la structure inductive de chaque type<fnref n="14" />.

<footnote n="12">12. Martin-Löf signale néanmoins les premières réflexions de Frege sur l'égalité qui rétrospective-ment semblent anticiper la notion d'égalité définitionnelle.</footnote>

<footnote n="13">13. Posant $1 = S(0) : \mathbb{N}$, on en déduit par exemple que $x + 1 = S(x) : \mathbb{N}$.</footnote>

<footnote n="14">14. Ce sont les règles dites d'égalité ou de calcul qui portent sur le récurseur traduisant la structure inductive d'un type. Dans le cas de l'addition des entiers, l'addition est définie en utilisant l'induction sur $\mathbb{N}$ via un récurseur noté natrec.</footnote>
Martin-Löf fait remarquer dans [4] que l'égalité définitionnelle est une relation entre des expressions linguistiques et non pas entre les objets que dénotent ces expressions, objets qui sont les mêmes. Il la caractérise de manière unique par les trois principes suivants :

1) L'attribution d'un nom à une expression est un égalité définitionnelle.

2) L'égalité définitionnelle est préservée par substitution.

3) L'égalité définitionnelle est réflexive, symétrique et transitive.

Il découle de la manière dont sont générées les égalités définitionnelles dans $\mathcal{T}$ une propriété importante : l'égalité définitionnelle est décidable : elle peut se vérifier par un simple calcul.

On peut remarquer que, pour les objets d'un type A donné, on a rencontré seulement deux formes de jugements, à savoir $(a : A)$ et $(a = b : A)$ dont l'une est une égalité définitionnelle. En fait, ce sont les deux seules formes de jugements impliquant des objets d'un type donné. Il existe deux autres formes de jugement impliquant seulement des types : $(A$ type) et $(A = B$ type), cette dernière étant aussi une égalité définitionnelle. Ces deux dernières formes de jugements possèdent les variantes suivantes : $(A$ prop) et $(A = B$ prop). En tout, on a quatre formes de jugement et ce sont les seules dans $\mathcal{T}$.

### 2.4.2. L'égalité propositionnelle

Puisque l'égalité définitionnelle est un jugement, ce n'est pas une proposition. Il en découle que l'on ne peut pas l'utiliser comme ingrédient dans la construction d'une proposition. Par exemple, si par définition j'appelle $f$ la fonction $((\lambda x)x^2 : \mathbb{N} \to \mathbb{N})$, cela n'a aucun sens de vouloir nier l'égalité définitionnelle correspondante (3). Autre exemple d'une certaine importance pour la suite : il n'est pas possible d'appliquer un raisonnement par récurrence sur une égalité définitionnelle. Néanmoins, les mathématiques ont un besoin essentiel de disposer d'une égalité qui puisse être utilisée dans les propositions comme le montre l'exemple (2) de la proposition exprimant un axiome de Peano.

L'égalité qui est utilisée dans les propositions est l'égalité propositionnelle. Cette égalité est elle-même une proposition dépendant de deux arguments. Précisément, étant donné un type $A$ et deux objets $a$ et $b$ de type $A$, on dispose dans $\mathcal{T}$ du jugement

$$a =_A b \text{ prop} \qquad (4)$$

qui introduit l'égalité propositionnelle relative au type $A$. Puisque $(a =_A b)$ est une proposition, c'est aussi un type dont les objets sont les objets-preuves de cette proposition. On dit que $a$ est propositionnellement égal à $b$ si la proposition $(a =_A b)$ est vraie, c'est-à-dire si on sait en produire un objet-preuve $p$, ce qui se traduit par le jugement $(p : a =_A b)$.

La première règle est que l'égalité définitionnelle entraîne l'égalité propositionnelle. Précisément, on dispose d'une règle qui, d'une égalité définitionnelle $(a = b : A)$ permet de déduire un objet $id(a)$ du type $(a =_A b)$, ce qui donne le jugement $(id(a) : a =_A b)$; en fait, $id(a)$ est l'élément canonique du type $(a =_A b)$.
On pourrait penser qu'une sorte de réciproque assure une forme d'équivalence entre les deux sortes d'égalité<fnref n="15" />. Il n'en est rien, au moins pour la version dite intentionnelle de la théorie des types qui s'est imposée comme la plus riche. Considérons par exemple la proposition $(0+x =_N x)$ dépendant du contexte $[x : N]$. On montre que cette proposition est vraie en en construisant un objet-preuve par exemple par induction sur $N$. Cependant, il n'y a aucune raison pour que les nombres $0+x$ et $x$ soient définitionnellement égaux.

### 3. Suite de choix et présentation de $\mathcal{T}_\infty$

Dans sa conférence [8], Martin-Löf se propose de décrire les fondements d'une extension nonstandard de $\mathcal{T}$ pour laquelle on pourrait disposer de propriétés constituant des analogues plus ou moins proches mais constructifs des trois principes fondamentaux de la théorie des ensembles internes IST d'E. Nelson[9] informellement décrits de la manière suivante :

- le principe de transfert selon lequel une propriété standard est vraie dans la théorie standard si et seulement si elle est vraie dans l'extension nonstandard;

- le principe d'idéalisation qui permet l'introduction d'entités nonstandard;

- le principe de standardisation qui permet d'associer à une proposition nonstandard un ensemble standard avec un lien fort entre les deux.

Le but de cette section et de donner la définition d'une extension nonstandard $\mathcal{T}_\infty$ de $\mathcal{T}$ en termes de suite de choix dans l'esprit de Martin-Löf. Auparavant, il est rappelé quelques éléments sur les suites de choix de L.E.J. Brouwer.

#### 3.1. Un concept intuitionniste qui remonte à Brouwer

Le concept de suite de choix a été introduit par L.E.J. Brouwer dans son entreprise d'une refondation des mathématiques sur une base radicalement constructive qu'il va ap-peler *l'intuitionnisme*. Dans les premiers écrits de Brouwer [2] sur l'intuitionnisme, ce dernier est caractérisé par les deux points suivants :

- le rejet de la loi du tiers exclu;

- l'introduction de processus séquentiels sans fin dont les termes successifs sont plus ou moins librement déterminés.

Ces processus sont les *suites de choix* que Brouwer utilise tout d'abord dans le but d'ob-tenir une notion du continu qui capte correctement l'intuition ancestrale qu'en a l'esprit

<footnote n="15">15. Dans le traité [5], l'équivalence en question résulte d'une "règle d'élimination" particulière fondant ce que l'on a appelé l'égalité propositionnelle *extensionnelle*. Il est apparu que cette règle n'avait pas la même forme que les autres règles d'élimination et qu'elle créait une faille dans le caractère prédicatif de $\mathcal{T}$. Par la suite, cette règle a été remplacée par une nouvelle qui est complètement en accord avec les autres règles d'élimination dans $\mathcal{T}$. L'égalité propositionnelle ainsi obtenue est dite *intentionnelle*.</footnote>
humain. Il estimait que la collection des seuls nombres réels constructifs était insuffisante pour représenter cette idée. Classiquement, on distingue les *lawlike sequences* et les suites de choix. Les premières sont complètement décrites par un loi, une méthode constructive prédéterminée qui indique comment elles sont engendrées. Les secondes sont non entièrement prédéterminées, toujours inachevées avec un développement futur plus ou moins incertain, ce qui n'interdit pas de raisonner rigoureusement sur de tels processus<fnref n="16" />

Le sujet des suites de choix est très peu connu dans l'ensemble de la communauté des mathématiciens. Pourtant, des études conséquentes ont été menées sur ce thème [3, 17], mais il est vrai que ces travaux ne sont pas d'accès faciles. En effet, ils présupposent une culture spécifique à la frontière de la logique et de l'intuitionnisme qui n'est guère partagée. Cela peut expliquer qu'auprès du commun des mathématiciens, la notion de suite de choix soit largement méconnue. Une autre raison plus fondamentale contribue à cette ignorance : le concept de suite de choix ne prend vraiment son sens que dans un cadre de pensée résolument non platonicien, dans lequel l'univers des objets mathématiques constitue une totalité en devenir et non prédéterminée. Il est clair que ce point de vue est à l'opposé de la philosophie implicite et spontanée qui accompagne la pratique des mathématiques classiques. En particulier, on peut estimer que la notion de suite de choix est littéralement écrasée, vidée de son sens original, si l'on en fait une lecture en termes de la notion de suite au sens usuel dans les mathématiques classiques. Pour éviter cet écueil, il faut arriver à concevoir une suite de choix comme étant une sorte d'objet dynamique dont le processus de construction n'est fondamentalement jamais achevé.

## 3.2. Type et objet standard ou nonstandard dans $T_∞$

Avant de définir l'extension nonstandard $T_∞$ de T, il est bon de préciser quelques points de terminologie qui seront d'un usage constant. La remarque basique fondant l'usage de l'adjectif *standard* est la suivante : puisque la nouvelle théorie $T_∞$ va être définie comme une extension de la théorie T, toute entité définie dans T peut être par- reillement définie dans $T_∞$ ; précisément, le procédé de définition de l'entité en question s'interprète comme un procédé de définition dans $T_∞$ d'une entité de même nature. Les entités en question sont les types et les objets de chacun de ces types, ce qui donne les deux cas suivants :

1) Supposons que G soit un type dans T. Cela signifie que l'on sait dériver dans T le jugement (G type). Puisque $T_∞$ est une extension de T, la même dérivation s'interprète tout autant comme une dérivation du même jugement (G type) dans $T_∞$. Dans ce cas, on dit que G est un *type standard* de $T_∞$. Par exemple, le type entier naturel $N$ est un type standard dans $T_∞$.

2) Supposons maintenant que G soit un type standard de $T_∞$ et que $(g : G)$ soit un jugement de T. Alors, $(g : G)$ est aussi un jugement de $T_∞$ et on dit que g est un *objet*

<footnote n="16">16. En gros, toute propriété d'une suite de choix doit pouvoir se lire sur un segment initial convenable de la suite.</footnote>
standard de type G. Par exemple, 0 est un objet standard de $\mathbb{N}$ dans $\mathcal{T}_\infty$.

Ce qui vient d'être dit pour les types et leurs objets vaut mutatis mutandis pour les propositions et leurs objets-preuves. L'adjectif nonstandard est parfois utilisé pour qualifier un type ou un objet défini dans $\mathcal{T}_\infty$ qui n'est pas standard en un sens plus ou moins restrictif : soit on ne sait pas montrer qu'il est standard, soit on sait montrer qu'il ne peut pas être standard. Par extension, on dit aussi que $\mathcal{T}$ est la théorie des types standard et que $\mathcal{T}_\infty$ est la théorie des types nonstandard.

### 3.3. Les axiomes nonstandard

On se propose maintenant de définir deux règles, les axiomes nonstandard, qui sont spécifiques à la théorie nonstandard $\mathcal{T}_\infty$. Dans l'esprit de l'analogie avec la théorie IST de Nelson, ces règles peuvent être interprétées comme une forme de principe d'idéalisation intuitionniste car elles forcent l'existence d'objets nonstandard dans $\mathbb{N}$. En fait, la première règle introduit de nouveaux nombres entiers et la seconde règle introduit des relations entre ces nombres qui sont des règles de calcul.

**ANS 1.** Etant donné un nombre standard $i : \mathbb{N}$, on peut introduire dans $\mathcal{T}_\infty$ une constante $\infty_i$ et le jugement

$$ \infty_i : \mathbb{N} \qquad (5) $$

**ANS 2.** Etant donné un nombre standard $i : \mathbb{N}$, on peut introduire dans $\mathcal{T}_\infty$ le jugement d'égalité définitionnelle

$$ \infty_i = S(\infty_{i+1}) : \mathbb{N} \qquad (6) $$

Dans le deuxième axiome, il est présupposé que l'on a préalablement appliqué deux fois la première règle afin de disposer de $\infty_i$ et $\infty_{S(i)}$. On peut noter une particularité de ces règles : la prémisse est un jugement dans la théorie standard $\mathcal{T}$, la conclusion est un jugement dans la théorie nonstandard $\mathcal{T}_\infty$.

Chacun des axiomes nonstandard n'est pas un axiome singulier mais un schéma d'axiomes paramétré par un nombre entier standard. A tout moment dans une dérivation de jugements dans $\mathcal{T}_\infty$, on a la possibilité de choisir un entier naturel standard $i$ et d'appliquer l'une ou l'autre des conclusions précisées dans les axiomes nonstandard pour ce choix<fnref n="17" />. Mais cela n'a pas de sens de vouloir appliquer l'un au l'autre des axiomes nonstandard simultanément pour toutes les entiers naturels standard de $i$.

Chaque nombre entier $\infty_i$ est a priori nonstandard mais il est de plus un bon candidat pour être infiniment grand. En effet, en appliquant sucessivement ces deux règles, on obtient

$$ \infty_i = \infty_{i+1} + 1 = \infty_{i+2} + 2 = \dots = \infty_{100} + 100 = \dots $$

si bien que $\infty_i$ est plus grand que 1, que 2, ..., que 100, ...

<footnote n="17">17. En toute généralité, cet entier $i$ peut être dépendant dans la théorie standard $\mathcal{T}$.</footnote>
Il ne faudrait pas croire que les nombres $\infty_i$ sont les seuls nombres nonstandard de $\mathcal{T}_\infty$. En fait, ces objets explicitement introduits ont de nombreuses répercussions sur l'ensemble de la théorie $\mathcal{T}_\infty$ puisque l'on peut former à partir d'eux de nouveaux types et de nouveaux objets dans $\mathcal{T}_\infty$.

Enfin, il faut noter que les deux axiomes nonstandard sont les deux seules ajouts à la théorie standard $\mathcal{T}$ pour obtenir la théorie nonstandard $\mathcal{T}_\infty$. Concrètement, cela signifie que les jugements obtenus dans $\mathcal{T}_\infty$ sont les jugements que l'on peut former en utilisant les règles usuelles de la théorie des types $\mathcal{T}$ et les deux axiomes nonstandard.

### 3.4. La suite de choix $\infty$

Grâce aux axiomes nonstandard, on introduit un nombre entier naturel nonstandard $\infty$ qui est conçu comme résultant de la suite d'égalités définitionnelles suivantes :

$$ 
\begin{align*}
\infty &= \infty_0 : \mathbb{N} \\
\infty_0 &= S(\infty_1) : \mathbb{N} \\
\infty_1 &= S(\infty_2) : \mathbb{N} \\
\infty_2 &= S(\infty_3) : \mathbb{N} \\
\dots
\end{align*}
\tag{7} $$

que Martin-Löf note aussi $\infty = S(S(S(...)))$.

Notons d'abord que $\infty$ est parfaitement défini dans $\mathcal{T}_\infty$ du fait simplement qu'il est posé égal à $\infty_0$ et que l'existence de ce dernier découle de l'application de ANS 1. Néanmoins, si on veut considérer (7) comme constituant une définition, cette dernière est non bien fondée car le processus de définition de $\infty$ se continue sans fin : la définition de $\infty$ fait intervenir $\infty_0$, qui à son tour fait intervenir $\infty_1$, qui à son tour etc. Mais puisque dans toute démonstration dans $\mathcal{T}_\infty$ l'on ne peut utiliser qu'un nombre fini d'occurences des axiomes nonstandard, la suite d'égalités (7) se borne systématiquement à un nombre fini de lignes. On peut à volonté rajouter une nouvelle ligne mais cela n'a pas de sens de vouloir aller à l'infini. Ainsi, cette pseudo définition n'est jamais achevée, ce qui présente une forte analogie avec les suites de choix de Brouwer. Suivant Martin-Löf, on convient que les axiomes nonstandard constituent en eux-même une nouvelle forme de suite de choix. Au prix d'une légère confusion<fnref n="18" />, cette suite de choix peut être identifié au nombre $\infty$.

L'intuition liée à la fois à la pseudo définition (7) et aux axiomes nonstandard est la suivante. Au début du processus définitionnel, $\infty$ est égal à $\infty_0$ et on ne sait rien de plus sur ce dernier sinon que c'est un nombre naturel. Sur cette seule base, $\infty_0$ est assimilable à une variable à valeurs dans $\mathbb{N}$. A la question de savoir ce qu'est cet élément $\infty_0$, on répond à l'étape suivante du processus en apportant une information supplémentaire mais incomplète, à savoir que $\infty_0 = S(\infty_1)$ où $\infty_1$ est un élément non déterminé de $\mathbb{N}$, c'est-à-dire assimilable à une variable à valeurs dans $\mathbb{N}$. On poursuit à l'étape suivante en posant

<footnote n="18">18. En tant que telle, la suite de choix est externe à la théorie $\mathcal{T}_\infty$ alors que le nombre $\infty$ est lui un objet légitime de $\mathcal{T}_\infty$.</footnote>
que $\infty_1 = S(\infty_2)$ où $\infty_2$ à son tour joue le rôle d'une variable à valeur dans $\mathbb{N}$, ce qui, ramené au niveau de $\infty$, donne la précision $\infty = S(S(\infty_2))$ avec $\infty_2 \in \mathbb{N}$ et ainsi de suite.

Remarquons que la suite $(\infty_i)$ est externe à la théorie $T_\infty$ : ce n'est pas un objet fonctionnel bien formé de la théorie des types nonstandard. D'ailleurs, si l'on suppose qu'il existe une suite $(\omega_n)_{n:\mathbb{N}}$ satisfaisant les jugements $\omega_n : \mathbb{N}$ et $\omega_n = S(\omega_{S(n)}) : \mathbb{N}$, on aboutit à une contradiction. En effet, on pourrait en déduire par récurrence que $\omega_0 = \omega_n + n$ est vraie pour tout entier $n$ ; en prenant pour $n$ le nombre $\omega_0 + 1$, on obtiendrait $\omega_0 = \omega_n \omega_{\omega_0+1} + \omega_0 + 1$ d'où $0 = \omega_n S(\omega_{\omega_0+1})$, ce qui montrerait que $0$ est égal au successeur d'un nombre naturel.

# 4. Voisinages, élimination de la suite de choix et principe de transfert

## 4.1. Voisinage et constante dominante

Tout jugement dans $T_\infty$ est basé sur les règles de cette théorie et chacune de ces règles n'est appliquée qu'un nombre fini de fois dans la démonstration de ce jugement. Dans la perspective de comprendre plus précisément la forme d'un tel jugement, il est important de considérer les différentes occurrences des axiomes nonstandard qui sont alors utilisées. Cela conduit à la notion suivante de voisinage<fnref n="19" />.

**Définition 1.** *Un voisinage U désigne un nombre fini d'informations de la forme (5) or (6) provenant d'un nombre fini d'application des axiomes nonstandard. Il est implicitement supposé que chaque déclaration de la forme (6) est précédée par les deux déclarations de la forme (5) qui introduisent les deux constantes nonstandard qui y sont impliquées.*

*Un voisinage V est plus fin qu'un voisinage U si les informations contenues dans U sont aussi dans V.*

*Le voisinage plein $U_f$ est le voisinage ne contenant aucune information. Tout autre voisinage est plus fin que $U_f$.*

Ainsi, tout voisinage $U$ est de la forme

$$ \begin{cases} \infty_{i_1} : \mathbb{N}, \dots, \infty_{i_n} : \mathbb{N} \\ \infty_{j_1} = S(\infty_{S(j_1)}) : \mathbb{N}, \dots, \infty_{j_m} = S(\infty_{S(j_m)}) : \mathbb{N} \end{cases} \quad (8) $$

où $i_1, \dots, i_n, j_1, \dots, j_m$ sont des nombres naturels standard et toutes les constantes non-standard qui apparaissent dans la seconde ligne sont déclarées dans la première. Enfin, il faut noter qu'un voisinage est totalement explicite : c'est une énumération concrète d'in-

<footnote n="19">19. L'usage de ce terme issu de la topologie provient d'un lien existant avec le concept général de topologie de Grothendieck qu'il n'est pas nécessaire de développer ici.</footnote>
formations. En particulier, la série de trois petits points utilisées dans la description (8) ne cache pas une forme d'induction abstraite.

**Définition 2.** Une constante nonstandard $\infty_i$ introduite dans un voisinage $U$ est appelée une constante dominante dans $U$ si et seulement si la seule condition qui lui est imposée dans $U$ est la contrainte de type $(\infty_i : \mathbb{N})$.

Ainsi, une constante dominante $\infty_i$ dans $U$ n'est pas l'une des constantes $\infty_{j_i}$ pour un $l = 1, \dots, m$ mentionnées dans la deuxième ligne de (8). Cela signifie que, en s'en tenant à l'information donnée dans $U$, cette constante $\infty_i$ n'est pas définitionnellement égale à $S(\infty_{S(i)})$.

Au contraire, une constante $\infty_j$ qui n'est pas dominante dans $U$ est jointe à une unique constante dominante $\infty_{S^k(j)}$ par une unique chaîne d'égalités définitionnelles introduite dans $U$ :

$$ \begin{array}{l} \infty_j = S(\infty_{S(j)}) : \mathbb{N}, \quad \infty_{S(j)} = S(\infty_{S^2(j)}) : \mathbb{N}, \dots \\ \qquad \dots, \quad \infty_{S^{k-1}(j)} = S(\infty_{S^k(j)}) : \mathbb{N} \end{array} $$

où $k$ est la longueur de la chaîne. Il en découle que cette constante $\infty_j$ est reliée à la constante dominante $\infty_{S^k(j)}$ par l'égalité définitionnelle

$$ \infty_j = S^k(\infty_{S^k(j)}) : \mathbb{N} \qquad (9) $$

## 4.2. Forme générale d'un jugement dans $\mathcal{T}_\infty$

Comme les axiomes nonstandard n'ajoutent pas de nouvelles formes de jugements, on voit que, dans $\mathcal{T}_\infty$, il y a seulement quatre formes de jugement qui sont mêmes que dans $\mathcal{T}$. De plus, à chaque jugement $\mathcal{J}$ de $\mathcal{T}_\infty$ on peut associer un voisinage $U$ dans lequel sont archivées les différentes occurrences des axiomes nonstandard utilisés dans la démonstration de $\mathcal{J}$. Cette relation entre un jugement et un voisinage est notée

$$ U \Vdash \mathcal{J} $$

et l'on dit que le voisinage $U$ force le jugement $\mathcal{J}$. Il en découle que chaque jugement dans $\mathcal{T}_\infty$ est de l'une des formes suivantes :

1) $(U \Vdash A)$ type.

2) $(U \Vdash A = B)$ type.

3) $(U \Vdash a : A)$ sachant que $(A)$ type.

4) $(U \Vdash a = b : A)$ sachant que $(A)$ type, $(a : A)$ et $(b : A)$.

où $U$ est un voisinage qui force le jugement en question. Remarquons que ce voisinage n'est pas unique. Par exemple, si $U \Vdash \mathcal{J}$ et si $V$ est un voisinage plus fin que $U$, alors $V \Vdash \mathcal{J}$. Cependant, tout jugement est produit par une dérivation, et cette dérivation met
en évidence explicitement un certain voisinage qui force le jugement considéré. Si la déduction d'un jugement $\mathcal{J}$ se fait sans utiliser les axiomes nonstandard, on peut considérer qu'il est forcé par le voisinage plein et écrire $U_f \Vdash \mathcal{J}$. Dans ce cas, $\mathcal{J}$ est aussi un jugement dérivable dans la théorie standard des types $\mathcal{T}$ et on dit que c'est un jugement standard.

Finalement, la situation la plus générale est celle d'un jugement dépendant d'un certain contexte, ce qui donne la forme la plus générale d'un jugement dans $\mathcal{T}_\infty$

$$ \Gamma \vdash (U \Vdash (\Delta \vdash \mathcal{J})) $$

où $\Gamma$ est un contexte standard (indépendant des axiomes nonstandard), $U$ est un voisinage qui indique les axiomes nonstandard utilisées dans la déduction du jugement, $\Delta$ est un context nonstandard (dépendant du voisinage $U$) et où $\vdash$ indique la dérivation utilisant seulement les règles standard de la théorie des types.

### 4.3. Elimination de la suite de choix

Dans [8] est évoquée sur un exemple simple une élimination de la suite de choix permettant d'associer à un jugement nonstandard un jugement standard qui lui est intimement lié. Voici une description d'une opération générale systématisant cette idée.

Soit $(U \Vdash \mathcal{J})$ un jugement dans $\mathcal{T}_\infty$ qui est forcé par un voisinage $U$. On va analyser le rôle dans la démonstration de $\mathcal{J}$ des constantes nonstandard archivées dans $U$ :

- Chaque constante $\infty_j$ qui n'est pas dominante pourrait tout autant être remplacée par une expression en fonction d'une constante dominante $\infty_{S^k(j)}$ en vertu de l'égalité définitionnelle (9).

- Chaque constante dominante $\infty_i$ est seulement soumise à la contrainte de type $\infty_i : \mathbb{N}$. En conséquence, son rôle dans la démonstration considérée est analogue à celui d'une variable $(x_i : \mathbb{N})$.

En conséquence, on considère la transformation opérant sur la forme linguistique de la démonstration de $\mathcal{J}$ (y compris $\mathcal{J}$) résultant des étapes suivantes :

1. On remplace chaque constante non dominante par l'expression en fonction d'une constante dominante décrite dans (9).

2. Supposons que les constantes dominantes soient

$$ \infty_{i_1}, \dots, \infty_{i_r} \qquad (10) $$

avec un ordre d'énumération fixé. Alors, pour chaque $k = 1, \dots, r$, on remplace la constante dominante $\infty_{i_k}$ par une variable $x_k$ soumise à la contrainte $(x_k : \mathbb{N})$. En procédant ainsi, on obtient la démonstration (standard, c'est-à-dire dans $\mathcal{T}$) d'un jugement $\mathcal{J}'$ dans $\mathcal{T}$, jugement qui est dépendant du contexte standard

$$ [x_1 : \mathbb{N}, \dots, x_r : \mathbb{N}] \qquad (11) $$
Réciproquement, du jugement standard dépendant $\mathcal{J}'$ on peut déduire le jugement non-standard initial $\mathcal{J}$ en remplaçant $x_k$ par $\infty_{i_k}$ pour $k = 1, \dots, r$. La transformation pré-cédente qui fait passer de $\mathcal{J}$ à $\mathcal{J}'$ est appelée l'élimination de la suite de choix dans un jugement forcé par un voisinage $U$. Voici à titre d'exemples ce que donne cette opération sur certaines formes de jugements. Tous les autres cas se traitent de manière analogue.

On suppose que $U$ est un voisinage dont les constantes dominantes sont notées comme dans (10).

1) L'élimination de la suite de choix dans un jugement

$$ U \Vdash A \text{ type} \qquad (12) $$

donne un jugement standard dépendant

$$ A'(x_1, \dots, x_r) \text{ type } [x_1 : \mathbb{N}, \dots, x_r : \mathbb{N}] \qquad (13) $$

qui est tel que

$$ A = A'(\infty_{i_1}, \dots, \infty_{i_r}) \text{ type} \qquad (14) $$

2) On suppose que l'on a le jugement ($U \Vdash A$ type) et que le résultat de l'élimination de la suite de choix sur ce jugement est noté comme dans (13) et (14). Alors, l'élimination de la suite de choix dans un jugement

$$ U \Vdash a : A $$

(forcé par le même voisinage $U$) donne un jugement standard dépendant

$$ a'(x_1, \dots, x_r) : A'(x_1, \dots, x_r) [x_1 : \mathbb{N}, \dots, x_r : \mathbb{N}] \qquad (15) $$

tel que

$$ a = a'(\infty_{i_1}, \dots, \infty_{i_r}) : A \qquad (16) $$

3) On suppose que l'on a un type standard $A$, autrement dit que ($A$ type) est un jugement dans $\mathcal{T}$. Alors, l'élimination de la suite de choix dans un jugement

$$ U \Vdash a : A $$

donne un jugement standard dépendant

$$ a'(x_1, \dots, x_r) : A [x_1 : \mathbb{N}, \dots, x_r : \mathbb{N}] \qquad (17) $$

tel que

$$ a = a'(\infty_{i_1}, \dots, \infty_{i_r}) : A \qquad (18) $$

Bien entendu, le résultat de l'élimination de la suite de choix dépend du voisinage $U$ choisi. Si dans l'un des deux résultats précédents, on remplace $U$ par un voisinage $V$ plus fin, il suffit de remplacer les constantes dominantes dans $U$ par leurs expressions en fonction des constantes dominantes dans $V$ pour obtenir une forme équivalente à celle donnée par l'élimination dans $U$.
### 4.4. Un principe de transfert

Dans cette sous-section, on énonce et justifie un résultat sur $\mathcal{T}_\infty$ qui est relativement proche du principe de transfert de l'analyse nonstandard usuelle.

**Théorème 1.** Soit A une proposition standard, c'est-à-dire telle que (A prop) est un jugement dérivable dans la théorie standard T. Alors, A est vraie dans T si et seulement si A est vraie dans $\mathcal{T}_\infty$.

*Preuve du théorème.*

(1.) Supposons que A soit vraie dans T. Cela signifie que l'on sait construire un objet-preuve de A dans T, ce qui revient à dire que l'on a un jugement ($p : A$) dérivable dans T. Puisque $\mathcal{T}_\infty$ est une extension de T, le jugement ($p : A$) est dérivable pareillement dans $\mathcal{T}_\infty$. Donc, $p$ est un objet-preuve de A dans $\mathcal{T}_\infty$, ce qui revient à dire que A est vraie dans $\mathcal{T}_\infty$.

(2.) Supposons maintenant que A soit vraie dans $\mathcal{T}_\infty$. Cela signifie que A possède un objet-preuve $a$ dans $\mathcal{T}_\infty$. Donc, on a le jugement ($a : A$) dans $\mathcal{T}_\infty$ et ce jugement est forcé par un certain voisinage $U$. On suppose que les constantes dominantes de $U$ sont notées comme dans (10). En procédant à l'élimination de la suite de choix sur le jugement $(U \Vdash a : A)$, on obtient un jugement standard dépendant

$$a'(x_1, \dots, x_r) : A \ [x_1 : \mathbb{N}, \dots, x_r : \mathbb{N}] \qquad (19)$$

tel que

$$a = a'(\infty_{i_1}, \dots, \infty_{i_r}) : A$$

De (19) on déduit le jugement standard

$$a'(0, \dots, 0) : A$$

ce qui montre que A est vraie dans T.

□

Il est intéressant de remarquer que c'est l'utilisation des objets-preuves dans $\mathcal{T}$ et $\mathcal{T}_\infty$ qui permet d'obtenir une justification aussi simple et claire de ce principe de transfert. Ce résultat est généralisable sous la forme suivante qui présente une certaine analogie avec le principe de transfert de la théorie IST.

**Corollaire 1.** On considère dans $\mathcal{T}$ un contexte

$C_1$ type

$C_2(x_1)$ type $[x_1 : C_1]$

$\vdots$

$C_n(x_1, \dots, x_{n-1})$ type $[x_1 : C_1, \dots, x_{n-1} : C_{n-1}(x_1, \dots, x_{n-2})]$

et une proposition standard dépendant de ce contexte

$A(x_1, \dots, x_n)$ prop $[x_1 : C_1, x_2 : C_2(x_1), \dots, x_n : C_n(x_1, \dots, x_{n-1})]$
Etant donnés des objets standard $a_1, \dots, a_n$ tels que

$$a_1 : C_1, a_2 : C_2(a_1), \dots, a_n : C_n(a_1, \dots, a_{n-1})$$

alors, la proposition $A(a_1, \dots, a_n)$ est vraie dans $\mathcal{T}$ si et seulement si elle est vraie dans $\mathcal{T}_\infty$.

La preuve en est immédiate car, la proposition $A(a_1, \dots, a_n)$ est standard sous les hypothèses de l'énoncé, et on peut donc lui appliquer le principe de transfert précédent.

## 5. Sur l'égalité de $\infty_i$ et $S^k(\infty_{S^k(i)})$

On a vu dans la sous-section 4.1 que dans un voisinage donné, une constante non dominante $\infty_i$ est reliée à une constante dominante $\infty_{S^k(i)}$ par une égalité définitionnelle ($\infty_i = S^k(\infty_{S^k(i)}) : \mathbb{N}$) qui s'est révélée cruciale pour l'étude de la forme des jugements de $\mathcal{T}_\infty$. On peut être tenté de penser que $\infty_i$ est définitionnellement égal à $S^k(\infty_{S^k(i)})$ quelque soit l'entier naturel standard $k$. Il est intéressant d'aller y voir de plus près, d'autant plus que ce point est un nœud délicat pour la suite de ce travail. L'étude qui suit a pour objet d'analyser finement pour quel entier naturel standard $k$ on obtient une telle égalité.

Etant donné un entier naturel standard $i$, on peut construire pas à pas le tableau suivant dans lequel la première colonne liste les occurrences successives de l'axiome ANS 1, la seconde colonne les occurrences successives de ANS 2 et la troisième colonne les égalités successives de la forme ($\infty_i = S^k(\infty_{S^k(i)}) : \mathbb{N}$) que l'on peut en déduire :

$$ \begin{array}{l@{\quad}l@{\quad}l} \infty_i : \mathbb{N} & , & \infty_i = S^0(\infty_{S^0(i)}) : \mathbb{N} \\ \infty_{S^1(i)} : \mathbb{N} & , & \infty_i = S(\infty_{S(i)}) : \mathbb{N} \\ \infty_{S^2(i)} : \mathbb{N} & , & \infty_{S(i)} = S(\infty_{S^2(i)}) : \mathbb{N} \\ \infty_{S^3(i)} : \mathbb{N} & , & \infty_{S^2(i)} = S(\infty_{S^3(i)}) : \mathbb{N} \\ \dots & \dots & \dots \end{array} \quad (20) $$

Pour obtenir l'égalité définitionnelle de $\infty_i$ et $S^k(\infty_{S^k(i)})$, on voit en observant (20), qu'un entier $k$ convenable est obtenu en comptant les occurrences de ANS 2 dans la deuxième colonnes jusqu'à la ligne souhaitée. De plus, compter ces occurrences signifie exactement que l'on construit ce nombre $k$ en même temps que l'on parcourt cette colonne : on part de la valeur initiale 0, puis on associe à l'égalité $\infty_i = S(\infty_{S(i)}) : \mathbb{N}$ le nombre $S(0)$, et on poursuit en associant à chaque nouvelle égalité rencontrée le successeur du nombre associé à l'égalité précédente. Lorsque l'on s'arrête, on a construit un entier naturel $k$ qui compte le nombre de symboles $S$ contigus (séparés par des parenthèses ouvrantes) qui apparaissent dans l'expression finale du nombre $k$

$$k = S(S(\dots S(0))) : \mathbb{N} \quad (21)$$
ainsi que dans l'égalité définitionnelle terminale (deux fois)

$$ \infty_i = S(S(\dots S(\infty_{S(S(...S(i)))))) : \mathbb{N} \qquad (22) $$

On convient d'appeler numérique explicite un entier naturel *k* satisfaisant une égalité définitionnelle de la forme (21).

En reproduisant le même assemblage de symboles *S* et de parenthèses que dans (21), on pose

$$ S^k(x) = S(S(\dots S(x))) : \mathbb{N} \ [x : \mathbb{N}]. \qquad (23) $$

Comme c'est l'habitude, on généralise cette écriture en définissant par induction sur *n* : $\mathbb{N}$ un objet dépendant

$$ S^n(x) : \mathbb{N} \ [x : \mathbb{N}, n : \mathbb{N}] $$

qui est tel que l'on a les égalités définitionnelles

$$ S^0(x) = x : \mathbb{N} \text{ et } S^{n+1}(x) = S(S^n(x)) : \mathbb{N} \ [x : \mathbb{N}, n : \mathbb{N}]. \qquad (24) $$

Cela devrait permettre de se débarrasser de l'encombrant assemblage de symboles *S* et de parenthèses dans (21) et (22) à condition de vérifier à chaque fois que le processus qui génère cet assemblage est compatible avec (24). C'est bien le cas pour l'assemblage qui apparaît dans (21) et celui qui est en indice du symbole $\infty$ dans (22). Mais cela n'est plus le cas pour l'assemblage qui est immédiatement à droite du signe = dans (22). En effet, si on écrit l'égalité (22) sous la forme $(\infty_i = S^{\{k\}}(\infty_{S^k(x)}) : \mathbb{N})$ pour un certain *k*, on déduit de ANS 2 que $(\infty_i = S^{\{k\}}(S(\infty_{S(S^k(x))})) : \mathbb{N})$. Cela amène à introduire un nouvel objet dépendant

$$ S^{\{n\}}(x) : \mathbb{N} \ [x : \mathbb{N}, n : \mathbb{N}] $$

qui est tel que l'on a les égalités définitionnelles

$$ S^{\{0\}}(x) = x : \mathbb{N} \text{ et } S^{\{n+1\}}(x) = S^{\{n\}}(S(x)) : \mathbb{N} \ [x : \mathbb{N}, n : \mathbb{N}]. \qquad (25) $$

La situation est un peu subtile car les objets dépendants $S^n(x)$ et $S^{\{n\}}(x)$ sont : 1) définitionnellement différents dans le contexte général $[x : \mathbb{N}, n : \mathbb{N}]$ puisqu'ils sont générés par des inductions différentes, 2) définitionnellement égaux lorsque *n* est défini explicite-ment comme *k* dans (21) car ils se réduisent alors à la même suite explicite de symboles comme dans (23) du fait de l'application des règles de calcul (24) et (25). De plus, on peut montrer qu'ils sont propositionnellement égaux pour tout *n*. Pour résumer, on peut se passer d'opérer la distinction entre $S^n(x)$ et $S^{\{n\}}(x)$ dans le cas où l'exposant *n* est un numérique explicite mais cette distinction peut devenir indispensable lorsque ce n'est pas le cas.

Compte tenu de ce tout qui précède, on peut réécrire (21)

$$ k = S^k(0) : \mathbb{N} \qquad (26) $$
et (22) sous la forme<fnref n="20" />

$$ \infty_i = S^{\{k\}}(\infty_{S^k(i)}) : \mathbb{N}. \qquad (27) $$

D'après ce qui précède, si $k$ est un numéral explicite, alors $k$ est non dépendant et il satisfait une égalité définitionnelle de la forme (26). En considérant la sémantique du récurseur natrec sur $\mathbb{N}$, on peut estimer qu'inversement, si $k$ est un entier naturel non dépendant qui de plus satisfait une égalité définitionnelle (26), alors $k$ est un numéral explicite et on a (27). En effet, le sens de ce récurseur est que le programme récursif qui calcule $S^k(0)$ se termine en produisant la forme explicite attendue.

# 6. Une forme de standardisation

Dans toute cette section, on considère une proposition nonstandard $A$ introduite par le jugement dans la théorie $\mathcal{T}_\infty$

$$ A \text{ prop} \qquad (28) $$

forcé par un certain voisinage $U$ dont les constantes dominantes sont $\infty_{i_1}, \dots, \infty_{i_m}$. L'élimination de la suite de choix dans ce jugement donne un jugement standard dépendant

$$ A'(x_1, \dots, x_m) \text{ prop } [x_1 : \mathbb{N}, \dots, x_m : \mathbb{N}] \qquad (29) $$

suivi du jugement nonstandard

$$ A = A'(\infty_{i_1}, \dots, \infty_{i_m}) \text{ prop} \qquad (30) $$

## 6.1. Vérité d'une proposition nonstandard

On se propose maintenant d'explicitier à quelle condition cette proposition nonstandard $A$ est vraie. C'est l'objet du résultat suivant.

**Théorème 2.** Sous les hypothèses et notations introduites ci-dessus, la proposition non-standard $A$ est vraie si et seulement s'il existe $m$ numéraux explicites<fnref n="21" /> $k_1, \dots, k_m$ dans $\mathcal{T}$ et un objet dépendant standard

$$ q(x_1, \dots, x_m) : A'(S^{\{k_1\}}(x_1), \dots, S^{\{k_m\}}(x_m)) [x_1 : \mathbb{N}, \dots, x_m : \mathbb{N}] \qquad (31) $$

*Démonstration.* Supposons donc que la proposition $A$ soit vraie : cela signifie que l'on peut dériver dans $\mathcal{T}_\infty$ un jugement

$$ p : A \qquad (32) $$

qui est forcé par un voisinage $V$ plus fin que $U$ dont les constants dominantes sont $\infty_{i'_1}, \dots, \infty_{i'_n}$. Pour chaque $s = 1, \dots, m$, il existe un unique $t_s$ dans $\{1, \dots, n\}$ tel

<footnote n="20">20. Dans laquelle on peut remplacer $S^{\{k\}}$ par $S^k$ puisque $k$ est par construction un numéral explicite.</footnote>

<footnote n="21">21. Voir la définition donnée après les égalité (21) et (22) et le paragraphe après l'égalité (27).</footnote>
que $\infty_{i_s}$ est relié à $\infty_{i'_{t_s}}$ par une chaîne de $k_s$ égalités définitionnelles dans V avec de plus $i'_{t_s}$ et $S^{\{k_s\}}(i_s)$ identiques. Par composition, on obtient l'égalité définitionnelle

$$ \infty_{i_s} = S^{\{k_s\}}(\infty_{S^{k_s}(i_s)}) : \mathbb{N} $$

si bien que l'on déduit de (30)

$$ A = A'\left(S^{\{k_1\}}(\infty_{S^{k_1}(i_1)}), \dots, S^{\{k_m\}}(\infty_{S^{k_m}(i_m)})\right) : \text{Prop} \quad (33) $$

Donc, l'élimination de la suite de choix dans le jugement (32) forcé par V fournit un jugement standard dépendant

$$ p'(x_1, \dots, x_n) : A'(S^{\{k_1\}}(x_{t_1}), \dots, S^{\{k_m\}}(x_{t_m})) [x_1 : \mathbb{N}, \dots, x_n : \mathbb{N}] \quad (34) $$

tel que

$$ p = p'(\infty_{i'_1}, \dots, \infty_{i'_n}) : A \quad (35) $$

On remarque que dans (34), l'objet $p'$ est donné comme dépendant d'un ensemble de variables $\{x_1, \dots, x_n\}$ qui contient généralement strictement l'ensemble de variables $\{x_{t_1}, \dots, x_{t_m}\}$ dont dépend la proposition. On effectue alors la transformation suivante : dans l'expression $p'(x_1, \dots, x_n)$, on attribue la valeur entière 0 à chaque variable $x_k$ qui n'appartient pas à $\{t_1, \dots, t_m\}$. Cela transforme $p'$ en un nouvel objet dépendant $q$

$$ q(x_{t_1}, \dots, x_{t_m}) : A'(S^{\{k_1\}}(x_{t_1}), \dots, S^{\{k_m\}}(x_{t_m})) [x_{t_1} : \mathbb{N}, \dots, x_{t_m} : \mathbb{N}] \quad (36) $$

ce qui montre que la condition de l'énoncé est bien nécessaire.

Supposons maintenant qu'il existe $m$ numéraux explicites $k_1, \dots, k_m$ et un objet dépendant standard $q$ satisfaisant (31). Alors, les axiomes nonstandard nous permettent d'introduire les constantes $\infty_{S^{k_1}(i_1)}, \dots, \infty_{S^{k_m}(i_m)}$, ce qui donne

$$ q(\infty_{S^{k_1}(i_1)}, \dots, \infty_{S^{k_m}(i_m)}) : A'(S^{\{k_1\}}(\infty_{S^{k_1}(i_1)}), \dots, S^{\{k_m\}}(\infty_{S^{k_m}(i_m)})) \quad (37) $$

Comme les entiers $k_1, \dots, k_m$ sont des numéraux explicites, on a les égalités définitionnelles $(\infty_{i_s} = S^{\{k_s\}}(\infty_{S^{k_s}(i_s)}) : \mathbb{N})$ pour $s : 1, \dots, m$. D'après (30) et (37) il vient

$$ q(\infty_{S^{k_1}(i_1)}, \dots, \infty_{S^{k_m}(i_m)}) : A $$

ce qui montre que la proposition A est vraie.

<figure><img src="image_2.png" /></figure>
## 6.2. Standardisation d'une proposition nonstandard

A nouveau, on considère notre proposition nonstandard A et le voisinage U forçant le jugement (A : Prop). Le théorème 2 conduit à considérer une proposition standard qui est une tentative<fnref n="22" /> de transcription formelle de l'éventuelle vérité de A.

**Définition 3.** La standardisation<fnref n="23" /> de la proposition A forcée par U est la proposition standard suivante

$$ (\exists k_1 : \mathbb{N}) \dots (\exists k_m : \mathbb{N}) (\forall x_1 : \mathbb{N}) \dots (\forall x_m : \mathbb{N}) A'\left(S^{\{k_1\}}(x_1), \dots, S^{\{k_m\}}(x_m)\right) \quad (38) $$
dépendant de A et de U, que l'on note $\langle A, U \rangle$.

Dans l'expression de la proposition $\langle A, U \rangle$, il n'est pas indifférent d'utiliser les expressions $S^{\{k_s\}}(x)$ ou $S^{k_s}(x)$ pour $s = 1, \dots, m$. En effet, loin d'être un numéral explique, chaque $k_s$ est une variable à valeur entière sous le champ d'un quantificateur. Voici maintenant un théorème qui peut être vu comme une forme faible de transfert entre une proposition nonstandard et sa standardisée. Ce résultat se place sous les hypothèses et conditions données au début de la section 6 ; néanmoins, pour faciliter la compréhension de l'énoncé, les données principales sont précisées à nouveau.

**Théorème 3.** On considère une proposition nonstandard A telle que le jugement (A : Prop) est forcé par un voisinage U et on note $\langle A, U \rangle$ la standardisée de A forcée par U. Alors :

1) À tout objet nonstandard a tel que le jugement (a : A) est forcé par un voisinage V plus fin que U, on peut associer la construction d'un objet standard $\langle a, U, V \rangle$ satisfaisant le jugement standard ($\langle a, U, V \rangle : \langle A, U \rangle$).

2) À tout objet b standard satisfaisant le jugement (b : $\langle A, U \rangle$), on peut associer la construction de m entiers naturels standard $l_1, \dots, l_m$, d'un voisinage W plus fin que U et d'un objet nonstandard $\uparrow b$ de sorte que

$$ \uparrow b : A'\left(S^{\{l_1\}}(\infty_{S^{l_1}(i_1)}), \dots, S^{\{l_m\}}(\infty_{S^{l_m}(i_m)})\right) \quad (39) $$

La comparaison de (30) et de (39) montre que les propositions nonstandard A et $A'(S^{\{l_1\}}(\infty_{S^{l_1}(i_1)}), \dots, S^{\{l_m\}}(\infty_{S^{l_m}(i_m)}))$ sont "proches" au sens où elles sont identiques lorsque $l_1, \dots, l_m$ sont des numéraux explicites. Evidemment, cette condition est

<footnote n="22">22. Cette tentative n'est pas parfaite car elle ne capte pas la condition imposée aux entiers $k_1, \dots, k_m$ d'être des numéraux explicites. Ce point n'est pas anodin car il explique en parti que la standardisation et la notion de proposition externe n'apporteront pas une totale satisfaction.</footnote>

<footnote n="23">23. Les connaisseurs de la théorie IST d'E. Nelson peuvent noter que la notion de standardisation présentée ici semble sans rapport avec celle qui s'exprime dans le principe de standardisation postulé dans IST.</footnote>
loin d'être vérifiée en général. On ne peut donc pas lire ce théorème comme énonçant que A est vraie si et seulement si $\langle A, U \rangle$ est vraie. Ce qui est avéré est que la vérité de A implique celle de $\langle A, U \rangle$. La réciproque n'est pas démontrée, sinon sous une forme faible.

### Démonstration.

Supposons que l'on connaisse un jugement $(a : A)$ forcé par un voisinage $V$ plus fin que $U$. Reprenant l'analyse développée dans la démonstration du théorème 2, on voit que l'objet standard $\langle a, U, V \rangle$ défini par

$$ \langle a, U, V \rangle =_{\text{def}} (k_1, (\dots, k_m, ((\lambda x_1)\dots(\lambda x_m)p''(x_1, \dots, x_m))\dots)) \quad (40) $$

est tel que $(\langle a, U, V \rangle : \langle A, U \rangle)$.

Réciproquement, supposons que l'on connaisse un jugement $(b : \langle A, U \rangle)$. A partir de $b$ et en utilisant un certain nombre de fois les projections d'un $\Sigma$-ensemble, on obtient $m$ nombres $l_1, \dots, l_m : \mathbb{N}$ et une fonction

$$ F : \left( \prod x_1 : \mathbb{N} \right) \dots \left( \prod x_m : \mathbb{N} \right) A' \left( S^{\{l_1\}}(x_1), \dots, S^{\{l_m\}}(x_m) \right) \quad (41) $$

L'axiome ANS 1 permet d'introduire les constantes $\infty_{S^{l_s}(i_s)}$ pour $s = 1, \dots, m$, et on peut définir l'objet

$$ \uparrow b =_{\text{def}} \text{apply}(\dots \text{apply}(\text{apply}(F, \infty_{S^{l_1}(i_1)}), \infty_{S^{l_2}(i_2)}), \dots, \infty_{S^{l_m}(i_m)}) \\ : A'(S^{\{l_1\}}(\infty_{S^{l_1}(i_1)}), \dots, S^{\{l_m\}}(\infty_{S^{l_m}(i_m)})) \quad (42) $$

ce qui constitue le jugement nonstandard (39). Ce jugement est clairement forcé par le voisinage $W$ obtenu en rajoutant dans le voisinage $U$ les constantes $S^{l_s}(\infty_{S^{l_s}(i_s)})$ pour $s = 1, \dots, m$. $\square$

# 7. Conclusion : vers une notion de proposition externe

## 7.1. Les propriétés externes de l'analyse nonstandard

L'un des intérêts majeurs de l'analyse nonstandard est d'introduire des propriétés externes qui permettent de formuler des critères simplifiés pour les diverses notions de convergence en analyse. Par exemple, une suite standard de nombres réels $(u_k)$ converge vers un nombre réel standard $a$ si et seulement si on peut déduire de $(k \approx +\infty)$ la propriété $(u_k \approx a)$

Dans cette conclusion, on examine un exemple particulier de propriété externe. Cependant, la procédure suivie pourrait s'appliquer à la plupart des propriétés externes de l'analyse nonstandard. La question posée est de savoir s'il est possible de définir dans le cadre
de $\mathcal{T}_\infty$ un équivalent de la propriété "être un entier infiniment grand" notée $(\nu \simeq +\infty)$ sur $\mathbb{N}$. Dans la théorie IST, cette propriété est définie par la formule

$$ (\nu \simeq +\infty) =_{\text{def}} (\forall n \in \mathbb{N}) (\text{st}(n) \implies (n \le \nu)) \quad (43) $$

où "st" désigne le prédicat "standard" introduit dans les fondements de IST pour qualifier les objets standard. Cette formule est dite externe car elle utilise ce prédicat qui est extérieur à la théorie ZFC. Bien entendu, il n'est pas possible dans notre cadre de reprendre la définition (43) car nous ne disposons pas d'un proposition analogue au prédicat "st" de IST. Pour contourner cette difficulté, on va adapter à la situation du présent texte l'argument esquissé par Martin-Löf dans [8]. Son idée est de standardiser la proposition nonstandard $(n \le \nu)$ puis de procéder à une quantification universelle sur la variable $n$. C'est ce qui va être fait dans la suite du texte. On verra aussi que cette solution astucieuse n'apporte pas une totale satisfaction.

## 7.2. La proposition externe $(\nu \simeq +\infty)_U$

Etant donnés deux nombres entiers naturels $n$ et $\nu$ dans $\mathcal{T}_\infty$ tels que $n$ soit standard, on considère la proposition $(n \le \nu)$ identifiée à $(\exists x : \mathbb{N})(n + x =_{\mathbb{N}} \nu)^{24}$. Le jugement nonstandard $(\nu : \mathbb{N})$ est forcé par un certain voisinage $U$ dont les constantes dominantes sont $\infty_{i_1}, \dots, \infty_{i_m}$ de sorte que l'élimination de la suite de choix sur ce jugement forcé par $U$ donne un entier standard dépendant

$$ N(x_1, \dots, x_m) : \mathbb{N} [x_1 : \mathbb{N}, \dots, x_m : \mathbb{N}] $$

tel que $(\nu = N(\infty_{i_1}, \dots, \infty_{i_m}) : \mathbb{N})$. On en déduit que le même voisinage $U$ force le jugement $((n \le \nu) \text{ prop})$ et que l'élimination de la suite de choix dans ce dernier jugement forcé par $U$ fournit la proposition standard dépendante

$$ (n \le N(x_1, \dots, x_m)) \text{ prop } [x_1 : \mathbb{N}, \dots, x_m : \mathbb{N}] $$

de sorte que $(n \le \nu)$ soit définitionnellement égal à $(n \le N(\infty_{i_1}, \dots, \infty_{i_m}))$. Cela permet de construire la proposition standard $\langle (n \le \nu), U \rangle$ puis de poser la définition

$$ (\nu \simeq +\infty)_U = (\forall n : \mathbb{N}) \langle (n \le \nu), U \rangle \text{ prop} \quad (44) $$

dont on peut vérifier qu'elle se développe sous la forme

$$ (\forall n : \mathbb{N})(\exists l_1 : \mathbb{N}) \dots (\exists l_m : \mathbb{N})(\forall x_1 : \mathbb{N}) \dots (\forall x_m : \mathbb{N}) \left( n \le N(S^{\{l_1\}}(x_1), \dots, S^{\{l_m\}}(x_m)) \right) \quad (45) $$

<footnote n="24">24. Dans ce travail, la définition précise de cette proposition n'a pas un rôle cruciale. Dans ([8]) Martin-Löf utilise une définition différente de l'ordre sur $\mathbb{N}$ qui est vue comme un type inductif d'ordre supérieur. Cette nouvelle définition permet de disposer d'une intéressante notion de système projectif définitionnel qu'il n'est pas nécessaire d'utiliser dans ce travail.</footnote>
Intuitivement, cette proposition est vraie dans le cas où $N(x_1, \dots, x_m)$ converge vers $+\infty$ lorsque chacune de ses variable tend vers $+\infty$<sup>25</sup>. Clairement la proposition $(\nu \simeq +\infty)_U$ est standard. Néanmoins, on peut la qualifier de proposition externe relativement à sa dépendance en $\nu$. En effet, $(\nu \simeq +\infty)_U$ n'est pas une proposition dépendant au sens habituel de la variable $\nu$: elle dépend aussi fortement du choix d'un voisinage forçant le jugement $(\nu : \mathbb{N})$. Lorsque l'on change de voisinage $U$ et lorsque l'on change d'entier nonstandard $\nu$, on change aussi substantiellement la forme même de la proposition $(\nu \simeq +\infty)_U$. De nombreux points restent à éclaircir relativement à cette notion de proposition externe. Dans le cadre de cette simple conclusion, on se contentera d'analyser l'important point suivant.

### 7.3. Conséquence de la vérité de $(\nu \simeq +\infty)_U$

On s'intéresse maintenant à la question suivante : est-ce que la vérité de la proposition externe $(\nu \simeq +\infty)_U$ implique que, pour chaque entier standard $n$, la proposition initiale $(n \le \nu)$ est vraie ? Si oui, cela montrerait que la proposition externe $(\nu \simeq +\infty)_U$ joue un rôle équivalent à la formule externe correspondante de l'analyse nonstandard usuelle. On suppose donc que $(\nu \simeq +\infty)_U$ est vraie : elle possède un objet-preuve, disons $q$ qui, d'après (45), est un objet fonctionnel

$$q : \left( \prod n : \mathbb{N} \right) \langle (n \le \nu), U \rangle$$

Pour chaque entier standard $n$, on obtient un objet-preuve standard

$$\text{apply}(q, n) : \langle (n \le \nu), U \rangle$$

D'après le théorème 3, on peut définir un objet spécifié par le jugement

$$\uparrow\text{apply}(q, n) : (n \le N(S^{\{l_1\}}(\infty_{S^{l_1}(i_1)}), \dots, S^{\{l_m\}}(\infty_{S^{l_m}(i_m)}))) \quad (46)$$

où $l_1, \dots, l_m$ dépendent de $q$ et de $n$. Arrivé à ce point, on retrouve la difficulté mise en lumière dans le théorème 3 et dans le commentaire qui suit ce résultat : l'entier non-standard $N(S^{\{l_1\}}(\infty_{S^{l_1}(i_1)}), \dots, S^{\{l_m\}}(\infty_{S^{l_m}(i_m)}))$ n'est pas en général définitionnellement égal à $\nu$ du fait qu'il n'est pas prouvé (et sans doute pas prouvable en général) que $S^{\{l_s\}}(\infty_{S^{l_s}(i_s)})$ soit définitionnellement égal à $\infty_{i_s}$ pour $s = 1, \dots, m$. En conséquence, la proposition qui apparaît dans le jugement (46) n'est pas définitionnellement égale à $(n \le \nu)$, même si elle en est structurellement proche.

<footnote n="25"><sup>25</sup> A titre d'exercice, on peut vérifier que le jugement $(\infty : \mathbb{N})$ est forcé par le voisinage $U_0$ réduit à l'unique jugement $(\infty_0 : \mathbb{N})$ et que la proposition correspondante $(\infty \simeq +\infty)_{U_0}$ prend la forme $((\forall n : \mathbb{N})(\exists l : \mathbb{N})(\forall x : \mathbb{N})(n \le S^{\{l\}}(x)))$. L'observation de cette proposition laisse à supposer qu'elle est vraie, ce qui peut être prouvé dans $\mathcal{T}$.</footnote>
## 7.4. Une forme d'induction externe ?

Il serait possible de contourner cette vraie difficulté liée à la rigidité de l'égalité définitionnelle si l'on savait montrer par induction sur $l$ que les nombres entiers nonstandard $\infty_i$ et $S^{\{l\}}(\infty_{S^l(i)})$ sont propositionnellement égaux quels que soient les entiers standard $i$ et $l$. En effet, on pourrait alors déduire de (46) et d'une propriété de substitution de l'égalité propositionnelle la construction d'un objet-preuve de $(n \le \nu)$. Sans entrer dans les détails techniques, cette piste semble échouer : l'induction sur $\mathbb{N}$ ne peut pas être mise directement en œuvre du fait du caractère externe de la suite de choix $\infty$. En l'état, nous ne sommes pas en mesure de répondre positivement à la question posée au début de la sous-section 7.3 précédente.

Une nouvelle piste à considérer pourrait être d'enrichir les axiomes nonstandard en rajoutant une "règle d'induction externe" opérant sur $\mathbb{N}$ et permettant d'obtenir l'égalité propositionnelle en question. Le sens de cette adjonction serait d'ajouter un contrôle sur le développement à long terme de la suite de choix alors que, pour l'instant, le contrôle opéré par l'égalité définitionnelle ne vaut que pour des développements quantifiés par des numéraux explicites. Une raison au moins rend crédible cette piste : de nombreuses formes d'analyse nonstandard basées sur une axiomatique minimaliste ont été dotées d'un principe de récurrence externe afin d'obtenir une théorie relativement opérationnelle <fnref n="26" />. Bien entendu, la mise en œuvre de cette idée dans le cadre de la théorie des types est autrement plus délicate que dans le cas des théories en question <fnref n="27" />. L'exploration de cette piste sort du cadre du présent travail mais elle pourra faire l'objet de développements ultérieurs.

## 8. Bibliographie

[1] E. BISHOP, « Foundations of Constructive Analysis », McGraw-Hill, 1967.

[2] L. E. J. BROUWER, In A. Heyting editor « L. E. J. Brouwer Collected Works I, Philosophy and Foundations of Mathematics », North-Holland Publishing Company, Amsterdam, 1975.

[3] G. KREISEL, « Lawless Sequences of Natural numbers », Compositio Math., vol. 20, 1968, pages 222-248.

[4] P. MARTIN-LÖF, « About Models for Intuitionistic Type Theory and the Notion of Definitional Equality », Proceeding of the Third Scandinavian Logic Symposium, Studies in Logic and Foundations of Mathematics, North-Holland Publishing Company, pages 81-109, Amsterdam, 1975.

<footnote n="26">26. La meilleure référence est sans conteste le superbe traité de Nelson sur les probabilités [10] qui est vraisemblablement à l'origine de ces axiomatiques minimales. A ce propos, comment ne pas rêver à une synthèse entre les idées de Nelson et de Martin-Löf ?</footnote>

<footnote n="27">27. Une modification intempestive et insuffisamment pensée pourrait faire perdre les avantages de la théorie des types.</footnote>
[5] P. MARTIN-LÖF, « Intuitionnistic Type Theory », *Bibliopolis*, Napoli, 1984.

[6] P. MARTIN-LÖF, « Mathematics of Infinity », In *Lecture Notes in Computer Science, COLOG-88 Computer Logic*, Springer-Verlag Berlin, pages 146-197, 1990.

[7] P. MARTIN-LÖF, « Choice Sequence in Type Theory », Handwritten notes by P. Mäenpää and A. Ranta on a lecture series given by P. Martin-Löf at Stockholm University in 1990-1991.

[8] P. MARTIN-LÖF, « Nonstandard Type Theory », Handwritten notes of a talk given at the Workshop Proof and Computation at Munich in 1999.

[9] E. NELSON, « Internal Set Theory : A new approach to nonstandard analysis », *Bulletin of the American Mathematical Society*, vol. 83, n° 6, pages 1165-1198, 1977.

[10] E. NELSON, « Radically Elementary Probability Theory », *Annals of Mathematical Studies, Princeton University Press*, 1987.

[11] B. NORDSTRÖM, K. PETERSSON, J.M. SMITH, « Programming in Martin-Löf Type Theory », *Oxford University Press*, 1990.
Out of print, available from www.cs.chalmers.se.Cs.Research/Logic.

[12] E. PALMGREN, « A constructive approach to nonstandard analysis », *Annals of Pure and Applied Logic*, vol. 73, pages 297-325, 1995.

[13] E. PALMGREN, « Developments in Constructive Nonstandard Analysis », *The Bulletin of Symbolic Logic*, vol. 4, n° 3, 1998.

[14] A. RANTA, « Type Theoretical Grammar », *Oxford Science Publications*, Chapter 2 and 8, 1994.

[15] J. RUOKOLAINEN, « Constructive nonstandard analysis without actual infinity », *PhD thesis*, University of Helsinki, Helsinki, 2004.

[16] P. SCHUSTER, U. BERGER, H. OSSWALD editors, « Reuniting the Antipodes - Constructive and Nonstandard Views of the Continuum », Springer, 2002.

[17] A.S. TROELSTRA, « Choice Sequences », *Oxford University Press*, Oxford, 1977.

[18] THE UNIVALENT FOUNDATIONS PROGRAM, « Homotopy Type Theory : Univalent Foundations of Mathematics », *Institute for Advanced Study*, 2013.
http://homotopytypetheory.org/book.