Proof Term Assignments and Intuitionistic Truth.

In 1994, Per Martin-Löf wrote Analytic and Synthetic Judgement in Type Theory, in which he convincingly showed that undecidability phenomena should be understood in terms of synthetic judgement, and demonstrated how the judgements of one theory may be made the propositions of another.

To be more precise, he considers a theory with conjunction and implication, and a single judgement:

\[P\ \text{true}\quad(A_1\ \text{true},A_2\ \text{true},\dots,A_{n-1}\ \text{true},A_n\ \text{true})\]

And the meaning of this judgement is “\(P\) is true under the assumptions \(A_1\) through \(A_n\)”.

This judgement is then given truth conditions across the propositions by the usual inference rules, a few of which look like this:

\[\begin{gather*} \dfrac{ Q\ \text{true}\quad (P\ \text{true}) }{ P\supset Q\ \text{true} }\supset\text{I}\\ % \dfrac{ P\ \text{true}\quad Q\ \text{true} }{ P\mathop{\&}Q\ \text{true} }\&\text{I} \end{gather*}\]

Now then, for any \(A,B\) we can prove the proposition \(A\supset(B\supset A\mathop{\&}B)\) in terms of these inference rules as follows:

\[ \dfrac{ \dfrac{ \dfrac{ \dfrac{}{A\ \text{true}\quad(A\ \text{true}, B\ \text{true})}\text{hyp}_2 \quad \dfrac{}{B\ \text{true}\quad(A\ \text{true}, B\ \text{true})}\text{hyp}_1 }{ A\mathop{\&}B\ \text{true}\quad(A\ \text{true}, B\ \text{true}) }\mathop{\&}\text{I} }{ B\supset A\mathop{\&}B\ \text{true}\quad(A\ \text{true}) }\supset\text{I} }{ A\supset(B\supset A\mathop{\&}B)\ \text{true} }\supset\text{I} \]

But it’s important to note that the premises and conclusions which occur between the horizontal lines are not essential to the structure of the proof: these are book-keeping. The data of the proof is the minimum whence we could derive this tree. So we could just as well write the proof like this:

\[ \supset\text{I}(A;B\supset A\mathop{\&}B; x. \supset\text{I}(B;A\mathop{\&}B;y. \&\text{I}(A;B;x;y))) \]

And in fact, we could even construct a proof theory around our logic with one form of judgement:

\[M : P \quad(x_1:A_1,x_2:A_2,\dots,x_{n-1}:A_{n-1},x_n:A_n)\]

And the meaning of this judgement is “\(M\) is a proof of \(P\) under the assumption that \(x_1\) through \(x_n\) are proofs of \(A_1\) through \(A_n\) respectively”. Here we will have rules like the following:

\[\begin{gather*} \dfrac{M:B\quad (x:A)}{\supset\text{I}(A;B;x.M):A\supset B}\supset\text{I} \end{gather*}\]

Now, note that we are calling this rule \(\supset\text{I}\), but that symbol is overloaded to denote a few things: it is the name of the implication introduction rule in the original logic, and it is part of the syntax of this proof term of assignment. In order to avoid confusing ourselves, we could rename the proof term \(\supset\text{I}(A;B;x.M)\) to \(\lambda(A;B;x.M)\), and \(\&\text{I}(A;B;M;N)\) to \(\mathsf{pair}(A;B;M;N)\). Then we’d have

\[\begin{gather*} \dfrac{M:B\quad (x:A)}{\lambda(A;B;x.M):A\supset B}\supset\text{I}\\ \dfrac{M:A\quad N:B}{\mathsf{pair}(A;B;M;N):A\mathop{\&}B}\&\text{I} \end{gather*}\]

But now, this is starting to look sort of like a lambda calculus. It turns out that the proof theory of the logic is indeed a monomorphic theory of types: these annotated lambda terms are simply another notation for the proof trees, nothing more.

two notions of propositions-as-types

