3.2 Propositions as types?
Until now, we have been following the straightforward “propositions as types” philosophy described in §1.11 (http://planetmath.org/111propositionsastypes), according to which English phrases such as “there exists an such that ” are interpreted by corresponding types such as , with the proof of a statement being regarded as judging some specific element to inhabit that type. However, we have also seen some ways in which the “logic” resulting from this reading seems unfamiliar to a classical mathematician. For instance, in Theorem 2.15.7 (http://planetmath.org/215universalproperties#Thmprethm3) we saw that the statement
|“If for all there exists an such that , then there exists a function such that for all we have ,”||(3.2.1)|
which looks like the classical axiom of choice, is always true under this reading. This is a noteworthy, and often useful, feature of the propositions-as-types logic, but it also illustrates how significantly it differs from the classical interpretation of logic, under which the axiom of choice is not a logical truth, but an additional “axiom”.
It is not the case that for all we have .
Recall that . We also read “it is not the case that …” as the operator . Thus, in order to prove this statement, it suffices to assume given some and construct an element of .
The idea of the following proof is to observe that , like any function in type theory, is “continuous”. By univalence, this implies that is natural with respect to equivalences of types. From this, and a fixed-point-free autoequivalence, we will be able to extract a contradiction.
Let be the equivalence defined by and , as in Example 3.1.9 (http://planetmath.org/31setsandntypes#Thmpreeg6). Let be the path corresponding to by univalence, i.e. . Then we have and
Hence, for any , we have
Now by (2.9.4) (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#S0.E3), transporting along in the type family is equal to the function which transports its argument along in the type family , applies , then transports the result along in the type family :
However, any two points are equal by function extensionality, since for any we have and thus we can derive any conclusion, in particular . Thus, we have , and so from we obtain an equality
Finally, as discussed in §2.10 (http://planetmath.org/210universesandtheunivalenceaxiom), transporting in the type family along the path is equivalent to applying the equivalence ; thus we have
However, we can also prove that
This follows from a case analysis on : both cases are immediate from the definition of and the fact that (Remark 2.12.6 (http://planetmath.org/212coproducts#Thmprermk1)). Thus, applying (3.2.4) to and (3.2.3), we obtain an element of . ∎
In particular, this implies that there can be no Hilbert-style “choice operator” which selects an element of every nonempty type. The point is that no such operator can be natural, and under the univalence axiom, all functions acting on types must be natural with respect to equivalences.
It is, however, still the case that for any ; see http://planetmath.org/node/87564Exercise 1.11.
It is not the case that for all we have .
Suppose we had . We will show that then , so that we can apply Theorem 3.2.2 (http://planetmath.org/32propositionsastypes#Thmprethm1). Thus, suppose and ; we want to construct an element of .
Now , so by case analysis, we may assume either for some , or for some . In the first case, we have , while in the second case we have and so we can obtain anything we wish (such as ). Thus, in both cases we have an element of , as desired. ∎
Thus, if we want to assume the univalence axiom (which, of course, we do) and still leave ourselves the option of classical reasoning (which is also desirable), we cannot use the unmodified propositions-as-types principle to interpret all informal mathematical statements into type theory, since then the law of excluded middle would be false. However, neither do we want to discard propositions-as-types entirely, because of its many good properties (such as simplicity, constructivity, and computability). We now discuss a modification of propositions-as-types which resolves these problems; in §3.10 (http://planetmath.org/310whenarepropositionstruncated) we will return to the question of which logic to use when.
|Title||3.2 Propositions as types?|