Peut-on prouver une faible normalisation du système F par induction sur un ordinal transfini

Une faible normalisation pour le calcul lambda typé simple peut être prouvée (Turing) par induction sur . Un calcul lambda étendu avec des récurseurs sur les nombres naturels (Gentzen) a une stratégie de normalisation faible par induction sur .ϵ $\omega^2$$\epsilon_0$

Qu'en est-il du système F (ou plus faible)? Existe-t-il une faible preuve de normalisation dans ce style? Sinon, cela peut-il être fait du tout?

Girard (1989) est l'étude la plus complète de la relation entre la théorie de la preuve constructive (qui est étroitement liée à la théorie des ordinaux constructifs) et l'arithmétique imprédicative de second ordre (qui, comme le souligne Ulrik, est de force équivalente au système F). Là, il s'appuie sur sa théorie des dilatateurs (1981), que je ne suis pas vraiment, mais je pense essentiellement fournit une théorie non constructive de la skolémisation d'ordre supérieur.

Je crois comprendre que vous ne pouvez pas exprimer les formules constructive dans le sens de Bishop — Martin-Löf, car elles sont imprédicatives d'une manière que vous ne pouvez pas éliminer en ajoutant une sorte de schéma d'induction de premier ordre.$\Sigma^1_2$

Je me souviens avoir suggéré à un théoricien ordinal que l'on pourrait simplement stipuler que l'on peut fonder un constructivisme imprédicatif dans une théorie des types basée sur le calcul lambda polymorphe, et utiliser la technique candidate à la réduction de la preuve SN de Girard pour le système F pour imposer un ordre total raisonnable sur l'univers des constructions, appelant les classes d'équivalence que vous obtenez de cela les ordinaux; il a dit quelque chose d'intelligent que j'ai retenu comme disant que vous pourriez le faire fonctionner, mais cela aurait tous les avantages du vol par rapport au travail honnête. Pour le faire fonctionner, il ne suffit pas que vous puissiez prouver dans la théorie des ensembles l'existence de tels ordinaux, vous auriez besoin d'une preuve constructive de trichotomie pour l'ordre.

En résumé, avec la notion régulière de construction intuitionniste due à Bishop — Martin-Löf, la littérature que je connais suggère fortement non. Si vous êtes opposé au travail honnête et que vous embrasseriez un constructivisme imprédicatif, alors je suppose que cela peut probablement être fait. Vous auriez naturellement besoin d'une théorie plus solide que le système F pour prouver de manière constructive la trichotomie requise, mais le calcul des constructions inductives fournit un candidat évident.

Les références

1. Girard, Jean-Yves (1981), -logic. I. Dilatateurs, Annals of Mathematical Logic 21 (2): 75-219.$\Pi^1_2$
2. Girard (1989) Théorie de la preuve et complexité logique, vol. I , Napoli: Bibliopolis. Il n'y a pas de volume II.

D'une manière très idiote, la normalisation faible pour tout système raisonnable peut être prouvée par induction sur un ordinal constructif, à condition bien sûr que la normalisation faible se vérifie. En effet, l'affirmation selon laquelle le système F a une faible normalisation est formalisable en arithmétique comme une phrase , et en tant que telle est prouvable (car c'est vrai) par induction transfinie le long d'une notation ordinale constructive non naturelle de hauteur ω 2 . (Voir cette question sur l'échange de pile de mathématiques pour savoir comment ce classement pourrait fonctionner.)$\Pi^0_2$$\omega^2$

$\varepsilon_0$$\Gamma_0$

Espérons qu'un jour, quelqu'un trouvera une notation ordinale pour l'arithmétique de second ordre que tout le monde conviendra est naturelle, et qui pourrait ensuite être utilisée de manière honnête pour prouver une faible normalisation pour le système F.

$\mathbb{N} \to \mathbb{N}$

De plus, je pense que l'arithmétique du second ordre est assez forte et qu'aucune borne supérieure constructive n'est encore connue pour son "ordinal théorique de preuve" ( l'art de l'analyse ordinale, section 3 ).

Je pense que cette limite ordinale constructive est ce qui est nécessaire pour faire l'induction que vous demandez.