7
$\begingroup$

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?

|cite|improve this question
$\endgroup$
  • 1
    $\begingroup$ This might be closer to Artemov's "logic of proofs" than to GL. $\endgroup$ – Emil Jeřábek Nov 21 '16 at 11:25
7
$\begingroup$

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.

|cite|improve this answer
$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – fhyve Nov 21 '16 at 20:39
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Nov 21 '16 at 21:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.