<p>In general, what we usually call the <em>logical relations argument</em> 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$.</p>

<p>This works perfectly fine for all kinds of type theories, including dependently typed theories, see e.g. Shürmann and Sarnat: <a href="http://www.pps.univ-paris-diderot.fr/~sarnat/slr.pdf">Structural Logical Relations</a> where a <em>predicative logic</em> (that of Twelf) is used to prove a certain property (decidability of equality) for a <em>predicative calculus</em> (simply typed $\lambda$-calculus) using logical relations.</p>

<p>As you may have suspected, however, it is <strong>not</strong> 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 <em>any</em> number of (predicative) universes.</p>

<p>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.</p>

CC BY-SA 3.0
2015-10-20T18:09:33.733Z
Wow, really? You can't prove System F normalizes in Agda? Do you have a citation for that?
Max New
CC BY-SA 3.0
2015-10-20T19:41:34.320Z
@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](https://www1.maths.leeds.ac.uk/~rathjen/typeOHIO.pdf) 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
CC BY-SA 3.0
2015-10-22T14:49:01.930Z
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
CC BY-SA 4.0
2018-06-08T04:08:27.020Z
@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
CC BY-SA 4.0
2021-03-23T18:27:02.160Z
https://fplab.bitbucket.io/posts/2012-12-06-induction-recursion.html by Venanzio Capretta
Łukasz Lew
CC BY-SA 4.0
2022-06-09T22:05:15.063Z
@Ł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
CC BY-SA 3.0
2015-10-20T16:02:34.333Z
2015-10-20T16:02:34.333Z
cody
<p>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).</p>

<p>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?</p>

<lo.logic><pl.programming-languages><type-theory><automated-theorem-proving>
Logical Reations for an Impredicative System in a Predicative MetaTheory
Max New
# Logical Reations for an Impredicative System in a Predicative MetaTheory

(Asked by: username_0 on 2015-10-20)

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?

**Tags:** lo.logic, pl.programming-languages, type-theory, automated-theorem-proving

---

## 1 answers

### Answer by username_1 on 2015-10-20. Score: 14 | Accepted answer

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](http://www.pps.univ-paris-diderot.fr/~sarnat/slr.pdf) 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.

> **Comments:**
> **username_0**: Wow, really? You can't prove System F normalizes in Agda? Do you have a citation for that?  
> **username_1**: @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](https://www1.maths.leeds.ac.uk/~rathjen/typeOHIO.pdf) 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.  
> **username_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  
> **username_2**: @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?  
> **username_2**: https://fplab.bitbucket.io/posts/2012-12-06-induction-recursion.html by Venanzio Capretta  
> **username_3**: @ŁukaszLew i am not sure if it's my browser but the link is horribly unreadable. everything is in its veery raw latex form.  

---

