The poset of truth values $\{ \mathsf{t},\mathsf{f}\} $ is Cartesian closed with product given by[1]

\begin{align*} \mathsf{t}\times \mathsf{t}& = \mathsf{t},\\ \mathsf{t}\times \mathsf{f}& = \mathsf{f},\\ \mathsf{f}\times \mathsf{t}& = \mathsf{f},\\ \mathsf{f}\times \mathsf{f}& = \mathsf{f}, \end{align*}

and internal Hom $\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }$ given by the partial order of $\{ \mathsf{t},\mathsf{f}\} $, i.e. by

\begin{align*} \mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{t}\webright ) & = \mathsf{t},\\ \mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{f}\webright ) & = \mathsf{f},\\ \mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright ) & = \mathsf{t},\\ \mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright ) & = \mathsf{t}. \end{align*}

Existence of Products
We claim that the products $\mathsf{t}\times \mathsf{t}$, $\mathsf{t}\times \mathsf{f}$, $\mathsf{f}\times \mathsf{t}$, and $\mathsf{f}\times \mathsf{f}$ satisfy the universal property of the product in $\{ \mathsf{t},\mathsf{f}\} $. Indeed, consider the diagrams
Here:

  1. If $P_{1}=\mathsf{t}$, then $p^{1}_{1}=p^{1}_{2}=\text{id}_{\mathsf{t}}$, and there’s indeed a unique morphism from $P_{1}$ to $\mathsf{t}$ making the diagram commute, namely $\text{id}_{\mathsf{t}}$;
  2. If $P_{1}=\mathsf{f}$, then $p^{1}_{1}=p^{1}_{2}$ are given by the unique morphism from $\mathsf{f}$ to $\mathsf{t}$, and there’s indeed a unique morphism from $P_{1}$ to $\mathsf{t}$ making the diagram commute, namely the unique morphism from $\mathsf{f}$ to $\mathsf{t}$;
  3. If $P_{2}=\mathsf{t}$, then there is no morphism $p^{2}_{2}$.
  4. If $P_{2}=\mathsf{f}$, then $p^{2}_{1}$ is the unique morphism from $\mathsf{f}$ to $\mathsf{t}$ while $p^{2}_{2}=\text{id}_{\mathsf{f}}$, and there’s indeed a unique morphism from $P_{2}$ to $\mathsf{f}$ making the diagram commute, namely $\text{id}_{\mathsf{f}}$;
  5. The proof for $P_{3}$ is similar to the one for $P_{2}$;
  6. If $P_{4}=\mathsf{t}$, then there is no morphism $p^{4}_{1}$ or $p^{4}_{2}$.
  7. If $P_{4}=\mathsf{f}$, then $p^{4}_{1}=p^{4}_{2}=\text{id}_{\mathsf{f}}$, and there’s indeed a unique morphism from $P_{4}$ to $\mathsf{f}$ making the diagram commute, namely $\text{id}_{\mathsf{f}}$.

Cartesian Closedness
We claim there’s a bijection

\[ \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (A\times B,C\webright )\cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (A,\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (B,C\webright )\webright ) \]

natural in $A,B,C\in \{ \mathsf{t},\mathsf{f}\} $. Indeed:

  • For $\webleft (A,B,C\webright )=\webleft (\mathsf{t},\mathsf{t},\mathsf{t}\webright )$, we have

    \begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t}\times \mathsf{t},\mathsf{t}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{t}\webright )\\ & = \webleft\{ \text{id}_{\mathsf{true}}\webright\} \\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{t}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{t}\webright )\webright ). \end{align*}

  • For $\webleft (A,B,C\webright )=\webleft (\mathsf{t},\mathsf{t},\mathsf{f}\webright )$, we have

    \begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t}\times \mathsf{t},\mathsf{f}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{f}\webright )\\ & = \emptyset \\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{f}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{f}\webright )\webright ). \end{align*}

  • For $\webleft (A,B,C\webright )=\webleft (\mathsf{t},\mathsf{f},\mathsf{t}\webright )$, we have

    \begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t}\times \mathsf{f},\mathsf{t}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \text{pt}\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\webright ). \end{align*}

  • For $\webleft (A,B,C\webright )=\webleft (\mathsf{t},\mathsf{f},\mathsf{f}\webright )$, we have

    \begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t}\times \mathsf{f},\mathsf{f}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \webleft\{ \text{id}_{\mathsf{false}}\webright\} \\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\webright ). \end{align*}

  • For $\webleft (A,B,C\webright )=\webleft (\mathsf{f},\mathsf{t},\mathsf{t}\webright )$, we have

    \begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f}\times \mathsf{t},\mathsf{t}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \text{pt}\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{t}\webright )\webright ). \end{align*}

  • For $\webleft (A,B,C\webright )=\webleft (\mathsf{f},\mathsf{t},\mathsf{f}\webright )$, we have

    \begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f}\times \mathsf{t},\mathsf{f}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \webleft\{ \text{id}_{\mathsf{false}}\webright\} \\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{f}\webright )\webright ). \end{align*}

  • For $\webleft (A,B,C\webright )=\webleft (\mathsf{f},\mathsf{f},\mathsf{t}\webright )$, we have

    \begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f}\times \mathsf{f},\mathsf{t}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \text{pt}\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\webright ). \end{align*}

  • For $\webleft (A,B,C\webright )=\webleft (\mathsf{f},\mathsf{f},\mathsf{f}\webright )$, we have

    \begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f}\times \mathsf{f},\mathsf{f}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & = \webleft\{ \text{id}_{\mathsf{false}}\webright\} \\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\webright ). \end{align*}

The proof of naturality is omitted.


Footnotes

[1] Note that $\times $ coincides with the “and” operator, while $\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }$ coincides with the logical implication operator.

Noticed something off, or have any comments? Feel free to reach out!


You can also use the contact form below: