Propriétés de Mahlo metaprédicative et explicite; une perspective de la théorie de la démonstration

Gerhard Jäger

Les cardianux de Mahlo et ses analogues récursifs ont joué un rôle important dans plusieurs domaines de la logique traditionnelle, principalement en théorie des ensembles et en théorie de la récursion. Par exemple, le plus petit ordinal de Mahlo récursif est le plus petit ordinal non-récursif sur le super-jump de Gandy; il est également l’ordinal de clôture de plusieures définitions inductives non-monotones intéressantes. Aussi, le segment initial de la hierarchie constructible jusqu’à cet ordinal donne le plus petit modèle standard du principe de réflexion Π_{2} pour les ensembles admissibles.

Le traitement de la propriété de Mahlo en théorie de la démonstration est plus récent. D’abord, une théorie des ensembles admissibles formalisant l’univers de Mahlo et un sous-système correspondant de l’analyse furent examinés par Rathjen. Puis, des axiomes du type Mahlo furent incorporés par Setzer à la théorie des types de Martin-Löf. L’investigation de la propriété de Mahlo dans le cadre de la mathématique explicite de Feferman découle des travaux de Jäger, Strahm et Studer.

Dans cette conférence je discuterai plusieurs aspects nouveaux de la propriété de Mahlo, en particulier depuis la perspective de la mathématique explicite. Je mentionnerai également d’autres principes voisins, dans des soussystèmes de l’arithmétique du second ordre. En ce faisant nous jetterons une lumière nouvelle sur la metaprédicativité, un domaine intéressant des systèmes formels se situant entre la prédicativité et l’imprédicativité.

Address: Institut für Informatik und angewandte Mathematik, Universität Bern, Neubrueckstrasse 10, CH-3012 Bern, Switzerland

E-mail: jaeger@iam.unibe.ch