This seems pretty straight-forward for many users of programming languages: but lost in the enthusiasm for the “Curry-Howard Correspondence” is the distinction between two very different notions of propositions-as-types: there is the syntactic correspondence, which we have observed above, and then the semantic correspondence, which is quite different.

syntactic propositions-as-types

The syntactic correspondence really holds quite on the nose: the formal proofs/derivations for the logic really are precisely the terms of this monomorphic lambda calculus, and the \(M:A\) judgement captures the idea that in a formal system, you should be able to decide when \(M\) is a proof of \(A\) simply by examining \(M\); this is to say, the judgement \(M:A\) is analytic.

Now, on the other hand, in the conception of Brouwer, “proof” was not about a sequence of well-formed formulas in a formal system. The kind of proof the intuitionist is interested in is not an algebraic game, but rather the characterization of the computations which may realize the truth of a proposition. For instance, let us consider the proof term assignment to intuitionistic predicate logic with equality and a universe, which is essentially Martin-Löf’s Intensional Type Theory; then the following judgement is evidently true:

\[ \lambda(\mathsf{Id}(\mathbb{U};\mathbf{1};\mathbf{0}); \mathbf{0}; p.\mathsf{coerce}(\mathbb{1};\mathbb{0};p;\bullet)) : \mathsf{Id}(\mathbb{U};\mathbf{1};\mathbf{0})\supset\mathbf{0} \]

This is a formal proof, but not the kind of proof that interests an intuitionist.

semantic propositions-as-types

Now, the latter notion of proof is captured by Martin-Löf’s meaning explanations and their metamathematical counterpart, the realizability interpretation. And whilst we asserted the validity of formal proofs with the judgement \(M:A\) we will use the judgement \(M\in A\) to assert that \(M\) is an element of \(A\), or \(M\) realizes \(A\); another notation is \(M\Vdash A\).

The meaning of the judgement \(P\supset Q\ \text{true}\) is

“If you know that \(Q\ \text{true}\) under the assumption that \(P\ \text{true}\), then you know that \(P\supset Q\ \text{true}\).”

However, the meaning explanation for the judgement \(M\in A\supset B\) is

\(M\) is (evaluates to a term) in the form \(\lambda(x. b(x))\) where we know \(b(x) \in B\) under the assumption \((x\in A).\)

Note that the term assignment under the judgement \(M\in A\) is polymorphic and unannotated, unlike the formal proofs which contain all the type information necessary with them in order for the judgement \(M:A\) to be analytic. It turns out that \(M\in A\) is a synthetic judgement (it does not suffice to examine \(M\) and \(A\) to determine whether \(M\in A\) is known).

Now then, under the meaning explanations, we have a much simpler proof term that gets at the root of the computational content of this proposition:

\[\lambda(x. \bullet) \in \mathsf{Id}(\mathbb{U};\mathbf{1};\mathbf{0})\supset\mathbf{0}\]

How shall we verify that this judgement is evident? Well, let us put it into English:

\(\lambda(x. \bullet)\) is in the form \(\lambda(x.b(x))\) where we know \(b(x)\in \mathbf{0}\) under the assumption \((x\in\mathsf{Id}(\mathbb{U};\mathbf{1};\mathbf{0}))\).

In order to understand this, we must unpack the meaning of a judgement under assumption:

\(\lambda(x. \bullet)\) is in the form \(\lambda(x.b(x))\) where we know \(b(x)\in \mathbf{0}\) for any arbitrary element \(x\) in the set \(\mathsf{Id}(\mathbb{U};\mathbf{1};\mathbf{0})\).

Then the evidence of this judgement is established as follows: \(\lambda(x.\bullet)\) is indeed of the form \(\lambda(x.b(x))\) by substituting \(\bullet\) for \(b(x)\); moreover, if we know that \(x\in\mathsf{Id}(\mathbb{U};\mathbf{1};\mathbf{0})\), then we know that \(\mathbf{1}=\mathbf{0}\in\mathbb{U}\), and thence for any \(M\) such that \(M\in\mathbf{1}\), then we also know \(M\in\mathbf{0}\); we know that \(\bullet\in\mathbf{1}\), and therefore we know \(\bullet\in\mathbf{0}\).

