Extreme non-choosiness

As a mathematician who's quite new to type theory, I have only vaguely internalised the fact that forall a.a and Pi a.a (or whatever the appropriate ASCII-isations are) mean the same thing. Thus, although it seems obvious to me that forall a.a is empty (or does one say uninhabited?), I was nonetheless quite startled to read the following in Barendregt's "Introduction to generalised type systems", p. 132:

… write \bot \equiv (\Pi \alpha : *. \alpha), which is the second-order definition of falsum.

I tried to re-cast this in language more familiar to me, and wound up with the statement that the product of all sets is empty.

Now, I know that type theories tend (understandably) to be biased more towards constructivist than traditional ZFC-based axiomatisations; but it seems to me that, beyond just saying that we don't assume the Axiom of Choice, this statement is saying that we take that axiom as the definition of ‘false’! Is the rejection of choosiness really so definitive, or am I just skipping over some point (like, say, that some sets are empty, so that including them in the product will naturally make it, too, empty)?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Yes, you're...

...skipping over exactly the point you identified. :)

Concretely, suppose that we have some e : forall a. a. Then, you could come up with an inhabitant of absolutely any type A by simply instantiating e with A, so that e [A] : A. So all types would be inhabited, and so the theory would be inconsistent. As an aside, this definition doesn't turn on either the classical/intuitionistic distinction, or on whether the axiom of choice holds -- the definition of false given above is exactly the same as in classical higher-order logic.

Whether or not and how the axiom of choice holds in type theory is a delicate question, and depends a lot on the definitions of truth and proposition we use. Type-theoretically, the type of the axiom of choice reads something like this:

   forall A : *, B : *, Q : A -> B -> *, 
      (forall a : A, exists b : B, Q(a, b)) -> 
      (exists f : A -> B, forall a : A, Q (a, f a))

That's kind of a beast of a type, but it just says that if for every a there is a b such that the predicate Q(a,b) holds, then there's a function from A to B which witnesses that property.

In type theories which have a propositions-as-types interpretation, this isn't just a sound axiom, it's actually a theorem! The reason is that the forall quantifier is a function space, and the existential is a pairing operation which pairs a value and a proof of the property. So the witnessing function is just the operation that throws away the proof:

   choice A B Q property = ((λa. fst(property a)), (λa. snd(property a)))

Martin-Lof type theory has this property, and so you'd be able to write pretty much this program in a language like Agda, for example.

OTOH, not all type theories have a props-as-types interpretation. Coq, for instance, does not -- it has a distinguished sort of propositions, which are defined to have no computational content. (This property is sometimes called "proof irrelevance".) As a result, the axiom of choice entails excluded middle for Coq.

You automatically get proof irrelevance in topos models of intuitionistic logic, since the truth values object is just a lattice (ie, a Heyting algebra), and so it equates all proofs of an entailment between truth values. Since these are the most common models of intuitionistic mathematics, people tend to assume choice is incompatible with intuitionistic mathematics. But the situation is actually more complicated than that!

An interesting point

Coq, for instance, does not -- it has a distinguished sort of propositions, which are defined to have no computational content. (This property is sometimes called "proof irrelevance".) As a result, the axiom of choice entails excluded middle for Coq.

Thanks for pointing this out Neel; I found this food for thought.

In particular, I think this dovetails with what I was saying in another thread about order and computation.

By erasing the inherent order of the computation through proof irrelevance, you create a system where choice is too powerful, i.e. choice can choose to reimpose ANY ordering.

Whereas, in a strictly computational system, you only get the orderings you can actually build, which limits the logical power of the system, especially with respect to excluded middle.

There are still some details of this that are still unclear to me, but, as I said, you have given me food for thought.

Thanks again!

In Haskell, say, it's not just the product

Let's look at this from the perspective of Haskell (or a total fragment thereof, I don't want to talk about bottoms) which I know much better than type theory in general.

In Haskell, forall a.a is, as Barendregt says, the uninhabited type. But, the following claim isn't quite true:

forall a.a and Pi a.a (or whatever the appropriate ASCII-isations are) mean the same thing

We can make it clear that forall a isn't just the product by considering forall a.[a] instead. ([] = List) This contains the single element: [].

Think about this from a set theory-like perspective. Pi a.[a] is a product object with the property that for each type X there is a function p:Pi a.[a] -> [X] that is the projection, and each element of Pi a.[a] is defined completely by its projections. (In Haskell, say, you don't have to write this projection explicitly, it's implicitly given to you for free.) We can easily make up a set-theoretical example. Pick some type X. Pick some non-empty element, E, of [X]. Choose an element of Pi a.[a] that projects to [] for every set except X where it projects to [E]. (Concretely, in C++ you could achieve this using template specialisation.) This is *not* an element of forall a.[a] and you can't construct it in Haskell.

The reason is that Haskell has a parametricity condition. It basically says that if we have the two projections p:forall a.[a]->[X] and q:forall a.[a]->[Y], and f:X->Y is *any* function we feel like, then q=fmap f.p. This is what results in the only element of forall a.[a] being [].

Category theoretically, products are the limits of functors from discrete categories. But forall a is the limit of a functor from the category of types and that category has lots of non-trivial arrows in it. In general, limits in categories with non-trivial arrows are subsets (pullbacks) of the full product. These extra arrows give the equations I listed above and are an example of parametricity and that is distinct (I think) from axiom of choice issues.

Not being a type theorist I won't comment on how, or even whether this applies more generally than in Haskell.