flypitch-notes.tex

\documentclass[11pt]{article}
\usepackage[margin=1in]{geometry}
\usepackage{tikz-cd}
\usepackage{graphicx}
\usepackage{hyperref}
\usepackage{amsmath,amsthm,amssymb,mathrsfs,mathabx}
\usepackage{enumitem}
\usepackage{csquotes}
\usepackage{parskip}
\usepackage{hyperref}
\usepackage{fixltx2e}
\usepackage{tcolorbox}
\usepackage{jmhmacros}
\usepackage{microtype} % thanks favonia

% % COPY THIS
 \usepackage[utf8x]{inputenc}
 \usepackage{color}
 \definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1}   % red
 \definecolor{tacticcolor}{rgb}{0.1, 0.2, 0.6}    % blue
 \definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4}   % grey
 \definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6}    % blue
 \definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1}      % green
 \definecolor{attributecolor}{rgb}{0.7, 0.1, 0.1} % red
 \usepackage{listings}
 \def\lstlanguagefiles{lstlean.tex}
 \lstset{language=lean,breakatwhitespace,xleftmargin=\parindent} % the last two options are optional
 \lstMakeShortInline" % optional, if you want to use the character " to open/close inline code
 % be careful, any instances of " inside a math environment will break compilation

 \newcommand{\arity}{\opn{arity}}
 \newcommand{\set}{\opn{set}}
 \newcommand{\ZFC}{\msf{ZFC}}
 \newcommand{\CH}{\msf{CH}}
 \newcommand{\bval}{\msf{.bval}}
 \newcommand{\func}{\msf{.func}}
 \newcommand{\type}{\msf{.type}}
\graphicspath{ {/home/pv/Pictures/latex/} }

\begin{document}

\title{Forcing and the independence of the continuum hypothesis}
\author{Jesse Han}
\date{\today}

\maketitle


\begin{abstract}
In these notes, intended as the plaintext part of the Flypitch project, we give a complete account of the independence of the continuum hypothesis from $\msf{ZFC}$, with special attention paid to comparing the different approaches: generic sets, Boolean-valued models, and double-negation sheaves.
\end{abstract}

\tableofcontents

% TODO(jesse) \newpage \section*{Introduction}

\newpage \section{Preliminaries}

\subsection{First-order logic}
\subsubsection{General logical symbols}
\definition{\label{def-general-logical-symbol} We reserve the following general logical symbols:
$$  \begin{gmatrix}
   \neg & \te{not}\\
 \lor   & \te{or}\\
 \land   & \te{and}\\
  \forall  & \te{for all}\\
  \exists & \te{exists}\\
  = & \te{equals}\\
  (,) & \te{parentheses} \\
  (x_i)_{i : \N}, (y_i)_{i : \N}, (z_i)_{i : \N} & \te{variables}
\end{gmatrix}$$
}

\subsubsection{First-order languages}
\definition{\label{def-language} A (first-order, one-sorted) \tbf{language} $\mc{L}$ comprises the following data:
  \bfenumerate{
  \item A collection of \tbf{constant symbols} $\msf{Const}(\mc{L})$,
  \item a collection of \tbf{relation symbols} $\msf{Rel}(\mc{L})$,
  \item a collection of \tbf{function symbols} $\msf{Funct}(\mc{L})$, and
  \item an assignment of each symbol $S : \msf{Const}(\mc{L}) \cup \msf{Rel}(\mc{L}) \cup \msf{Funct}(\mc{L})$ to a natural number $\opn{arity}(S) : \mbb{N}$.
    }
  }

Whenever we interpret a language on some carrier $A$, we mean for constants $c$ to be interpreted as elements of $A^{\opn{arity}(c)}$, relations $R$ to be interpreted as subsets of $A^{\opn{arity}(R)}$, and for function symbols to be interpreted as functions $A^{\opn{arity}(f)} \to A$.

  \example{
    \begin{itemize}
    \item The language of groups comprises a $1$-ary constant symbol for the identity and a $2$-ary function for group multiplication.

    \item The language of rings comprises constant symbols $0$ and $1$ and $2$-ary functions for addition and multiplication.

     \item The language of set theory comprises just one $2$-ary relation $\in$.
    \end{itemize}
  }

\subsubsection{Terms, formulas, and sentences}
\definition{\label{def-term} A \tbf{term} is a string of symbols defined by structural induction as follows:
  \begin{enumerate}
  \item Any variable $v$ is a term.
  \item Any constant $c$ is a term.
  \item If $t_1, \dots, t_n$ are terms of arities $a_1, \dots, a_n$, then $(t_1, \dots, t_n)$ is a term of arity $a_1 + \dots + a_n$.
  \item If $t$ is a term and $f$ is a function symbol with matching arities, then $f t$ is a term.
  \end{enumerate}
}

Whenever we interpret our language on a carrier $A$, we mean for terms to be interpreted as functions into $A$ which we can construct by composing existing constants (constant functions), basic functions (i.e. the interpretations of the function symbols), and variables (identity).

\definition{\label{def-formula} A \tbf{formula} is defined by structural induction as follows:
  \begin{enumerate}
  \item If $t_1$ and $t_2$ are terms of the same arity, $t_1 = t_2$ is a formula.
  \item If $t$ is a term and $R$ is a relation symbol, and $t$ and $R$ have the same arity, then $R t$ is a formula.
  \item If $\varphi$ is a formula, $\neg \varphi$ is a formula.
  \item If $\varphi$ and $\psi$ are formulas, then $\varphi \lor \psi$ is a formula.
  \item If $\varphi$ and $\psi$ are formulas, then $\varphi \land \psi$ is a formula.
  \item If $\varphi$ is a formula containing a variable $v$, then $\exists v \varphi$ is a formula.
  \item If $\varphi$ is a formula containing a variable $v$, then $\forall v \varphi v$ is a formula.
  \end{enumerate}
}

\definition{\label{def-free-variable}
  Let $\varphi$ be a formula containing the variables $x_1, \dots, x_n$. We say that the variable $x_k$ is \tbf{free} if $x_k$ is not contained in a subformula of the form $\exists x_k \psi$ or $\forall x_k \psi$.

  $x_k$ is \tbf{bound} if it is not free.
}

\definition{\label{def-sentence}
  A formula is a \tbf{sentence} (or \tbf{statement}) if it contains no free variables.

  We write $\msf{Formulas}(\mc{L})$ for all the first-order formulas of $\mc{L}$, and we write $\msf{Sentences}(\mc{L})$ for all the first-order sentences of $\mc{L}$.
}

By convention, we always include sentences called $\true$ and $\false$.


\subsubsection{Predicate calculus and provability}
Throughout this section, we fix a language $\mc{L}$.
% \definition{
%   \label{def-propositional-function}
%   Fix an $n > 1$. The collection of functions $\{\false, \true\}^n \to \{\false, \true\}$ inherits the structure of a Boolean algebra by performing operations pointwise.

%   A \tbf{propositional function} $\{\false, \true\}^n \to \{\false, \true\}$ is defined inductively as follows:
%   \begin{enumerate}
%   \item Every projection $(\epsilon_1, \dots, \epsilon_n) \mapsto \epsilon_k$ is a propositional function.
%   \item If $P$ and $Q$ are propositional functions, then so are
%     $$
% \neg P, P \land Q, P \lor Q, P \to Q, \te{ and } P \leftrightarrow Q.
%     $$
%   \end{enumerate}

% A propositional function is a \tbf{tautology} if it is constantly true.
% }

\definition{
  \label{def-tautology}
  \label{def-propositional-function}
  A \tbf{propositional function} is a function $f : \msf{Prop}^k \to \msf{Prop}$, for some $1 < k : \N$ which we define inductively as follows:
  \begin{enumerate}
  \item The constant functions to $\true$ and $\false$ are propositional functions.
  \item Each projection $(P_1, \dots, P_k) \mapsto P_j$ is a propositional function.
  \item If $f$ and $g$ are propositional functions, so are
    $$
\neg f, f \land g, f \lor g, f \rightarrow g, \te{ and } f \leftrightarrow g,
$$
where the operations above are carried out pointwise in $\msf{Prop}$.
  \end{enumerate}
$f$ is a \tbf{tautology} if $\vdash \forall \vec{p} : \msf{Prop}^k, f \vec{p} \leftrightarrow \true$.
}

\definition{
  \label{def-propositional-combination}
  A \tbf{propositional combination} is a function $f : \msf{Sentences}(\mc{L})^k \to \msf{Sentences}(\mc{L})^k$, for some $1 < k : \N$ which we define inductively as follows:
  \begin{enumerate}
  \item Each projection $(B_1, \dots, B_k) \mapsto B_j$ is a propositional combination.
  \item If $f$ and $g$ are propositional combinations, so are
    $$\neg f, f \land g, f \lor g, f \rightarrow g, \te{ and } f \leftrightarrow g,$$
    where the operations are carried out pointwise in $\msf{Sentences}(\mc{L})$.
  \end{enumerate}
}

By sending projections to projections and symbols $(\neg, \land, \lor, \rightarrow, \leftrightarrow)$ to the corresponding operations on $\msf{Prop}$, every propositional combination $f : \msf{Sentences}(\mc{L})^{k} \to \msf{Sentences}(\mc{L})$ can be realized as a propositional function $\mbf{r}(f) : \msf{Prop}^k \to \msf{Prop}$.

\definition{
  \label{def-predicate-calculus}
  The \tbf{predicate calculus} comprises the following rules for deducing sentences from other sentences. We call deducible sentences \tbf{valid}, and write $\entails_{\mc{L}} \varphi$ to mean that the $\mc{L}$-sentence $\varphi$ is valid (and to disambiguate from $\entails$, which when used unadorned means ``provable in the metatheory).

\alphenumerate{
\item (Rule of the propositional calculus) if $f$ is a propositional combination taking $k$ arguments such that $\mbf{r}(f)$ is a tautology, then for any $k$ sentences $A_1, \dots, A_k$, the value of the propositional combination $f(\varphi_1, \dots, \varphi_k)$ is a valid sentence.

\item (Rule of modus ponens) If $A$ and $A \to B$ are valid, then $B$ is valid.

\item (Rules of equality)
  \bfenumerate{
  \item $\forall x, x = x$, $\forall x \forall y, x = y \wedge y = x$, and $\forall x \forall y \forall z, x = y \wedge y = z \rightarrow x = z$ are all valid.
  \item Let $\varphi(x)$ be a formula whose only free variable is $x$. Then
    $$
\forall x \forall y, (x = y) \rightarrow (\varphi(x) \rightarrow \varphi(y))
$$
is valid.
  }
\item (Change of variable)
  If $A$ is a sentence and $A'$ represents $A$ with all instances of a variable $x$ switched to $y$, then $A \leftrightarrow A'$ is valid.

\item (Rule of specialization ``$\forall$-elimination'')
  Let $c$ be any constant symbol, and let $\varphi(x)$ be a formula whose only free variable is $x$. Then $(\forall x \varphi(x)) \to \varphi(c)$ is valid.

\item (``$\neg$-introduction'')
  If $\neg A \leftrightarrow (A \to \false)$ is valid.

\item (Generalization of constants ``$\forall$-introduction'') \label{forall-introduction}
  Let $B$ be a sentence which does not contain the constant $c$ or the variable $x$. Let $\varphi(x)$ be some formula such that $\varphi(c) \to B$ is valid. Then $\exists x \varphi(x) \to B$ is also valid.\footnote{In particular, using the next rule, if $\neg \varphi(c) \to \false$ is valid, so is $\exists x \neg \varphi(x) \to \false$, so is $\neg \exists x \neg \varphi(x)$, and therefore so is $\forall x \varphi(x)$.}

\item (de Morgan laws)
  Let $\varphi(x)$ have $x$ as its only free variable. Let $B$ be a sentence which does not contain $x$. Then the following are valid statements:
  $$(\neg (\forall x \varphi(x))) \leftrightarrow (\exists x \neg \varphi(x))$$
  $$((\forall x \varphi(x)) \wedge B ) \leftrightarrow \left((\forall x(\varphi(x) \wedge  B\right)$$
  $$((\exists x \varphi(x)) \wedge B ) \leftrightarrow \left((\exists x(\varphi(x) \wedge B\right)$$
  }
  }

  \definition{\label{def-provable} \label{def-consistent} Let $S$ be a collection of sentences. \bfenumerate{
      \item We say that $A$ is provable from $S$ if there exist finitely many $B_1, \dots, B_n : S$ such that $\left(B_1 \wedge \dots \wedge B_n \right) \to A$ is valid.

      \item  We say that $S$ is consistent if $\false$ is not valid.
      }
    }

    \remark{
One may wonder why we work with a type of formulas and not with a collection of $\Prop$s directly. The problem with this is that everything needs to be typed, and so to reason about a predicate (say ``$\in$'') using $\Prop$, we need some carrier type $A$ such that $\in : A \to A \to \Prop$, so that e.g. $\in$ satisfies the axioms of set theory. But then what does it mean for some other type $B$ to have an interpretation of $\in$ and the axioms it satisfies? There then needs to be a separate predicate $\in_B : B \to B \to \Prop$ satisfying the same \emph{kind} of $\Prop$s as $\in : A \to A \to \Prop$. We could proceed to define a typeclass of such $(B, \in_B)$, and we would then be working with models of set theory, but we would lack a way to reason syntactically about the axioms themselves.
      }


      \subsection{Models and satisfiability}
      For the remainder of this section we fix a language $\mc{L}$.
\definition{
  \label{def-theory}
 An \tbf{$\mc{L}$-theory} is a collection of sentences from $\msf{Sentences}(\mc{L})$.
}

\definition{
  \label{def-structure}
  An \tbf{$\mc{L}$-structure} comprises the following data:
  \bfenumerate{
  \item A carrier type $A$,
  \item an assignment of every $c : \msf{Const}(\mc{L})$ to a $c^A : A^{\opn{arity}(c)}$,
  \item an assignment of every $R : \msf{Rel}(\mc{L})$ to a subtype $R^A : A^{\opn{arity}(R)} \to \msf{Prop}$,
  \item an assignment of every $f : \msf{Funct}(\mc{L})$ to a function $f^A : A^{\opn{arity}(f)} \to A$.
    }
  }
  \definition{
    \label{def-
      realization-of-terms}
    Let $A$ be an $\mc{L}$-structure. Using the data of $A$ being an $\mc{L}$-structure, we can inductively assign to every term $t$ (of arity $k$ and containing $n$ free variables) a \tbf{realization} $\mbf{r}(t) : A^n \to A^k$, as follows:
    \begin{enumerate}
    \item If $t = v$ for a variable $v$, $\mbf{r}(t) = \id_A = \lambda v, v$.
    \item If $t = c$ for a constant symbol $c$, $\mbf{r}(t) = A^0 \overset{c^A}{\to} A$.
    \item If $t = (t_1, \dots, t_m)$, then $\mbf{r}(t) = \mbf{r}(t_1) \times \dots \times \mbf{r}(t_m)$.
    \item If $t = f(t_0)$ for some function symbol $f$, then $\mbf{r}(t) = f^A \circ \mbf{r}(t_0)$.
    \end{enumerate}
    }

  \definition{
    \label{def-realization-of-formulas}
    Let $A$ be an $\mc{L}$-structure. Using the data of $A$ being an $\mc{L}$-structure, we can inductively assign to every formula $\varphi(x_1, \dots, x_n)$ (where $x_1, \dots, x_n$ exhaust the free variables of $\varphi$) a \tbf{realization} $\mbf{r}(\varphi) : A^n \to \msf{Prop}$, as follows:
    \begin{enumerate}
    \item If $\varphi$ is of the form $t_1 = t_2$, then $\mbf{r}(\varphi)$ is $\mbf{r}(t_1) = \mbf{r}(t_2)$ (where symbolic equality is realized as true equality).

    \item If $\varphi$ is of the form $R(t)$, $\mbf{r}(R(t))$ is $R^A(\mbf{r}(t))$.

    \item If $\varphi$ is of the form $\neg \psi$, then $\mbf{r}(\varphi)$ is $\neg \mbf{r}(\psi)$.

    \item If $\varphi$ is of the form $\psi \lor \psi'$, then $\mbf{r}(\varphi)$ is $\mbf{r}(\psi) \lor \mbf{r}(\psi')$.

    \item If $\varphi$ is of the form $\psi \land \psi'$, then $\mbf{r}(\varphi)$ is $\mbf{r}(\psi) \land \mbf{r}(\psi')$.

    \item If $\varphi$ is of the form $\exists v \psi$, then $\mbf{r}(\varphi)$ is $\exists v \mbf{r}(\varphi)$.

     \item If $\varphi$ is of the form $\forall v \psi$, then $\mbf{r}(\varphi)$ is $\forall v \mbf{r}(\varphi)$.
    \end{enumerate}
  }

  In particular, each sentence $\varphi$ is sent to a $\msf{Prop}$ $\mbf{r}(\varphi)$.


  \definition{
    \label{def-satisfiability}
    Let $A$ be an $\mc{L}$-structure, and let $\varphi$ be a sentence. We say that $A$ \tbf{satisfies} $\varphi$, written
    $$
A \models \varphi,
$$
if $\entails \mbf{r}(\varphi)$.
}

\definition{
  \label{def-model}
Let $T$ be an $\mc{L}$-theory, and let $A$ be an $\mc{L}$-structure. We say that $A$ is a \tbf{model} of $T$ if for every sentence $\varphi : T$, $A \models \varphi$.
}

\example{
(Line graph)  The \tbf{language of graphs} $\mc{L}_{\msf{Graph}}$ comprises a single $2$-ary relation symbol $E$.

  The \tbf{theory of graphs} $\msf{Graph}$ comprises the sentence $\forall x \forall y \left(E(x,y) \leftrightarrow E(y,x)\right)$.

  The natural numbers $\N$ can be viewed as a model of $\msf{Graph}$ as follows. We realize $E$ as the set
  $$
(y = \opn{succ} x) \lor (x = \opn{succ} y) : \N \to \N  \to \msf{Prop}
$$
which is clearly symmetric.
}

\example{
  Let $\Mod(\msf{Graph})$ be the collection of graphs.\footnote{Warning: this is ``large'', so lives in the next universe up: one can interpret a trivial edge relation on \emph{every} type in the current universe.} A \tbf{graph property} is a map $P : \Mod(\msf{Graph}) \to \Prop$ such that whenever $G \simeq G'$, $P(G) \leftrightarrow P(G')$. We say that $G$ \emph{satisfies} $P$ if $P(g) \leftrightarrow \true$. A graph property is additionally said to be \emph{monotone} if whenever $G \subseteq G'$ is a subgraph, then $P(G') \rightarrow P(G)$.

  For example, the property of being a complete graph is not monotone, while the property of being cycle-free is.

  The \tbf{graph evasiveness conjecture} says that for every monotone graph property $P$ and every $n : \N$, one needs to ask $\binom{n}{2}$ questions of the form ``is there an edge between $v$ and $w$'' to determine if an arbitrary graph on $n$ vertices satisfies $P$.
  }