One proposition’s proof is another proof’s derivation

Now, the evidence I gave above for the judgement \(\lambda(x.\bullet)\in\mathsf{Id}(\mathbb{U};\mathbf{1};\mathbf{0})\) may look like informal reasoning, but it can also be characterized as a derivation in the theory. And if it can be characterized as a derivation, then we can have a proof term assignment for it:

\[ \dfrac{ E(x)::b(x)\in B\quad (x\in x::A) }{ \supset\text{I}(A;B;x.E(x)) :: \lambda(x.b(x)) \in A\supset B }\supset\text{I} \]

But if you squint at the above rule, it has essentially the same structure as the proof term assignment \(\lambda(A;B;x.b(x)) : A\supset B\), and so it seems like we are back where we started. It is clear, then, that the term \(\lambda(\mathsf{Id}(\mathbb{U};\mathbf{1};\mathbf{0}); \mathbf{0}; p.\mathsf{coerce}(\mathbb{1};\mathbb{0};p;\bullet))\) may be construed both as a formal proof that \(\mathsf{Id}(\mathbb{U};\mathbf{1};\mathbf{0})\supset\mathbf{0}\ \text{true}\), and also as a derivation or evidence that \(\lambda(x.\bullet) \in \mathsf{Id}(\mathbb{U};\mathbf{1};\mathbf{0})\supset\mathbf{0}\).

Interlude: formal proof vs proof object

Crucially, in case it is not yet apparant, we are dealing with two different kinds of proof. The one is “formal proof” or “derivation”, which corresponds to evidence of a judgement; and the other is “proof object”, which corresponds to proof of a proposition.

Now, in theories that have a judgement like \(M\mathop\heartsuit A\), you can often construe the terms in the first position as “proof terms” and those in the second position as “propositions”. And indeed, in intensional theories like those of Coq or Agda, the judgement is \(M:A\) and not \(M\in A\), and \(M\) is construed as a proof of \(A\); and this is a reasonable characterization from the perspective of such theories.

But starting from a theory like Nuprl’s, it is clear that its meta-level sequent proofs are the things which correspond with the terms of Agda and Coq, whereas Nuprl’s actual proof terms which appear on the lefthand side of the \(M\in A\) judgement have no parallel internally in Agda or Coq. As a result, one can consider the meta-level in Nuprl as analogous to the object-level in intensional theories, except that in addition to containing the same derivations, it also contains many more interesting and useful things, such as sequent-style rules, derived rules, tactics, etc. Not to mention the wealth of subtle propositions and types which may be defined once one has made peace with the idea of working at the meta-level, embedding the type theory in a rich logical framework.

Now, Coq has tactics as well, but this comes through bolting on a second theory of formal proof on top of what was already a theory of formal proof (the Coq term language). This redundant extra layer in an intensional theory is inevitable, since there is no means to access the true object language under the meaning explanations and the intuitionistic interpretation of logic, which is not the annotated proof term assignments of the predicate logic, but rather the untyped lambda calculus: a system of computation, and only computation.

Next time

I’d like to note that there are a number of ways to make theories of formal proof, like Agda and Coq, less arduous to work with. Bidirectional type checking and elaboration can help a lot, and go a long way in making the proof term assignment resemble at a surface-level the unannotated computational realizers of Martin-Löf’s polymorphic, extensional type theory.

Since this has already grown too lengthy, I shall continue next time with motivation for why someone would want to bother working at the meta-level in a theory with synthetic judgement, as you do in Nuprl, as opposed to working at the object-level of an analytic theory whose terms resemble derivations in the former, as you do in Agda.

Thanks to Darryl McAdams, Darin Morrison and Bob Harper for conversations leading up to this post. Thanks also to Darryl McAdams and Anthony Cowley for corrections to typographical errors.

Suggested Readings