¿Podemos demostrar una normalización débil para el Sistema F por inducción en un ordinal transfinito?

La normalización débil para el cálculo lambda simple mecanografiado se puede probar (Turing) por inducción en . Un cálculo lambda extendido con recursores en números naturales (Gentzen) tiene una estrategia de normalización débil por inducción en .$\omega^2$$\epsilon_0$

¿Qué pasa con el Sistema F (o más débil)? ¿Hay una prueba de normalización débil en este estilo? Si no, ¿se puede hacer?

El estudio más completo de la relación entre la teoría de la prueba constructiva (que está estrechamente relacionada con la teoría de los ordinales constructivos) y la aritmética implícita de segundo orden (que, como señala Ulrik, es equivalente en fuerza al Sistema F) es Girard (1989). Allí se basa en su teoría de los dilatadores (1981), que realmente no sigo, pero creo que esencialmente proporciona una teoría no constructiva de la esolemización de orden superior.

Tengo entendido que no puede expresar fórmulas constructiva en el sentido de Bishop-Martin-Löf, porque son impredecibles de una manera que no puede eliminar agregando ningún tipo de esquema de inducción de primer orden.$\Sigma^1_2$

Recuerdo haberle sugerido a un teórico ordinal que uno podría simplemente estipular que se puede fundamentar un constructivismo impredecible en una teoría de tipos basada en el cálculo lambda polimórfico, y usar la técnica de candidato de reducción de la prueba SN de Girard para que el Sistema F imponga un orden total razonable el universo de construcciones, llamando a las clases de equivalencia que obtienes de esto los ordinales; Dijo algo inteligente que le quité diciendo que podría hacer que eso funcione, pero que tendría todas las ventajas del robo sobre el trabajo honesto. Para que funcione, no es lo suficientemente bueno como para demostrar en la teoría de conjuntos la existencia de tales ordinales, necesitaría una prueba constructiva de tricotomía para el pedido.

En resumen, con la noción regular de construcción intuicionista debida a Bishop-Martin-Löf, la literatura que conozco sugiere fuertemente que no. Si eres reacio al trabajo honesto y abrazarías un constructivismo impredecible, entonces supongo que probablemente se pueda hacer. Naturalmente, necesitará una teoría más sólida de que el Sistema F demuestre de manera constructiva la tricotomía requerida, pero el cálculo de construcciones inductivas proporciona un candidato obvio.

Referencias

1. Girard, Jean-Yves (1981), lógica. I. Dilators, Annals of Mathematical Logic 21 (2): 75–219.$\Pi^1_2$
2. Girard (1989) Teoría de la prueba y complejidad lógica, vol. Yo , Napoli: Bibliopolis. No hay volumen II.

De una manera muy tonta, la normalización débil para cualquier sistema razonable puede probarse por inducción en un ordinal constructivo, siempre que, por supuesto, se mantenga la normalización débil. De hecho, la afirmación de que el Sistema F tiene una normalización débil es formalizable en aritmética como una oración , y como tal es demostrable (ya que es cierto) por inducción transfinita a lo largo de una notación ordinal constructiva no natural de altura ω 2 . (Vea esta pregunta sobre el intercambio de pila de matemáticas para saber cómo podría funcionar este orden).$\Pi^0_2$$\omega^2$

$\varepsilon_0$$\Gamma_0$

Esperemos que algún día alguien presente una notación ordinal para la aritmética de segundo orden que todos estarán de acuerdo en que es natural, y que luego podría usarse de manera honesta para demostrar una normalización débil para el Sistema F.

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

Además, creo que la aritmética de segundo orden es bastante fuerte y que aún no se conoce un límite superior constructivo por su "prueba ordinal teórica" ​​( El arte del análisis ordinal, sección 3 ).

Creo que este límite ordinal constructivo es lo que se necesita para hacer la inducción que solicita.