\example{\label{example-PA}
  (Peano arithmetic)

  The \tbf{language of Peano arithmetic} $\mc{L}_{\msf{PA}}$ comprises:
  \begin{enumerate}
  \item A $1$-ary constant $0$.
  \item Three function symbols $\opn{succ}, +, \times$.
  \end{enumerate}

  The \tbf{theory of Peano arithmetic} $\msf{PA}$ comprises:
  \begin{enumerate}
  \item $\forall x, s(x) \neq 0$
  \item $\forall x \forall y, (s(x) = s(y)) \to x = y$
  \item $\forall x, x + 0 = x$
  \item $\forall x \forall y, x + s(y) = s(x + y)$
  \item $\forall x, x \times 0 = 0$
  \item $\forall x \forall y, x \times S(y) = (x \times y) + x$
  \item[Schema:] For every $\mc{L}_{\msf{PA}}$-formula $\varphi(x)$ with one free variable $x$,
    $$
\medleft \varphi(0) \land \forall x (\varphi(x) \rightarrow  \varphi(\opn{succ} x) ) \medright \rightarrow \forall x \varphi(x).
    $$
  \end{enumerate}

  The \tbf{standard model} of $\msf{PA}$ is $\N$ with $0$ realized as $0 : \N$, $\opn{succ}$ realized as $\opn{succ} : \N \to \N$, $+$ realized as $+ : \N \to \N \to \N$, and $\times$ realized as $\times : \N \to \N \to \N$.
}

By recursing on the inductive type of valid sentences and replacing every rule of the propositional calculus with the corresponding deduction rule for $\msf{Prop}$, we can construct for every valid $\mc{L}$-sentence $\varphi$ a proof that $\mbf{r}(\varphi) \leftrightarrow \true.$

That is the soundness theorem. (In what follows, taking $\psi$ to be $\true$ yields the assertion in the previous paragraph.)

\theorem{\label{theorem-soundness} (Soundness theorem)
  For every $\mc{L}$-structure and any sentences $\varphi, \psi : \msf{Sentences}(\mc{L})$, $$\entails_{\mc{L}} \varphi \to \psi \hspace{4mm} \implies \hspace{4mm} \entails \mbf{r}(\varphi) \to \mbf{r}(\psi).$$
}


This happens regardless of which $\mc{L}$-structure is doing the realizing. When the $\mc{L}$-structure itself is a model of a theory $T$, then whenever $T \entails_{\mc{L}} \psi$, then since there is some sentence $\varphi : T$ such that $\entails_{\mc{L}}\varphi \to \psi$, $\msf{Prop}$'s modus ponens tells us that the model satisfies $\psi$ also.

  \example{
    For example, suppose we're working in the language of graphs expanded with two $1$-ary constants $a$ and $b$, and we know that there is some model $M$ such that $M$ satisfies the sole axiom that $E$ is symmetric. We can show
    $$
\vdash (\forall x \forall y, \mbf{r}(E)(x,y) \leftrightarrow \mbf{r}(E)(y,x)) \rightarrow \mbf{r}(E)(\mbf{r}(a), \mbf{r}(b)) \leftrightarrow \mbf{r}(E)(\mbf{r}(b), \mbf{r}(a))
$$
because we already know the antecedent and can apply $\msf{Prop}$'s $\forall$-elimination.
}

The converse of \myref{Theorem}{theorem-soundness} is false. There may be some things which are incidentally true about the model which are not universally valid.
\example{
  Working again in the language of graphs, consider a complete graph on $n$ vertices. Call this model $M$. $M$ happens to satisfy the $\mc{L}$-sentence
  $$
\medleft \forall x \forall y, E(x,y) \leftrightarrow E(y,x) \medright \rightarrow \medleft \forall x \forall y \forall z, E(x,y) \land E(y,z) \rightarrow E(x,z)\medright,
$$
but this is not a valid $\mc{L}$-sentence. (Indeed, if it were, then the soundness theorem would imply that \emph{every} graph has a transitive edge relation, which is not true.)
}

It will turn out that we can do the next best thing. If we rule out this kind of exception by requiring that $M \models \varphi$ \emph{for every $\mc{L}$-structure} $M$ (resp. every model $M$ of $T$), then it follows that $\entails_{\mc{L}} \varphi$ (resp. $T \entails_{\mc{L}} \varphi$). This is the completeness theorem.

  \subsection{The completeness theorem}
In this section, our goal will be to prove the \tbf{completeness theorem}:
\theorem{\label{theorem-completeness} Let $T$ be an $\mc{L}$-theory. $T$ is consistent if and only if there exists a model of $T$.}

First we will prove that if there exists a model $M$ of $T$, then $T$ is consistent.

\begin{proof}
  We will show the contrapositive: if $T$ is inconsistent, then there does not exist a model $M$ of $T$.

  Indeed, suppose that $T$ is inconsistent. Suppose there is a model $M$. Then by the soundness theorem, $M \models \false$. By definition, this means that
  $$
\entails \false,
$$
so we have shown that
$$
\entails \te{($T$ inconsistent) $\wedge$ (there exists a model $M$ of $T$) $\rightarrow \false$}
$$
which is equivalent to
$$
\entails (T \te{ not inconsistent}) \lor (T \te{ does not have a model}),
$$
which is equivalent to
$$
\entails T \te{ inconsistent } \rightarrow T \te{ does not have a model.}
$$
Taking the contrapositive, we conclude that if $T$ has a model, then $T$ is consistent.
\end{proof}

It then remains to show that if $T$ is consistent, $T$ has a model. We will use the Henkin construction.

% We will first prove \myref{Theorem}{theorem-completeness} in the case where the language $\mc{L}$ of $T$ is \emph{relational}, i.e. has no function symbols. Later, we will show that to every theory $\mc{L}$-theory $T$ we can associate a relational language $\mc{L}_{\opn{rel}}$ and an $\mc{L}_{\opn{rel}}$-theory $T_{\opn{rel}}$ by replacing function symbols with their graph relations. Then we will show that if $T$ is consistent, so is $T_{\opn{rel}}$, and that every model of $T_{\opn{rel}}$ gives rise to a model of $T$, which will give the full completeness theorem.

% Before proceeding, we prove a lemma, valid for any consistent theory in any language.

% \lemma{Suppose $T$ is consistent. Let $\varphi$ be an $\mc{L}$-sentence. Then $T \cup \{\varphi\}$ is consistent or $T \cup \{\neg \varphi\}$ is consistent.}

% \begin{proof}
%   Suppose that both $T \cup \{\varphi\}$ and $T \cup \{ \neg \varphi\}$ are inconsistent. Then there exist sentences $\sigma$ and $\rho$ from $T$ such that
%   $$
% \entails_{\mc{L}} (\sigma \wedge \varphi) \to \false \hspace{2mm} \te{ and } \hspace{2mm} \entails_{\mc{L}} (\rho \wedge \neg \varphi) \to \false.
% $$
% By $\neg$-introduction, we get
% $$
% \entails_{\mc{L}} \neg \left(\sigma \wedge \varphi\right) \hspace{2mm} \te{ and } \hspace{2mm} \entails_{\mc{L}} \neg \left(\rho \wedge \neg \varphi\right)
% $$
% and by $\wedge$-introduction, we get
% $$
% \entails_{\mc{L}} \left(\neg(\sigma \wedge \varphi) \right) \wedge \left(\neg (\rho \wedge \neg \varphi) \right).
% $$
% Since the finitary de Morgan laws are tautologies in the sense of \ref{def-tautology}, it follows that
% $$
% \entails_{\mc{L}} \neg \left(\sigma \lor \varphi \lor \rho \lor \neg \varphi\right).
% $$
% Since the metatheory satisfies the law of the excluded middle, we have that the law of the excluded middle for $\mc{L}$-formulas is a tautology in the sense of \ref{def-tautology}. Therefore,
% $$
% \entails_{\mc{L}} \neg(\sigma \lor \rho) \Leftrightarrow \entails_{\mc{L}} \neg \sigma \land \neg \rho,
% $$
% so by $\wedge$-elimination,
% $\entails_{\mc{L}} \neg \sigma$ and $\entails_{\mc{L}} \neg \rho$, so $T$ is inconsistent.
% \end{proof}

% \theorem{
% \label{theorem-propositional-completeness} Suppose that $S$ is a relational theory, containing no quantifiers, and which is consistent. Then $S$ has a model.
% }

% \begin{proof}
%   We start by choosing a well-ordering of $S$, which induces a well-ordering of the constant and relation symbols which appear in $S$. In turn, this induces a lexicographic ordering on all sentences of the form $c_i = c_j$ and $R_{\beta}(c_1, \dots, c_n)$ where $c_i, c_j$ and $R_{\beta}$ are constant and relation symbols occuring in $S$. Collect these sentences into a single well-ordered set $(F_{\alpha})$.

%   Now, we inductively decide whether the $F_{\alpha}$ should be true or false consistent with $S$. We put $G_{0} \dfeq F_0$ if $S \cup \{F_0\}$ is consistent; otherwise we put $G_0 \dfeq \neg F_0$. Similarly, for $\beta > 0$ we put $G_{\beta} \dfeq F_{\beta}$ if $S \cup \{G_{\alpha} \stbar \alpha < \beta\} \cup \{F_{\beta}\}$ is consistent, and we put $G_{\beta} \dfeq \neg F_{\beta}$ otherwise.

%   From the previous lemma, at each stage $\beta$ of this construction, $S_{\beta} \dfeq S \cup \{G_{\alpha} \stbar \alpha < \beta\}$ is consistent. Since any inconsistency is derivable from finitely many other sentences, the union
%   $$
% H \dfeq \bigcup_{\beta} S_{\beta}
% $$
% is consistent.

% Now, there is a natural equivalence relation on the collection $\mc{C}$ of all constant symbols which occur in $H$, given by $$ c \sim_{\mc{C}} c' \iff c = c' : H .$$ Since $\mc{C}$ is well-ordered, we may pick the least element of each $\sim_{\mc{C}}$-class, and collect them as $\mc{C}'$. We will make $\mc{C'}$ into a model of $H$. First, we realize every constant symbol $c$ as the chosen least representative of its $\sim_{\mc{C}}$-class.

% For every ($n$-ary) relation symbol $R_{\beta}$, we realize $R_{\beta}$ by putting
% $$
% R_{\beta}^{\mc{C}} \left(c_1, \dots, c_n\right) \leftrightarrow \medleft R(c_1, \dots, c_n) : H \medright.
% $$

% It remains to show that $M$ is a model of $S$. Since $S$ was quantifier-free, then by the inductive definition of formulas, every sentence in $S$ is a Boolean combination of atomic sentences (precisely the $F_{\alpha}$) or their negations. Let $\varphi : S$. We can additionally rearrange $\varphi$ into a disjunctive normal form, so that
% $$
% \varphi \equiv \bigvee_{i \leq n} \left(\bigwedge_{j \leq m_i}L^i_j\right),
% $$
% where each $L^i_j$ is an atomic or negated-atomic sentence. For each disjunctand $\bigwedge_{j \leq m_i} L^i_j$, we have each of the $L^i_j$ belong to $\{F_{\alpha}\}$, so either $L^i_j$ or $\neg L^i_j$ belongs to the $\{G_{\alpha}\}$. It follows that if for every $\bigwedge_{j \leq m_i} L^i_j$, there exists some $L^i_{j}$ such that $\neg L^i_j$ is in $\{G_{\alpha}\}$, then $H \entails \neg \varphi$ is inconsistent. Therefore, there must be some disjunctand $\bigwedge_{j \leq m_i} L^i_j$ such that every $L^i_j$ is in $\{G_{\alpha}\}$.

% Since $M$ was designed to satisfy the $G_{\alpha}$, the propositional calculus implies that $M \models \varphi$. Since $\varphi : S$ was arbitrary, $M \models S$.
% \end{proof}

% \definition{
% Let us say that two $\mc{L}$-theories $T$ and $T'$ are \emph{equivalent} if every sentence of $T$ can be proved from $T'$ and every sentence of $T'$ can be proved from $T$. It is easy to see that if $T$ and $T'$ are equivalent, $T$ is consistent if and only if $T'$ is consistent.
% }

% \definition{
% We say that a sentence $\varphi$ is in \tbf{prenex normal form} if any quantifiers occurying in $\varphi$ occur together at the beginning of $\varphi$. We say that a theory is in prenex normal form if every sentence in $T$ is in prenex normal form.
% }

% \lemma{
% Every theory $T$ is equivalent to a theory $T'$ in prenex normal form.
%   }

%   \begin{proof}
%     Apply the change-of-variables rule and the de Morgan rules for quantifiers to change any sentence not in the desired form into one in $T'$.
%   \end{proof}

% \theorem{\label{theorem-relational-completeness}Now suppose that $S$ is a relational theory, which possibly contains quantifiers, and is consistent. Then $S$ has a model.}
% \begin{proof}
%   Let $T$ be a theory whose sentences are either quantifier-free or begin with a quantifier. We expand $T$ (and the language) as follows: for every sentence in $T$ of the form $\exists x \varphi(x)$, we expand the language by a new constant symbol $c$ and adjoin to $T$ the sentence $\varphi(c)$, and for every sentence in $T$ of the form $\forall x \varphi(x)$ and every constant $c$ already occuring in $T$, we adjoin the sentence $\varphi(c)$. We call the result of this process $T^*$.

%   We observe that whenever $T$ is consistent, so is $T^*$: if $T^* \entails_{\mc{L}} \false$, then there are finitely many sentences $\varphi_1, \dots, \varphi_n$ from $T^*$ such that $\entails_{\mc{L}}\left(\bigwedge_{i} \varphi_i \right) \to \false$. We regroup this conjunction according to whether or not $\varphi_i$ contains a new constant symbol or not, viz.
%   $$
% \entails_{\mc{L}} \left(\bigwedge_{i} \varphi_i \right) \wedge \left(\bigwedge_{j} \psi_j(c_j)\right) \to \false,
% $$ where $c_j$ are the new constant symbols. Applying the generalization of constants deduction rule and the de Morgan rules, we conclude that
% $$
% \entails_{\mc{L}} \left(\bigwedge_{i} \varphi_i \right) \wedge \left(\exists x_j\bigwedge_{j} \psi_j(x_j)\right) \to \false
% $$
% and therefore
% $$
% \entails_{\mc{L}} \left(\bigwedge_{i} \varphi_i \right) \wedge \left(\bigvee_{j} \neg \exists x_j \psi_j(x_j)\right).
% $$
% So, for some $j$, $\entails_{\mc{L}} \exists x_j \psi_j(x_j)$, but by construction $\exists x_j \psi_j(x_j) : T$ for $\psi_j(c_j)$ to be in $T^*$. Therefore, $T$ is not consistent.

% Now let $S$ be any consistent theory. We put $S_0 \dfeq S$ and if $S_n$ has already been defined, we put $S_{n+1} \dfeq \left(S_n\right)^*$. Then we obtain a consistent limit theory $\ol{S} \dfeq \bigcup_{n \in \N} S_n$, and we define the model $M$ as we did in the quantifier-free case for the quantifier-free part of $\ol{S}$.
% \end{proof}

% \proposition{\label{prop-T-rel-is-conservative}
% Let $T$ be an $\mc{L}$-theory, and let $T_{\opn{rel}}$ be the associated $\mc{L}_{\opn{rel}}$-theory obtained by replacing function symbols with their graphs. Then any model $M_{\opn{rel}} \models T_{\opn{rel}}$ can be viewed as a model $M \models T$.
% }

% \begin{proof}[Sketch.]
% For every function symbol $f$ of $\mc{L}$, we interpret $f$ as the function specified by the graph relation $\Gamma_f$ in $\mc{L}_{\opn{rel}}$, which was axiomatized in $T_{\opn{rel}}$ to be the graph of a function. This gives an $\mc{L}$-structure $M$. Since $M \models T_{\opn{rel}}$ and every sentence of $T_{\opn{rel}}$ is either a modified version of a sentence in $T$ or asserts that a new relation is a graph of a function, $M \models T$.
% \end{proof}

