Reações lógicas para um sistema impredicativo em uma meta-teoria preditiva

14

As relações lógicas para linguagens impredicativas como o Sistema F parecem depender criticamente da impredicatividade da lógica ambiental. Especificamente, a interpretação para o tipo forall será definida em termos de todas as relações digitadas. Em um sistema impredicativo (como CiC / Coq), tudo bem, mas parece impossível em um sistema predicativo (como o Agda).

Como isso pode ser feito? Por exemplo, como você provaria a normalização do Sistema F no Agda? Você tem que construir seu próprio universo impredicativo?

Max Novo
fonte

Respostas:

14

Em geral, o que geralmente chamamos de argumento das relações lógicas não está realmente ligado à impredicatividade: a idéia principal é simplesmente interpretar termos em alguma álgebra abstrata e representar tipos como uma relação ( n- ária) R A n .UMAnRUMAn

Isso funciona perfeitamente para todos os tipos de teorias de tipos, incluindo teorias de tipo dependente, veja, por exemplo, Shürmann e Sarnat: Relações Lógicas Estruturais, onde uma lógica predicativa (a de Twelf) é usada para provar uma certa propriedade (decidibilidade da igualdade) para um cálculo predicativo (simplesmente digitado calcculus) usando relações lógicas.λ

Como você pode ter suspeitado, no entanto, é não possível comprovar normalização do sistema de F em Agda (se Agda não é segredo mais forte do que o esperado, ou seja, sobre a força da teoria dos tipos Martin-Löf com um monte de universos). Isto é porque a normalização do sistema de F implica consistência de segunda ordem aritmética ( ), que é mais forte do que a teoria ML tipo com qualquer número de (predicativos) universos.PUMA2

No entanto, é instrutivo descobrir exatamente onde a prova dá errado na Agda. Realmente ocorre quando você tenta definir a interpretação das relações lógicas da quantificação impredicativa. A interpretação dos conectivos não impredicativos embora (incluindo quantificação "dependente") é kosher em uma teoria como a Agda.

cody
fonte
1
Uau! Sério? Você não pode provar que o Sistema F normaliza no Agda? Você tem uma citação para isso?
Max New
2
@ MaxNew: Isso é realmente muito difícil de encontrar uma citação. O mais próximo que posso encontrar é A força de algumas teorias de tipos de Martin-Löf, que definitivamente resolve a questão de uma teoria predicativa com um único universo e algum tipo de indução. Mas a Agda tem a terrível recursão de indução que a torna muito mais poderosa.
Cody
1
Devo acrescentar, porém, que a recursão por indução é mais fraca que a quantificação impredicativa em certos casos, como é bem explicado aqui: fplab.bitbucket.org/posts/2012-12-06-induction-recursion.html
cody
1
Infelizmente, o link não funciona mais. Você consegue encontrar esse conteúdo novamente? Você conhece novas publicações na área da formalização da impredicatividade?
asukasz Lew