The publication of the Homotopy Type Theory book has renewed interest in type theory as a foundation for mathematics, and spurred computer scientists to investigate the computational meaning of higher-dimensional types. As I mentioned in a previous post, what makes HoTT work so well for homotopy theory is that it is *constructive*, which means, at the very least, that it does not postulate that all types are decidable. By Hedberg’s Theorem any type with decidable equality is a set (homotopy 0-type), so a blanket adoption of the classical law of the excluded middle would immediately rule out any higher-dimensional structure.

To my way of thinking, the denial of the universal validity of the excluded middle is not the *defining* feature of constructivity, but rather a *characteristic* feature of constructivity—it is the smoke, not the locomotive. But what, then, is the deeper meaning of constructivity that gives rise to the denial of many classical patterns of reasoning, such as proof by contradiction or reasoning by cases on whether a proposition is true or not? Although the full story is not yet completely clear, a necessary condition is that a constructive theory be *proof relevant*, meaning that proofs are mathematical objects like any other, and that they play a role in the development of constructive mathematics unlike their role in classical mathematics.

The most obvious manifestation of proof relevance is the defining characteristic of HoTT, that *proofs of equality* correspond to *paths in a space*. Paths may be thought of as evidence for the equality of their endpoints. That this is a good notion of equality follows from the homotopy invariance of the constructs of type theory: everything in sight respects paths (that is, respect the groupoid structure of types). More generally, theorems in HoTT tend to characterize the space of proofs of a proposition, rather than simply state that the corresponding type is inhabited. For example, the univalence axiom itself states an equivalence between proofs of equivalence of types in a universe and equivalences between these types. This sort of reasoning may take some getting used to, but its beauty is, to my way of thinking, undeniable. Classical modes of thought may be recovered by explicitly obliterating the structure of proofs using truncation. Sometimes this is the best or only available way to state a theorem, but usually one tends to say more than just that a type is inhabited, or that two types are mutually inhabited. In this respect the constructive viewpoint *enriches*, rather than *diminishes*, classical mathematics, a point that even the greatest mathematician of the 20th century, David Hilbert, seems to have missed.

The concept of proof relevance in HoTT seems to have revived a very common misunderstanding about the nature of proofs. Many people have been trained to think that a proof is a derivation in an axiomatic theory, such as set theory, a viewpoint often promoted in textbooks and bolstered by the argument that an informal proof can always be written out in full in this form, even if we don’t do that as a matter of course. It is a short step from there to the conclusion that proofs are therefore mathematical objects, even in classical set theory, because we can treat the derivations as elements of an inductively defined set (famously, the set of natural numbers, but more realistically using more natural representations of abstract syntax such as the s-expression formalism introduced by McCarthy in 1960 for exactly this purpose). From this point of view many people are left confused about the stress on “proofs as mathematical objects” as a defining characteristic of HoTT, and wonder what could be original about that.

The key to recognize that *a proof is not a formal proof*. To avoid further confusion, I hasten to add that by “formal” I do not mean “rigorous”, but rather “represented in a formal system” such as the axiomatic theory of sets. A *formal proof* is an element of a computably enumerable set generated by the axioms and rules of the formal theory. A *proof* is an argument that demonstrates the truth of a proposition. While formal proofs are always proofs (at least, under the assumption of consistency of the underlying formal theory), a proof need not be, or even have a representation as, a formal proof. The principal example of this distinction is Goedel’s Theorem, which proves that the computably enumerable set of formal provable propositions in axiomatic arithmetic is not decidable. The key step is to devise a self-referential proposition that (a) is not formally provable, but (b) has a proof that shows that it is true. The crux of the argument is that *once you fix the rules of proof, you automatically miss out true things that are not provable in that fixed system*.

Now comes the confusing part. HoTT is defined as a formal system, so why doesn’t the same argument apply? It does, pretty much verbatim! But this has no bearing on “proof relevance” in HoTT, because the proofs that are relevant are not the formal proofs (derivations) defining HoTT as a formal system. Rather proofs are formulated internally as objects of the type theory, and there is no commitment *a priori* to being the only forms of proof there are. Thus, for example, we may easily see that there are only countably many functions definable in HoTT from the outside (because it is defined by a formal system), but within the theory any function space on an infinite type has uncountably many elements. There is no contradiction, because the proofs of implications, being internal functions, are not identified with codes of formal derivations, and hence are not denumerable.

