3.6 The logic of mere propositions
We mentioned in §1.1 (http://planetmath.org/11typetheoryversussettheory) that in contrast to type theory, which has only one basic notion (types), set-theoretic foundations have two basic notions: sets and propositions. Thus, a classical mathematician is accustomed to manipulating these two kinds of objects separately.
It is possible to recover a similar dichotomy in type theory, with the role of the set-theoretic propositions being played by the types (and type families) that are mere propositions. In many cases, the logical connectives and quantifiers can be represented in this logic by simply restricting the corresponding type-former to the mere propositions. Of course, this requires knowing that the type-former in question preserves mere propositions.
If is any type and is such that for all , the type is a mere proposition, then is a mere proposition. The proof is just like Example 3.1.6 (http://planetmath.org/31setsandntypes#Thmpreeg5) but simpler: given , for any we have since is a mere proposition. But then by function extensionality, we have .
In particular, if is a mere proposition, then so is regardless of what is. In even more particular, since is a mere proposition, so is . Thus, the connectives “implies” and “not” preserve mere propositions, as does the quantifier “for all”.
On the other hand, some type formers do not preserve mere propositions. Even if and are mere propositions, will not in general be. For instance, is a mere proposition, but is not. Logically speaking, is a “purely constructive” sort of “or”: a witness of it contains the additional information of which disjunct is true. Sometimes this is very useful, but if we want a more classical sort of “or” that preserves mere propositions, we need a way to “truncate” this type into a mere proposition by forgetting this additional information.
The same issue arises with the -type . This is a purely constructive interpretation of “there exists an such that ” which remembers the witness , and hence is not generally a mere proposition even if each type is. (Recall that we observed in §3.5 (http://planetmath.org/35subsetsandpropositionalresizing) that can also be regarded as “the subset of those such that ”.)
|Title||3.6 The logic of mere propositions|