# What is the proof-theoretic significance of the existence of a Brown-Palsberg self-interpreter for system $F_\omega$?

In A Self-Interpreter for F-omega, 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?

• This might be closer to Artemov's "logic of proofs" than to GL. – Emil Jeřábek Nov 21 '16 at 11:25

There is no proof significance, since already Gödel's $T$ has a Brown-Palsberg self-interpreter for free. We need a better definition of a typed self-interpreter.