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 .UMAnR ⊆ An
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.P A2
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.