Para sistemas sin tipos dependientes, como el sistema de tipos Hindley-Milner, los tipos corresponden a fórmulas de lógica intuicionista. Allí sabemos que sus modelos son álgebras de Heyting y, en particular, para refutar una fórmula, podemos restringir a un álgebra de Heyting donde cada fórmula está representada por un subconjunto abierto de .
Por ejemplo, si queremos mostrar que no está habitada, construimos un mapeo partir de fórmulas para abrir subconjuntos de definiendo: Luego Esto muestra que la fórmula original no puede ser demostrable, ya que tenemos un modelo donde no es cierto, o de manera equivalente (por el isomorfismo de Curry-Howard) el tipo no puede ser habitado.ϕ R ϕ ( α )ϕ ( α → ⊥ )
Otra posibilidad sería utilizar marcos Kriepke .
¿Existen métodos similares para sistemas con tipos dependientes? ¿Como alguna generalización de álgebras de Heyting o cuadros de Kripke?
Nota: No estoy solicitando un procedimiento de decisión, sé que no puede haber ninguno. Solo pido un mecanismo que permita presenciar la imposibilidad de probar una fórmula, para convencer a alguien de que no es demostrable.