A new feature of this year’s summer school was a reduction in the number of lectures, and an addition of daily open problem sessions for reviewing the day’s material. This turned out to be a great idea for everyone, because it gave us more informal time together, and gave the students a better chance at digesting a mountain of material. It also turned out to be a bit of an embarrassment for me, because I posed a question off the top of my head for which I thought I had two proofs, neither of which turned out to be valid. The claimed theorem is, in fact, true, and one of my proofs is easily corrected to resolve the matter (the other, curiously, remains irredeemable for reasons I’ll explain shortly). The whole episode is rather interesting, so let me recount a version of it here for your enjoyment.

The context of the discussion was *extensional* *type theory*, or *ETT*, which is characterized by an identification of judgemental with propositional equality: if you can prove that two objects are equal,then they are interchangeable for all purposes without specific arrangement. The alternative, *intensional type theory*,or *ITT*, regards judgemental equality as definitional equality (symbolic evaluation), and gives computational meaning to proofs of equality of objects of a type, allowing in particular transport across two instances of a family whose indices are equal. NuPRL is an example of an ETT; CiC is an example of an ITT.

Within the framework of ETT, the principle of *function extensionality* comes “for free”, because you can prove it to hold within the theory. Function extensionality states that whenever . That is, two functions are if they are equal on all arguments (and, implicitly, respect equality of arguments). Function extensionality holds *definitionally* if your definitional equivalence includes the and rules, but in any case does not have the same force as extensional *equality*. Function extensionality as a principle of equality cannot be derived in ITT, but must be added as an additional postulate (or derived from a stronger postulate, such as univalence or the existence of a one-dimensional interval type).

Regardless of whether we are working in an extensional or an intensional theory, it is easy to see that all functions of type definable in type theory are computable. For example, we may show that all such functions may be encoded as recursive functions in the sense of Kleene, or in a more modern formulation we may give a structural operational semantics that provides a deterministic execution model for such functions (given , run on until it stops, and yield that as result). Of course the proof relies on some fairly involved meta-theory, but it is all constructively valid (in an informal sense) and hence provides a legitimate computational interpretation of the theory. Another way to say the same thing is to say that the comprehension principles of type theory are such that every object deemed to exist has a well-defined computational meaning, so it follows that all functions defined within it are going to be computable.

This is all just another instance of *Church’s Law*, the scientific law stating that any formalism for defining computable functions will turn out to be equivalent to, say, the λ-calculus when it comes to definability of number-theoretic functions. (Ordinarily Church’s Law is called *Church’s Thesis*, but for reasons given in my *Practical Foundations* book, I prefer to give it the full status of a scientific law.) Type theory is, in this respect, no better than any other formalism for defining computable functions. By now we have such faith in Church’s Law that this remark is completely unsurprising, even boring to state explicitly.

So it may come as a surprise to learn that *Church’s Law is false*. I’m being provocative here, so let me explain what I mean before I get flamed to death on the internet. The point I wish to make is that there is an important distinction between the *external* and the *internal* properties of a theory. For example, in first-order logic the Löwenheim-Skolem Theorem tells us that if a first-order theory has an infinite model, then it has a countable model. This implies that, *externally to ZF set theory,* there are only countably many sets, even though *internally* *to ZF* *set theory* we can carry out Cantor’s argument to show that the powerset operation takes us to exponentially higher cardinalities far beyond the countable. One may say that the “reason” is that the evidence for the countability of sets is a bijection that is not definable within the theory, so that it cannot “understand” its own limitations. This is a good thing.

The situation with Church’s Law in type theory is similar. *Externally* we know that every function on the natural numbers is computable. But what about *internally*? The internal statement of Church’s Law is this: , where the notation means, informally, that is the code of a program that, when executed on input , evaluates to . In Kleene’s original notation this would be rendered as , where the predicate encodes the operational semantics, and the predicate extracts the answer from a successful computation. Note that the expansion makes use of the identity type at the type . The claim is that Church’s Law, stated as a type (proposition) within ETT, is false, which is to say that it entails a contradiction.

When I posed this as an exercise at the summer school, I had in mind two different proofs, which I will now sketch. Neither is valid, but there is a valid proof that I’ll come to afterwards.

Both proofs begin by applying the so-called Axiom of Choice. For those not familiar with type theory, the “axiom” of choice is in fact a *theorem*, stating that every total binary relation contains a function. Explicitly,

