lob.lagda

\input{./header.tex}

\title{Lӧb's Theorem}
\subtitle{A functional pearl of dependently typed quining}

\maketitle

%\category{CR-number}{subcategory}{third-level}

% general terms are not compulsory anymore,
% you may leave them out
%\terms
%Agda, Lob, quine, self-reference

\keywords
Agda, Lӧb's theorem, quine, self-reference, type theory

\AgdaHide{
  \begin{code}
module lob where
  \end{code}
}

\begin{abstract}
Lӧb's theorem states that to prove that a proposition is provable, it
is sufficient to prove the proposition under the assumption that it is
provable.  The Curry-Howard isomorphism identifies formal proofs with
abstract syntax trees of programs; Lӧb's theorem thus implies, for
total languages which validate it, that self-interpreters are
impossible.  We formalize a few variations of Lӧb's theorem in Agda
using an inductive-inductive encoding of terms indexed over types.  We
verify the consistency of our formalizations relative to Agda by
giving them semantics via interpretation functions.
\end{abstract}

% \todo{Should we unify the various repr-like functions (repr, add-quote, ⌜_⌝ᵀ, ⌜_⌝ᵗ, ⌜_⌝ᶜ)?}

\section{Introduction}

\begin{quotation}
\noindent \textit{If P's answer is `Bad!', Q will suddenly stop. \\
But otherwise, Q will go back to the top, \\
and start off again, looping endlessly back, \\
till the universe dies and turns frozen and black.}
\end{quotation}
\begin{flushright}
Excerpt from \emph{Scooping the Loop Snooper: A proof that the Halting Problem is undecidable} \cite{loopsnoop}
\end{flushright}

 Lӧb's theorem has a variety of applications, from providing an
 induction rule for program semantics involving a ``later''
 operator~\cite{appel2007very}, to proving incompleteness of a logical
 theory as a trivial corollary, from acting as a no-go theorem for a
 large class of self-interpreters, to allowing robust cooperation in
 the Prisoner's Dilemma with Source
 Code~\cite{BaraszChristianoFallensteinEtAl2014}, and even in one case
 curing social anxiety~\cite{Yudkowsky2014}.

 In this paper, after introducing the content of Lӧb's theorem, we
 will present in Agda three formalizations of type-theoretic languages
 and prove Lӧb's theorem in and about these languages: one that shows
 the theorem is admissible as an axiom in a wide range of situations,
 one which proves Lӧb's theorem by assuming as an axiom the existence
 of quines (programs which output their own source code), and one
 which constructs the proof under even weaker assumptions; see
 \autoref{sec:prior-work-and-new} for details.

 ``What is Lӧb's theorem, this versatile tool with wondrous
 applications?'' you may ask.

 Consider the sentence ``if this sentence is true, then you, dear
 reader, are the most awesome person in the world.''  Suppose that
 this sentence is true.  Then you are the most awesome person in the
 world.  Since this is exactly what the sentence asserts, the sentence
 is true, and you are the most awesome person in the world.  For those
 more comfortable with symbolic logic, we can let $X$ be the statement
 ``you, dear reader, are the most awesome person in the world'', and
 we can let $A$ be the statement ``if this sentence is true, then
 $X$''.  Since we have that $A$ and $A → X$ are the same, if we assume
 $A$, we are also assuming $A → X$, and hence we have $X$.  Thus since
 assuming $A$ yields $X$, we have that $A → X$.  What went
 wrong?\footnote{Those unfamiliar with conditionals should note that
 the ``if \ldots\space then \ldots'' we use here is the logical
 ``if'', where ``if false then $X$'' is always true, and not the
 counter-factual ``if''.}

 It can be made quite clear that something is wrong; the more common
 form of this sentence is used to prove the existence of Santa Claus
 to logical children: considering the sentence ``if this sentence is
 true, then Santa Claus exists'', we can prove that Santa Claus
 exists.  By the same logic, though, we can prove that Santa Claus
 does not exist by considering the sentence ``if this sentence is
 true, then Santa Claus does not exist.''  Whether you consider it
 absurd that Santa Claus exist, or absurd that Santa Claus not exist,
 surely you will consider it absurd that Santa Claus both exist and
 not exist.  This is known as Curry's Paradox.

 The problem is that the phrase ``this sentence is true'' is not a
 valid mathematical assertion; no language can encode a truth
 predicate for itself~\cite{tarski1936undefinability}.  However, some
 languages \emph{can} encode assertions about
 \emph{provability}~\cite{godel1931formal}.  In
 \autoref{sec:quine-curry}, we will dig into the difference between
 truth predicates and provability predicates from a computational
 perspective.  We will present an argument for the indefinability of
 truth and for the definability of provability, which we hope will
 prove enlightening when we get to the formalization of Lӧb's theorem
 itself.

 Now consider the sentence ``if this sentence is provable, then Santa
 Claus exists.''  To prove that that sentence is true, we suppose that
 it is provable.  We must now show that Santa Claus exists.  \emph{If
 provability implies truth}, then the sentence is true, and thus Santa
 Claus exists.  Hence, if we can assume that provability implies
 truth, then we can prove that the sentence is true.  This, in a
 nutshell, is Lӧb's theorem: to prove $X$, it suffices to prove that
 $X$ is true whenever $X$ is provable.  If we let $□ X$ denote the
 assertion ``$X$ is provable,'' then, symbolically, Lӧb's theorem
 becomes: $$□ (□ X → X) → □ X.$$ Note that Gӧdel's incompleteness
 theorem follows trivially from Lӧb's theorem: by instantiating $X$
 with a contradiction, we can see that it's impossible for provability
 to imply truth for propositions which are not already true.

 Note that Lӧb's theorem is specific to the formal system and to the
 notion of probability used.  In particular, the formal system must be
 powerful enough to talk about which of its sentences are provable;
 examples of such formal systems include Peano Arithmetic, Martin--Lӧf
 Type Theory, and Gӧdel-Lӧb Modal Logic.  In this paper, we fix formal
 systems by formalizing them as object languages in Agda, and we fix
 formalizations of provability in those systems by treating each
 formalized language as the metalanguage for some formalization of
 itself.

\section{Quines and the Curry--Howard Isomorphism} \label{sec:quine-curry}

 Let us now return to the question we posed above: what went wrong
 with our original sentence?  The answer is that self-reference with
 truth is impossible, and the clearest way we know to argue for this is
 via the Curry--Howard Isomorphism; in a particular technical sense,
 the problem is that self-reference with truth fails to terminate.

 The Curry--Howard Isomorphism establishes an equivalence between
 types and propositions, between (well-typed, terminating, functional)
 programs and proofs.  See \autoref{table:curry-howard} for some
 examples.  Now we ask: what corresponds to a formalization of
 provability?  A proof of $P$ is a terminating functional program
 which is well-typed at the type corresponding to $P$.  To assert that
 $P$ is provable is to assert that the type corresponding to $P$ is
 inhabited.  Thus an encoding of a proof is an encoding of a program.
 Although mathematicians typically use Gӧdel codes to encode
 propositions and proofs, a more natural choice of encoding programs
 is abstract syntax trees (ASTs).  In particular, a valid syntactic
 proof of a given (syntactic) proposition corresponds to a well-typed
 syntax tree for an inhabitant of the corresponding syntactic type.
 Other formalizations of self-representation of programs in programs
 abound~\cite{church1940formulation,Davies:2001:MAS:382780.382785,geuvers2014church,Kiselyov2012,DBLP:conf/ershov/Mogensen01,PFENNING1991137,scott1963system,nott31169,Berarducci1985,brown2016breaking}.

 Note well that the type \mintinline{Agda}|(□ X → X)| is the type of
 functions that take syntax trees and evaluate them; it is the type
 of an interpreter or an unquoter.

  \begin{table}
  \begin{center}
  \begin{tabular}{ccc}
  Logic & Programming & Set Theory \\ \hline
  Proposition & Type & Set of Proofs \\
  Proof & Program & Element \\
  Implication (→) & Function (→) & Function  \\
  Conjunction (∧) & Pairing (,) & Cartesian Product (×)  \\
  Disjunction (∨) & Sum (+) & Disjoint Union (⊔) \\
  Gӧdel codes & ASTs & --- \\
  □ X → X & Interpreters & --- \\
  (In)completeness & Halting problem & ---
  \end{tabular}
  \end{center}
  \caption{The Curry-Howard Isomorphism between mathematical logic and functional programming} \label{table:curry-howard}
  \end{table}

% Unless otherwise specified, we will henceforth consider only
% well-typed, terminating programs; when we say ``program'', the
% adjectives ``well-typed'' and ``terminating'' are implied.

% Before diving into Lӧb's theorem in detail, we'll first visit a
% standard paradigm for formalizing the syntax of dependent type
% theory. (\todo{Move this?})

 What is the computational equivalent of the sentence ``If this
 sentence is provable, then $X$''?  It will be something of the form
 ``??? → $X$''.  As a warm-up, let's look at a Python program that
 outputs its own source code.

 There are three genuinely distinct solutions, the first of which is
 degenerate, and the second of which is cheeky.  These solutions are:
 \label{sec:python-quine}
 \begin{itemize}
   \item The empty program, which outputs nothing.
   \item The code
     \mintinline{Python}|print(open(__file__, 'r').read())|,
     which relies on the Python interpreter to get the
     source code of the program.

   \item A program with a ``template'' which contains a copy of the
     source code of all of the program except for the template itself,
     leaving a hole where the template should be.  The program then
     substitutes a quoted copy of the template into the hole in the
     template itself.  In code, we can use Python's
     \mintinline{Python}|repr| to get a quoted copy of the template,
     and we do substitution using Python's replacement syntax: for
     example, \mintinline{Python}|("foo %s bar" % "baz")| becomes
     \mintinline{Python}|"foo baz bar"|.  Our third solution, in code,
     is thus:
\begin{minted}[mathescape,
%               numbersep=5pt,
               gobble=2,
%               frame=lines,
%               framesep=2mm%
]{Python}
  T = 'T = %s\nprint(T %% repr(T))'
  print(T % repr(T))
\end{minted}

    The functional equivalent, which does not use assignment, and
    which we will be using later on in this paper, is:
\begin{minted}[mathescape,gobble=2]{Python}
  (lambda T: T % repr(T))
   ('(lambda T: T %% repr(T))\n (%s)')
\end{minted}

  \end{itemize}

 We can use this technique, known as
 quining~\cite{hofstadter1980godel,kleene1952introduction}, to
 describe self-referential programs.

 Suppose Python had a function □ that took a quoted representation of
 a Martin--Lӧf type (as a Python string), and returned a Python object
 representing the Martin--Lӧf type of ASTs of
 Martin--Lӧf programs inhabiting that type.  Now consider the program
\begin{minted}[mathescape,gobble=2,]{Python}
  φ = (lambda T: □(T % repr(T)))
       ('(lambda T: □(T %% repr(T)))\n (%s)')
\end{minted}

  The variable \mintinline{Python}|φ| evaluates to the type of ASTs of
  programs inhabiting the type corresponding to
  \mintinline{Python}|T % repr(T)|, where \mintinline{Python}|T| is
  \mintinline{Python}|'(lambda T: □(T %% repr(T)))\n (%s)'|. What
  Martin--Lӧf type does this string, \mintinline{Python}|T % repr(T)|,
  represent? It represents \mintinline{Python}|□(T % repr(T))|, of
  course. Hence \mintinline{Python}|φ| is the type of syntax trees of
  programs that produce proofs of \mintinline{Python}|φ|----in other
  words, \mintinline{Python}|φ| is a Henkin sentence.


  Taking it one step further, assume Python has a function
  \mintinline{Python}|Π(a, b)| which takes two Python representations
  of Martin--Lӧf types and produces the Martin--Lӧf type
  \mintinline{Agda}|(a → b)| of functions from \mintinline{Agda}|a| to
  \mintinline{Agda}|b|.  If we also assume that these functions exist
  in the term language of string representations of Martin--Lӧf types,
  we can consider the function
\begin{minted}[mathescape,gobble=2]{Python}
  def Lob(X):
    T = '(lambda T: Π(□(T %% repr(T)), X))(%s)'
    φ = Π(□(T % repr(T)), X)
    return φ
\end{minted}

  What does \mintinline{Python}|Lob(X)| return?  It returns the type
  \mintinline{Python}|φ| of abstract syntax trees of programs
  producing proofs that ``if \mintinline{Python}|φ| is provable, then
  \mintinline{Python}|X|.''  Concretely, \mintinline{Python}|Lob(⊥)|
  returns the type of programs which prove Martin--Lӧf type theory
  consistent, \mintinline{Python}|Lob(SantaClaus)| returns the variant
  of the Santa Claus sentence that says ``if this sentence is
  provable, then Santa Claus exists.''

  Let us now try producing the true Santa Claus sentence, the one
  that says ``If this sentence is true, Santa Claus exists.'' We need
  a function \mintinline{Python}|Eval| which takes a string
  representing a Martin--Lӧf program, and evaluates it to produce a
  term. Consider the Python program
\begin{minted}[mathescape,gobble=2,]{Python}
  def Tarski(X):
    T = '(lambda T: Π(Eval(T %% repr(T)), X)(%s)'
    φ = Π(Eval(T % repr(T)), X)
    return φ
\end{minted}

  Running \mintinline{Python}|Eval(T % repr(T))| tries to produce a
  term that is the type of functions from
  \mintinline{Python}|Eval(T % repr(T))| to
  \mintinline{Python}|X|. Note that \mintinline{Python}|φ| is itself
  the type of functions from \mintinline{Python}|Eval(T % repr(T))| to
  \mintinline{Python}|X|.  If \mintinline{Python}|Eval(T % repr(T))|
  could produce a term of type \mintinline{Python}|φ|, then
  \mintinline{Python}|φ| would evaluate to the type
  \mintinline{Python}|φ → X|, giving us a bona fide Santa Claus
  sentence. However, \mintinline{Python}|Eval(T % repr(T))| attempts
  to produce the type of functions from \mintinline{Python}|Eval(T %
  repr(T))| to \mintinline{Python}|X| by evaluating
  \mintinline{Python}|Eval(T % repr(T))|.  This throws the function
  \mintinline{Python}|Tarski| into an infinite loop which never
  terminates. (Indeed, choosing \mintinline{Python}|X = ⊥| it's
  trivial to show that there's no way to write
  \mintinline{Python}|Eval| such that \mintinline{Python}|Tarski|
  halts, unless Martin--Lӧf type theory is inconsistent.)

\section{Abstract Syntax Trees for Dependent Type Theory} \label{sec:local-interpretation}

  The idea of formalizing a type of syntax trees which only permits
  well-typed programs is common in the
  literature~\cite{mcbride2010outrageous,Chapman200921,danielsson2006formalisation}.
  For example, here is a very simple (and incomplete) formalization
  with dependent function types ($\Pi$), a unit type (⊤), an empty
  type (⊥), and functions ($\lambda$).

  We will use some standard data type declarations, which are provided
  for completeness in \autoref{sec:common}.
 \AgdaHide{
  \begin{code}
open import common public
  \end{code}
}
\AgdaHide{
  \begin{code}
module dependent-type-theory where
  \end{code}
}

\noindent
\begin{code}
 mutual
  infixl 2 _▻_

  data Context : Set where
   ε : Context
   _▻_ : (Γ : Context) → Type Γ → Context

  data Type : Context → Set where
   ‘⊤’ : ∀ {Γ} → Type Γ
   ‘⊥’ : ∀ {Γ} → Type Γ
   ‘Π’ : ∀ {Γ}
     → (A : Type Γ) → Type (Γ ▻ A) → Type Γ

  data Term : {Γ : Context} → Type Γ → Set where
   ‘tt’ : ∀ {Γ} → Term {Γ} ‘⊤’
   ‘λ’ : ∀ {Γ A B} → Term B → Term {Γ} (‘Π’ A B)
 \end{code}

  An easy way to check consistency of a syntactic theory which is
  weaker than the theory of the ambient proof assistant is to define
  an interpretation function, also commonly known as an unquoter, or a
  denotation function, from the syntax into the universe of types.
  This function gives a semantic model to the syntax.  Here is an
  example of such a function:

\begin{code}
 mutual
  ⟦_⟧ᶜ : Context → Set
  ⟦ ε ⟧ᶜ     = ⊤
  ⟦ Γ ▻ T ⟧ᶜ = Σ ⟦ Γ ⟧ᶜ ⟦ T ⟧ᵀ

  ⟦_⟧ᵀ : ∀ {Γ}
    → Type Γ → ⟦ Γ ⟧ᶜ → Set
  ⟦ ‘⊤’ ⟧ᵀ Γ⇓     = ⊤
  ⟦ ‘⊥’ ⟧ᵀ Γ⇓     = ⊥
  ⟦ ‘Π’ A B ⟧ᵀ Γ⇓ = (x : ⟦ A ⟧ᵀ Γ⇓) → ⟦ B ⟧ᵀ (Γ⇓ , x)

  ⟦_⟧ᵗ : ∀ {Γ T}
    → Term {Γ} T → (Γ⇓ : ⟦ Γ ⟧ᶜ) → ⟦ T ⟧ᵀ Γ⇓
  ⟦ ‘tt’ ⟧ᵗ Γ⇓    = tt
  ⟦ ‘λ’ f ⟧ᵗ Γ⇓ x = ⟦ f ⟧ᵗ (Γ⇓ , x)
\end{code}

  Note that this interpretation function has an essential property
  that we will call \emph{locality}: the interpretation of any given
  constructor does not require doing case analysis on any of its
  arguments.  By contrast, one could imagine an interpretation
  function that interpreted function types differently depending on
  their domain and codomain; for example, one might interpret
  \mintinline{Agda}|(‘⊥’ ‘→’ A)| as \mintinline{Agda}|⊤|, or one might
  interpret an equality type differently at each type, as in
  Observational Type Theory~\cite{Altenkirch:2007:OE:1292597.1292608}.

\section{This Paper}

 In this paper, we make extensive use of this trick for validating
 models.  In \autoref{sec:12-lines}, we formalize the simplest syntax
 that supports Lӧb's theorem and prove it sound relative to Agda in 12
 lines of code; the understanding is that this syntax could be
 extended to support basically anything you might want.  We then
 present in \autoref{sec:extended-trivial} an extended version of this
 solution, which supports enough operations that we can prove our
 syntax sound (consistent), incomplete, and nonempty.  In a hundred
 lines of code, we prove Lӧb's theorem in
 \autoref{sec:100-lines-quine} under the assumption that we are given
 a quine; this is basically the well-typed functional version of the
 program that uses \mintinline{Python}|open(__file__, 'r').read()|.
 After taking a digression for an application of Lӧb's theorem to the
 prisoner's dilemma in \autoref{sec:prisoner}, we sketch in
 \autoref{sec:only-add-quote} our implementation of Lӧb's theorem
 (code in the supplemental material) based on only the assumption that
 we can add a level of quotation to our syntax tree; this is the
 equivalent of letting the compiler implement
 \mintinline{Python}|repr|, rather than implementing it ourselves.  We
 close in \autoref{sec:future-work} with some discussion about avenues
 for removing the hard-coded \mintinline{Python}|repr|.

\section{Prior Work} \label{sec:prior-work-and-new}

 There exist a number of implementations or formalizations of various
 flavors of Lӧb's theorem in the literature.
 \Citeauthor{appel2007very} use Lӧb's theorem as an induction rule for
 program logics in Coq~\cite{appel2007very}.
 \Citeauthor{piponi-from-l-theorem-to-spreadsheet} formalizes a rule
 with the same shape as Lӧb's theorem in Haskell, and uses it for,
 among other things, spreadsheet
 evaluation~\cite{piponi-from-l-theorem-to-spreadsheet}.
 \Citeauthor{SimmonsToninho2012} formalize a constructive provability
 logic in Agda, and prove Lӧb's theorem within that
 logic~\cite{SimmonsToninho2012}.

 Gӧdel's incompleteness theorems, easy corollaries to Lӧb's theorem,
 have been formally verified numerous
 times~\cite{Shankar:1986:PM:913294,shankar1997metamathematics,DBLP:journals/corr/abs-cs-0505034,paulson2015mechanised}.

 To our knowledge, our twelve line proof is the shortest
 self-contained formally verified proof of the admissibility of Lӧb's
 theorem to date.  We are not aware of other formally verified proofs
 of Lӧb's theorem which interpret the modal □ operator as an
 inductively defined type of syntax trees of proofs of a given
 theorem, as we do in this formalization, though presumably the modal
 □ operator \citeauthor{SimmonsToninho2012} could be interpreted as
 such syntax trees.  Finally, we are not aware of other work which
 uses the trick of talking about a local interpretation function (as
 described at the end of \autoref{sec:local-interpretation}) to talk
 about consistent extensions to classes of encodings of type theory.

\section{Trivial Encoding} \label{sec:12-lines}
\AgdaHide{
  \begin{code}
module trivial-encoding where
 infixr 1 _‘→’_
  \end{code}
}

 We begin with a language that supports almost nothing other than
 Lӧb's theorem.  We use \mintinline{Agda}|□ T| to denote the type of
 \mintinline{Agda}|Term|s of whose syntactic type is
 \mintinline{Agda}|T|.  We use \mintinline{Agda}|‘□’ T| to denote the
 syntactic type corresponding to the type of (syntactic) terms whose
 syntactic type is \mintinline{Agda}|T|.  For example, the type of a
 \mintinline{Python}|repr| which operated on syntax trees would be
 \mintinline{Agda}|□ T → □ (‘□’ T)|.

\begin{code}
 data Type : Set where
   _‘→’_ : Type → Type → Type
   ‘□’ : Type → Type

 data □ : Type → Set where
   Lӧb : ∀ {X} → □ (‘□’ X ‘→’ X) → □ X
\end{code}
 The only term supported by our term language is Lӧb's theorem.  We
 can prove this language consistent relative to Agda with an
 interpreter:

\begin{code}
 ⟦_⟧ᵀ : Type → Set
 ⟦ A ‘→’ B ⟧ᵀ = ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ
 ⟦ ‘□’ T ⟧ᵀ   = □ T

 ⟦_⟧ᵗ : ∀ {T : Type} → □ T → ⟦ T ⟧ᵀ
 ⟦ Lӧb □‘X’→X ⟧ᵗ = ⟦ □‘X’→X ⟧ᵗ (Lӧb □‘X’→X)
\end{code}
 To interpret Lӧb's theorem applied to the syntax for a compiler $f$
 (\mintinline{Agda}|□‘X’→X| in the code above), we interpret $f$, and
 then apply this interpretation to the constructor
 \mintinline{Agda}|Lӧb| applied to $f$.

 Finally, we tie it all together:

\begin{code}
 lӧb : ∀ {‘X’} → □ (‘□’ ‘X’ ‘→’ ‘X’) → ⟦ ‘X’ ⟧ᵀ
 lӧb f = ⟦ Lӧb f ⟧ᵗ
\end{code}

 This code is deceptively short, with all of the interesting work
 happening in the interpretation of \mintinline{Agda}|Lӧb|.

 What have we actually proven, here?  It may seem as though we've
 proven absolutely nothing, or it may seem as though we've proven that
 Lӧb's theorem always holds.  Neither of these is the case.  The
 latter is ruled out, for example, by the existence of an
 self-interpreter for
 F$_\omega$~\cite{brown2016breaking}.\footnote{One may wonder how
 exactly the self-interpreter for F$_\omega$ does not contradict this
 theorem.  In private conversations with Matt Brown, we found that the
 F$_\omega$ self-interpreter does not have a separate syntax for
 types, instead indexing its terms over types in the metalanguage.
 This means that the type of Lӧb's theorem becomes either
 \mintinline{Agda}|□ (□ X → X) → □ X|, which is not strictly positive,
 or \mintinline{Agda}|□ (X → X) → □ X|, which, on interpretation, must
 be filled with a general fixpoint operator.  Such an operator is
 well-known to be inconsistent.}

 We have proven the following.  Suppose you have a formalization of
 type theory which has a syntax for types, and a syntax for terms
 indexed over those types.  If there is a ``local explanation'' for
 the system being sound, i.e., an interpretation function where each
 rule does not need to know about the full list of constructors, then
 it is consistent to add a constructor for Lӧb's theorem to your
 syntax.  This means that it is impossible to contradict Lӧb's theorem
 no matter what (consistent) constructors you add.  We will see in the
 next section how this gives incompleteness, and discuss in later
 sections how to \emph{prove Lӧb's theorem}, rather than simply
 proving that it is consistent to assume.

\section{Encoding with Soundness, Incompleteness, and Non-Emptiness} \label{sec:extended-trivial}

 By augmenting our representation with top (\mintinline{Agda}|‘⊤’|)
 and bottom (\mintinline{Agda}|‘⊥’|) types, and a unique inhabitant of
 \mintinline{Agda}|‘⊤’|, we can prove soundness, incompleteness, and
 non-emptiness.

\AgdaHide{
  \begin{code}
module sound-incomplete-nonempty where
 infixr 1 _‘→’_
  \end{code}
}

\begin{code}
 data Type : Set where
  _‘→’_ : Type → Type → Type
  ‘□’ : Type → Type
  ‘⊤’ : Type
  ‘⊥’ : Type

 ---- "□" is sometimes written as "Term"
 data □ : Type → Set where
  Lӧb : ∀ {X} → □ (‘□’ X ‘→’ X) → □ X
  ‘tt’ : □ ‘⊤’

 ⟦_⟧ᵀ : Type → Set
 ⟦ A ‘→’ B ⟧ᵀ = ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ
 ⟦ ‘□’ T ⟧ᵀ   = □ T
 ⟦ ‘⊤’ ⟧ᵀ     = ⊤
 ⟦ ‘⊥’ ⟧ᵀ     = ⊥

 ⟦_⟧ᵗ : ∀ {T : Type} → □ T → ⟦ T ⟧ᵀ
 ⟦ Lӧb □‘X’→X ⟧ᵗ = ⟦ □‘X’→X ⟧ᵗ (Lӧb □‘X’→X)
 ⟦ ‘tt’ ⟧ᵗ = tt

 ‘¬’_ : Type → Type
 ‘¬’ T = T ‘→’ ‘⊥’

 lӧb : ∀ {‘X’} → □ (‘□’ ‘X’ ‘→’ ‘X’) → ⟦ ‘X’ ⟧ᵀ
 lӧb f = ⟦ Lӧb f ⟧ᵗ

 ---- There is no syntactic proof of absurdity
 soundness : ¬ □ ‘⊥’
 soundness x = ⟦ x ⟧ᵗ

 ---- but it would be absurd to have a syntactic
 ---- proof of that fact
 incompleteness : ¬ □ (‘¬’ (‘□’ ‘⊥’))
 incompleteness = lӧb

 ---- However, there are syntactic proofs of some
 ---- things (namely ⊤)
 non-emptiness : □ ‘⊤’
 non-emptiness = ‘tt’

 ---- There are no syntactic interpreters, things
 ---- which, at any type, evaluate code at that
 ---- type to produce its result.
 no-interpreters : ¬ (∀ {‘X’} → □ (‘□’ ‘X’ ‘→’ ‘X’))
 no-interpreters interp = lӧb (interp {‘⊥’})
\end{code}

  What is this incompleteness theorem?  Gӧdel's incompleteness theorem
  is typically interpreted as ``there exist true but unprovable
  statements.''  In intuitionistic logic, this is hardly surprising.
  A more accurate rendition of the theorem in Agda might be ``there
  exist true but inadmissible statements,'' i.e., there are statements
  which are provable meta-theoretically, but which lead to
  (meta-theoretically--provable) inconsistency if assumed at the
  object level.

  This may seem a bit esoteric, so let's back up a bit, and make it
  more concrete.  Let's begin by banishing ``truth''.  Sometimes it is
  useful to formalize a notion of provability.  For example, you might
  want to show neither assuming $T$ nor assuming $¬T$ yields a proof
  of contradiction.  You cannot phrase this is $¬T ∧ ¬¬T$, for that is
  absurd.  Instead, you want to say something like $(¬□T) ∧ ¬□(¬T)$,
  i.e., it would be absurd to have a proof object of either $T$ or of
  $¬T$.  After a while, you might find that meta-programming in this
  formal syntax is nice, and you might want it to be able to formalize
  every proof, so that you can do all of your solving reflectively.
  If you're like us, you might even want to reason about the
  reflective tactics themselves in a reflective manner; you'd want to
  be able to add levels of quotation to quoted things to talk about
  such tactics.

  The incompleteness theorem, then, is this: your reflective system,
  no matter how powerful, cannot formalize every proof.  For any fixed
  language of syntactic proofs which is powerful enough to represent
  itself, there will always be some valid proofs that you cannot
  reflect into your syntax.  In particular, you might be able to prove
  that your syntax has no proofs of ⊥ (by interpreting any such
  proof).  But you'll be unable to quote that proof.  This is what the
  incompleteness theorem stated above says.  Incompleteness,
  fundamentally, is a result about the limitations of formalizing
  provability.

\section{Encoding with Quines} \label{sec:100-lines-quine}

 \AgdaHide{
  \begin{code}
module lob-by-quines where
  \end{code}
}

 We now weaken our assumptions further.  Rather than assuming Lӧb's
 theorem, we instead assume only a type-level quine in our
 representation.  Recall that a \emph{quine} is a program that outputs
 some function of its own source code.  A \emph{type-level quine at ϕ}
 is program that outputs the result of evaluating the function ϕ on
 the abstract syntax tree of its own type.  Letting
 \mintinline{Agda}|Quine ϕ| denote the constructor for a type-level
 quine at ϕ, we have an isomorphism between \mintinline{Agda}|Quine ϕ|
 and \mintinline{Agda}|ϕ ⌜ Quine ϕ ⌝ᵀ|, where
 \mintinline{Agda}|⌜ Quine ϕ ⌝ᵀ| is the abstract syntax tree for the
 source code of \mintinline{Agda}|Quine ϕ|.  Note that we assume
 constructors for ``adding a level of quotation'', turning abstract
 syntax trees for programs of type $T$ into abstract syntax trees for
 abstract syntax trees for programs of type $T$; this corresponds to
 \mintinline{Python}|repr|.

\AgdaHide{
\begin{code}
 infixl 3 _‘’ₐ_
 infixl 3 _w‘‘’’ₐ_
 infixl 3 _‘’_
 infixl 2 _▻_
 infixr 2 _‘∘’_
 infixr 1 _‘→’_
\end{code}
}

 We begin with an encoding of contexts and types, repeating from above
 the constructors of ‘→’, ‘□’, ‘⊤’, and ‘⊥’.  We add to this a
 constructor for quines (\mintinline{Agda}|Quine|), and a constructor
 for syntax trees of types in the empty context (‘Typeε’).  Finally,
 rather than proving weakening and substitution as mutually recursive
 definitions, we take the easier but more verbose route of adding
 constructors that allow adding and substituting extra terms in the
 context. Note that ‘□’ is now a function of the represented language,
 rather than a meta-level operator.

% \todo{Does this need more explanation?}
% \todo{\cite{mcbride2010outrageous}}

 Note that we use the infix operator \mintinline{Agda}|_‘’_| to denote
 substitution.

\begin{code}
 mutual
  data Context : Set where
   ε : Context
   _▻_ : (Γ : Context) → Type Γ → Context

  data Type : Context → Set where
   _‘→’_ : ∀ {Γ} → Type Γ → Type Γ → Type Γ
   ‘⊤’ : ∀ {Γ} → Type Γ
   ‘⊥’ : ∀ {Γ} → Type Γ
   ‘Typeε’ : ∀ {Γ} → Type Γ
   ‘□’ : ∀ {Γ} → Type (Γ ▻ ‘Typeε’)
   Quine : Type (ε ▻ ‘Typeε’) → Type ε
   W : ∀ {Γ A}
     → Type Γ → Type (Γ ▻ A)
   W₁ : ∀ {Γ A B}
     → Type (Γ ▻ B) → Type (Γ ▻ A ▻ (W B))
   _‘’_ : ∀ {Γ A}
     → Type (Γ ▻ A) → Term A → Type Γ
\end{code}

  In addition to ‘λ’ and ‘tt’, we now have the AST-equivalents of
  Python's \mintinline{Python}|repr|, which we denote as
  \mintinline{Agda}|⌜_⌝ᵀ| for the type-level add-quote function, and
  \mintinline{Agda}|⌜_⌝ᵗ| for the term-level add-quote function.  We
  add constructors \mintinline{Agda}|quine→| and
  \mintinline{Agda}|quine←| that exhibit the isomorphism that defines
  our type-level quine constructor, though we elide a constructor
  declaring that these are inverses, as we found it unnecessary.

  To construct the proof of Lӧb's theorem, we need a few other
  standard constructors, such as \mintinline{Agda}|‘VAR₀’|, which
  references a term in the context; \mintinline{Agda}|_‘’ₐ_|, which we
  use to denote function application; \mintinline{Agda}|_‘∘’_|, a
  function composition operator; and \mintinline{Agda}|‘⌜‘VAR₀’⌝ᵗ’|,
  the variant of \mintinline{Agda}|‘VAR₀’| which adds an extra level
  of syntax-trees. We also include a number of constructors that
  handle weakening and substitution; this allows us to avoid both
  inductive-recursive definitions of weakening and substitution, and
  avoid defining a judgmental equality or conversion relation.

\begin{code}
  data Term : {Γ : Context} → Type Γ → Set where
   ‘λ’ : ∀ {Γ A B}
     → Term {Γ ▻ A} (W B) → Term (A ‘→’ B)
   ‘tt’ : ∀ {Γ}
     → Term {Γ} ‘⊤’
   ⌜_⌝ᵀ : ∀ {Γ} ---- type-level repr
     → Type ε
     → Term {Γ} ‘Typeε’
   ⌜_⌝ᵗ : ∀ {Γ T} ---- term-level repr
     → Term {ε} T
     → Term {Γ} (‘□’ ‘’ ⌜ T ⌝ᵀ)
   quine→ : ∀ {ϕ}
     → Term {ε} (Quine ϕ           ‘→’ ϕ ‘’ ⌜ Quine ϕ ⌝ᵀ)
   quine← : ∀ {ϕ}
     → Term {ε} (ϕ ‘’ ⌜ Quine ϕ ⌝ᵀ ‘→’ Quine ϕ)
   ---- The constructors below here are for
   ---- variables, weakening, and substitution
   ‘VAR₀’ : ∀ {Γ T}
     → Term {Γ ▻ T} (W T)
   _‘’ₐ_ : ∀ {Γ A B}
    → Term {Γ} (A ‘→’ B)
    → Term {Γ} A
    → Term {Γ} B
   _‘∘’_ : ∀ {Γ A B C}
    → Term {Γ} (B ‘→’ C)
    → Term {Γ} (A ‘→’ B)
    → Term {Γ} (A ‘→’ C)
   ‘⌜‘VAR₀’⌝ᵗ’ : ∀ {T}
     → Term {ε ▻ ‘□’ ‘’ ⌜ T ⌝ᵀ}
            (W (‘□’ ‘’ ⌜ ‘□’ ‘’ ⌜ T ⌝ᵀ ⌝ᵀ))
   →SW₁SV→W : ∀ {Γ T X A B} {x : Term {Γ} X}
     → Term (T ‘→’ (W₁ A ‘’ ‘VAR₀’ ‘→’ W B) ‘’ x)
     → Term (T ‘→’ A ‘’ x ‘→’ B)
   ←SW₁SV→W : ∀ {Γ T X A B} {x : Term {Γ} X}
     → Term ((W₁ A ‘’ ‘VAR₀’ ‘→’ W B) ‘’ x ‘→’ T)
     → Term ((A ‘’ x ‘→’ B) ‘→’ T)
   w : ∀ {Γ A T} → Term A → Term {Γ ▻ T} (W A)
   w→ : ∀ {Γ A B X}
    → Term {Γ} (A ‘→’ B)
    → Term {Γ ▻ X} (W A ‘→’ W B)
   _w‘‘’’ₐ_ : ∀ {A B T}
    → Term {ε ▻ T} (W (‘□’ ‘’ ⌜ A ‘→’ B ⌝ᵀ))
    → Term {ε ▻ T} (W (‘□’ ‘’ ⌜ A ⌝ᵀ))
    → Term {ε ▻ T} (W (‘□’ ‘’ ⌜ B ⌝ᵀ))

 □ : Type ε → Set _
 □ = Term {ε}
\end{code}

 To verify the soundness of our syntax, we provide a model for it and
 an interpretation into that model.  We call particular attention to
 the interpretation of \mintinline{Agda}|‘□’|, which is just
 \mintinline{Agda}|Term {ε}|; to \mintinline{Agda}|Quine ϕ|, which is
 the interpretation of \mintinline{Agda}|ϕ| applied to
 \mintinline{Agda}|Quine ϕ|; and to the interpretations of the quine
 isomorphism functions, which are just the identity functions.

\begin{code}
 max-level : Level
 max-level = lzero   ---- also works for higher levels

 mutual
  ⟦_⟧ᶜ : (Γ : Context) → Set (lsuc max-level)
  ⟦ ε ⟧ᶜ  = ⊤
  ⟦ Γ ▻ T ⟧ᶜ = Σ ⟦ Γ ⟧ᶜ ⟦ T ⟧ᵀ

  ⟦_⟧ᵀ : ∀ {Γ}
    → Type Γ → ⟦ Γ ⟧ᶜ → Set max-level
  ⟦ ‘Typeε’ ⟧ᵀ Γ⇓ = Lifted (Type ε)
  ⟦ ‘□’ ⟧ᵀ Γ⇓ = Lifted (Term {ε} (lower (snd Γ⇓)))
  ⟦ Quine ϕ ⟧ᵀ Γ⇓ = ⟦ ϕ ⟧ᵀ (Γ⇓ , lift (Quine ϕ))
  ---- The rest of the type-level interpretations
  ---- are the obvious ones, if a bit obscured by
  ---- carrying around the context.
  ⟦ A ‘→’ B ⟧ᵀ Γ⇓ = ⟦ A ⟧ᵀ Γ⇓ → ⟦ B ⟧ᵀ Γ⇓
  ⟦ ‘⊤’ ⟧ᵀ Γ⇓ = ⊤
  ⟦ ‘⊥’ ⟧ᵀ Γ⇓ = ⊥
  ⟦ W T ⟧ᵀ Γ⇓ = ⟦ T ⟧ᵀ (fst Γ⇓)
  ⟦ W₁ T ⟧ᵀ Γ⇓ = ⟦ T ⟧ᵀ (fst (fst Γ⇓) , snd Γ⇓)
  ⟦ T ‘’ x ⟧ᵀ Γ⇓ = ⟦ T ⟧ᵀ (Γ⇓ , ⟦ x ⟧ᵗ Γ⇓)

  ⟦_⟧ᵗ : ∀ {Γ T}
    → Term {Γ} T → (Γ⇓ : ⟦ Γ ⟧ᶜ) → ⟦ T ⟧ᵀ Γ⇓
  ⟦ ⌜ x ⌝ᵀ ⟧ᵗ Γ⇓ = lift x
  ⟦ ⌜ x ⌝ᵗ ⟧ᵗ Γ⇓ = lift x
  ⟦ quine→ ⟧ᵗ Γ⇓ x = x
  ⟦ quine← ⟧ᵗ Γ⇓ x = x
  ---- The rest of the term-level interpretations
  ---- are the obvious ones, if a bit obscured by
  ---- carrying around the context.
  ⟦ ‘λ’ f ⟧ᵗ Γ⇓ x = ⟦ f ⟧ᵗ (Γ⇓ , x)
  ⟦ ‘tt’ ⟧ᵗ  Γ⇓ = tt
  ⟦ ‘VAR₀’ ⟧ᵗ Γ⇓ = snd Γ⇓
  ⟦ ‘⌜‘VAR₀’⌝ᵗ’ ⟧ᵗ Γ⇓ = lift ⌜ lower (snd Γ⇓) ⌝ᵗ
  ⟦ g ‘∘’ f ⟧ᵗ Γ⇓ x = ⟦ g ⟧ᵗ Γ⇓ (⟦ f ⟧ᵗ Γ⇓ x)
  ⟦ f ‘’ₐ x ⟧ᵗ Γ⇓ = ⟦ f ⟧ᵗ Γ⇓ (⟦ x ⟧ᵗ Γ⇓)
  ⟦ ←SW₁SV→W f ⟧ᵗ = ⟦ f ⟧ᵗ
  ⟦ →SW₁SV→W f ⟧ᵗ = ⟦ f ⟧ᵗ
  ⟦ w x ⟧ᵗ Γ⇓ = ⟦ x ⟧ᵗ (fst Γ⇓)
  ⟦ w→ f ⟧ᵗ Γ⇓ = ⟦ f ⟧ᵗ (fst Γ⇓)
  ⟦ f w‘‘’’ₐ x ⟧ᵗ Γ⇓
    = lift (lower (⟦ f ⟧ᵗ Γ⇓) ‘’ₐ lower (⟦ x ⟧ᵗ Γ⇓))
\end{code}

 To prove Lӧb's theorem, we must create the sentence ``if this
 sentence is provable, then $X$'', and then provide and inhabitant of
 that type.  We can define this sentence, which we call
 \mintinline{Agda}|‘H’|, as the type-level quine at the function
 $\lambda v.\ □ v → ‘X’$.  We can then convert back and forth between
 the types \mintinline{Agda}|□ ‘H’| and \mintinline{Agda}|□ ‘H’ → ‘X’|
 with our quine isomorphism functions, and a bit of quotation magic
 and function application gives us a term of type
 \mintinline{Agda}|□ ‘H’ → □ ‘X’|; this corresponds to the inference
 of the provability of Santa Claus' existence from the assumption that
 the sentence is provable.  We compose this with the assumption of
 Lӧb's theorem, that \mintinline{Agda}|□ ‘X’ → ‘X’|, to get a term of
 type \mintinline{Agda}|□ ‘H’ → ‘X’|, i.e., a term of type
 \mintinline{Agda}|‘H’|; this is the inference that when provability
 implies truth, Santa Claus exists, and hence that the sentence is
 provable.  Finally, we apply this to its own quotation, obtaining a
 term of type \mintinline{Agda}|□ ‘X’|, i.e., a proof that Santa Claus
 exists.

\begin{code}
 module inner (‘X’ : Type ε)
              (‘f’ : Term {ε} (‘□’ ‘’ ⌜ ‘X’ ⌝ᵀ ‘→’ ‘X’))
        where
  ‘H’ : Type ε
  ‘H’ = Quine (W₁ ‘□’ ‘’ ‘VAR₀’ ‘→’ W ‘X’)

  ‘toH’ : □ ((‘□’ ‘’ ⌜ ‘H’ ⌝ᵀ ‘→’ ‘X’) ‘→’ ‘H’)
  ‘toH’ = ←SW₁SV→W quine←

  ‘fromH’ : □ (‘H’ ‘→’ (‘□’ ‘’ ⌜ ‘H’ ⌝ᵀ ‘→’ ‘X’))
  ‘fromH’ = →SW₁SV→W quine→

  ‘□‘H’→□‘X’’ : □ (‘□’ ‘’ ⌜ ‘H’ ⌝ᵀ ‘→’ ‘□’ ‘’ ⌜ ‘X’ ⌝ᵀ)
  ‘□‘H’→□‘X’’
    = ‘λ’ (w ⌜ ‘fromH’ ⌝ᵗ
          w‘‘’’ₐ ‘VAR₀’
          w‘‘’’ₐ ‘⌜‘VAR₀’⌝ᵗ’)

  ‘h’ : Term ‘H’
  ‘h’ = ‘toH’ ‘’ₐ (‘f’ ‘∘’ ‘□‘H’→□‘X’’)

  Lӧb : □ ‘X’
  Lӧb = ‘fromH’ ‘’ₐ ‘h’ ‘’ₐ ⌜ ‘h’ ⌝ᵗ

 Lӧb : ∀ {X} → □ (‘□’ ‘’ ⌜ X ⌝ᵀ ‘→’ X) → □ X
 Lӧb {X} f = inner.Lӧb X f

 ⟦_⟧ : Type ε → Set _
 ⟦ T ⟧ = ⟦ T ⟧ᵀ tt

 ‘¬’_ : ∀ {Γ} → Type Γ → Type Γ
 ‘¬’ T = T ‘→’ ‘⊥’

 lӧb : ∀ {‘X’} → □ (‘□’ ‘’ ⌜ ‘X’ ⌝ᵀ ‘→’ ‘X’) → ⟦ ‘X’ ⟧
 lӧb f = ⟦_⟧ᵗ (Lӧb f) tt
\end{code}

 As above, we can again prove soundness, incompleteness, and non-emptiness.

\begin{code}
 incompleteness : ¬ □ (‘¬’ (‘□’ ‘’ ⌜ ‘⊥’ ⌝ᵀ))
 incompleteness = lӧb

 soundness : ¬ □ ‘⊥’
 soundness x = ⟦ x ⟧ᵗ tt

 non-emptiness : Σ (Type ε) (λ T → □ T)
 non-emptiness = ‘⊤’ , ‘tt’

\end{code}

\section{Digression: Application of Quining to The Prisoner's Dilemma} \label{sec:prisoner}

  In this section, we use a slightly more enriched encoding of syntax;
  see \autoref{sec:prisoners-dilemma-lob-encoding} for details.

\AgdaHide{
  \begin{code}
module prisoners-dilemma where
 open import prisoners-dilemma-lob public
  \end{code}
}

  \subsection{The Prisoner's Dilemma}

    The Prisoner's Dilemma is a classic problem in game theory.  Two
    people have been arrested as suspects in a crime and are being
    held in solitary confinement, with no means of communication.  The
    investigators offer each of them a plea bargain: a decreased
    sentence for ratting out the other person.  Each suspect can then
    choose to either cooperate with the other suspect by remaining
    silent, or defect by ratting out the other suspect.  The possible
    outcomes are summarized in~\autoref{tab:prisoner-payoff}.

\begin{table}
\begin{center}
\begin{tabular}{c|cc}
\backslashbox{$B$ Says}{$A$ Says} & Cooperate & Defect \\ \hline
Cooperate & (1 year, 1 year) & (0 years, 3 years) \\
Defect & (3 years, 0 years) & (2 years, 2 years)
\end{tabular}
\caption{The payoff matrix for the prisoner's dilemma; each cell contains (the years $A$ spends in prison, the years $B$ spends in prison).} \label{tab:prisoner-payoff}
\end{center}
\end{table}

    Suspect $A$ might reason thusly: ``Suppose the other suspect
    cooperates with me.  Then I'd get off with no prison time if I
    defected, while I'd have to spend a year in prison if I cooperate.
    Similarly, if the other suspect defects, then I'd get two years in
    prison for defecting, and three for cooperating.  In all cases, I
    do better by defecting.''  If suspect $B$ reasons similarly, then
    both decide to defect, and both get two years in prison, despite
    the fact that both prefer the (Cooperate, Cooperate) outcome over
    the (Defect, Defect) outcome!

  \subsection{Adding Source Code}

    We have the intuition that if both suspects are good at reasoning,
    and both know that they'll reason the same way, then they should
    be able to mutually cooperate.  One way to formalize this is to
    talk about programs (rather than people) playing the prisoner's
    dilemma, and to allow each program access to its own source code
    and its opponent's source
    code~\cite{BaraszChristianoFallensteinEtAl2014}.

    We have formalized this framework in Agda: we use
    \mintinline{Agda}|‘Bot’| to denote the type of programs that can
    play in such a prisoner's dilemma; each one takes in source code
    for two \mintinline{Agda}|‘Bot’|s and outputs a proposition which
    is true (a type which is inhabited) if and only if it cooperates
    with its opponent.  Said another way, the output of each bot is a
    proposition describing the assertion that it cooperates with its
    opponent.

\begin{code}
 open lob

 ---- ‘Bot’ is defined as the fixed point of
 ---- ‘Bot’
 ----   ↔ (Term ‘Bot’ → Term ‘Bot’ → ‘Type’)
 ‘Bot’ : ∀ {Γ} → Type Γ
 ‘Bot’ {Γ}
   = Quine (W₁ ‘Term’ ‘’ ‘VAR₀’
            ‘→’ W₁ ‘Term’ ‘’ ‘VAR₀’
            ‘→’ W (‘Type’ Γ))
\end{code}

  To construct an executable bot, we could do a bounded search for
  proofs of this proposition; one useful method described in
  \cite{BaraszChristianoFallensteinEtAl2014} is to use Kripke frames.
  This computation is, however, beyond the scope of this paper.

  The assertion that a bot \mintinline{Agda}|b₁| cooperates with a bot
  \mintinline{Agda}|b₂| is the result of interpreting the source code
  for the bot, and feeding the resulting function the source code for
  \mintinline{Agda}|b₁| and \mintinline{Agda}|b₂|.

\begin{code}
 ---- N.B. "□" means "Term {ε}", i.e., a term in
 ---- the empty context
 _cooperates-with_ : □ ‘Bot’ → □ ‘Bot’ → Type ε
 b₁ cooperates-with b₂ = lower (⟦ b₁ ⟧ᵗ tt (lift b₁) (lift b₂))
\end{code}

  We now provide a convenience constructor for building bots, based on
  the definition of quines, and present three relatively simple bots:
  DefectBot, CooperateBot, and FairBot.

\begin{code}
 make-bot : ∀ {Γ}
   → Term {Γ ▻ ‘□’ ‘Bot’ ▻ W (‘□’ ‘Bot’)}
          (W (W (‘Type’ Γ)))
   → Term {Γ} ‘Bot’
 make-bot t
   = ←SW₁SV→SW₁SV→W
     quine← ‘’ₐ ‘λ’ (→w (‘λ’ t))

 ‘DefectBot’    : □ ‘Bot’
 ‘CooperateBot’ : □ ‘Bot’
 ‘FairBot’      : □ ‘Bot’
\end{code}

  The first two bots are very simple: DefectBot never cooperates (the
  assertion that DefectBot cooperates is a contradiction), while
  CooperateBot always cooperates.  We define these bots, and prove
  that DefectBot never cooperates and CooperateBot always cooperates.

\begin{code}
 ‘DefectBot’    = make-bot (w (w ⌜ ‘⊥’ ⌝ᵀ))
 ‘CooperateBot’ = make-bot (w (w ⌜ ‘⊤’ ⌝ᵀ))

 DB-defects : ∀ {b}
   → ¬ ⟦ ‘DefectBot’ cooperates-with b ⟧
 DB-defects {b} pf = pf

 CB-cooperates : ∀ {b}
   → ⟦ ‘CooperateBot’ cooperates-with b ⟧
 CB-cooperates {b} = tt
\end{code}

  We can do better than DefectBot, though, now that we have source
  code.  FairBot cooperates with you if and only if it can find a
  proof that you cooperate with FairBot.  By Lӧb's theorem, to prove
  that FairBot cooperates with itself, it suffices to prove that if
  there is a proof that FairBot cooperates with itself, then FairBot
  does, in fact, cooperate with itself.  This is obvious, though:
  FairBot decides whether or not to cooperate with itself by searching
  for a proof that it does, in fact, cooperate with itself.

  To define FairBot, we first define what it means for the other bot
  to cooperate with some particular bot.

\begin{code}
 ---- We can "evaluate" a bot to turn it into a
 ---- function accepting the source code of two
 ---- bots.
 ‘eval-bot’ : ∀ {Γ}
   → Term {Γ} (‘Bot’
              ‘→’ (‘□’ ‘Bot’ ‘→’ ‘□’ ‘Bot’ ‘→’ ‘Type’ Γ))
 ‘eval-bot’ = →SW₁SV→SW₁SV→W quine→

 ---- We can quote this, and get a function that
 ---- takes the source code for a bot, and
 ---- outputs the source code for a function that
 ---- takes (the source code for) that bot's
 ---- opponent, and returns an assertion of
 ---- cooperation with that opponent
 ‘‘eval-bot’’ : ∀ {Γ}
   → Term {Γ} (‘□’ ‘Bot’
     ‘→’ ‘□’ ({- other -} ‘□’ ‘Bot’ ‘→’ ‘Type’ Γ))
 ‘‘eval-bot’’
   = ‘λ’ (w ⌜ ‘eval-bot’ ⌝ᵗ
         w‘‘’’ₐ ‘VAR₀’
         w‘‘’’ₐ ‘⌜‘VAR₀’⌝ᵗ’)

 ---- The assertion "our opponent cooperates with
 ---- a bot b" is equivalent to the evaluation of
 ---- our opponent, applied to b.  Most of the
 ---- noise in this statement is manipulation of
 ---- weakening and substitution.
 ‘other-cooperates-with’ : ∀ {Γ}
   → Term {Γ
      ▻ ‘□’ ‘Bot’
      ▻ W (‘□’ ‘Bot’)}
     (W (W (‘□’ ‘Bot’)) ‘→’ W (W (‘□’ (‘Type’ Γ))))
 ‘other-cooperates-with’ {Γ}
   = ‘eval-other'’
     ‘∘’ w→ (w (w→ (w (‘λ’ ‘⌜‘VAR₀’⌝ᵗ’))))
  where
   ‘eval-other’
     : Term {Γ ▻ ‘□’ ‘Bot’ ▻ W (‘□’ ‘Bot’)}
            (W (W (‘□’ (‘□’ ‘Bot’ ‘→’ ‘Type’ Γ))))
   ‘eval-other’
     = w→ (w (w→ (w ‘‘eval-bot’’))) ‘’ₐ ‘VAR₀’

   ‘eval-other'’
     : Term (W (W (‘□’ (‘□’ ‘Bot’)))
             ‘→’ W (W (‘□’ (‘Type’ Γ))))
   ‘eval-other'’
     = ww→ (w→ (w (w→ (w ‘‘’ₐ’))) ‘’ₐ ‘eval-other’)

 ---- A bot gets its own source code as the first
 ---- argument (of two)
 ‘self’ : ∀ {Γ}
   → Term {Γ ▻ ‘□’ ‘Bot’ ▻ W (‘□’ ‘Bot’)}
          (W (W (‘□’ ‘Bot’)))
 ‘self’ = w ‘VAR₀’

 ---- A bot gets its opponent's source code as
 ---- the second argument (of two)
 ‘other’ : ∀ {Γ}
   → Term {Γ ▻ ‘□’ ‘Bot’ ▻ W (‘□’ ‘Bot’)}
          (W (W (‘□’ ‘Bot’)))
 ‘other’ = ‘VAR₀’

 ---- FairBot is the bot that cooperates iff its
 ---- opponent cooperates with it
 ‘FairBot’
   = make-bot (‘‘□’’ (‘other-cooperates-with’ ‘’ₐ ‘self’))
\end{code}

  We leave the proof that this formalization of FairBot cooperates
  with itself as an exercise for the reader. In
  \autoref{sec:fair-bot-self-cooperates}, we present an alternative
  formalization with a simple proof that FairBot cooperates with
  itself, but with no general definition of the type of bots; we
  relegate this code to an appendix so as to not confuse the reader by
  introducing a different way of handling contexts and weakening in
  the middle of this paper.

\section{Encoding with an Add-Quote Function} \label{sec:only-add-quote}

  Now we return to our proving of Lӧb's theorem.  Included in the
  artifact for this paper\footnote{In \texttt{lob-build-quine.lagda}.}
  is code that replaces the \mintinline{Agda}|Quine| constructor with
  simpler constructors.  Because the lack of β-reduction in the syntax
  clouds the main points and makes the code rather verbose, we do not
  include the code in the paper, and instead describe the most
  interesting and central points.

  Recall our Python quine from \autoref{sec:python-quine}:
\begin{minted}[gobble=1]{Python}
 (lambda T: Π(□(T % repr(T)), X))
  ('(lambda T: Π(□(T %% repr(T)), X))\n (%s)')
\end{minted}

  To translate this into Agda, we need to give a type to
  \mintinline{Agda}|T|. Clearly, \mintinline{Agda}|T| needs to be of
  type \mintinline{Agda}|Type ???| for some context
  \mintinline{Agda}|???|.  Since we need to be able to substitute
  something into that context, we must have
  \mintinline{Agda}|T : Type (Γ ▻ ???)|, i.e., \mintinline{Agda}|T|
  must be a syntax tree for a type, with a hole in it.

  What's the shape of the thing being substituted?  Well, it's a
  syntax tree for a type with a hole in it.  What shape does that hole
  have?  The shape is that of a syntax tree with a hole in
  it\ldots\space Uh-oh.  Our quine's type, na\"ively, is infinite!

  We know of two ways to work around this.  Classical mathematics,
  which uses Gӧdel codes instead of abstract syntax trees, uses an
  untyped representation of proofs.  It's only later in the proof of
  Lӧb's theorem that a notion of a formula being ``well-formed'' is
  introduced.

  Here, we describe an alternate approach.  Rather than giving up
  types all-together, we can ``box'' the type of the hole, to hide it.
  Using \mintinline{Agda}|fst| and \mintinline{Agda}|snd| to denote
  projections from a Σ type, using \mintinline{Agda}|⌜ A ⌝| to denote
  the abstract syntax tree for \mintinline{Agda}|A|,\footnote{Note
  that \mintinline{Agda}|⌜_⌝| would not be a function in the language,
  but a meta-level operation.} and using \mintinline{Agda}|%s| to
  denote the first variable in the context (written as
  \mintinline{Agda}|‘VAR₀’| in previous formalizations above), we can
  write:

  \begin{minted}[gobble=1]{Agda}
 dummy : Type (ε ▻ ⌜Σ Context Type⌝)
 repr : Σ Context Type → Term {ε} ⌜Σ Context Type⌝

 cast-fst
   : Σ Context Type → Type (ε ▻ ⌜Σ Context Type⌝)
 cast-fst (ε ▻ ⌜Σ Context Type⌝ , T) = T
 cast-fst (_ , _) = dummy

 LӧbSentence : Type ε
 LӧbSentence
   = (λ (T : Σ Context Type)
        → □ (cast-fst T % repr T) ‘→’ X)
       ( ε ▻ ⌜Σ Context Type⌝
       , ⌜ (λ (T : Σ Context Type)
              → □ (cast-fst T % repr T) ‘→’ X)
             (%s) ⌝
  \end{minted}

  In this pseudo-Agda code, \mintinline{Agda}|cast-fst| unboxes the
  sentence that it gets, and returns it if it is the right type.
  Since the sentence is, in fact, always the right type, what we do in
  the other cases doesn't matter.

  Summing up, the key ingredients to this construction are:
  \begin{itemize}

    \item A type of syntactic terms indexed over a type of syntactic
      types (and contexts)

    \item Decidable equality on syntactic contexts at a particular
      point (in particular, at \mintinline{Agda}|Σ Context Type|),
      with appropriate reduction on equal things

    \item Σ types, projections, and appropriate reduction on their
      projections

    \item Function types

    \item A function \mintinline{Agda}|repr| which adds a level of
      quotation to any syntax tree

    \item Syntax trees for all of the above

  \end{itemize}

  In any formalization of dependent type theory with all of these
  ingredients, we can prove Lӧb's theorem.

\section{Conclusion} \label{sec:future-work}

  What remains to be done is formalizing Martin--Lӧf type theory
  without assuming \mintinline{Agda}|repr| and without assuming a
  constructor for the type of syntax trees
  (\mintinline{Agda}|‘Context’|, \mintinline{Agda}|‘Type’|, and
  \mintinline{Agda}|‘Term’| or \mintinline{Agda}|‘□’| in our
  formalizations).  We would instead support inductive types, and
  construct these operators as inductive types and as folds over
  inductive types.

  If you take away only three things from this paper, take away these:
  \begin{enumerate}
    \item There will always be some true things which are not possible
      to say, no matter how good you are at talking in type theory
      about type theory.

    \item Giving meaning to syntax in a way that doesn't use cases
      inside cases allows you to talk about when it's okay to add new
      syntax.

    % \todo{Find an Up-Goer Five way to say "syntax" that doesn't give away the game}

    \item If believing in something is enough to make it true, then
      it already is.  Dream big.
  \end{enumerate}

\appendix
\input{./common.tex}
\input{./prisoners-dilemma-lob.tex}
\AgdaHide{
  \begin{code}
import fair-bot-self-cooperates
  \end{code}
}
\input{./fair-bot-self-cooperates.tex}
%\input{./lob-build-quine.tex}
\inputacknowledgements

%\printbibliography
\bibliographystyle{abbrvnat}
\bibliography{lob}

\end{document}