Podemos provar uma fraca normalização do Sistema F por indução em um ordinal transfinito

Normalização fraca para o cálculo lambda de tipo simples pode ser comprovada (Turing) por indução em . Um cálculo lambda estendido com recursores em números naturais (Gentzen) possui uma estratégia de normalização fraca por indução em .$\omega^2$$\epsilon_0$

E o Sistema F (ou mais fraco)? Existe uma prova fraca de normalização nesse estilo? Caso contrário, isso pode ser feito?

A pesquisa mais abrangente da relação entre a teoria da prova construtiva (que está intimamente ligada à teoria dos ordinais construtivos) e a aritmética impredicativa de segunda ordem (que, como Ulrik aponta é equivalente em força ao Sistema F), é Girard (1989). Lá ele constrói sua teoria dos dilatadores (1981), que eu realmente não sigo, mas acho que essencialmente fornece uma teoria não construtiva da skolemização de ordem superior.

Meu entendimento é que você não pode expressar fórmulas de forma construtiva no sentido de Bishop-Martin-Löf, porque eles são impredicativa de uma forma que você não pode eliminar através da adição de qualquer tipo de esquema de indução de primeira ordem.$\Sigma^1_2$

Lembro-me de sugerir a um teórico ordinal que alguém poderia simplesmente estipular que você pode fundamentar um construtivismo impredicativo em uma teoria de tipos baseada no cálculo lambda polimórfico e usar a técnica candidata a redução da prova SN de Girard para o Sistema F para impor uma ordem total razoável. o universo das construções, chamando as classes de equivalência que você obtém disso dos ordinais; ele disse algo inteligente que eu disse que você poderia fazer com que isso funcionasse, mas teria todas as vantagens de roubo sobre trabalho honesto. Para que funcione, não é bom o suficiente para que você possa provar na teoria dos conjuntos a existência de tais ordinais; você precisaria de uma prova construtiva de tricotomia para a ordem.

Em resumo, com a noção regular de construção intuicionista devida a Bishop-Martin-Löf, a literatura que conheço sugere fortemente que não. Se você é avesso a um trabalho honesto e adota um construtivismo impredicativo, meu palpite é que provavelmente isso pode ser feito. Naturalmente, você precisaria de uma teoria mais forte de que o Sistema F para provar construtivamente a tricotomia necessária, mas o Cálculo de Construções Indutivas fornece um candidato óbvio.

Referências

1. Girard, Jean-Yves (1981), -Logic. I. Dilatadores, Anais da Lógica Matemática 21 (2): 75-219.$\Pi^1_2$
2. Girard (1989) Proof Theory and Logical Complexity, vol. Eu , Napoli: Bibliopolis. Não há volume II.

De uma maneira muito tola, a fraca normalização para qualquer sistema razoável pode ser comprovada por indução em um ordinal construtivo, desde que, naturalmente, essa fraca normalização se mantenha. De fato, a afirmação de que o Sistema F tem normalização fraca é formalizável na aritmética como uma sentença de e, como tal, é comprovável (uma vez que é verdade) por indução transfinita ao longo de uma notação ordinal construtiva não natural de altura ω 2 . (Veja esta pergunta na troca de pilhas matemáticas para saber como essa ordem poderia funcionar.)$\Pi^0_2$$\omega^2$

$\varepsilon_0$$\Gamma_0$

Esperançosamente, um dia alguém criará uma notação ordinal para a aritmética de segunda ordem que todos concordam que é natural e que isso poderia ser usado de maneira honesta para provar a fraca normalização do Sistema F.

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

Além disso, acho que a aritmética de segunda ordem é bastante forte e que nenhum limite superior construtivo ainda é conhecido por seu "ordinal teórico da prova" ( The art of ordinal analysis, seção 3 ).

Eu acho que esse limite ordinal construtivo é o que é necessário para fazer a indução solicitada.