2.6 KiB
title: Uniquness of the absurdity proofs in Cartesian closed categories tags: category theory date: 2015-08-12 00:00
Adding the DNE to CCCs collapses them into Boolean algebras:
Suppose \mathcal{C} is a Cartesian closed category.
We can show that if \mathcal{C} has a family of isomorphisms between A and (A \to 0) \to 0, then \mathcal{C} is a poset (and a Boolean algebra).
Proposition.
For any object A of \mathcal{C}, A \times 0 \simeq 0.
Proof.
${\mathit{\mathop{Hom}}}(A \times 0, B) \simeq {\mathit{\mathop{Hom}}}(0 \times A, B) \simeq {\mathit{\mathop{Hom}}}(0, B^A)
\simeq 1$.
Therefore, A \times 0 is an initial object in \mathcal{C}.
Clearly (\pi_2, \bot_{A \times 0}) establishes the isomorphism.
Qed
Proposition.
Given a morphism f : A \to 0, we can conclude that A \simeq 0.
Proof.
The isomorphism is witnessed by (f, \bot_A) : A \to A \times 0 \simeq 0 (where
\bot_A : 0 \to A is the unique initial morphism).
Qed
We have seen that given the morphism f : A \to 0 we can construct an
iso A \simeq 0. In particular, that means that there can be at
most one arrow between A and 0; interpreting arrows as
"proofs" or "proof object", that means that in the intuitionistic
calculus there is at most one proof/realizer of the negation (up to
isomorphism).
Now, returning to the original question, how do CCCs with
double-negation elimination look like? Specifically, we want to show
that if in \mathcal{C} there is an isomorphism between A and
0^{(0^A)} for all objects A, then the categorical structure
collapses into a Boolean algebra.
We say that a category has double negation elimination if for every A, it is the case that A \simeq 0^{(0^A)}.
Proposition.
Given a category with double negation elimination and two morphisms f, g : A \to B, it
is the case that f = g.
Proof.
Let i be the isomorphism between B and 0^{(0^B)}. Then,
$i \circ f, i \circ g \in {\mathit{\mathop{Hom}}}(A, 0^{(0^B)}) \simeq {\mathit{\mathop{Hom}}}(A \times
(0^B), 0)$.
But the latter set can contain at most one element; thus,
i \circ f = i \circ g. Because i is an isomorphism, f = g.
Qed
It might be worth noting that in "standard" cartesian closed
categories, a morphism i : B \to 0^{(0^B)} serve as a coequalizer of
f and g. Perhaps stretching the analogy a bit, we can view i as
"equalizes" two constructive proofs of B into a single classical
proof.
See also
- A categorical characterization of Boolean algebras by M.E. Szabo