There is a close analogy, previously noted in this blog, with Church’s Law. Accepting Church’s Law internally amounts to fixing the programming language used to define functions in advance, permitting us to show, for example, that certain programs are not expressible in that language. But HoTT does not commit to Church’s Law, so such arguments amount to showing that, for example, there is no Turing machine to decide halting for Turing machines, but allowing that there could be constructive functions (say, equipped with oracles) that make such decisions.

The theory of formal proofs, often called proof theory, was dubbed *metamathematics* by Kleene. Until the development of type theory the study of proofs was confined to metamathematics. But now in the brave new world of *constructive mathematics* as embodied in HoTT, proofs (not just formal proofs) have pride of place in mathematics, and provide opportunities for expressing concepts clearly and cleanly that were hitherto obscured or even hidden from our view.

*Update*: Corrected silly wording mistake.

Oh, Robert, as I’m sure you know and really did mean, part of the point of a formal system is that the family of

proofsisdecidable: one needn’t be smarter than a machine to decide the grammar and correctness of a Formal-Proof; it’s the essential image of this set under taking conclusions, the set ofprovable propositionsthat is in general recursively enumerable but not decidable.Right.

To understand the constructive interpretation of mathematical language it is indeed essential to appreciate that the notion of proof involved is not that of a formal proof in a formal system of deduction. But to say of Gödel’s proof that it “proves that the computably enumerable set of formal proofs in axiomatic arithmetic is not decidable” is nonsense. The set of formal proofs in any formal theory is trivially decidable. What the incompleteness theorem shows is that the set of arithmetical truths is productive.

> Rather proofs are formulated internally as objects of the type theory, and there is no commitment a priori to being the only forms of proof there are.

Just to make sure I understand – here you mean that there is no commitment a priori to *formal proofs* being the only forms of *internal proof objects* there are, correct?

right

“Goedel’s Theorem, which proves that the computably enumerable set of formal proofs in axiomatic arithmetic is not decidable”

Goedel’s First Incompleteness Theorem does not show the consistency of arithmetic, so it leaves open the possibility that arithmetic is inconsistent, in which case the set of formal proofs is trivially decidable.

Furthermore, if a formal system is inconsistent, then all propositions are of course provable, but I don’t know that you would consider Goedel’s proposition to be “true” in your intended sense (Tarski’s)? Probably not. (On the other hand, if you are assuming the system is consistent, it is perhaps no surprise that you can find new truths which were previously unprovable.)

So, out of curiosity, how do you decide which formal systems are inconsistent?

Well, you cannot in general. The intuitionistic approach has been to build up starting with computation as the fundamental concept. That’s the method I still believe in, though HoTT currently lacks a computational justification.

Well, I was really asking Frederic; and my point is that it’s a bit disingenuous to emphasize that Arithmetic *might* be “trivially decidable”, when 1) no-one believes Arithmetic to be inconsistent, and almost everyone who thinks about it believes he knows a model of Arithmetic 2) Gentzen reduced the consistency of Arithmetic to the well-foundedness of a particular order on finite trees, which is similarly believable and 3) even if a system happens to be inconsistent, and hence “trivially decidable”, the mere machine that replies “Theorem” on every propositional query without working isn’t evidence of such decidability; only a derivation of “false” in such-and-such formal system is.

I was thinking of the most basic form of incompleteness theorem, which assumes soundness (the axioms of arithmetic are true, because you can prove them to be so using well-accepted mathematical reasoning), just to make my point as simply as possible. One can weaken the assumption to formal consistency, but that would be tangential to my main point, which is simply to distinguish the concept of a formal proof from the concept of a proof, and in particular that no notion of formal proof can capture the notion of proof. I realize that this is “old hat”, but the point comes up again and again, and was recently a topic surrounding the concept of “proof relevant mathematics” that is central to HoTT, so I thought I would take a stab at explaining what is going on.

I think this confusion is why the book tries to use words like “witness” and “evidence” instead of “proof” to refer to the “relevant” objects inside the theory.