<p>There is no proof significance, since already <a href="http://math.andrej.com/2016/01/04/a-brown-palsberg-self-interpreter-for-godels-system-t/" rel="noreferrer">Gödel's $T$ has a Brown-Palsberg self-interpreter for free</a>. We need a better definition of a typed self-interpreter.</p>

CC BY-SA 3.0
2016-11-21T20:39:33.943Z
But what about their "deep" interpreter? They seem to be able to do non-trivial things with it. For example, they have a normalization checker, which usually implies a proof of consistency of a type theory.
fhyve
CC BY-SA 3.0
2016-11-21T21:06:12.893Z
Their interpreter seems to have some structurally desirable properties, but their *definition* of interpreter allows for trivial solutions, such as the one linked to in my answer.  As far as I can tell nothing much is going on here. For instance, the normalization checker is just a simple recursion on the structure of the term.
Andrej Bauer
CC BY-SA 3.0
2016-11-21T13:37:49.987Z
2016-11-21T13:52:16.417Z
2016-11-21T13:52:16.417Z
Andrej Bauer
<p>In <a href="http://web.cs.ucla.edu/~palsberg/paper/popl16-full.pdf">A Self-Interpreter for F-omega</a>, Brown and Palsberg construct for each term of each type $x:T$ a representation $\bar x : \Box T$ (a metatheoretical function which can't be represented in the language), and an interpretation function $u_T : \Box T \to T$. This is reminiscent of GL provability logic, which in particular abstracts how PA can represent its own proof theory. But while the representation looks like the axiom $\vdash T \implies \vdash \Box T$, the second $\vdash \Box T \to T$ is inconsistent with GL. </p>

<p>So what sort of gadget is this, in logical terms? </p>

<p>Can it be used at all to talk about the metatheory of F-omega?</p>

<p>What would a representation operation that satisfies the axioms of GL look like? </p>

CC BY-SA 3.0
2016-11-21T11:25:20.713Z
This might be closer to Artemov's "logic of proofs" than to GL.
Emil Jeřábek
<type-theory><proof-theory>
What is the proof-theoretic significance of the existence of a Brown-Palsberg self-interpreter for system $F_\omega$?
fhyve
# What is the proof-theoretic significance of the existence of a Brown-Palsberg self-interpreter for system $F_\omega$?

(Asked by: username_0 on 2016-11-21)

In [A Self-Interpreter for F-omega](http://web.cs.ucla.edu/~palsberg/paper/popl16-full.pdf), Brown and Palsberg construct for each term of each type $x:T$ a representation $\bar x : \Box T$ (a metatheoretical function which can't be represented in the language), and an interpretation function $u\_T : \Box T \to T$. This is reminiscent of GL provability logic, which in particular abstracts how PA can represent its own proof theory. But while the representation looks like the axiom $\vdash T \implies \vdash \Box T$, the second $\vdash \Box T \to T$ is inconsistent with GL.

So what sort of gadget is this, in logical terms?

Can it be used at all to talk about the metatheory of F-omega?

What would a representation operation that satisfies the axioms of GL look like?

**Tags:** type-theory, proof-theory

> **Comments:**
> **username_1**: This might be closer to Artemov's "logic of proofs" than to GL.  

---

## 1 answers

### Answer by username_2 on 2016-11-21. Score: 8

There is no proof significance, since already [Gödel's $T$ has a Brown-Palsberg self-interpreter for free](http://math.andrej.com/2016/01/04/a-brown-palsberg-self-interpreter-for-godels-system-t/). We need a better definition of a typed self-interpreter.

> **Comments:**
> **username_0**: But what about their "deep" interpreter? They seem to be able to do non-trivial things with it. For example, they have a normalization checker, which usually implies a proof of consistency of a type theory.  
> **username_2**: Their interpreter seems to have some structurally desirable properties, but their *definition* of interpreter allows for trivial solutions, such as the one linked to in my answer.  As far as I can tell nothing much is going on here. For instance, the normalization checker is just a simple recursion on the structure of the term.  

---