The function is the “choice function” that associates a witness to the totality of to each argument . In the present case if we postulate Church’s Law, then by the axiom of choice we have

.

That is, the functional picks out, for each function in , a (code for a) program that witnesses the computability of . This should already seem suspicious, because by function extensionality the functional must assign the *same* program to any two extensionally equal functions.

We may easily see that is injective, for if is , then both track both and , and hence and are (extensionally) equal. Thus we have an injection from into , which seems “impossible” … except that it is not! Let’s try the proof that this is impossible, and see where it breaks down. Suppose that is injective. Define , and consider so and we are done. Not so fast! Since is only injective, and not necessarily surjective, it is not clear how to define . The obvious idea is to send to , and any outside the image of to, say, the identity. But there is no reason to suppose that the image of is decidable, so the attempted definition breaks down. I hacked around with this for a while, trying to exploit properties of to repair the proof (rather than work with a general injection, focus on the specific functional ), but failed. Andrej Bauer pointed out to me, to my surprise, that there is a model of ETT (which he constructed) that contains an injection of into ! So there is no possibility of rescuing this line of argument.

(Incidentally, we can show within ETT that there is no *bijection* between and , using surjectivity to rescue the proof attempt above. Curiously, Lawvere has shown that there can be no *surjection* from onto , but this does not seem to help in the present situation. This shows that the concept of countability is more subtle in the constructive setting than in the classical setting.)

But I had another argument in mind, so I was not worried. The functional provides a decision procedure for equality for the type : given , compare with . Surely this is impossible! But one cannot prove *within type theory* that is undecidable, because type theory is consistent with the law of the excluded middle, which states that every proposition is decidable. (Indeed, type theory proves that excluded middle is irrefutable for any particular proposition : .) So this proof also fails!

At this point it started to seem as though Church’s Law could be independent of ETT, as startling as that sounds. For ITT it is more plausible: equality of functions is definitional, so one could imagine associating an index with each function without disrupting anything. But for ETT this seemed implausible to me. Andrej pointed me to a paper by Maietti and Sambin that states that Church’s Law is incompatible with function extensionality and choice. So there must be *another* proof that refutes Church’s Law, and indeed there is one based on the aforementioned decidability of function equivalence (but with a slightly different line of reasoning than the one I suggested).

First, note that we can use the equality test for functions in to check for halting. Using the predicate described above, we can define a function that is constantly iff a given (code of a) program never halts on given input. We may then use the above-mentioned equality test to check for halting. So it suffices to show that the halting problem for (codes of) functions and inputs is not computable to complete the refutation of the internal form of Church’s Law.

Specifically, assume given that, given a code for a function and an input, yields or according to whether or not that function halts when applied to that input. Define by , the usual diagonal function. Now apply the functional obtained from Church’s Law using the Axiom of Choice to obtain , the code for the function , and consider to derive the needed contradiction. Notice that we have used Church’s Law here to obtain a code for the type-theoretic diagonal function, which is then passed to the halting tester in the usual way.

As you can see, the revised argument follows along lines similar to what I had originally envisioned (in the second version), but requires a bit more effort to push through the proof properly. (Incidentally, I don’t think the argument can be made to work in pure ITT, but perhaps it would go through for ITT enriched with function extensionality.)

Thus, Church’s Law is *false* internally to extensional type theory, even though it is evidently *true* externally for that theory. You can see the similarity to the situation in first-order logic described earlier. Even though all functions of type are computable, type theory itself is not capable of recognizing this fact (at least, not in the extensional case). And this is a good thing, not a bad thing! The whole beauty of constructive mathematics lies in the fact that it is *just mathematics*, free of any self-conscious recognition that we are writing programs when proving theorems constructively. We never have to reason about machine indices or any such nonsense, we just do mathematics under the discipline of not assuming that every proposition is decidable. One benefit is that the same mathematics admits interpretation not only in terms of computability, but also in terms of continuity in topological spaces, establishing a deep connection between two seemingly disparate topics.

(Hat tip to Andrej Bauer for help in sorting all this out. Here’s a link to a talk and a paper about the construction of a model of ETT in which there is an injection from to .)

*Update*: word-smithing.

Reading this together with your next post has confused me about what you mean by the word “proposition”. In the next post, you made the point that not every construction is a proof, i.e. not every type is a proposition; but you didn’t say how you want to decide whether a given type is a proposition.

