|
RÉSUMÉ.
Partant de son travail Mathematics of Infinity (1989),
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 une communication de 1999,
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 sa communication de 1999. 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 (1989), 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
a communication in 1999, 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
his communication of 1999. 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.
|
présentation