conclusion.tex

\section{Forcing in a More General Context}\label{sec:conclusion}

Having proven the independence of the continuum hypothesis, I wanted
to take a little time to discuss how this proof fits into a broader
context. In general forcing is incredibly useful for establishing
independence results in both set theory and type theory. This proof
shows how syntactic forcing proofs can be smoothly translated into a
proof about toposes. I am not capable of speaking of interesting
results established in set theory using forcing but several
developments in type theory have used a topos-theoretic forcing
technique. Specifically,~\citet{Coquand:12} represents a coherent
introduction to some of the developments done in~\citet{Coquand:04}
and~\citet{Coquand:16}. This work was developed in
the~\citet{Jaber:14}. While not directly using topos-theoretic
forcing,~\citet{Escardo:13} and~\citet{Sterling:16} are both results
about type theory done by a similar technique.

The alternative characterization of forcing in terms of boolean valued
models was explored by Scott and others during the 60s and 70s. These
are remarkably topos-theoretic semantics in which the validity of a
statement isn't a simple boolean but given in terms of an element of a
complete boolean lattice. By quotienting this lattice by a particular
ultrafilter one can translate forcing proofs into this framework. I am
not well positioned to recommend literature on this
but~\citet{Jech:08} contains an approachable introduction and our own
Clive Newstead has produced notes on this~\cite{Newstead:12}.

More familiar to logicians will be Kripke semantics and Beth
semantics. In these we index the $\Vdash$ relation with a ``world'' at
which we consider it. These worlds are assumed to form a preorder
which is intended to represent time with $w_1 \le w_2$ implying that
$w_2$ is a possible future of $w_1$. Kripke semantics correspond
closely to presheaf semantics on the poset of worlds. Beth semantics
add the local character sheaves enjoy to the semantics. Accordingly
then, Kripke semantics, step-indexed logical relations, and Beth
semantics in general can be translated as a special case of the
Kripke-Joyal semantics for the internal logic of some presheaf or
sheaf topos. This idea for intuitionistic logic was discussed
in~\citet{Fourman:82} and~\citet{Fourman:13}. Kripke and Beth
semantics are given a lengthy consideration in~\citet{Dummett:00}
and~\citet{Troelstra:88}. Recently, the more topos-theoretic approach
that has been present in developments like~\citet{Dreyer:09} has been
made explicit in the work of~\citet{Birkedal:11}.