# 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.

###### Example 3.6.1.

If $A$ and $B$ are mere propositions, so is $A\mathrm{\times}B$.
This is easy to show using the characterization^{} of paths in products^{}, just like Example 3.1.5 (http://planetmath.org/31setsandntypes#Thmpreeg4) but simpler.
Thus, the connective “and” preserves mere propositions.

###### Example 3.6.2.

If $A$ is any type and $B\mathrm{:}A\mathrm{\to}\mathrm{U}$ is such that for all $x\mathrm{:}A$, the type $B\mathit{}\mathrm{(}x\mathrm{)}$ is a mere proposition, then ${\mathrm{\prod}}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}B\mathit{}\mathrm{(}x\mathrm{)}$ is a mere proposition. The proof is just like Example 3.1.6 (http://planetmath.org/31setsandntypes#Thmpreeg5) but simpler: given $f\mathrm{,}g\mathrm{:}{\mathrm{\prod}}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}B\mathit{}\mathrm{(}x\mathrm{)}$, for any $x\mathrm{:}A$ we have $f\mathit{}\mathrm{(}x\mathrm{)}\mathrm{=}g\mathit{}\mathrm{(}x\mathrm{)}$ since $B\mathit{}\mathrm{(}x\mathrm{)}$ is a mere proposition. But then by function extensionality, we have $f\mathrm{=}g$.

In particular, if $B$ is a mere proposition, then so is $A\mathrm{\to}B$ regardless of what $A$ is. In even more particular, since $\mathrm{0}$ is a mere proposition, so is $\mathrm{\neg}A\mathrm{\equiv}\mathrm{(}A\mathrm{\to}\mathrm{0}\mathrm{)}$. 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 $A$ and $B$ are mere propositions, $A+B$ will not in general be.
For instance, $\mathrm{\U0001d7cf}$ is a mere proposition, but $\mathrm{\U0001d7d0}=\mathrm{\U0001d7cf}+\mathrm{\U0001d7cf}$ is not.
Logically speaking, $A+B$ 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 $\mathrm{\Sigma}$-type ${\sum}_{(x:A)}P(x)$.
This is a purely constructive interpretation^{} of “there exists an $x:A$ such that $P(x)$” which remembers the witness $x$, and hence is not generally a mere proposition even if each type $P(x)$ is.
(Recall that we observed in §3.5 (http://planetmath.org/35subsetsandpropositionalresizing) that ${\sum}_{(x:A)}P(x)$ can also be regarded as “the subset of those $x:A$ such that $P(x)$”.)

Title | 3.6 The logic of mere propositions |
---|---|

\metatable |