\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}