In my limited experience, it seems that the most common answer is to regard as propositions those types that are subsingletons, a.k.a. proof-irrelevant, a.k.a. (-1)-truncated or h-level 1 (in the language of homotopy type theory). But in that case, the quantifier “there exists” has to be interpreted not by a -type but by a squashed version of it. Then the axiom of choice is no longer a theorem and can be false, while Church’s Law would be (where denotes a squash type) and can be true (as it is in the effective topos). (Please correct me if my understanding of any of this is wrong.)

Since in this post you say that AC is a theorem and CL is false, using the non-squashed versions of both, I gather that this is not the meaning of “proposition” you prefer. So what, for you, makes a type into a proposition? Is it just the intent to regard it as such?

My two cents: It’s the intent. If we had to specify which types are “propositions” in a formal sense, it would make most sense to reserve this term for subsingleton ((-1)-truncated) types. But as we know, to truncate types is to throw out a lot of useful homotopical — and even 0-dimensional — information.

I think Bob is drawing an informal distinction between types which can be regarded meaningfully as theorems in a logic, and types which only express constructions (whatever that means). When people first learn about props-as-types, they are told that every program proves a theorem; they often respond with a question like, “What theorem does fib :: Int -> Int prove?” The answer is of course that it’s a useless theorem (\x. 0 or \x. x are suitable proofs) but a perfectly sensible construction, about which we might perhaps wish to prove interesting theorems.

What Carlo says.

Okay, thanks! I don’t like it, but at least now I understand it. (-:

Cool post, Bob. Two typos in the paragraph where you complete the proof: H(x,x) should be h(x,x), and h(d,d) should be h(n,n).

Corrected, thanks.

@andrej: It is exactly this (perhaps somewhat boring) interpretation of Church’s Law as “quote” that I am curious about. Perhaps I have drunk too much intensional-equality kool-aid, but one of the promised benefits of intensional equality is that we are not forced to identify operations of different complexity as equal (e.g. bogosort and quicksort). As far as extensional type theory is concerned, whether we define our sorting function as quicksort or bogosort does not matter: there is only one true sorting function, and all sorting functions are equal to it.

On the other hand, if we can safely add a “quote” function to intensional type theory, then we can distinguish between the two sorts, and then we can (hopefully) prove that quicksort is efficient under a chosen evaluation scheme. We could still perhaps keep a notion of extensional equality for functions as equality-of-function-application — not as convenient, maybe, but not necessarily impossible.

Why does abandoning this idea in favor of e.g. extensional type theory trouble me? Because then, if we have a proof the correctness of our tree implementation in (dependent type theory based) TheoremProver, and we want to prove that it also has the right complexity guarantees, then it seems we have two choices: 1. analyze the complexity outside of TheoremProver or 2. build a new theory of computation within TheoremProver and rewrite our tree in that embedded language. Certainly (2) works, but then is there a strong reason to prefer TheoremProver to e.g. HOL? (perhaps an affirmative answer to that question would be comforting.)

@Frederic: typically Church’s Law does not compute anything. For example, in the effective topos it is realized by the (code of) identity function. The reason is simple: since everything is represented by Gödel codes anyhow, it is trivially the case that every function has a code. I do not know of a model in which Church’s Law has an interesting computational meaning. In a programming language it corresponds to “unquote” or “disassemble”: given a value of functional type, it returns its source code (given as an abstract syntax tree, or just as a pointer to a block of machine code).

The internal Church’s Law (I love calling it a “law”!) is a very extreme axiom which fails in most realizability models. It says something like “everything we see is not only made of Gödel codes, these codes are visible to us”. Church’s Law in our universe would say not only that we’re being simulated by a computer, but also that we have access to God’s source code. An extreme position indeed.

Very thought provoking! I wonder, though, if we aren’t potentially losing something by making functions so extensional. If we stick with intensional type theory and add a version of Church’s Law that computes, we might be able to prove interesting things: e.g. that our definition of mergesort is polynomial time computable. With function extensionality, even though we only have computable functions we are completely forbidden to mention how they are computed, as your example shows — and so if we want to prove anything about their intension (like that they terminate within a reasonable amount of time) within our extensional theorem prover, we have to build a whole internal theory and rewrite all of our functions within it. It just seems a bit unsavory that within type theory, we are already going to a lot of effort to show that our functions compute in bounded time and yet cannot use this information directly.