15

Logical Relations for Impredicative languages like System F seem to rely critically on impredicativity of the ambient logic. Specifically, the interpretation for the forall-type will be defined in terms of all typed relations. In an impredicative system (like CiC/Coq) that's fine, but it seems to be impossible in a predicative system (like Agda).

How can this be done? For example, how would you prove normalization for System F in Agda? Do you have to build your own impredicative universe?

Max New
  • 1,675
  • 9
  • 24

1 Answers1

14

In general, what we usually call the logical relations argument isn't really linked to impredicativity: the main idea is simply to interpret terms in some abstract algebra $\cal A$, and to represent types as a ($n$-ary) relation $R \subseteq \cal A^n$.

This works perfectly fine for all kinds of type theories, including dependently typed theories, see e.g. Shürmann and Sarnat: Structural Logical Relations where a predicative logic (that of Twelf) is used to prove a certain property (decidability of equality) for a predicative calculus (simply typed $\lambda$-calculus) using logical relations.

As you may have suspected, however, it is not possible to prove normalization of system F in Agda (if Agda isn't secretly stronger than expected, i.e. about the strength of Martin-Löf type theory with a bunch of universes). This is because normalization of system F implies consistency of 2nd order arithmetic ($\mathrm{PA}_2$) which is stronger than M-L type theory with any number of (predicative) universes.

It's instructive to work out exactly where the proof goes wrong in Agda, though. It indeed occurs when you try to define the logical relations interpretation of the impredicative quantification. The interpretation of the non-impredicative connectives though (including "dependent" quantification) is kosher in a theory like Agda.

cody
  • 13,861
  • 1
  • 49
  • 103
  • 1
    Wow, really? You can't prove System F normalizes in Agda? Do you have a citation for that? – Max New Oct 20 '15 at 18:09
  • 3
    @MaxNew: This is actually quite difficult to find a citation for. The closest I can find is The Strength of Some Martin-Löf Type Theories which definitely settles the question for a predicative theory with a single universe and some kind of induction. But Agda has the terrifying induction recursion which makes it vastly more powerful. – cody Oct 20 '15 at 19:41
  • 1
    I should add though, that induction recursion is known to be weaker than impredicative quantification in certain cases, as is nicely explained here: http://fplab.bitbucket.org/posts/2012-12-06-induction-recursion.html – cody Oct 22 '15 at 14:49
  • 1
    @cody Unfortunately, the link does not work any more. Are you able to find this content again? Are you aware of new publications in the area of formalizing impredicativity? – Łukasz Lew Jun 08 '18 at 04:08
  • 1
    https://fplab.bitbucket.io/posts/2012-12-06-induction-recursion.html by Venanzio Capretta – Łukasz Lew Mar 23 '21 at 18:27
  • @ŁukaszLew i am not sure if it's my browser but the link is horribly unreadable. everything is in its veery raw latex form. – Jason Hu Jun 09 '22 at 22:05