% \proposition{
% Let $T$ be an $\mc{L}$-theory. If $T$ is consistent, then $T_{\opn{rel}}$ is consistent.
% }
% \begin{proof}[Sketch.]
%  Suppose towards the contrapositive that $T_{\opn{rel}}$ is inconsistent. Then there is a proof from $T_{\opn{rel}}$ of $\false$. It suffices to show that replacing the graphs $\Gamma_f$ by the functions $f$ induces a deduction-preserving map from the valid $\mc{L}_{\opn{rel}}$-sentences to the valid $\mc{L}$-sentences, for then we will have a proof from $T$ of $\false$. This can be done by induction and a case-by-case analysis of the rules of deduction.
% \end{proof}

\subsubsection{The Henkin construction}
\definition{\label{def-henkin-theory} Let $T$ be an $\mc{L}$-theory. We say that $T$ is a \tbf{Henkin theory} if, for every formula $\varphi(x)$, there is a constant $c : \msf{Const}(\mc{L})$ such that
  $T \entails_{\mc{L}} (\exists x \varphi(x)) \rightarrow \varphi(c).$}

\example{\label{fields-henkin} Let $\mc{L}_{\opn{field}}$ be the language of fields, which we define to be $\{0, 1, +, \times, (-)^{-1}\}$ (the usual language of rings augmented with an inversion operation), and let $T$ be the usual axiomatization of a field of characteristic zero. $T$ is not a Henkin theory, for there is no constant $c$ such that e.g. $c = (1 + 1)^{-1}$.}

  \example{\label{true-arithmetic-is-not-a-Henkin-theory} Let $\mc{L}_{\msf{PA}}$ be the language of Peano arithmetic (see \myref{Example}{example-PA}). Let $T$ be the collection of all $\mc{L}_{\msf{PA}}$-sentences $\psi$ such that $N \models \psi$. Then $T$ certainly contains the sentence $\exists x \forall y, x \cdot y = y$. However, $1 = \opn{succ} \hspace{1mm}0$ is not a constant in the language, but rather a term. So $T$ is not a Henkin theory.

    However, if we \emph{expand} $\mc{L}_{\msf{PA}}$ to a language $\mc{L}'$ with a constant symbol $c_n$ for every natural number $n$, and if we let $T'$ be the collection all $\mc{L}'$-sentences $\psi$ such that $\N$ (viewed in the natural way as a model of $\mc{L}'$) satisfies $\psi$, then $T'$ \emph{is} a Henkin theory.
  }

  \proposition{\label{prop-extend-henkin}
    Let $T$ be an $\mc{L}$-theory. If $T$ is consistent, then there exists a language $\mc{L}'$ extending $L$ and an $\mc{L}'$-theory $T'$ extending $T$ viewed as an $\mc{L}$'-theory, such that $T'$ is a Henkin theory.

    Furthermore, if $T$ is consistent, then $T'$ is consistent.
}

\begin{proof}
  Put $\mc{L}_0 \dfeq \mc{L}$ and $T_0 \dfeq T$. We define a chain of languages $\mc{L}_i$ and for each $i$ we define an $\mc{L}_i$-theory $T_i$ as follows: given $\mc{L}_n$ and $\mc{T}_n$, let $\mc{L}_{n+1}$ be the language obtained by adding a constant $c_{\varphi, x}$ where $\varphi$ ranges over all $\mc{L}_{n}$-formulas and $x$ ranges over the free variables of $\varphi$.

  Having defined $\mc{L}_{n+1}$, we now define $T_{n+1}$ to be
  $$
T_{n} \cup \{\exists x \varphi(x) \rightarrow \varphi(c_{\varphi,x})\}_{\varphi, x}
$$
where above we have adjoined a sentence saying that the newly-adjoined constant $c_{\varphi,x}$ behaves as expected.

We put $$T' \dfeq \displaystyle \bigcup_{n \opn{:} \N} T_n.$$ By construction, $T'$ is a Henkin theory.

It remains to show that if $T$ is consistent, so is $T'$. If $T \entails_{\mc{L}} \psi$, then from the finiteness of proofs, we must have that $T_n \entails_{\mc{L}} \psi$ for some $n$. So, to show $T'$ is consistent, it suffices to show that for each $n$, $T_n$ is consistent.

We induct on $n$. The base case $T = T_0$ is by assumption. For the induction step, we must show that if $T_n$ is consistent, then $T_{n+1}$ is consistent.

Suppose towards the contrapositive that $T_{n+1}$ is inconsistent. Since $T_{n+1}$ is obtained by adjoining formulas of the form $\exists x \varphi(x) \rightarrow \varphi(c)$, there must be finitely many such formulas $\psi_1, \dots, \psi_m : T_{n+1} \backslash T_n$ of this form, along with finitely many formulas $\rho_1, \dots, \rho_n$ from $T_n$, such that
$$
\entails_{\mc{L}_{n+1}} \rho_1 \wedge \dots \wedge \rho_n \wedge \psi_1 \wedge \dots \wedge \psi_m \to \false.
$$
By material implication, we get that
$$
\entails_{\mc{L}_{n+1}} \rho_1 \wedge \dots \wedge \rho_n \wedge \psi_1 \wedge \dots \wedge \psi_{m-1} \to \neg \psi_m,
$$
which is equivalent to
$$
\entails_{\mc{L}_{n+1}} \rho_1 \wedge \dots \wedge \rho_n \wedge \psi_1 \wedge \dots \wedge \psi_{m-1} \to \neg (\exists x \varphi_m(x) \rightarrow \varphi_m(c_m)),
$$
which is equivalent to
$$
\entails_{\mc{L}_{n+1}} \rho_1 \wedge \dots \wedge \rho_n \wedge \psi_1 \wedge \dots \wedge \psi_{m-1} \to (\exists x \varphi_m(x)) \wedge \neg \varphi_m(c_m)),
$$
and since $c_m$ does not occur in the premise of the implication, we have that
$$
\entails_{\mc{L}_{n+1}} \rho_1 \wedge \dots \wedge \rho_n \wedge \psi_1 \wedge \dots \wedge \psi_{m-1} \to (\exists x \varphi_m(x)) \wedge \forall x \neg \varphi_m(x))
$$
and therefore
$$
\entails_{\mc{L}_{n+1}} \rho_1 \wedge \dots \wedge \rho_n \wedge \psi_1 \wedge \dots \wedge \psi_{m-1} \to \false.
$$
We conclude that $$\rho_1 \wedge \dots \wedge \rho_n \wedge \psi_1 \wedge \dots \wedge \psi_{m-1}$$ is inconsistent. Repeating this argument, we eliminate all the $\psi_i$ and conclude that $\rho_1 \wedge \dots \wedge \rho_n$ is inconsistent, and therefore that $T$ is inconsistent.
\end{proof}

\newcommand{\term}{\opn{term}}
\definition{
  \label{def-term-model}
  To any Henkin $\mc{L}$-theory $T$, we can associate a canonical structure (a ``term model'') $\opn{term}(T)$ built from the closed terms (i.e. those not containing any variables).

  First, we take the collection $A$ of all closed $\mc{L}$-terms. We define a relation $E : A \to A \to \Prop$, with the convention that $\entails E \hspace{2mm} a_1 \hspace{2mm}  a_2 \leftrightarrow \true$ if and only if $T \entails_{\mc{L}} a_1 = a_2$. By the rules about equality that we have stipulated as part of the predicate calculus, $E$ is an equivalence relation.

  We put $\wt{A} \dfeq A/E$. This will be the underlying type of the model.

  For a constant $c : \msf{Const}(\mc{L})$, we put $c^{\wt{A}} \dfeq c/E$ ($c$ belongs to $\mc{L}_0$, and so is a closed term of $\mc{L}'$).

  For a relation symbol $R : \msf{Rel}(\mc{L})$, we define $R^{\wt{A}} : \wt{A}^{\arity(R)} \to \Prop$ by $R^{\wt{A}}\left(a_1/E, \dots, a_n/E\right) \leftrightarrow T' \entails_{\mc{L}} R(a_1, \dots, a_n)$.

  For a function symbol $f : \msf{Funct}(\mc{L})$, we define $f^{\wt{A}} : \wt{A}^{\arity(f)} \to \wt{A}$ by
  $$
\lambda a_1/E \hspace{2mm} \dots \hspace{2mm} a_n/E, f(a_1, \dots, a_n)/E.
$$
This completes the definition of $\term(T)$.
}
By the soundness theorem, if $T$ is inconsistent, then $\term(T)$ cannot be a model of $T$. But, under suitable assumptions, the inverse is true.

\definition{
  \label{def-complete-theory}
An $\mc{L}$-theory $T$ is \tbf{complete} if for every $\mc{L}$-sentence $\psi$,
  $$
\entails \left(T \entails_{\mc{L}} \psi\right) \lor \left(T \entails_{\mc{L}} \neg \psi\right).
  $$
  }

  \remark{
    Excluded middle in $\Prop$ implies that for any $\mc{L}$-structure $M$ and every $\mc{L}$-sentence $\psi$,
    $$
\entails (M \models \psi) \lor (M \models \neg \psi),
$$
and therefore that the $\mc{L}$-theory of an $\mc{L}$-structure (i.e. the collection of all sentences true in the structure) is complete.
    }

    By invoking the axiom of choice, we can extend any consistent theory to a complete consistent theory. We will prove this.

    \proposition{Let $T$ be a consistent $\mc{L}$-theory.uuuu There exists a complete, consistent $\mc{L}$-theory $T'$ which contains $T$.
      \label{prop-complete-extension}
    }

    To prove this, we will use Zorn's lemma. To start the argument, we prove the following lemma.

        \lemma{Suppose $T$ is consistent. Let $\varphi$ be an $\mc{L}$-sentence. Then $T \cup \{\varphi\}$ is consistent or $T \cup \{\neg \varphi\}$ is consistent.}

\begin{proof}
  Suppose that both $T \cup \{\varphi\}$ and $T \cup \{ \neg \varphi\}$ are inconsistent. Then there exist sentences $\sigma$ and $\rho$ from $T$ such that
  $$
\entails_{\mc{L}} (\sigma \wedge \varphi) \to \false \hspace{2mm} \te{ and } \hspace{2mm} \entails_{\mc{L}} (\rho \wedge \neg \varphi) \to \false.
$$
By $\neg$-introduction, we get
$$
\entails_{\mc{L}} \neg \left(\sigma \wedge \varphi\right) \hspace{2mm} \te{ and } \hspace{2mm} \entails_{\mc{L}} \neg \left(\rho \wedge \neg \varphi\right)
$$
and by $\wedge$-introduction, we get
$$
\entails_{\mc{L}} \left(\neg(\sigma \wedge \varphi) \right) \wedge \left(\neg (\rho \wedge \neg \varphi) \right).
$$
Since the finitary de Morgan laws are tautologies in the sense of \ref{def-tautology}, it follows that
$$
\entails_{\mc{L}} \neg \left(\sigma \lor \varphi \lor \rho \lor \neg \varphi\right).
$$
Since the metatheory satisfies the law of the excluded middle, we have that the law of the excluded middle for $\mc{L}$-formulas is a tautology in the sense of \ref{def-tautology}. Therefore,
$$
\entails_{\mc{L}} \neg(\sigma \lor \rho) \Leftrightarrow \entails_{\mc{L}} \neg \sigma \land \neg \rho,
$$
so by $\wedge$-elimination,
$\entails_{\mc{L}} \neg \sigma$ and $\entails_{\mc{L}} \neg \rho$, so $T$ is inconsistent.
\end{proof}


    \begin{proof}[Proof of \ref{prop-complete-extension}.]
      Consider the poset of proper consistent extensions of $T$. If $T$ is not complete, then the previous lemma shows that this poset is nonempty.

      Now we show that we can take the union of a chain in this poset and obtain an upper bound on that chain.

      Indeed, let $(T_i)_{i \in I}$ be a chain in this poset, and let $T_{\infty}$ be its union. This is clearly a theory which contains all the theories in the chain (and also $T$). We need to show that it is consistent. Indeed, if it were inconsistent, then by the finiteness of proofs, there exists some $T_n$ such that $T_n \entails_{\mc{L}} \false$.

      This now fits the hypotheses of Zorn's lemma, which gives us a maximal consistent extension of $T'$ of $T$. If $T'$ were not complete, then the previous lemma shows that we can extend it.
    \end{proof}

\theorem{\label{theorem-henkin-completeness}
  Let $T$ be a complete Henkin $\mc{L}$-theory. If $T$ is consistent, then $\term(T)$ is a model of $T$.
}
\begin{proof}
  We will show that for every $\psi : \msf{Sentences}(\mc{L})$,
$$
T \entails_{\mc{L}} \psi \iff \term(T) \models \psi.
$$
We will do this by a structural induction on formulas. In the base case, we have atomic sentences.

\begin{itemize}
\item If $T \entails_{\mc{L}} \psi$ and $\psi$ is of the form $a_1 = a_2$ where $a_1$ and $a_2$ are closed terms, then since $T \entails_{\mc{L}} a_1 = a_2$, then $\entails a_1^{\wt{A}} = a_2^{\wt{A}}$ (in $\wt{A}$), so $\term(T) \models \psi$.

   Conversely, if $\term(T) \models \psi$, then $\entails a_1^{\wt{A}} = a_2^{\wt{A}}$, so by definition of the equivalence relation we used to define $\wt{A}$, $T \entails_{\mc{L}} a_1 = a_2$.

\item If $T \entails_{\mc{L}} \psi$ and $\psi$ is of the form $R(a_1, \dots, a_n)$ where $R$ is a relation symbol and $a_1, \dots, a_n$ are closed terms, then since $T \entails_{\mc{L}} R(a_1, \dots, a_n)$, we have that $\entails R^{\wt{A}}(a_1^{\wt{A}}, \dots, a_n^{\wt{A}})$.

   Conversely, if $\term(T) \models \psi$, then $\entails R^{\wt{A}}(a_1^{\wt{A}}, \dots, a_n^{\wt{A}})$, so by definition of how we interpreted $\mc{L}$ onto $\wt{A}$, $T \entails_{\mc{L}} R(a_1, \dots, a_n)$.

\item If $T \entails_{\mc{L}} \psi$ and $\psi$ is of the form $\varphi_1 \wedge \varphi_2$, then by $\wedge$-elimination in $\msf{Sentences}(\mc{L})$, $$\entails (T \entails_{\mc{L}} \psi) \rightarrow (T \entails_{\mc{L}} \varphi_1) \wedge (T \entails_{\mc{L}} \varphi_2).$$ By the induction hypothesis, $\term(T) \models \varphi_1$ and $\term(T) \models \varphi_2$, so by $\wedge$-introduction in $\Prop$, $\term(T) \models \varphi_1 \wedge \varphi_2$.

   Conversely, if $\term(T) \models \varphi_1 \wedge \varphi_2$, then by $\wedge$-elimination in $\Prop$, $\term(T) \models \varphi_1$ and $\term(T) \models \varphi_2$. By the induction hypothesis, $T \entails_{\mc{L}} \varphi_1$ and $T \entails_{\mc{L}} \varphi_2$, so by $\wedge$-introduction in $\msf{Sentences}(\mc{L})$, $T \entails_{\mc{L}} \varphi_1 \wedge \varphi_2$.

\item Suppose $T \entails_{\mc{L}} \psi$ and $\psi$ is of the form $\neg \varphi$. The induction hypothesis says that $T \entails_{\mc{L}} \varphi$ if and only if $\term(T) \models \varphi$. Since $T$ is consistent, $T \not \entails_{\mc{L}} \varphi$. Therefore, by the induction hypothesis, $\term(T) \not \models \varphi$. By the law of the excluded middle, $\term(T) \models \neg \varphi$.

 Conversely, suppose that $\term(T) \models \neg \varphi$. Then $\term(T) \not \models \varphi$, so by the induction hypothesis, $T$ does not prove $\varphi$. Since $T$ was complete, $T \entails_{\mc{L}} \varphi$.

We omit the cases for $\wedge$ and $\rightarrow$, which are entirely analogous.

We conclude that whenever $\psi$ is quantifier-free, $T \entails_{\mc{L}} \psi$ if and only if $\term(T) \models \psi$.

To complete the proof, we must take care of quantifiers.

\item Suppose that $T \entails_{\mc{L}} \exists x \varphi(x)$, where $\varphi(x)$ satisfies the induction hypothesis that if we substitute a closed term $c$ for $x$, $\varphi(c)$ is a sentence such that $T \entails_{\mc{L}} \varphi(c)$ if and only if $\term(T) \models \varphi(c)$.

  Then, since $T$ is a Henkin theory, there exists some $c$ such that
  $$
T \entails_{\mc{L}} \varphi(c).
$$
By the induction hypothesis, we have that
$$
\term(T) \models \varphi(c),
$$
and therefore by $\exists$-introduction in $\Prop$, we conclude that
$$
\term(T) \models \exists x \varphi(x).
$$

Conversely, suppose that $\term(T) \models \exists x \varphi(x)$. By $\exists$-elimination in $\Prop$, there exists some $a/E : \wt{A}$ such that $\entails \mbf{r}(\varphi)(a/E)$, which is equivalent to $\term(T) \models \varphi(a)$. By the induction hypothesis, $T \entails_{\mc{L}} \varphi(a)$, and by $\exists$-introduction in $\msf{Sentences}(\mc{L})$, $T \entails_{\mc{L}} \exists x \varphi(x)$.

\item Similarly, suppose that $T \entails_{\mc{L}} \forall x \varphi(x)$, where $\varphi(x)$ satisfies the induction hypothesis that if we substitute a closed term $c$ for $x$, $\varphi(c)$ is a sentence such that $T \entails_{\mc{L}} \varphi(c)$ if and only if $\term(T) \models \varphi(c)$.

  Then by $\forall$-elimination in $\msf{Sentences}(\mc{L})$, we have that for every constant $c : \msf{Const}(\mc{L})$, $T \entails_{\mc{L}} \varphi(c)$. By the induction hypothesis, $\term(T) \models \varphi(c)$. Since the interpretations of $c$ exhaust $\term(T)$, we conclude by $\forall$-introduction in $\Prop$ that $\term(T) \models \forall x \varphi(x)$.

  Conversely, suppose that $\term(T) \models \forall x \varphi(x)$. By $\forall$-elimination in $\Prop$, for every $a/E \in \wt{A}$, $\entails \mbf{r}(\varphi)(a/E)$, which is equivalent to $\term(T) \models \varphi(a)$. By the induction hypothesis, for every $c : \msf{Const}(\mc{L})$, $T \entails_{\mc{L}} \varphi(c)$.

  Suppose towards a contradiction that $T$ does not prove $\forall x \varphi(x)$. Since $T$ was complete, $T$ proves $\exists x \neg \varphi(x)$. Since we have already proved the cases for $\exists and \neg$, we conclude that $\term(T) \models \exists x \neg \varphi(x)$, and by the axiom of choice we can find a witness $c \in \term(T)$ such that $\term(T) \models \neg \varphi(c)$. This contradicts the conclusion of the previous paragraph.
\end{itemize}
\end{proof}

\corollary{
Let $T$ be a consistent $\mc{L}$-theory. Then $T$ has a model.
}

\begin{proof}
  By \ref{prop-extend-henkin}, extend $T$ to a Henkin theory $T'$. By \ref{prop-complete-extension}, extend $T'$ to a complete theory $T''$.

  $T''$ is again Henkin: for any formula $\varphi(x)$, there already exists a $c$ such that $T' \entails_{L'} \exists x \varphi(x) \leftrightarrow \varphi(x)$, and $T''$ contains all the sentences of $T'$.

  By \ref{theorem-henkin-completeness}, $\term(T'')$ is a model of $T''$. Since $T''$ contains $T$, $\term(T'')$ is also a model of $T$.
\end{proof}

This completes the proof of the completeness theorem.

\subsection{The L\"owenheim-Skolem theorem}
\remph{TODO}
\newpage \section{$\msf{ZFC}$}
The language $\mc{L}_{\msf{ZFC}}$ of set theory comprises just one $2$-ary relation $\in$. Now we give the definition of the $\mc{L}_{\msf{ZFC}}$-theory $\msf{ZFC}$.

\definition{
  \label{def-zfc}
  $\msf{ZFC}$ is defined to be the collection of following axioms and axiom schemas:
  \begin{description}
  \item[Extensionality] \label{zfc-extensionality} $$
\forall x \forall y (\forall z( z \in x \leftrightarrow z \in y) \to x = y).
$$
This says that every set is determined by its elements.

\notation{In what follows, we write ``$x \subseteq y$'' to abbreviate the formal statement $\forall z \in x, z \in y$.}
\item[Empty set] \label{zfc-empty-set}
  $$
\exists x \forall y (\neg y \in x).
$$
Viewing a model of $\msf{ZFC}$ as a directed tree, this says that every model has a least (``root'') element.
\item[Pairing] \label{zfc-pairing}
  $$
\forall x \forall y \exists z \forall w (w \in z \leftrightarrow w = x \lor w = y)
$$
This axiom says that we can form unordered pairs.

\notation{We denote $z$ as above by $\{x, y\}$, adopt the convention that $\{x\} \dfeq \{x,x\}$, and we implement ordered pairs with \emph{Kuratowski ordered pairs}, viz. $(x,y) \dfeq \{\{x\}, \{x,y\}\}$.}

Now that we have defined ordered pairs, we can define functions (internal to $\msf{ZFC}$):
\definition{
A \tbf{function} is a set $f$ of ordered pairs such that $(x,y) \wedge (x,z) \rightarrow y = z$.
}
\item[Union] \label{zfc-union}
  $$
\forall x \exists y \forall z (z \in y \leftrightarrow \exists t(z \in t \wedge t \in x)).
$$
This says that the $y$ above is the union of all the members of $x$. Applying \ref{zfc-pairing}, we conclude that given sets $x$ and $y$, there exists $z$ such that $z = x \cup y$.

  \definition{
    Let $x$ be a set. We denote the \tbf{successor} of $x$ to be the set $\succ x \dfeq x \cup \{x\}$.
  }

\item[Infinity] \label{zfc-infinity}
  $$
\exists x \left(\emptyset \in x \wedge \forall y( y \in x \rightarrow \succ y \in x) \right).
$$

\item[Replacement] \label{zfc-replacement}
    Let $\varphi(x,y, t_1, \dots, t_k)$ be an $\mc{L}_{\msf{ZFC}}$-formula with at least two free variables. For each such formula,
  $$
\forall t_1 \dots \forall t_k (\forall x \exists! y \varphi(x,y,t_1, \dots, t_k) \to \forall u \exists v \forall r( r \in v \leftrightarrow \exists s (s \in u \wedge \varphi(s,r,t_1, \dots, t_k)))).
  $$
  is an axiom of $\msf{ZFC}$.

  This axiom says that if for fixed terms $t_1, \dots, t_k$, $\varphi(x,y,t_1, \dots, t_k)$ is the graph of a function sending $x$ to $y$, then for each set $u$, the image of $u$ under this function is again a set.

  Note that the quantifiers above can range over the entire model of $\msf{ZFC}$.

\item[Powerset] \label{zfc-powerset}
  $$
\forall x \exists y \forall z (z \in y \leftrightarrow z \subseteq x).
$$
\item[Choice] \label{zfc-choice} Let $y : x \to z$ abbreviate the $\mc{L}_{\msf{ZFC}}$-formula which says that $y$ is a function from $x$ to $z$.
  $$
\forall y \forall y \forall z, y : x \to z \wedge (y \neq \emptyset) \rightarrow \left( \exists f (f : x \to (\bigcup z) \wedge \forall a \in x, f(a) \in y(x)) \right).
  $$
More clearly, this says that for every $x$-indexed family of sets $z$, there exists a section to the projection $\bigcup z \twoheadrightarrow x$.
\item[Regularity] \label{zfc-regularity}
  $$
\forall x \exists y  (x = \emptyset \lor (y \in x \wedge \forall z (z \in x \to \neg z \in y)))
$$
This asserts that every set contains an element which is minimal with respect to $\in$.
\end{description}
}

\subsection{Ordinal numbers}
\definition{
  \label{def-zfc-relation}
We say that $y$ is a (binary) \tbf{relation} on $x$ if $y$ is a set of ordered pairs from $X$.
  }
\definition{
  \label{well-ordering}
  We say that a relation $<$ on $x$ is a \tbf{well-ordering} if:
  \begin{enumerate}
  \item $$\forall a \forall b, a = b \lor a < b \lor b <a.$$
  \item $$\forall a \forall b \forall c, a < b \wedge b < c \rightarrow a < c.$$
  \item $$\forall s \subseteq x, s \neq \emptyset \rightarrow \exists a(a \in x \wedge \forall b(b \in s \to \neg a < b)).$$
    \end{enumerate}
  }

  \definition{
A set $x$ is called \tbf{transitive} if $y \in x, z \in y \rightarrow z \in x$.
    }
\definition{
  \label{def-ordinal} We say that a set $\alpha$ is an \tbf{ordinal} if it is well-ordered by the membership relation $\in$ and it is transitive. We abbreviate this assertion by $\opn{Ord} \alpha$.
  }
\subsection{Cardinal numbers}

\definition{
  \label{def-cardinal-number}
  A set $x$ is a \tbf{cardinal number} if it is an ordinal number satisfying the following extra property: for every $y \in x$, there exists no bijection between $y$ and $x$.}

\newpage \section{Boolean-valued models}
\subsection{Boolean algebras}
\newcommand{\lt}{<}

\definition{
  A \tbf{preorder} $B$ is a type $B$ equipped with relations $\leq$ and $\lt$ satisfying the following properties:
  \begin{enumerate}
  \item $\forall a : B, a \leq a$
  \item $\forall a, b, c : B, a \leq b \to b \leq c \to a \leq c$
  \item $\forall a, b : B, a \leq b \land \neg b \leq a$
  \item $\forall a, b : B, a < b \leftrightarrow (a \leq b \land \neg b \leq a)$
  \end{enumerate}
  }

\definition{
  A \tbf{partial order} $B$ is a preorder such that the $\leq$ relation is antisymmetric:
  $$
\forall a, b : B, a \leq b \to b \leq a \to a = b.
  $$
  }

\definition{
  A \tbf{join-semilattice} $B$ is a partial order with binary sup operation $\sqcup$ which satisfies the following properties:
  \begin{enumerate}
  \item $\forall a, b : B, a \leq a \sqcup b$
  \item $\forall a, b : B, b \leq a \sqcup b$
  \item $\forall a, b, c : B, a \leq c \to b \leq c \to a \sqcup b \leq c$.
  \end{enumerate}
  }

\definition{
  A \tbf{meet-semilattice} $B$ is a partial order with a binary infimum operation $\sqcap$ which satisfies the following properties:
  \begin{enumerate}
  \item $ \forall a, b : B, a \sqcap b \leq a$
  \item $\forall a, b : B, a \sqcap b \leq b$
  \item $\forall a, b, c : B, a \leq b \to a \leq c \to a \leq b \sqcap c$.
  \end{enumerate}
  }

\definition{
A \tbf{lattice} $B$ is a join-semilattice which is also a meet-semilattice.
  }

\definition{
  A \tbf{distributive lattice} $B$ is a lattice which satisfies the following property:\footnote{From the \lstinline{mathlib} docstring: a distributive lattice can be defined to satisfy any of four equivalent distribution properties (of sup over inf or inf over sup, on the left or right). A classic example of a distributive lattice is the lattice of subsets of a set, and in fact this example is generic in the sense that every distributive lattice is realizable as a sublattice of a powerset lattice.}
  $$
\label{le-sup-inf} \forall x, y,z : B, (x \sqcup y) \sqcap (x \sqcup z) \leq x \sqcup (y \sqcap z).
  $$}

\definition{
A lattice $B$ has a \tbf{bottom element} $\bot$ if for every $a : B, \bot \leq a$,
  }
\definition{
A lattice $B$ has a \tbf{top element} $\top$ if for every $a : B, a \leq \top$.
  }

\definition{
  A \tbf{bounded lattice} is a lattice with a top and bottom element.
}

\definition{
  \label{def-bounded-distributive-lattice}
  A \tbf{bounded distributive lattice} is a distributive lattice which is bounded.
  }

\definition{
  \label{def-boolean-algebra} A \tbf{Boolean algebra} $B$ is a bounded distributive lattice such that:
  \begin{enumerate}
  \item For every $a : B$, there exists an element $\neg a : B$ which satisfies the following properties:
    \begin{enumerate}
    \item $\forall x : B, x \sqcap \neg x = \bot$
    \item $\forall x : B, x \sqcup \neg x = \top$
    \end{enumerate}
  \item We additionally specify a \tbf{complementation operator} $\lambda x, y, x - y : B \to B$ which satisfies the property:
    $$
    \forall x, y : B, x - y = x \sqcap \neg y.
    $$
  \end{enumerate}
  }

  \definition{
    For convenience, we accumulate the previous definitions into a complete axiomatization of a Boolean algebra. A Boolean algebra is a type $B$ with a specification of binary ordering relations $\leq$, $\lt$, a binary sup operation $\sqcup$, a binary inf operation $\sqcap$, top and bottom elements $\top$, $\bot$, a unary negation operator $\neg$, and a binary subtraction operator $-$, satisfying the following properties:
\begin{enumerate}
\item $\forall (a : B), a ≤ a$
\item $(a b, c_1 : B), a \leq b → b \leq c_1 → a \leq c_1$
\item $(\forall (a, b : B), a < b \iff a \leq b \land ¬b \leq a)$
\item $(a, b : B), a \leq b \to b \leq a \to a = b$
\item $ \forall (a, b : B), a \leq a \sqcup b$
\item $ \forall (a, b : B), b \leq a \sqcup b$
\item $\forall (a, b, c_1 : B), a \leq c_1 \to b \leq c_1 \to a \sqcup b \leq c_1$
\item $\forall (a, b : B), a \sqcap b \leq a$
\item $\forall (a, b : B), a \sqcap b \leq b$
\item $\forall (a, b, c_1 : B), a \leq b \to a \leq c_1 \to a \leq b \sqcap c_1$
\item $\forall (x, y, z : B), (x \sqcup y) \sqcap (x \sqcup z) \leq x \sqcup y \sqcap z$
\item $\forall (a : B), a \leq ⊤$
\item $\forall (a : B), \bot \leq a$
\item $\forall (x : B), x \sqcap -x = ⊥$
\item $\forall (x : B), x \sqcup -x = ⊤$
\item $\forall (x, y : B), x - y = x \sqcap -y$
  \end{enumerate}
}

\definition{
A \tbf{complete lattice} $B$ is a bounded lattice which has operations $\opn{Sup}, \opn{Inf} : \opn{set} B \to B$,
  }

\definition{
  A \tbf{complete distributive lattice} $B$ is a complete lattice which additionally satisfies the following properties:
  \begin{enumerate}
  \item $\forall a : B, s : \opn{set} B, \left(\bigsqcap_{b \in s}, a \sqcup b \leq a \sqcup \opn{Inf} s\right)$
    \item $\forall a : B, s : \opn{set} B, a \sqcap \opn{Sup} s \leq \left(\bigsqcup_{b \in s}, a \sqcap b \right).$
  \end{enumerate}
  }

\definition{
A \tbf{complete Boolean algebra} $B$ is a Boolean algebra which is also a complete distributive lattice.
}

\subsection{Boolean-valued models}
Fix $\mc{L}$ a first-order language and $T$ an $\mc{L}$-theory. Fix $\mbb{B}$ a Boolean algebra.

\newcommand{\bv}[2]{[[#2]]^{#1}}
\definition{\label{def-boolean-valued-structure}
  A \tbf{$\mbb{B}$-valued $\mc{L}$-structure} is the following data:
  \bfenumerate{
  \item A carrier type $A$,
  \item an assignment of every $c : \msf{Const}(\mc{L})$ to a $c^A : A^{\opn{arity}(c)}$,
  \item an assignment of every $R : \msf{Rel}(\mc{L})$ to a $\mbb{B}$-valued map $R^A : A^{\opn{arity}(R)} \to \mbb{B}$; in particular an assignment of a binary $\mbb{B}$-valued map for the equality symbol, and
  \item an assignment of every $f : \msf{Funct}(\mc{L})$ to a function $f^A : A^{\opn{arity}(f)} \to A$.
  }
  If $\phi(\vec{x})$ is a formula, we write $[[\phi(\vec{x})]]^A$ to mean $\phi(\vec{x})$ viewed as a $\mbb{B}$-valued function (taking as many arguments as it has free variables).
  The previous data must satisfy the following properties:
  \begin{enumerate}
  \item For every $a : A$, $[[a = a]]^A = 1$.
  \item For every $a, b: A$, $\bv{A}{a = b} = \bv{A}{b = a}$.
  \item For every $a, b, c : A$, $\bv{A}{a = b} \sqcap \bv{A}{b = c} \leq \bv{A}{a = c}$.
  \item For every $n$-ary function symbol $R$, and for all $n$-tuples $(a_1, \dots, a_n)$ and $(b_1, \dots, b_n)$,
    $$
\left( \bigsqcap_{i = 1}^n \bv{A}{a_i = b_i} \right) \sqcap \bv{A}{R(a_1, \dots, a_n)} \leq \bv{A}{R(b_1, \dots, b_n)}
$$
\item For every $n$-ary function symbol $f$, for every $a, b : A$ and every $(a_1, \dots, a_n)$ and $(b_1, \dots, b_n)$ in $A^n$, the followng three properties hold:
  $$
\left(\bigsqcap_{i = 1}^n \bv{A} {a_i = b_i} \right)\sqcap \bv{A}{f(a_1, \dots, a_N) = a} \leq \bv{A}{f(b_1, \dots, b_n) = b},
$$
$$
\bigsqcup_{a : A} \bv{A}{f(a_1, \dots, a_n) = a}, \te{ and }
$$
$$
\bv{A}{f(a_1, \dots, a_n) = a} \sqcap \bv{A}{f(a_1, \dots, a_n) = b} \leq \bv{A}{a = b}.
$$
  \end{enumerate}
}

\subsection{An example of a Boolean-valued model (experimental)}

A preset is a type-indexed family of presets.

This means that there is an associated indicator function on the ``disjoint union'' of all types, and it is 1 if and only if its argument is inside the indexing type.

Let $\mbb{B}$ be a complete Boolean algebra. We construct a $\mbb{B}$-valued model analogous to the standard model $\mbb{W}$ as follows:

A \tbf{$\mbb{B}$-valued preset} is an $\alpha$-indexed family of $\mbb{B}$-valued presets $ \times $ $\mbb{B}$ (i.e. a type-indexed family of presets with Boolean truth values for membership).

Such objects are called $\mbb{B}$-names. A $\mbb{B}$-name $u$ is specified by the following data:
\begin{enumerate}
\item An indexing type $\alpha$.
\item An indexing function $A : \alpha \to \opn{bSet} \mathbb{B}$.
\item A truth-value function $B : \alpha \to \mathbb{B}$.
\end{enumerate}
\newcommand{\B}{\mathbb{B}}
\section{The maximum principle}
\definition{\label{def-antichain}
  Let $\B$ be a bounded lattice. An \tbf{antichain} in $\B$ is a subset $A \subseteq \B$ satisfying the following property:
  $$
\forall x \in S, \forall y \in S, \left(x \neq y \to x \sqcap y = \bot\right).
  $$
}

\definition{\label{def-indexed-antichain}
  Let $\B$ be a bounded lattice. An \tbf{indexed antichain} is the data of a type $I$ and a map $\msf{A} : I \to \B$ satisfying the following property:
  $$
\forall i, j : I, \left(i \neq j \to \msf{A}(i) \sqcap \msf{A}(j) = \bot\right).
  $$
  }
\definition{\label{def-mixture}
  Let $I$ be a type, and let $\msf{A} : I \to \B$ be an indexed antichain. Let $u : I \to V^\B$ be an $I$-indexed family of $\B$-valued sets. The \tbf{mixture} of $u$ with respect to $A$ is the following $\B$-valued set, which we will specify by the data $\langle \alpha_{\mu}, A_{\mu}, B_{\mu} \rangle$:
  \begin{itemize}
  \item $\alpha_{\mu}$ is defined to be the $\Sigma$-type
    $$
\alpha_{\mu} \dfeq \Sigma_{(i : I)} \alpha_{u(i)}.
$$
\item $A_{\mu}$ is defined to be the map
  $$
\left(A_{\mu} : \alpha_{\mu} \to V^\B  \right) \dfeq \lambda \langle i, x \rangle, A_{u(i)} (x).
  $$
\item $B_{\mu}$ is defined to be the map
  $$
\left(B_{\mu} : \alpha_{\mu} \to \B \right) \dfeq \lambda \langle i, x \rangle, \bigsqcup(j : \iota), \msf{A}(j) \sqcap (A_{u(i)} x) \in^\B u(j).
  $$
  \end{itemize}
}

We focus on a special case of mixtures when $I$ is a type with only two elements.

\definition{\label{def-two-term-mixture}
  Let $a_1, a_2 : \B$, and let $u_1, u_2 \in V^\B$. The \tbf{two-term mixture} of $u_1$ and $u_2$ is the following $\B$-valued set, given by the data $\langle \alpha_{\mu}, A_{\mu}, B_{\mu} \rangle$:
  \begin{itemize}
  \item $\alpha_{\mu} \dfeq \alpha_{u_1} \oplus \alpha_{u_2}$.
  \item $\left(A_{\mu} : \alpha_{\mu} \to V^\B \right) \dfeq \lambda a, A_{u_1} a$ (if $a : \alpha_{u_1}$), and $\lambda a, A_{u_2} a$ otherwise.
  \item $\left(B_{\mu} : \alpha_{\mu} \to \B \right) \dfeq \lambda (a : \alpha_{u_1} \oplus \alpha_{u_2}), \left(a_1 \sqcap (A_{\mu}(a) \in^\B u_1)\right) \sqcup \left(a_2 \sqcap (A_{\mu}(a) \in^\B u_2\right)$
  \end{itemize}
We write $a_1 \cdot u_1 + a_2 \cdot u_2$ for the two-term mixture of $u_1$ and $u_2$ with respect to $a_1$ and $a_2$.
}


\subsubsection{Corollaries of the maximum principle}
  \lemma{\label{lemma-two-term-mixture-membership}
    Let $X$ be a $\B$-valued set, and let $u_1$ and $u_2$ be $\B$-valued sets such that $u_1 \in^\B X = \top$ and $u_2 \in^\B X = \top$. Let $a_1$ and $a_2$ be an antichain such that $a_1 \sqcup a_2 = \top$.

    Then $a_1 \cdot u_1 + a_2 \cdot u_2 \in^\B X = \top$.
  }
  \begin{proof}
    Let $U = a_1 \cdot u_1 + a_2 \cdot u_2$.
    We must show that
    $$
    \top \leq U \in^\B X. % \bigsqcup_{i_y : \alpha_X} B_X (i_y) \sqcap (a_1 \cdot u_1 + a_2 \cdot u_2) =^\B A_X(i_y).
    $$

    By the mixing lemma, we have that $a_1 \leq U =^\B u_1$ and that $a_2 \leq U =^\B u_2$. Therefore, $a_1 \sqcup a_2 = \top \leq U =^\B u_1 \sqcup U =^\B u_2$.

    Conjuncting this with the facts that $T \leq u_1 \in^\B X$ and $T \leq u_2 \in^\B X$ and then eliminating the previous Boolean-valued disjunction, we see that it suffices to prove that
    $$
    (U =^\B u_1) \sqcap (u_1 \in^\B X) \leq U \in^\B X \te{ and } (U=^\B u_1) \sqcap (u_2 \in^\B X) \leq U \in^\B X,
    $$
    and both of these obligations are precisely the left $=^\B$-extensionality of $\in^\B$.
  \end{proof}

\lemma{\label{lemma-two-term-mixture-subset}
Let $X$ be a $\B$-valued set, and let $u_1$ and $u_2$ be $\B$-valued sets% such that $u_1 \in^\B X = \top$ and $u_2 \in^\B X = \top$
. Let $a_1$ and $a_2$ be an antichain such that $a_1 \sqcup a_2 = \top$, such that $a_1 = u_2 \subseteq^\B u_1$. Then $\top \leq u_2 \subseteq^\B a_1 \cdot u_1 + a_2 \cdot u_2$.
}
\begin{proof}
  Let $U$ be the two-term mixture $a_1 \cdot u_1 + a_2 \cdot u_2$. We need to show that
  $$
\top \leq \bigsqcap_{w : V^\B} w \in^\B u_2 \Rightarrow w \in^\B U,
$$
i.e. that for every $w : V^\B$,
$$
w \in^\B u_2 \leq w \in^\B U.
$$
Unfolding the definition of $\in^\B$, we restate our goal as:
$$
\bigsqcup_{i_y : \alpha_{u_2}} B_{u_2}(i_y) \sqcap w =^\B A_{u_2}(i_y) \leq \bigsqcup_{i_z : \alpha_{U}} B_U(i_z) \sqcap w =^\B A_U(i_z).
$$
Eliminating the existential quantifier on the left, we fix an arbitrary $i : \alpha_{u_2}$ and now must show that:
$$
B_{u_2}(i) \sqcap w =^\B A_{u_2}(i) \leq \bigsqcup_{i_z : \alpha_{U}} B_U(i_z) \sqcap w =^\B A_U(i_z).
$$
Instantiating the existential quantifier on the right with $i$, it now suffices to show:
$$
B_{u_2}(i) \sqcap w =^\B A_{u_2}(i) \leq B_U(i) \sqcap w =^\B A_{u_2}(i),
$$
and cancelling like terms, it suffices to show that
$$
\left(B_{u_2}(i)\leq B_U(i)\right) \iff \left(B_{u_2} \leq \left(a_1 \sqcap A_{U}(i) \in^\B u_1 \right) \sqcup \left(a_2 \sqcap A_{U}(i) \in^\B u_2 \right)\right).
$$
Rewriting the right hand side with de Morgan's law and splitting into cases, we see that it now suffices to show:
\begin{enumerate}
\item $B_{u_2}(i) \leq (a_1 \sqcup a_2) = \top$.
\item $B_{u_2}(i) \leq (a_1 \sqcup A_{u_2}(i) \in^\B u_2)$.
\item $B_{u_2}(i) \leq (a_2 \sqcup A_{u_2}(i) \in^\B u_1)$.
\item $B_{u_2}(i) \leq (A_{u_2}(i) \in^\B u_2)$.
\end{enumerate}

All the cases except $(3)$ follow immediately from previous results.

For $(3)$, note that we have by assumption that $a_2 = (\neg (u_2 \subseteq^\B u_1)) \sqcup A_{u_2}(i) \in^\B u_1$, so now our goal is to show
$$
B_{u_2}(i) \leq (u_2 \subseteq^\B u_1) \Rightarrow A_{u_2}(i) \in^\B u_1 \iff \left((u_2 \subseteq^\B u_1) \sqcap B_{u_2}(i) \leq A_{u_2}(i) \in^\B u_1\right).
$$
Instantiating the universal quantifier on the left hand side with $A_{u_2}(i)$, it now suffices to show that
$$
A_{u_2}(i) \in^\B u_2 \Rightarrow A_{u_2}(i) \in^\B u_1 \sqcap B_{u_2}(i) \leq A_{u_2}(i) \in^\B u_1.
$$
Since $B_{u_2}(i) \leq A_{u_2}(i) \in^\B u_2$, we are finished after applying $\leq$-transitivity and Boolean-valued implication elimination.
\end{proof}

\lemma{\label{lemma-maximum-principle-corollary}
  Let $\phi : V^\B \to \B$ be an $=^\B$-extensional function, such that $[[\exists x \phi(x)]] = \top$.
  \bfenumerate{
  \item For every $\B$-valued set $v$, there exists a $\B$-valued set $u$ such that $\phi(u) = 1$ and $\phi(v) = [[u = v]]$.
  \item If $\psi : V^\B \to \B$ is another $=^\B$-extensional function, such that for every $u$, $\phi(u) = \top$ implies $\psi(u)=\top$, then
    $$
    \left(\bigsqcap_{(x : V^\B)} \phi(x) \rightarrow \psi(x)\right) = \top.
    $$
  }}
\begin{proof}
  \bfenumerate{
  \item Since $[[\exists x \phi(x)]] = \top$, we obtain, using the maximum principle, a $w$ such that $\phi(w) = \top$.

    Put $b = \phi(v)$, and let $u$ be the two-term mixture $u = b \cdot v + (\neg b) \cdot w$.
    We make the following observations:
    \begin{enumerate}
    \item $b \leq u =^\B v$ by the mixing lemma.
    \item $b \leq \phi(v)$ by reflexivity.
    \item $\neg b \leq u =^\B w$ by the mixing lemma.
    \item $\neg b \leq \phi(w)$ because everything is bounded by $\top$.
    \end{enumerate}

    Putting these observations together, we conclude that
    $$
    \top = b \sqcup \neg b \leq [[u = v \sqcap \phi(v)]] \sqcup [[u = w \sqcap \phi(w)]] \leq [[\phi(u)]].
    $$
    It remains to show that $\phi(v) = [[u = v]]$. Since $\phi$ is $=^\B$-extensional, we have the inequality
    $$
[[u = v]] = [[u = v]] \sqcap [[\phi(u)]] \leq [[\phi(v)]].
$$
Conversely, by definition of $u$,
$$
\phi(v) = b \leq [[u = v]].
$$
\item Let $v \in V^\B$. We may use part $(1)$ to choose $u \in V^\B$ such that $\phi(u) = \top$, and such that $\phi(v) = u =^\B v$.

  Our goal is then to show that $\phi (v) \leq \psi (v)$. So, we calculate
  $$
\phi(v) \leq \phi(v) \sqcap \top = \phi(v) \sqcap \psi(u) = (u =^\B v) \sqcap \psi(u) \leq \psi(v),
$$
since $\psi$ was $=^\B$-extensional.
  }
\end{proof}

\section{The fundamental theorem of forcing for Boolean-valued models}
The aim of this section is to prove the \emph{fundamental theorem of forcing} (for Boolean-valued models), which states that for any complete Boolean algebra $B$, $V^B$ satisfies all the ZFC axioms.

\subsection{Powersets in $V^\B$}
\definition{\label{def-set-of-indicator} Let $u : V^\B$ be a $\B$-valued set. Let $\chi : \alpha_u \to \B$ be a function. We associate to $\chi$ a $\B$-valued set $\wt{\chi}$, which we think of as being the subset of $u$ induced by $\chi$. We define $\wt{\chi}$ by specifying the data $\langle \alpha, A, B\rangle$:
  \begin{itemize}
  \item $\alpha \dfeq \alpha_u$,
  \item $A \dfeq A_u$,
  \item $B \dfeq \chi$.
  \end{itemize}
}

\definition{\label{def-powerset} Let $u$ be a $\B$-valued set. We define the $\tbf{powerset}$ $\mc{P}(u) : V^\B := \langle \alpha, A, B \rangle$ as follows:
  \begin{itemize}
  \item $\alpha \dfeq \alpha_u \to \B$,
  \item $A : \alpha \to V^\B \dfeq \lambda \chi : \alpha_u \to \B, \wt{\chi}$,
  \item $B : \alpha \to \B \dfeq \lambda \chi : \alpha_u \to \B, \wt{\chi} \subseteq^\B u$.
  \end{itemize}
}

\subsection{The axiom of choice}

Let $x$ be a $\B$-set. By the maximum principle, there exists a $\B$-set $u_x$ such that
$[[u_x \in x]] = \bigsqcup_{(y : V^B)} [[y \in x]]$. By the axiom of choice in the metatheory, we can then define a \emph{global choice function} $\msf{choice} : \opn{bSet} \B \to \opn{bSet} \B$.

Na\"ively, this is not a choice function from the point of view of $V^\B$, as it may not be $=^\B$-extensional.

However, by restricting $\msf{choice}$ to a $\B$-set, we can fulfill the requirements of $(\msf{AC'})$.

\definition{\label{bv-ac1}
The \emph{axiom of choice} is the sentence ($\msf{AC}$):
$$
\forall u, \exists f, \left[\opn{Fun}(f) \land \left( \dom(f) = u \right) \land \left(\forall x, x \in u \to \left( x \neq \emptyset \to f(x) \in x \right)\right)\right].
$$}


It is provably equivalent over $\msf{ZF}$ to the following sentence\footnote{See \url{http://us.metamath.org/mpeuni/ac3.html}}:
\definition{\label{bv-ac2} ($\msf{AC'}$):
$$
\forall x, \exists y, \forall z, z \in x \to \left( z \neq \emptyset \to \exists! w, \left(w \in z \to \exists v, \left( v \in y \to \left( z \in v \land w \in v \right)\right)\right)\right).
$$
}

\theorem{\label{bv-ac2-valid}
The sentence $\msf{AC'}$ has truth value $\top$ in $V^B$.
}

\begin{proof}
  Translated into Boolean truth values, we see that
  $$
[[\msf{AC'}]] = \bigsqcap_{(x : V^B)} \bigsqcup_{(y : V^B)} \bigsqcap_{(z : V^B)} [[z \in x]] \Rightarrow \left([[z = \emptyset]] \Rightarrow \bot \right) $$ $$ \Rightarrow (\bigsqcup!_{(w : V^B)} [[w \in z]] \Rightarrow \bigsqcup_{(v : V^B)} [[v \in y]] \Rightarrow [[z \in v]] \sqcap [[w \in v]].
$$
It then suffices to show that for every $x : V^B$,
$$
\top \leq \bigsqcup_{(y : V^B)} \bigsqcap_{(z : V^B)} [[z \in x]] \Rightarrow \left([[z = \emptyset]] \Rightarrow \bot \right) $$ $$ \Rightarrow (\bigsqcup!_{(w : V^B)} [[w \in z]] \Rightarrow \bigsqcup_{(v : V^B)} [[v \in y]] \Rightarrow [[z \in v]] \sqcap [[w \in v]].
$$
We will finish the proof by constructing a $y$ with which we instantiate the (Boolean-valued) existential quantifier.

Before proceeding with the construction, we indicate how the argument would proceed after instantiating the $y$, which will expose the properties that such a $y$ must satisfy.

So, fix a $y$. Instantiating the quantifier, we now have to show
$$
\top \leq \bigsqcap_{(z : V^B)} [[z \in x]] \Rightarrow \left([[z = \emptyset]] \Rightarrow \bot \right) $$ $$ \Rightarrow (\bigsqcup!_{(w : V^B)} [[w \in z]] \Rightarrow \bigsqcup_{(v : V^B)} [[v \in y]] \Rightarrow [[z \in v]] \sqcap [[w \in v]].
$$
Introducing the $z$, we then have to show that for any $z : V^B$,
$$
\top \leq [[z \in x]] \Rightarrow \left([[z = \emptyset]] \Rightarrow \bot \right) $$ $$ \Rightarrow (\bigsqcup!_{(w : V^B)} [[w \in z]] \Rightarrow \bigsqcup_{(v : V^B)} [[v \in y]] \Rightarrow [[z \in v]] \sqcap [[w \in v]].
$$
Introducing the implications (using, say, the deduction theorem), it suffices to show that
$$[[z \in x]] \Rightarrow \left([[z = \emptyset]] \Rightarrow \bot \right) \leq (\bigsqcup!_{(w : V^B)} [[w \in z]] \Rightarrow \bigsqcup_{(v : V^B)} [[v \in y]] \Rightarrow [[z \in v]] \sqcap [[w \in v]].
$$
It is easy to see that for any $z : V^B$, $$[[z = \emptyset]] = \bigsqcap_{w : V^B} [[w \in z]] \Rightarrow \bot.$$ Let $u_z$ be the witness produced by the maximum principle such that
$$
[[u_z \in z]] = \bigsqcup_{(w : V^B)} [[w \in z]].
$$
% Simplifying the left-hand side of our goal, it now suffices to show that for an arbitrary $w : V^B$,
Therefore, it suffices to show that
$$
[[z \in x]] \sqcap [[u_z \in z]] \leq (\bigsqcup!_{(w : V^B)} [[w \in z]] \Rightarrow \bigsqcup_{(v : V^B)} [[v \in y]] \Rightarrow [[z \in v]] \sqcap [[w \in v]].
$$
Instantiating the quantifier on the right-hand side with $u_z$ and unfolding the definition of the Boolean-valued version of the bounded ``exists unique'' quantifier, it now suffices to show that
$$
[[z \in x]] \sqcap [[u_z \in z]] \leq \bigsqcap_{(w' : V^B)} [[w' \in z]] \Rightarrow \left( \bigsqcup_{(v : V^B)} [[v \in y]] \sqcap [[z \in v]] \sqcap [[w' \in v]] \right) \Rightarrow [[w' = u_z]].
$$
Now we describe how to construct the necessary $y$.

\remph{TODO(jesse): Fix this to include injectivization and finish the proof.}

\end{proof}


\subsubsection{Zorn's lemma}
The axiom of choice is equivalent to the following version of Zorn's lemma, which states that any set whose members are ordered by $\subseteq$ and is closed under unions of chains contains a maximal element.
\definition{\label{bv_zorn} ($\msf{ZL}$):
$$
\forall x, (\forall y, (y \subseteq x \land \forall w_1 \in y, \forall w_2 \in y, w_1 \subseteq w_2 \lor w_2 \subseteq w_1) \implies$$ $$(\bigcup y ) \in x) \implies \exists m \in x, \forall z \in x, m \subseteq x \implies m = x$$}

The aim of this section is to prove the following theorem:

\theorem{Zorn's lemma has truth-value $\top$ in $V^B$.}

To do this, we introduce the notion of a \emph{core} of a $\B$-valued set.

\definition{\label{def-core}
  Let $u$ be a $\B$-valued set. Let $S$ be a set of $\B$-valued sets. We say that $S$ is a \tbf{core} for $u$ if the following properties hold:
\bfenumerate{
  \item For every $v \in S$, $[[x \in u]] = 1$, and
  \item For each $y \in V^B$ such that $[[y \in u]] = 1$, there exists a \emph{unique} $v_y \in S$ such that $[[y = v_y]] = 1$.
}
  }

\lemma{\label{lemma-cores-exist}
Let $u$ be a $\B$-valued set. There exists a set of $\B$-valued sets $S$ which is a core for $u$.
}
\begin{proof}
  Fix $x : V^\B$. We define the set
  $$
  f_x \dfeq \{(a, u_B (a) \sqcap u_A (a)  =^\B x) \stbar a \in u_{\alpha}\}.
  $$
  That is, $f_x$ is the graph-relation of the map
  $$
\lambda a : u_{\alpha}, u_B (a) \sqcap u_A (a) =^\B x.
$$
As such, $f_x : \opn{set} (u_{\alpha} \times \beta)$. Consider the map
$$
(\lambda x : V^\B, f_x) : V^\B \to \opn{set}(u_{\alpha} \times \beta).
$$

Since $\opn{set}(u_{\alpha} \times \beta)$ is a small type, we may perform the same type of smallness argument as we did for the maximum principle, and select lifts of every fiber, obtaining a set $S' : \set V^\B$ which satisfies the following property: for every $x$, there exists a $y$ in $S'$ such that $f_x = f_y$.

There is an equivalence relation $\sim$ on $V^B$, defined by $x_1 \sim x_2 \iff \left(x_1 =^\B x_2 = \top\right)$. This restricts to an equivalence relation on any subset of $V^\B$. In particular, we consider the restriction of $\sim$ to the subset of $S'' \dfeq \{x \in S' \stbar x \in^\B u = \top\}$. We define $S$ to be a transversal of the $\sim$-equivalence classes of $S''$.

It remains to verify that $S$ is a core for $u$. Since $S \subseteq S''$ and $S''$ by definition is made up of $\B$-valued sets $x$ such that $x \in^\B u = \top$, item $\bfe{i}$ of the definition of a core is satisfied.

To verify item $\bfe{ii}$, let $y : V^\B$ such that $y \in^\B u = \top$. By construction of $S'$, there exists a $y' \in S'$ such that $f_{y'} = f_y$. Since the supremum of (the values of) $f_y$ is $\top$, the supremum of (the values of) $f_{y'}$ is $\top$, and therefore $y' \in^\B u = \top$. By construction of $S''$, there exists a unique $y'' \in S''$ such that $y'' =^\B y' = \top$.

We claim that $y =^\B y'' = \top$. To prove this claim, by the transitivity of Boolean-valued equality, it suffices to show that $y =^\B y' = \top$. % We calculate:

Let $a$ be an arbitrary element of $\alpha_u$. By the transitivity of $=^\B$,
$$
y =^\B A_u a \sqcap A_u a =^\B y' \leq y =^\B y'.
$$
This is equivalent to
$$
\left(\bigsqcup_{(a : \alpha_u)} y =^\B A_u a \sqcap A_u a =^\B y'\right) \leq y =^\B y',
$$
and it is easy to check that this implies
$$
\left(\bigsqcup_{(a : \alpha_u)} B_u a \sqcap y =^\B A_u a \sqcap A_u a =^\B y' \sqcap B_u a \right) \leq y =^\B y'
$$
Since $f_y = f_{y'}$, the left-hand side of this can be rewritten to
$$
\left(\bigsqcup_{(a : \alpha_u)} B_u a \sqcap y =^\B A_u a \sqcap B_u a \sqcap y =^\B A_u a \right) \leq y =^\B y',
$$
and it follows that
$
\displaystyle{\top \leq y \in^\B u = \bigsqcup B_u a \sqcap y =^\B A_u a \leq y =^\B y'},
$, as required.

To complete the proof, we must show that $y''$ is unique for $y$. So, let $y'''$ be an element of $S''$ such that $y''' =^\B y = \top$. To show that $y''' = y''$, it suffices to show that $y''' =^\B y' = \top$, because then $y'''$ will belong to the $\sim$-class of $y'$ and by construction of $S''$, $y'''$ will have to be equal to $y''$.

However, we have already seen that $y =^\B y' = \top$, so this follows from the transitivity of $=^\B$.

\end{proof}

\remark{If $u$ is nonempty with truth-value $\top$, then the maximum principle ensures that any core of $u$ is nonempty.}

\lemma{\label{lemma-core}
Let $u$ be a $\B$-valued set such that $[[u \neq \emptyset]] = \top$. Let $S$ be a core for $u$. Then for any $B$-valued set $x$, there exists a $y \in S$ such that $[[x = y]] = [[x \in u]]$.
}
\begin{proof}
  Up to an equality of terms in $\B$, this is exactly \ref{lemma-maximum-principle-corollary}.
\end{proof}

\begin{proof}[Proof of \ref{bv_zorn}]
  Let $X$ be a $\B$-valued set such that $(X, \subseteq)$ is a nonempty inductive partially ordered set. To prove Zorn's lemma, we must show that $X$ has a maximal element.

  Let $S$ be a core for $X$. We define the relation $\leq : S \to S \to \Prop$ as follows:
  $$
\lambda s_1 s_2, [[s_1 \subseteq s_2]] = \top.
$$
It is easy to check that $\leq$ is a partial order on $S$. To apply the Zorn's lemma available in the metatheory, we must show that $\leq$ is inductive, i.e. that every chain has an upper bound.

So, fix a chain $C$ of $S$. We can turn $C$ into a $\B$-valued set $\wh{C}$ by declaring the truth-value of all elements to be $\top$.

We claim that if $C$ was a chain in $S$, then $V^\B \models^\B \wh{C}$ ``is a chain in $X$.''
\begin{proof}[Proof of claim.]
  Formally, ``$\wh{C}$ is a chain'' is the sentence
  $$
\forall u_1 \in \wh{C}, \forall u_2 \in \wh{C}, u_1 \subseteq u_2 \lor u_2 \subseteq u_1,
$$
and so we must show that
$$
\top \leq \bigsqcap_{u_1 \in C} \bigsqcap_{u_2 \in C} u_1 \subseteq^\B u_2 \lor u_2 \subseteq^\B u_1,
$$
or equivalently,
$$
\forall u_1 \in C, \forall u_2 \in C, T \leq u_1 \subseteq^\B u_2 \lor u_2 \subseteq^B u_1.
$$

So, fix $u_1$ and $u_2$ in $C$. Since $C$ was a chain in $S$, either $[[u_1 \subseteq u_2]] = \top$ or $[[u_2 \subseteq u_1]] = \top$.

Without loss of generality, suppose that $[[u_1 \subseteq u_2]] = \top$, as the other case is entirely symmetric. Then $\top \leq u_1 \subseteq^\B u_2$, and by the transitivity of $\leq$, it suffices to show that
$$
u_1 \subseteq^\B u_2 \leq u_1 \subseteq^\B u_2 \sqcup u_2 \subseteq^\B u_1,
$$
which immediately follows from the defining property of the binary sup.

That $\wh{C}$ is a chain in $X$ means that
$$
\top \leq \bigsqcap_{u \in C} u \in^\B X.
$$
But, each $u$ belongs to $C$, which is a subset of a core $S$ for $X$, so $u \in^\B X = \top$.
\end{proof}

Now we claim that for any chain $C$ in $S$, there exists a $u : V^\B$ such that $V^\B \models^\B$ ``$u$ is an upper bound for $\wh{C}$ in $X$''.

\begin{proof}[Proof of claim.]
  We will use $u = \bigcup \wh{C}$. We need to to show two things:
  \bfenumerate{
  \item $\top \leq u \in^\B X$, and
  \item $\top \leq \bigsqcap_{w \in C} w \subseteq^\B u$.
  }
  Item \bfe{ii} is an immediate consequence of the specification of the $\B$-valued unionset operation.

  For item \bfe{i}, we have by assumption that $X$ is inductive, so that
  $$
  T \leq \bigsqcap_{(Y : V^\B)} \left(\left(Y \subseteq^\B X \sqcap \left(\bigsqcap_{w_1 \in Y} \bigsqcap_{w_2 \in Y} w_1 \subseteq^\B w_2 \sqcup w_2 \subseteq^\B w_1\right)\right) \Rightarrow (\bigcup Y) \in^\B X\right)
  $$
  $$
\leq \left(u \subseteq^\B X \sqcap \left(\bigsqcap_{w_1 \in u} \bigsqcap_{w_2 \in u} w_1 \subseteq^\B w_2 \sqcup w_2 \subseteq^\B w_1\right)\right) \Rightarrow (\bigcup Y) \in^\B X
  $$
  Therefore, it suffices to show that
  $$
T \leq \left(\wh{C} \subseteq^\B X \sqcap \left(\bigsqcap_{w_1 \in\wh{C}} \bigsqcap_{w_2 \in\wh{C}} w_1 \subseteq^\B w_2 \sqcup w_2 \subseteq^\B w_1\right)\right),
$$
and so it suffices to show:
\begin{enumerate}
\item $\displaystyle{T \leq\wh{C} \subseteq^\B X}$, and
\item $\displaystyle{T \leq \left(\bigsqcap_{w_1 \in\wh{C}} \bigsqcap_{w_2 \in\wh{C}} w_1 \subseteq^\B w_2 \sqcup w_2 \subseteq^\B w_1\right)}$,
\end{enumerate}

This is exactly the conclusion of the previous claim.
\end{proof}

In particular, $[[u \in x]] = \top$, so by virtue of $S$ being a core, there exists a $w \in S$ such that $[[w = u]] = \top$. Then $w$ is an upper bound for $C$ in $S$: for any other $w' \in S$, $[[w' \in \wh{C}]] = 1$, so $[[w' \subseteq w]] = \top$, and therefore $w' \leq w$.

So $S$ is inductive and we may apply Zorn's lemma. Therefore, $S$ has a maximal element $c$. Since $S$ is a core, $[[c \in X]] = \top$.

To finish the proof, it now suffices to show that $c$ is a maximal element of $X$. That is, we must show that
$$
V^\B \models^\B \forall x \in X, c \subseteq x \to x = c.
$$
That is, we must show that
$$
\top \leq \bigsqcap_{(x \in X)} c \subseteq^\B x \Rightarrow x =^\B c.
$$
Introducing the universal quantifier, it suffices to show that for any $x \in V^\B$,
$$
\top \leq x \in^\B X \Rightarrow c \subseteq^\B x \Rightarrow x =^\B c,
$$
and introducing the implication, it suffices to show that
$$
x \in^\B X \leq c \subseteq^\B x \Rightarrow x =^\B c.
$$
By \ref{lemma-core}, we can find a $y$ such that $x \in^\B X = [[x = y]]$, so we rewrite the above inequality to
$$
[[x = y]] \leq c \subseteq^\B x \Rightarrow x =^\B c.
$$
Introducing another implication, we have
$$
[[x = y]] \sqcap c \subseteq^\B x \leq [[x = c]].
$$
since $\subseteq^\B$ is $=^\B$-extensional, by applying the transitivity of $\leq$, it now suffices to show that
$$
[[x = y]] \sqcap (c \subseteq^\B y) \leq [[x = c]].
$$
If we can show that $c \subseteq^\B y \leq [[y = c]]$, then we are done, by applying transitivity of $\leq$ and then by applying the transitivity of $=^\B$.

Let $a : \B$ be $c \subseteq^\B y$. We let $v$ be the two-term mixture $a \cdot y + (\neg a) \cdot c$.

We claim that $v \in^\B X = \top$.
\begin{proof}[Proof of claim.]
This follows directly from \ref{lemma-two-term-mixture-membership}.
\end{proof}

By virtue of $S$ being a core, there exists a $z \in S$ such that $[[v = z]] = \top$.

We claim that $[[c \subseteq v]] = \top$.
\begin{proof}[Proof of claim.]
This follows directly from \ref{lemma-two-term-mixture-subset}.
\end{proof}

Since $[[v = z]]$, it follows that $[[c \subseteq z]] = \top$, and therefore
$$
c \leq z
$$
in $S$, and since $c$ is $\leq$-maximal, $c = z$, so $c =^\B z = \top$.

Now we calculate:
\begin{align*}
  [[c \subseteq y]] = a &\leq [[y = v]]\\
                        &\leq [[y = v]] \sqcap [[v = z]]\\
                        &\leq [[y = z]] = [[y = c]],
\end{align*}
and the proof is complete.
\end{proof}

\subsection{Consequences of the axiom of choice}

\definition
{Let $x$ and $y$ be $\B$-valued sets.

We say that $x$ is \tbf{larger than} $y$, written $y \prec x$ if there exists a surjection from $x$ onto $y$. We put $x \prec y$ if and only if $x$ is not 

We say that $x$ \tbf{injects into} $y$, written $x \preceq y$, if ``there exists an injection from $x$ into $y$'' has truth-value $\top$.}

\lemma{\label{lt_of_le_of_lt} Let $x, y$ and $z$ be $\B$-valued sets. Then for all $\Gamma : \B$,
  $$
\Gamma \leq \left(\left(x \preceq y\right) \sqcap \left( y \prec z \right)\right) \Rightarrow \left( x \prec z \right).
  $$
}
\begin{proof}
  It suffices to show that
  \begin{align*}
          \Gamma &\leq x \preceq y \\
      \Gamma &\leq y \prec z \\
      \Gamma &\leq - x \prec z \\
      \vdash \Gamma &\leq \bot.
  \end{align*}

  We have that $\Gamma \leq - x \prec z$ expands to $\Gamma \leq \text{``there exists a surjection from $x$ onto $z$''}$. To obtain $\Gamma \leq \bot$, it suffices to show that
  $$
\Gamma \leq - y \prec z,
$$
i.e. it suffices to exhibit some $g$ such that $\Gamma \leq \text{``$g$ is a surjection from $y$ onto $z$''}$.

\remph{TODO}(jesse): finish this
\end{proof}

\subsection{Ordinals in $V^\B$}
\newcommand{\Ord}{\opn{Ord}}
\lemma{\label{lemma-no-new-ordinals}
  Let $u \in V^\B$. Then
  $$
\Ord^\B(u) = \bigsqcup_{\alpha : \opn{ORD}} u =^\B \check{\alpha}.
  $$
}

\begin{proof}
  Since the property of being an ordinal is preserved by taking check-names, for an arbitrary ordinal $\alpha$,
  $$
u =^\B \check{\alpha} = u =^\B \check{\alpha} \sqcap \top = u =^\B \check{\alpha} \sqcap \Ord^\B(\check{\alpha}) \leq \Ord^\B(u),
$$
since the interpretation of any first-order formula is $=^\B$-extensional. So, the inequality
$$
\bigsqcup_{\alpha : \opn{ORD}} u =^\B \check{\alpha} \leq \Ord^\B(u)
$$
follows.

To show the other direction, we first note that since $\eta \neq \xi \implies \check{\eta} =^\B \check{\xi} = \bot$, for any $x : \alpha_u$, the map $\xi \mapsto A_u(x) =^\B \check{\xi}$ is injective when restricted to $D_X \dfeq \{\xi : A_u(x) =^\B \check{\xi} > \bot\}$ (as a function into $\B$).

Since $\B$ is small, so is $D_X$. Put $D = \bigcup_{x : \alpha_u} D_x.$

If $\alpha_0$ is an ordinal greater than every ordinal in $D$, then for every $x : a_u$,
$$
\check{\alpha_0} =^\B A_u(x) = 0,
$$
so
$$
\check{\alpha_0} \in^\B u = 0.
$$
Since the ordinals are well-ordered and satisfy a trichotomy with respect to $\in$, it follows that
$$
\Ord^\B(u) \leq u \in^\B \check{\alpha_0} \sqcup u =^\B \check{\alpha_0} \sqcup \check{\alpha_0} \in^\B u.
$$
Therefore, $\Ord^\B(u) \leq u \in^\B \check{\alpha_0} \sqcup u =^\B \check{\alpha_0}$.

In the first case, $u \in^\B \check{\alpha_0}$, and is therefore equal to some member of $\alpha_0$, which must be the check-name of an ordinal, and therefore an ordinal.

In the second case, $u =^\B \check{\alpha_0}$ obviously implies that there exists an ordinal whose check-name is equal to $u$.
\end{proof}

\subsection{The Cohen poset and the Boolean algebra of regular opens}
The complete Boolean algebra that we will use for forcing the negation of $\CH$ is the \tbf{algebra of regular opens} on a product topological space.

\newcommand{\RO}{\opn{RO}}

\definition{
  \label{def-regular-open}
  Let $(X, \tau)$ be a topological space, where $\tau$ is the collection of open sets in the space. An open set $U \in \tau$ is \tbf{regular} if $U$ is the interior of the closure of $U$.
We denote the collection of regular opens of $(X, \tau)$ by $\RO(X)$.
}

\lemma{
  \label{lemma-regular-open-boolean-algebra}
  For any topological space $X$, $\RO(X)$ is a complete Boolean algebra.
}
\begin{proof}
 \remph{TODO}(floris)
\end{proof}

\subsection{The consistency of $\neg \CH$}
By the Boolean-valued soundness theorem, if $\ZFC$ proves $\msf{CH}$, then $\msf{CH}$ has truth-value $\top$ in every Boolean-valued model of $\ZFC$. Therefore, to show $\neg \left(\ZFC \vdash \CH\right)$, it suffices to show that there exists a Boolean-valued model of $\ZFC$ where $\CH$ has truth-value not equal to $\top$.

Throughout the rest of this section, $\mc{S}$ will denote the type of $\Prop$-valued functions on $\aleph_2 \times \aleph_0$.

We will show that $\CH$ is not true in $V^{\B}$, where $\B$ is defined to be the complete Boolean algebra of regular opens of $\mc{S}$. Our goal will be to prove:

\theorem{\label{theorem-ch-not-true} $\CH$ is not true in $V^\B$. Specifically, $V^\B \models \aleph_2 \leq \left|2^{\aleph}\right|$.}

Before proceeding with the proof of \ref{theorem-ch-not-true}, we set up some prerequisite definitions and lemmas.

\lemma{\label{B-CCC} $\B$ has the countable chain condition.}
\begin{proof}
  \remph{TODO}(floris) %TODO
\end{proof}

\lemma{\label{lemma-CCC-0}
$\check{\aleph_1}$ is a cardinal.
}
\begin{proof}
  It suffices to show that for every $f \in V^\B$ and $\eta \in \aleph_1$ (in $V^\B$) that
  $$
a(f, \eta) = [[ \te{$f$ is a function whose domain is $\eta$ and whose range is $\aleph_1$}]] = \bot.
$$
So, suppose towards a contradiction that there exists some $f \in V^\B$ and $\eta \in \aleph_1$ such that $a(f,\eta) > 0$. Since $\eta$ is an ordinal, we have that $\eta$ is equal to some $\check{\beta}$.

We claim that $\beta < \aleph_1$. For otherwise, $\aleph_1 \subseteq \beta$, so then
$$
\check{\aleph_1} \subseteq \check{\beta} = \eta,
$$
and therefore $\eta \in \eta$, a contradiction.

So, we may assume that $\beta < \aleph_1$. Therefore, $\beta$ is countable.

We have that
$$
a \leq \bigsqcap_{\eta < \aleph_1} \bigsqcup_{\xi < \beta} [[f(\wt{xi}) = \check{\xi}]] \sqcap a
$$
(This restriction of quantifiers can be proved using a similar argument as above.)

Then for each $\eta < \aleph_1$, there exists a least $\xi_{\eta} < \beta$ such that
$$
[[f(\check{\xi_{\eta}}) = \wt{\eta}]] \sqcap a \neq 0.
$$
Since the map $\eta \mapsto \xi_{\eta}$ is a map from the uncountable $\aleph_1$ to the countable $\beta$, there must exist a $\gamma < \beta$ such that the fiber of this map over $\gamma$ is uncountable.

It is then easy to check that the set
$$
\left\{f(\check{\gamma}) =^\B \check{\eta} \sqcap a : \eta \in X\right\}
$$
is an uncountable antichain in $B$, which contradicts the fact that $B$ had the CCC.
\end{proof}

\lemma{\label{lemma-CCC-1} In $V^\B$. $\aleph_{\check 1} \subseteq \check{\aleph_{1}}$.}
\begin{proof}
  By the universal property of the cardinal successor operation (this is using the fact that $\check{\aleph_1}$ is actually a cardinal), it suffices to show that $\aleph_{\check{0}} \subsetneq \check{\aleph_1}$. We have that $\aleph_{\check{0}} = \check{\aleph_0}$, so it suffices to show that $\check{\aleph_0} \subsetneq \check{\aleph_1}$. Since the check-name of an ordinal is an ordinal, this is equivalent to showing that $\check{\aleph_0} \in \check{\aleph_1}$. This follows from the facts that $\aleph_0 \in \aleph_1$ and taking check-names preserves membership.
\end{proof}

% \lemma{\label{lemma-CCC-2} In $V^\B$, $\aleph_{\check 2} \subseteq \check{\aleph_{2}}.$}
% \begin{proof}
%   It suffices to show that $\top \leq \aleph_{\check{1}} \subsetneq \check{\aleph_2}$,
%   because we have that $\aleph_{\check{1}} \subset \aleph_{\check{2}}$, and $\aleph_{\check{2}}$, being the cardinal successor of $\aleph_{\check{1}}$, is $\subseteq$ of anything larger than $\aleph_{\check{1}}$.

%   To show that $\top \leq \aleph_{\check{1}} \subsetneq \check{\aleph_2}$, it suffices to show $\aleph_{\check{1}} \subseteq \check{\aleph_1}$, and this is the conclusion of \ref{lemma-CCC-1}.
% \end{proof}

\lemma{\label{lemma-function-mk} Let $u$ be a $\B$-valued set, and let $F : \alpha_u \to V^\B$ be a function which is $=^\B$-extensional, i.e. for every $i$ and $j$ in $\alpha_u$, $A_u(i) =^\B A_u(j) \leq F(i) =^\B F(j)$. Then $V^\B$ thinks the set of all pairs $(A_u(i), F(i))$ is a function from $u$ to $\langle \alpha_u, F, \lambda i, \top\rangle$.}

\lemma{\label{lemma-function-mk-inj} Let $u$ be a $\B$-valued set, and let $F : \alpha_u \to V^\B$ be a function as in \ref{lemma-function-mk}. If, for every $i$ and $j$ in $\alpha_u$, if $i \neq j$ then $F(i) =^\B F(j) \leq \bot$, then $V^\B$ thinks $\wt{F}$ is injective.}


\definition{\label{def-principal-open} Let $(a,b) : A \times B$. The \tbf{principal open} associated to $(a,b)$ is the collection of all subsets $S$ of $A \times B$ such that $(a,b) \in S$. We denote it by $\mbf{P}_{(a,b)}$. It is a regular open in the product topology on $\opn{set}(A \times B)$.}

\definition{\label{def-cohen-real}
  For each $\nu < \aleph_2$, we define a $\B$-valued set $u_{\nu}$ (which we will think of as a new subset of $\aleph_0$).

  Let $\chi_{\nu} : \alpha_{\aleph_0} \to \B$ be the function defined by $\lambda n : \mathbb{N}, \mbf{P}_{(\nu, n)}.$ We define
  $$
u_{\nu} \dfeq \wt{\chi_{\nu}}
$$
(see \ref{def-set-of-indicator} for a definition of the notation $\chi \mapsto \wt{\chi}$). Each $u_{\nu}$ is called a \tbf{Cohen real}.}

This lemma says that $V^\B$ thinks that every Cohen real is a subset of $\aleph_0$:
\lemma{\label{lemma-cohen-reals-subset}
$u_{\nu} \subseteq^\B \aleph_0 = \top$.
}
\begin{proof}
  By definition, $\subseteq^\B$ unfolds to
  $$
u_{\nu} \subseteq^\B \aleph_0= \bigsqcap_{k : \alpha_{u_{\nu}}} B_{u_{\nu}}(k) \Rightarrow A_{u_{\nu}}(k) \in^\B \aleph_0,
$$
and since it suffices to show that
$$
\top \leq \bigsqcap_{k : \alpha_{u_{\nu}}} B_{u_{\nu}}(k) \Rightarrow A_{u_{\nu}}(k) \in^\B \aleph_0,
$$
then this is equivalent to showing that for every $k : \N$,
$$
\top \leq B_{u_{\nu}}(k) \Rightarrow A_{u_{\nu}}(k) \in^\B \aleph_0
$$
However, by the definition of $\wt{\chi}$, $A_{u_{\nu}}(k)$ is actually just $A_{\aleph_0}$, so this becomes
$$
\top \leq \top \Rightarrow A_{\aleph_0}(k) \in^\B \aleph_0 \iff \top \leq A_{\aleph_0}(k) \in^\B \aleph_0,
$$
and since what $V^\B$ thinks is $\aleph_0$ is actually $\check{\aleph_0}$, this is equivalent to checking that $\top$ is less than or equal to the truth-value of ``the check-name of a finite ordinal is a member of the check-name of $\omega$''. Since this is always true in $V$, this is always true in $V^\B$, so our goal reduces to $\top \leq \top$ and is proved.
\end{proof}

This lemma says that $V^\B$ thinks that every Cohen real is \emph{distinct}:
\lemma{\label{lemma-cohen-reals-distinct}
  Let $\mu$ and $\nu$ belong to $\opn{set}\left(\opn{set}(\aleph)\right)$. If $\mu \neq \nu$, then $u_{\mu} =^\B u_{\nu} = \bot$.
}
\begin{proof}
  Suppose towards a contradiction that there exist $\mu$ and $\nu$ which are distinct such that $u_{\mu} =^\B u_{\nu} > \bot$. Since the Cohen poset $P$ is a basis for the Boolean algebra of regular opens, there exists a $p \in P$ such that $p \Vdash u_{\mu} = \mu_{\nu}$. Viewing $p$ as a partial function with a finite domain, we may choose an $n : \N$ such that for every $\xi : \aleph_2$, $(\xi, n)$ is not in $\dom(p)$.

  We now a define an extension $p'$ of $p$, so that $p \leq p$. Put
  $$
  p' \dfeq p \cup \{((\mu, n), 1)\} \cup \{(\nu, n), 0)\},
  $$
  That is, we define $p'$ to be equal to $p$ everywhere except at $(\mu, n)$ and $(\nu, n)$.\, on which we define the values of $p'$ to be $1$ and $0$, respectively. (This extension is well-defined since $n$ was chosen to not occur in the domain of $p$.)

  Then $p' \Vdash \check{n} \in u_{\mu} \land \check{n} \not \in u_{\nu}$. It follows that $p' \Vdash u_{\mu} \neq u_{\nu}$. However, since $p' \leq p$, $p'$ forces every statement that $p$ forces, so
  $$
p' \Vdash u_{\mu} = u_{\nu},
$$
a contradiction.
\end{proof}
\begin{proof}[Proof of \ref{theorem-ch-not-true}]
It remains to construct a map from $\aleph_{\check{2}}$ to $\mc{P}(\aleph)$ which $V^\B$ believes is injective. We do this by internalizing to $V^\B$ the map $\nu \mapsto u_{\nu}$. In \ref{lemma-function-mk} we saw how a function out of the domain of a $\B$-valued set could be internalized into a function in $V^\B$. Applying the same construction here, we obtain
$$
f : V^\B := \langle \alpha, A, B \rangle,
$$
where:
\begin{itemize}
\item $\alpha \dfeq \alpha_{\check{\aleph_2}}$
\item $A \dfeq F$
\item $B \dfeq \lambda \_, \top$
\end{itemize}

Since $V^\B$ believes the values of the function are all distinct, it follows from \ref{lemma-function-mk-inj} that the function is injective.

By \ref{lemma-cohen-reals-subset}, $V^\B$ thinks this is an injective function into $\mc{P}(\aleph)$.

Since $\B$ has the countable chain condition, by \ref{lemma-CCC-1} we have that $\aleph_1$ is a subset of $\check{\aleph_1}$. Since taking check-names preserves subsets, $\check{\aleph_1}$ is a subset of $\check{\aleph_2}$ of strictly smaller cardinality. Therefore, $V^\B$ thinks that $\aleph_1$ is strictly smaller than $\mc{P}(\N)$: the continuum hypothesis is false in $V^\B$.
\end{proof}

\subsection{A direct proof that cardinal inequalities are preserved assuming CCC}
The proof in this section is adapted from Manin's \emph{A Course in Mathematical Logic for Mathematicians}, Propositions 8.9-8.12.

\definition{
  We define the map $\psi : V^\B \to V^\B \to \B$
  by
  $$
\psi(x,y) \dfeq \bigsqcup_{f : V^\B} (\msf{func}(f) \sqcap \left(\bigsqcap_{v : V^\B} (v \in^\B y) \Rightarrow \left(\bigsqcup_{w : V^\B} w \in^\B x \sqcap (w,v) \in^\B f\right)\right).
  $$
  }

  \theorem{\label{CCC-cardinal-inequalities} Let $s$ and $t$ be sets in $V$ such that $|s| < |t|$ and $|s| \geq \aleph_0$. Assume that $\B$ has the countable chain condition.

Then $\psi(\check{s}, \check{t}) = \bot$.}

\begin{proof}
%   It suffices to show that for any $\Gamma$, $\Gamma \leq \psi(\check{s}, \check{t}) \Rightarrow \bot$. Throughout the rest of this proof we will abuse notation and identify $\Gamma$ with any necessary specializations. Introducing the implication, we have that $\Gamma \leq \psi(\check{s}, \check{t})$ and it suffices to show that $\Gamma \leq \bot$.

%   Casing on $\psi$, we fix an $f : V^\B$ such that $\Gamma \leq \msf{func}(f)$ and
%   $$
% \Gamma \leq \left(\bigsqcap_{v : V^\B} (v \in^\B y) \Rightarrow \left(\bigsqcup_{w : V^\B} w \in^\B x \sqcap (w,v) \in^\B f\right)\right).
% $$
% Introducing the implication, we obtain a $v$ such that $\Gamma \leq v \in^\B y$ and
% $$
% \Gamma \leq \bigsqcup_{w : V^\B} w \in^\B x \sqcap (w,v) \in^\B f.
% $$

% Suppose towards a contradiction that $\bot < \Gamma$. Then
% $$
% \bot < \bigsqcup_{w : V^\B} w \in^\B x \sqcap (w,v) \in^\B f
% $$

\end{proof}

\section{The consistency of $\mathsf{CH}$}

\subsection{Forcing $\mathsf{CH}$}

\definition{Let $\kappa$ be a cardinal, and let $X$ and $Y$ be sets. The \tbf{collapsing forcing notion} $C_{\kappa}(X,Y)$ is the collection of all partial maps $x \to y$ whose domains have cardinality $< \kappa$, with $q \leq p$ iff $q$ extends $p$.}

\definition{Let $\kappa$ be a cardinal, and let $X$ and $Y$ be sets. The \tbf{collapsing topology} on $Y^X$ is defined by the following collection of basic open sets (so that it is finer than the product topology):
  $$
\mc{D}_p \dfeq \{f : X \to Y \stbar p \subseteq f\}.
$$
Let $\left(Y^X, \{\mc{D}_p \stbar p : C_{\kappa}(X,Y)\}\right)$ denote $Y^X$ equipped with the collapsing topology.
}

\definition{
  Let $\kappa$ be a cardinal, and let $X$ and $Y$ be sets. The \tbf{collapsing algebra} $B_{\kappa}(X,Y)$ is defined to be
  $$
  \RO\left( Y^X, \mc{D} \right).
  $$
}

\lemma{\label{B-completes-C} Let $\kappa$ be a cardinal, and let $X$ and $Y$ be sets. Then
  $B_{\kappa}(X,Y)$ is a Boolean completion of $C_{\kappa}(X,Y)$.}

\begin{proof}

\end{proof}
\lemma {\label{omega-closed} $B_{\kappa}(X,Y)$ satisfies the following property: for every $\omega$-indexed descending chain
  $$
D_{p_0} \supseteq \cdots \supseteq D_{p_n} \supseteq \cdots,
$$
there exists a $p_{\omega}$ such that
$$
D_{p_0} \supseteq \cdots \supseteq D_{p_n} \supseteq \cdots \supseteq D_{p_{\omega}}.
$$}

\begin{proof}
  This follows from the fact that a countable union of compatible countable partial functions is again a countable partial function.
\end{proof}

\lemma{\label{omega-closed'} $B_{\kappa}(X,Y)$ satisfies the following property: for every $\omega$-indexed chain $s : \omega \to B_\kappa(X,Y)$ such that $s(0) \supseteq \cdots \supseteq s(n) \supseteq \cdots$ and such that for every $n$, $\bigsqcap_{i \leq n} s(n) \neq \emptyset$,
  $$
\left(\bigcap_{n : \omega} s(n)\right) \neq \emptyset.
$$}

\begin{proof}
  This should follow from the prevous lemma.
\end{proof}

\lemma{\label{lemma-powerset-comparison} Let $X$ be a set. Then for any Boolean algebra $\beta$,
$$\top \leq \check{\mathcal{P}(X)} \subseteq^\beta \mathcal{P}(\check{X}).$$
}

\begin{proof}

\end{proof}
From now one, we fix the collapsing algebra $\B=B_{\aleph_1}(\aleph_1,\mc{P}(\omega))$.

\lemma{In $V^\B$, we have $\vDash \mathcal{P}(\check{X}) \subseteq^\B \check{\mathcal{P}(X)}$.}

\begin{proof}

\end{proof}

\lemma{\label{aleph-one-comparison} For any Boolean algebra $\beta$ we have
$\top \leq \check{\aleph_1} \subseteq^\beta \aleph_1$.
}

\begin{proof}

\end{proof}

\lemma{\label{aleph-one-is-aleph-one} In $V^\B$ we have $\aleph_1 \subseteq^\B \check{\aleph_1}$.}

\begin{proof}

\end{proof}

\definition{\label{collapsing-map-chi} We define $\chi_{\pi}$ to be the following function:
$$
\chi_{\pi} : \check{(\aleph_1)} \to \check{\mc{P}(\omega)} \dfeq (\eta, S) \mapsto \{g : \aleph_1 \to \mc{P}(\omega) \stbar g (\eta) = S \}.
$$
}

\lemma{\label{pi-extensional} $\top \leq (\pi$ is extensional). }

\begin{proof}
  See the formalization.
\end{proof}


\lemma{\label{pi-functional} $\top \leq (\pi$ is functional). }

\begin{proof}
  See the formalization.
\end{proof}

\lemma{\label{pi-surjection} $\top \leq (\pi$ is a surjection). }

\begin{proof}
  See the formalization.
\end{proof}

\definition{\label{collapsing-map} We define a $\B$-valued set $\pi$ which we will show is a surjection from $\check{\aleph_1}$ to $\check{\mc{P}(\omega)}$.

  $\pi$ is defined to be the subset of $\check{\aleph_1} \times \check{\mc{P}(\omega)}$ induced by $\chi_{\pi}$.
  }

\theorem{\label{new-surjection} In $V^\B$,
  $$
\top \leq \text{there exists a surjection from $\aleph_1$ to the continuum}.
$$}

\begin{proof}
  Use $\pi$.
\end{proof}

\theorem{\label{CH-consistent}
Suppose that $\aleph_1 = \check{\aleph_1}$ and $\mc{P}(\check{\omega}) = \check{\mc{P}(\omega)}$. Then
  $$
\top \leq - \bigsqcup_x \bigsqcup_y \omega \prec x \sqcap x \prec y \sqcap y \preceq \mathcal{P}(\omega).
  $$
That is, $V^\B \vDash \CH.$
}

\begin{proof}
  Rewriting negation as an implication of $\bot$ and rewriting using the deduction theorem, it suffices to prove that
  $$
\bigsqcup_x \bigsqcup_y \omega \prec x \sqcap x \prec y \sqcap y \preceq \mathcal{P}(\omega) \leq \bot.
$$
Eliminating the existential quantifiers, it suffices to show that for an arbitrary $x$ and $y$,
$$
\omega \prec x \sqcap x \prec y \sqcap y \preceq \mathcal{P}(\omega) \leq \bot.
$$
Tidying the context, it suffices to show that for an arbitrary context $\Gamma$,
\begin{align}
  \Gamma &\leq \omega \prec x \\
  \Gamma &\leq x \prec y \\
  \Gamma &\leq y \preceq \mathcal{P}(\omega) \\
  \vdash \Gamma &\leq \bot.
\end{align}
Since $\Gamma \leq \omega \prec x$, it follows from the universal property of $\omega$ that $\Gamma \leq \aleph_1 \preceq x$.

Since $\Gamma \leq x \prec y$, it follows that $\Gamma \leq \aleph_1 \prec y$.

Since $\Gamma \leq y \preceq \mathcal{P}(\omega)$, it follows that $\Gamma \prec \aleph_1 \prec \mathcal{P}(\omega)$.

By \myref{Lemma}{new-surjection}, we have that $\Gamma \leq - \left( \aleph_1 \prec \mathcal{P}(\omega)\right)$, so it follows that $\Gamma \leq \bot$, as required.

\end{proof}

To finish the argument, we need to show that $\check{\aleph_1} = \aleph_1$ and that $\check{\mc{P}(\omega)} = \mc{P}(\omega)$.

\theorem{\label{no-new-surjections-onto-aleph-one} If $V^\B \vDash$ ``f is a surjective function from $\omega$ onto $\check{\aleph_1}$'', then there exists a surjective function $g : \omega \to \aleph_1$ in $V$.}

\begin{proof}
  \remph{TODO}
\end{proof}

\theorem{\label{continuum-is-continuum} $V^\B \vDash$ ``$\forall S, S$ is a member of $\mc{P}(\omega)$ iff $S$ is a member of $\check{\mc{P}(\omega)}$ ''}
\begin{proof}
  Since $V^\B \vDash \check{\mc{P}(\omega)} \subseteq^\B \mc{P}(\omega)$, it suffices to show that $V^\B \vDash \mc{P}(\omega) \subseteq^\B  \check{\mc{P}(\omega)} $. That is, we must show that
  $$
V^\B \vDash \bigsqcap (\chi : \omega \to \B), \wt{\chi} \subseteq^\B \omega \Rightarrow \bigsqcup_{S : 2^\omega} \check{\mc{P}(\omega)}\bval(S) \sqcap \wt{\chi} =^\B \check{S}.
$$
By some easy lemmas, we see that this is equivalent to showing that
$$
\forall (\chi : \omega \to \B), V^\B \vDash \bigsqcup_{S : 2^\omega} \wt{\chi} =^\B \check{S}.
$$

Fix an arbitrary $\chi$. Unfolding the definition of $\B$-valued equality and simplifying the $\bval$s of check-names, it suffices to show that
$$
V^\B \vDash \bigsqcup_{S : 2^\omega} \left(\bigsqcap_{n : \omega} \chi(n) \Rightarrow \bigsqcup_{k : S} \check{n} =^\B \check{k} \right) \sqcap \left( \bigsqcap_{k : S} \bigsqcup_{n : \omega} \chi(n) \sqcap \check{n} =^\B \check{k} \right).
$$

Inspecting the conjuncts, we see that the terms of the left conjunct reduce to $\top$ if $n \in S$ and to $- \chi(n)$ if $n \notin S$. The right conjunct as a whole reduces to $\bigsqcap_k \chi(k)$. Therefore, it is equivalent to show
$$
\top \leq \bigsqcup_{S : 2^\omega} \left(\bigsqcap_{n : \neg S} \neg \chi(n)\right) \sqcap \left(  \bigsqcap_{k : S} \chi(k) \right).
$$

Since indexed suprema are the regular-open closure of the union, it suffices to show that
$$
\bigcup_{S : 2^\omega} \left(\bigsqcap_{n : \neg S} \neg \chi(n)\right) \sqcap \left(  \bigsqcap_{k : S} \chi(k) \right)
$$
is dense. That is, for every $p : C_{\aleph_1}(\aleph_1, 2^\omega)$, we must show that
$$
D_p \cap \bigcup_{S : 2^\omega} \left(\bigsqcap_{n : \neg S} \neg \chi(n)\right) \sqcap \left(  \bigsqcap_{k : S} \chi(k) \right) \neq \emptyset.
$$
That is, we must show that there exists some $S : 2^\omega$ such that
$$
D_p \cap \left(\left(\bigsqcap_{n : \neg S} \neg \chi(n)\right) \sqcap \left(  \bigsqcap_{k : S} \chi(k) \right) \right) \neq \emptyset.
$$

Let $S = \{ m : \omega \stbar \neg \chi(m) \cap D_p \} = \emptyset $.

We define $S$ by induction. We put $0 \in S$ if and only if $\chi(0) \sqcap D_p = \emptyset$.

If $k$ has already been decided, put $\sigma(k) \chi(k)$ to be $\chi(k)$ if $k \in S$, and $\neg \chi(k)$ otherwise.

If $0, \dots, n$ have already been decided, then we put $(n+1) \in S$ if and only if
$$
\left(\left(\bigsqcap_{k \leq n} \sigma(k)\chi(k)\right) \sqcap - \chi(n+1)\right) \sqcap D_p = \emptyset.
$$

That concludes the construction of $S$. By construction, and because $\B$ is $\omega$-closed, we conclude that $$D_p \cap \left(\left(\bigsqcap_{n : \neg S} \neg \chi(n)\right) \sqcap \left(  \bigsqcap_{k : S} \chi(k) \right) \right) \neq \emptyset.$$
\end{proof}

It might be easier, however, to prove the following theorem, and then deduce \ref{continuum-is-continuum} by constructing (in $V^\B$) the equivalence between $\mathcal{P}(\omega)$ and $2^\omega$:

\theorem{Let $y$ be a $\B$-valued set. Then $V^\B \vDash$  `` $\forall G, G \in^\B (\check{y})^\omega \Leftrightarrow G \in^\B \check{(y^\omega)}$.''}

\begin{proof}
  Since $V^\B \vDash \check{(y^\omega)} \subseteq \check{y}^\omega$, it suffices to show that
  $V^\B \vDash \check{y}^\omega \subseteq \check{(y^\omega)}$.

  That is, we need to show that for every $\chi : \omega \times y \to \B$,
  $$
V^\B \vDash \msf{is\_func}(\omega) (y) (\wt{\chi}) \Rightarrow \bigsqcup_{f : \omega \to y} \check{f} =^\B \wt{\chi}.
$$
Tidying the context, it suffices to show that for an arbitrary $\Gamma : \B$ such that $\Gamma \leq \msf{is\_func}(\omega) (y) (\wt{\chi})$,
$$
\Gamma \leq \bigsqcup_{f : \omega \to y} \check{f} =^\B \wt{\chi}.
$$

Since indexed suprema are the regular-open closure of the union, it suffices to show that the quantity on the right is dense on the regular open $\msf{is\_func}(\omega) (y) (\wt{\chi})$. To show this, it suffices\footnote{TODO(jesse): formally state and prove this.} to show that for every basic open $D_p$ such that $D_p' := D_p \cap \msf{is\_func}(\omega) (y) (\wt{\chi})$ is not $\bot$, we have that
$$
\bot < D_p' \cap \bigcup_{f : \omega \to y} \check{f} =^\B \wt{\chi}.
$$
This follows immediately by applying \myref{Lemma}{lemma-AE-of-check-func-check'} using the $\omega$-closedness of $\B$, with $\Gamma = D_p'$.

% remark(jesse): while this proof still works as in the specialized case of powersets, it actually obscures the _real_ technique of proof, which is the AE_of_..._check lemma
% Applying subset-extensionality, it suffices to show that
% $$
% \Gamma \leq \bigsqcup_{f : \omega \to y} \wt{\chi} \subseteq^\B \check{f} \sqcap \check{f} \subseteq^\B \wt{\chi} 
% $$
% This unfolds to
% $$
% \Gamma \leq \bigsqcup_{f : \omega \to y} \left( \bigsqcap_{(n, j)} (n,j) \in^\B \wt{\chi} \Rightarrow (n,j) \in^\B \check{f} \right) \sqcap \left( \bigsqcap_{(n, j)} (n,j) \in^\B \check{f} \Rightarrow (n,j) \in^\B \wt{\chi} \right).
% $$
% As above, the terms of the left conjunct is $\top$ if $f (n) = j$, and $\neg \chi(n,j)$ otherwise, and the terms of the right conjunct are $\top$ if $f (n) \neq j$ and $\chi(n,j)$ otherwise. Therefore, this simplifies to

% $$
% \Gamma \leq \bigsqcup_{f : \omega \to y} \left(\bigsqcap_{(n,j) \in f} \chi(n,j) \right) \sqcap \left( \bigsqcap_{(n,j) \not \in f} \neg \chi(n,j) \right).
% $$
\end{proof}

\lemma{\label{lemma-AE-of-check-func-check}
  Let $y : V$, $g : V^\B$, and $\Gamma : \B$ satisfy that $\bot < \Gamma$ and $\Gamma \leq \msf{is\_func}(\omega) (\check{y}) (g)$. Then for every $n : \omega$, there exists a $j : y$ and a $\Gamma' : \B$ such that $\bot < \Gamma' \leq \msf{is\_func}(\omega) (\check{y}) (g) \sqcap (n,j) \in^\B g$, and $\Gamma' \leq \Gamma$.
}
\begin{proof}
  See proof of lemma \lstinline{AE_of_check_func_check} in the formalization.
\end{proof}

\lemma{\label{lemma-AE-of-check-func-check'}
  Let $\B$ be a nontrivial complete Boolean algebra. Suppose that $\B$ is $\omega$-closed. Let $y : V$,$g : V^\B$, and $\Gamma : \B$ satisfy that $\bot < \Gamma$ and $\Gamma \leq \msf{is\_func}(\omega) (\check{y}) (g)$. Then there exists an $f : V$ and a $\Gamma'$ such that $\bot < \Gamma' \leq \Gamma$ and $\Gamma' \leq g =^\B \check{f}$.
}
\begin{proof}
  We simultaneously define, by recursion on $\omega$, a function $B_{(-)} : \omega \to \B$ and a function $f : \omega \to y$:

  For the base case, $B_0$ is the $\Gamma'$ witnessing the conclusion of \myref{Lemma}{lemma-AE-of-check-func-check} with $n = 0$, and $f(0)$ is the $j$ from the same conclusion.

  At the induction step, we have defined $B_0,...,B_n$ and $f(0),...,f(n)$.
  Since $B_n \leq \msf{is\_func}(\omega) (\check{y}) (g)$, we can apply \myref{Lemma}{lemma-AE-of-check-func-check} again with $\Gamma := \B_n$.

  Note that by inspecting the definition of the $B_i$, we see that actually, for every $n$,
  $$
B_n \leq \msf{is\_func}(\omega) (\check{y}) (g) \sqcap (0, f(0)) \in^\B g \sqcap \cdots \sqcap (n, f(n)) \in^\B g.
$$

Since $\B$ is $\omega$-closed, and all finite fragments of the intersection $\bigsqcap_i B_i$ are nonempty, $\bigsqcap B_i$ is nonempty, and so there exists some $B_{\infty}$ such that for every $n$, $B_{\infty} \leq B_n$. Evidently, $B_\infty \leq \bigsqcap_{n : \N} \bigsqcap_{j : y} (n,j) in^\B \check{f} \Rightarrow (n,j) \in^\B g$, and since $g$ was a function, we conclude that $B_{\infty} \leq \check{f} =^\B g$. Therefore, $B_\infty$ is the required $\Gamma'$.
\end{proof}

% To do this, we will need to reflect functions. Our next goal is to prove the following theorem.

% \theorem{\label{reflect-function-main} Let $x$ and $y$ be pre-sets, and let $f$ be a $\B$-valued set such that $V^\B \vDash$ $f$ is a function from $\check{x} \to \check{y}$. Then there exists a pre-set $g$ such that $V \vDash$ $g$ is a function from $x \to y$ and $\check{g} = f$.}

% \lemma{\label{reflect-function-AE} Let $x$ and $y$ be pre-sets, and $f$ be a definite $\B$-valued set such that $V^\B \vDash$ $f$ is a function from $\check{x}$ to $\check{y}$. Then the following statement is true:
%   $$
%   \forall i : x\type, \exists j : y\type, \top \leq \left(\check{x}\func(i), \check{y}\func(j)\right) \in^\B f.
%   $$}

% \begin{proof}

%   Since
%   $$
%   \top \leq \left(\bigsqcap_v v \in^\B \check{x} \Rightarrow \bigsqcup_w w \in^\B\check{y}\sqcap (v,w) \in^\B f\right) \sqcap \left( \opn{ext}(f)  \right),
%   $$
%   we have
%   $$
% \top \leq \left( \bigsqcap_v v \in^\B \check{x} \Rightarrow \bigsqcup_w w \in^\B\check{y} \sqcap (v,w) \in^\B f\right).
% $$
% Localizing the quantifiers, we have
% $$
% \top \leq \left( \bigsqcap_{i : x\type} \check{x}\bval (i) \Rightarrow \bigsqcup_{j : y\type} \check{y}\bval(j) \sqcap (x\func(i),y\func(j)) \in^\B f \right).
% $$

% Since the $\bval$s of a check-name are always $\top$, this simplifies to

% $$
% \top \leq \left( \bigsqcap_{i : x\type} \top \Rightarrow \bigsqcup_{j : y\type}  (\check{x}\func(i),\check{y}\func(j)) \in^\B f \right).
% $$

% Since for any $a$, $\top \Rightarrow a = (- \top) \sqcup a = a,$ this simplifies to

% $$
% \top \leq \left( \bigsqcap_{i : x\type} \bigsqcup_{j : y\type}  (\check{x}\func(i),\check{y}\func(j)) \in^\B f \right).
% $$

% Now, fix an arbitrary $i : x\type$.
% $$
% \top \leq \left( \bigsqcup_{j : y\type}  (\check{x}\func(i),\check{y}\func(j)) \in^\B f \right).
% $$

% Since $\top \leq f \subset^\B \check{x} \times \check{y}$ (i.e., $V^\B$ thinks $f$ is a subset of a check-name), it follows that there exists a $j : y\type$ such that
% $$
% \top \leq \left( (\check{x}\func(i), \check{y}\func(j)) \in^\B f \right).
% $$
% \end{proof}

% \lemma{\label{reflect-function-AE} Let $x$ and $y$ be pre-sets, and $f$ be a definite $\B$-valued set such that $V^\B \vDash$ $f$ is a function from $\check{x}$ to $\check{y}$. We define the \textbf{reflection} of $f$ to be the following pre-set. \remph{TODO}(jesse) finish this}


\subsection{The constructible universe $\mathsf{L}$}

\section{Generic sets: Cohen's original proof}

\section{Sheaves and filterquotients}

\end{document}