%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% to do:
%      
%      
%      

%      
%      give prop monotonicity, local character
%      
%      
%         
%
% questions:
%       can i delete the abstraction from cat. syntax?
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\documentclass [11pt, a4paper, titlepage]{article}

\usepackage[utf8]{inputenc}

%\usepackage{setspace}
%\setlength{\oddsidemargin}{0.5cm}
%\setlength{\textwidth}{15cm}  

\usepackage{textcomp}

\usepackage{verbatim}
\usepackage{graphicx}
\usepackage{url}

\usepackage{amsmath, amssymb, amsfonts, amsthm}
\usepackage{amscd}
\usepackage[all,2cell]{xy} \UseAllTwocells \SilentMatrices \SelectTips{cm}{10}% commutative diagrams
%\usepackage{pb-diagram}

\usepackage[square]{natbib}
%\usepackage{textcomp}
\bibliographystyle{alpha} %harvard-methode

\date{\today}
\author{Benedikt Ahrens}
\title{What is truth?}


\newtheoremstyle{mydefinition}
 {\topsep} % Platz vor dem Theorem
 {\topsep} % Platz nach dem Theorem
 {} % Schrift im Theorem
 {} % Einrueckung (empty = keine Einrueckung, \parindent = Normale Paragrapheneinrueckung)
 {} % Schrift in der Kopfzeile des Theorems
 {} % Punktation nach dem Theoremkopf
 {10pt} %     Space after thm head (\newline = linebreak)
 {{\bfseries\thmnumber{#2 }\thmname{#1}}\emph{\thmnote{ #3}}:} % Kopfformatierung

\newtheoremstyle{myplain}
 {\topsep} % Platz vor dem Theorem
 {\topsep} % Platz nach dem Theorem
 {\itshape} % Schrift im Theorem
 {} % Einrueckung (empty = keine Einrueckung, \parindent = Normale Paragrapheneinrueckung)
 {} % Schrift in der Kopfzeile des Theorems
 {} % Punktation nach dem Theoremkopf
 {10pt} %     Space after thm head (\newline = linebreak)
 {{\bfseries\thmnumber{#2 }\thmname{#1}}\thmnote{ #3}:} % Kopfformatierung

\newtheoremstyle{myremark}
 {\topsep} % Platz vor dem Theorem
 {\topsep} % Platz nach dem Theorem
 {} % Schrift im Theorem
 {} % Einrueckung (empty = keine Einrueckung, \parindent = Normale Paragrapheneinrueckung)
 {} % Schrift in der Kopfzeile des Theorems
 {} % Punktation nach dem Theoremkopf
 {10pt} %     Space after thm head (\newline = linebreak)
 {{\bfseries\thmnumber{#2 }\thmname{#1}}\emph{\thmnote{ #3}}:} % Kopfformatierung

\newtheoremstyle{mybeweis}
 {\topsep} % Platz vor dem Theorem
 {\topsep} % Platz nach dem Theorem
 {} % Schrift im Theorem
 {} % Einrueckung (empty = keine Einrueckung, \parindent = Normale Paragrapheneinrueckung)
 {\itshape} % Schrift in der Kopfzeile des Theorems
 {} % Punktation nach dem Theoremkopf
 {7pt} %     Space after thm head (\newline = linebreak)
 {\thmnumber{#2}\thmname{#1}\thmnote{ #3}:} % Kopfformatierung
%{\thmnumber{ #2 }\thmname{#1}\thmnote{#3}:} % Kopfformatierung

% Theoremumgebungen fuer das Skript definieren
\theoremstyle{mydefinition}
\newtheorem{definition}{Definition}[section]
%\newtheorem{defundsatz}[definition]{Definition und Satz}

\theoremstyle{myplain}
\newtheorem{prop}[definition]{Proposition}
\newtheorem{theorem}[definition]{Theorem}
\newtheorem*{satz*}{Satz}
\newtheorem{lemma}[definition]{Lemma}
\newtheorem{cor}[definition]{Corollary}

\theoremstyle{myremark}
\newtheorem{example}[definition]{Example}
\newtheorem*{example*}{Example}
\newtheorem{remark}[definition]{Remark}
\newtheorem{notation}[definition]{notation}
\newtheorem*{remark*}{Remark}

\theoremstyle{mybeweis}
\newtheorem*{pro}{Proof}

\numberwithin{equation}{section}

\DeclareMathOperator{\card}{card}
\DeclareMathOperator{\MP}{MP}
\DeclareMathOperator{\Gen}{Gen}
\DeclareMathOperator{\Ax}{Ax}
\DeclareMathOperator{\true}{true}
\DeclareMathOperator{\false}{false}
\DeclareMathOperator{\charmap}{char}
\DeclareMathOperator{\Img}{Im}
\DeclareMathOperator{\Sub}{Sub}
\DeclareMathOperator{\Open}{Open}
\DeclareMathOperator{\Id}{Id}
\DeclareMathOperator{\id}{id}
\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\target}{target}
\DeclareMathOperator{\source}{source}
\DeclareMathOperator{\WPT}{WPT}
\DeclareMathOperator{\RZC}{RZC}
\DeclareMathOperator{\ZFC}{ZFC}



\newcommand{\comp}{\circ}
\newcommand{\halmos}{\quad\hfill\mbox{$\Box$}}  % Beweisendezeichen
%\newcommand{\spspace}{~\vspace{-6mm}}
\newcommand{\C}{\mathbf{C}}
\newcommand{\D}{\mathbf{D}}
\newcommand{\T}{\mathcal{T}}
\newcommand{\ot}{\leftarrow}
\newcommand{\monic}{\rightarrowtail}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\xrap}{\to}
\newcommand{\si}{{\sigma}}
\newcommand{\pu}{\partial_u}
\newcommand{\TSet}{{T\text{-}\Set}}
\newcommand{\TauSet}{{\T\text{-}\Set}}
\newcommand{\es}{\emptyset}


\begin{document}

%\maketitle
%\onehalfspacing
%\newpage

\begin{titlepage}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% TITELBLATT

\pagestyle{empty}       % keine Seitennummer
\begin{center}
%\includegraphics{logo_unsa.eps}
\end{center}

\begin{center}
%\vspace*{1cm}
{\huge {\sc Faculty of Sciences}}\\
\vspace*{1cm}
{\Large {\sc Department of Mathematics}} 
\\
\vspace*{3cm}
{\Huge {\bf What is truth?}}
\\
\vspace*{2.5cm}
{\Large Report} \linebreak \\
{\Large Master 2} \linebreak \\
{\Large 2007/2008 }\\
\vspace*{2.5cm}
{\Large 
\begin{tabular}{ll}
Author: & Benedikt Ahrens\\
Supervisor: & Andr\'e Hirschowitz 
\end{tabular}
}
\end{center}

\newpage
\end{titlepage}

\tableofcontents

\newpage
\setcounter{page}{3}
%\setcounter{section}{-1}
\addcontentsline{toc}{section}{Introduction}
\section*{Introduction}
%In reality it might be difficult to define the word "truth". A look on the corresponding wikipedia entry \cite{wiki:truth} will reveal a good dozen of truth definitions, originating mainly in Ancient Greece, Middle Ages and the Age of Enlightenment. 
In general it might be difficult to define the validity or "truth" of a statement. 
In the mathematical sense, however, truth should be defined rigourously. Starting from some basic statements which are supposed to be true, we hope to obtain - \emph{deduce} - new true statements by logical reasoning. But what is a valid deduction and how do the initially true statements influence the set of deducible statements? To understand this it is necessary to \emph{formalize} the process of deduction. This involves the creation of an appropriate language to express unambiguously the statements as well as precise rules for deduction steps. 

Formalizing the way of reasoning also opens new possibilities for mathematicians. A formal language can be understood by machines, which can be used to check the validity of logical reasoning or even create valid deductions themselves. A mathematician working with the help of a machine could leave technical details to the machine and concentrate on the creative part of mathematics. For more information on this topic, see \citep{harrison-form} and \citep{simpson}.

In the first section we give a general definition of a \emph{typed syntax of higher order.}\footnote{There might arise confusion from the following notations: a \emph{syntax} of higher order is a syntax with variable-binding constructors, whereas a higher order \emph{language/logic} in contrast to a first order language is a language in which there is quantification also over the predicates, not just over variables of type \emph{term}. The language $\hat\Sigma_S$ is a first order language/logic, but a higher order syntax.
}This definition is more sophisticated than the one which can be found e.\ g.\ in \citep{manin}. Its advantages are an economical treatment of variables and a built-in structure for the substitution. As an example we present the signature $\Sigma_S$ consisting of logical and set-theoretical symbols. Its induced language $\hat\Sigma_S$ is hence suitable to express statements of set theory. This language has the types \emph{term} and \emph{formula}, but there is no subdivision between different types of terms. As a consequence the quantifiers $\forall$ and $\exists$ range over the whole universe of the interpretation (c.\ f.\ below).

The second and third section are dedicated to the \emph{interpretion} of a formal language. More precisely, in the second section we give a model-theoretical interpretation of the language $\hat	\Sigma_S$ into a universe of sets $M$. 
%In order to do so, we will have to practice set theory in $M$ in an informal way. 
%In order to define the interpretation of the expressions of $\Sigma_S$ we will use set-theoretical means in $M$, using the same methods as of what 
In particular, we define the validity of a set-theoretical formula of $\hat\Sigma_S$ by checking the ``external'' validity of a set-theoretical formula in $M$.
This circularity is explained in \citep{tourlakis} by distinguishing ``real mathematics" from ``syntactic replicas [...]  built within real mathematics", the latter being the formal theory.  In the third section we associate to a \emph{topos} $\T$ a typed higher order syntax $\hat\Sigma_\T$, where the types are the objects of $\T$. Expressions of type $\Omega$, the \emph{subobject classifier} of $\T$, are the formulae of $\hat\Sigma_\T$. The language is also suitable for constructing set-theoretical expressions. In contrast to $\hat\Sigma_S$ the language $\hat\Sigma_\T$ has different types of terms. 
Here the quantifiers $\forall$ and $\exists$ are always \emph{restricted to one type}. That means that they do not range over the whole universe but only over those objects of the universe which are of the corresponding type. 
Another significant difference is that $\hat\Sigma_S$ is a \emph{first order language}, i.\ e.\ there is no quantification over formulae, while in $\hat\Sigma_\T$ there is such quantification (c.\ f.\  \ref{prop:boolean}). The language $\hat\Sigma_\T$ is hence a \emph{second order language}.
The circularity we encounter in the model-theoretical interpretation is avoided in the categorical approach. 

\section{Syntax - Building Trees}
\subsection{Monads \& Modules}

We presume some knowledge about category theory, as can be found e.\ g.\ in \citep{maclane}, \citep{aac} or the first chapter of \citep{sheaves}.

In this subsection we give some definitions and propositions without proofs. The latters can all be found in \citep{julianna}
%explain higher order typed syntax with monads
\begin{definition}
 A \emph{monad} of the category $\Set$ of sets is a triple $(T, \eta, \mu)$ consisting of a functor $T:\Set \to \Set$ and two natural transformations $\eta : \Id_\Set \xrap T$ and $\mu:T^2 \xrap T$ such that the following diagrams commute for any set $X$: 
%\begin{equation}
%\begin{xy}
%\xymatrix {
%T X \ar[r]^{T \eta_X} \ar[rd]_{Id_{T X}} & T^2 X \ar[d]|{\mu_X} \ar@{}[ld]|/-.8em/{I.} \ar@{}[rd]|/-.8em/{II.} & T X \ar[l]_{\eta_{T X}} \ar[dl]^{Id_{T X}}\\
% & T X &
%}
%\end{xy}
%\label{eta}
%\end{equation}

\begin{equation*}
\begin{xy}
\xymatrix{
T X \ar[r]^{T \eta_X} \ar@2{-}[rd] & T^2 X \ar[d]|{\mu_X} \ar@{}[ld] \ar@{}[rd] & T X \ar[l]_{\eta_{T X}} \ar@2{-}[dl] & T^3 X \ar[r]^{\mu_{TX}} \ar[d]_{T\mu_X} & T^2 X \ar[d]^{\mu_X} \\
& T X, & &T^2 X \ar[r]_{\mu_X} & T X.
}
\end{xy}
%\label{mu}
\end{equation*}
\label{monade}
\end{definition}


\begin{definition}\label{star} 
 For a set $X$ of $\Set$ we define $X^*$ to be the disjoint union of $X$ with an element $\infty_X$.
For a morphism of sets $f: X \to Y$ we define $f^*:X^* \to Y^*$ to be such that $f^*|_X = f$ and $f(\infty_X) = \infty_Y$. This makes ${(\_)}^*:\Set\to \Set$ a functor.
\end{definition}

\begin{comment}
\begin{definition}
Given a monad $R$, we construct its {\em derived} monad $R'$ by setting for each $X$ in $\Set$:
\begin{equation*}
R' X := R (X^*).
\end{equation*}
For any morphism of sets $f:X\to Y$ we set:
\begin{equation*}
 R' f := R (f^*).
\end{equation*}

\end{definition}

\begin{prop}
The derived monad $R'$ of a monad $R$ is a monad.
\label{rem_monade_der}
\end{prop}

\begin{definition}
Let $(T,\eta^{(T)},\mu^{(T)})$ and $(S,\eta^{(S)},\mu^{(S)})$ be two monads. A {\em morphism of monads} $\tau$ is a natural transformation $\tau: T \xrap S$ which is compatible with  $\eta^{(T)}$, $\eta^{(S)}$, $\mu^{(T)}$ et $\mu^{(S)}$. That means that it renders commutative, for any set $X$ of $\Set$, the following diagrams:
%\begin{equation}
%\begin{xy}
%\xymatrix{
%X \ar[r]^{\eta^{(T)}_X} \ar[rd]_{\eta^{(S)}_X} & TX \ar[d]^{\tau_X}\\
% & SX
%}
%\end{xy}
%\label{tau_eta}
%\end{equation}
\begin{equation*}
\begin{xy}
\xymatrix{
 X \ar[r]^{\eta^{(T)}_X} \ar[rd]_{\eta^{(S)}_X} & TX \ar[d]^{\tau_X} & & TTX \ar[ld]_{T \tau_X} \ar[rd]^{\tau_{TX}} \ar[rr]^{\mu^{(T)}_X} & & TX \ar[dd]^{\tau_X} \\
& SX,& TSX \ar[rd]_{\tau_{SX}} & & STX \ar[ld]^{S \tau_X} & \\
 & & & SSX \ar[rr]_{\mu^{(S)}_X} & & SX,
}
\end{xy}
%\label{tau_mu}
\end{equation*}
\label{monade_mor}
where the diamond-shaped diagram commutes already because of the naturality of $\tau$.
\end{definition}
\end{comment}

\begin{definition}
Let $R$ be a monad. A {\em module} $(M,\sigma)$ over $R$ consists of a functor $M$ and a natural transformation $\sigma : MR \xrap M$, called {\em substitution}, such that the following diagram commutes for any set $X$:
\begin{equation*}
\begin{xy}
\xymatrix{
MRRX \ar[r]^{\sigma_{RX}} \ar[d]_{M \mu_X} & MRX \ar[d]^{\sigma_X} \\
MRX \ar[r]_{ \sigma_X} & MX.
}
\end{xy}
%\label{sigma}
\end{equation*}
\label{module}
\end{definition}

\begin{definition}
Let $R$ be a monad and $(M,\sigma^{(M)})$ and $(N,\sigma^{(N)})$ two $R$--modules. A {\em morphism of modules} $F$ is a natural transformation which is compatible with $\sigma^{(M)}$ and $\sigma^{(N)}$. That means that it renders commutative, for any set $X$ of $\Set$, the diagram:
\begin{equation*}
\begin{xy}
\xymatrix{
MRX \ar[r]^{\sigma^{(M)}_X} \ar[d]_{F_{RX}} & MX \ar[d]^{F_X} \\
NRX \ar[r]_{\sigma^{(N)}_X} & NX.
}
\end{xy}
%\label{F}
\end{equation*}
\label{module_mor}
\end{definition}

\begin{definition}
Let $R$ be a monad and $M$ an $R$--module. We construct its {\em derived module} $M'$ by setting for each $X$ in $\Set$: 
\begin{equation*}
 M'(X) := M(X^*).
\end{equation*}
For any morphism of sets $f:X\to Y$ we set:
\begin{equation*}
 M'f := M(f^*).
\end{equation*}
\end{definition}

\begin{prop}
The derived module $M'$ of an $R$--module $M$ is an $R$--module.
\end{prop}

\begin{remark}
Let $R$ be a monad, let $(M,\si^{(M)})$ and $(N,\si^{(N)})$ be two $R$--modules. The cartesian product $M \times N$ is again an $R$--module.
\end{remark}

The languages which are interesting for us have at least two \emph{types}: they consist of \emph{terms} and \emph{formulae}. 
But we might also want to have terms of different types. In mathematics, for example, we want to have variables of type integer, real, etc..
In order to treat this typing appropriately, we have to work in the category $T$-$\Set$, where $T$ is an object of $\Set$ and is chosen to be the set of types. Hence the elements of $T$ are sometimes called types. The objects of $\TSet$ are the $T$-indexed families of sets, and an arrow $f$ of $\TSet$ is a $T$-indexed family of maps of sets:
\begin{equation*}
f:X\to Y \quad = \quad\prod_{t\in T} f_t:X_t\to Y_t,
\end{equation*}
i.\ e.\ every $f_t:X_t\to Y_t$ is an arrow in the category $\Set$. This notion is called the ``inverse" in \citep{julianna}.

The notion of monad and module now can be transferred literally to the category $T$-$\Set$. We now desire to have an analogon to the derived module.
\begin{definition}\label{def:partial_star}
 For $X = (X_t)_{t\in T}$ and $u\in T$ we define $X^{*_u}$ to be the object of $\TSet$ such that $X_t=X^{*_u}_t$ for all $t\neq u$ and $X^{*_u}_u = (X_u)^*$ in the sense of remark \ref{star}. The operation ${(\_)}^{*_u}: \TSet\to \TSet$ can be made into a functor in the obvious way.
\end{definition}



\begin{definition}
Let $R$ be a monad of $\TSet$ and $M$ be an $R$--module. We construct the {\em derived module with respect to} $u \in T$ of $M$ by setting for any $X$ of $\TSet$
\begin{equation*}
 \pu M (X):= M (X^{*_u})
\end{equation*}
 and for any morphism $h$ in $\TSet$:
\begin{equation*}
 \pu M h := M h^{*_u}.
\end{equation*}
\end{definition}

\begin{remark}\label{rem:factor}$ $
\begin{enumerate} 
 \item The operation $\TSet \to \Set, X\mapsto X_t$ can be extended to a functor.
 \item \label{factor:2}Let $(R,\eta,\mu)$ be a monad of $\TSet$ and let $F:\TSet\to\Set$ be any functor. Then $F\comp R$ is an $R$-module with substitution $\sigma = F(\mu)$.
  \item For any $u \in T$ the derived module w.\ r.\ t.\ $u\in T$, $\pu M:\TSet\to \TSet$, of the $R$--module $M$ is again an $R$--module.
 \end{enumerate}
\end{remark}


\subsection{Signatures \& Representations; The Signature $\Sigma_S$}

Let $T$ be a set. The elements of this set are called \emph{types}. 
\begin{definition}
 A \emph{$T$-typed higher order signature} consists of a set $\Sigma$ of symbols and a function $a$, called \emph{arity}, assigning to each symbol $s$ of $S$ a tuple $a(s)=(s_0; \bar s_1, \ldots, \bar s_n)$, where $s_0\in T$ and $ \bar s_i=(s_{i,0}; s_{i,1},\ldots,s_{i,n_i})$ ($i=1,\ldots,n$) are nonempty finite sequences in $T$.
\end{definition}
A signature is in fact the \emph{alphabet} we use to build expressions. The type $s_0$ denotes the type of the resulting term constructed by the use of the corresponding symbol whereas the $s_i$ denote the type of the arguments. We sometimes identify the symbol with its arity.

\begin{definition}
Let $R$ be a monad of $\TSet$. 
 For $\bar s=(s_0; s)$ consisting of an element $s_0\in T$ and a (maybe empty) finite sequence $s=(s_1, \ldots, s_n)$ of elements in $T$ we define
\begin{equation*}
 R^{\bar s}: X \mapsto R(X^{s})_{s_0},
\end{equation*}
where $X^{s} := X^{*_{s_1},\ldots, *_{s_n}}$. In other words, regarding $R$ as an $R$-module, we define 
\begin{equation*}
 R^{\bar s}(X)= \bigl(\partial_{s_1}\ldots\partial_{s_n}R(X)\bigr)_{s_0}.
\end{equation*}
%
This defines a functor $\TSet\to \Set$.
\end{definition}

\begin{lemma}
 For any $u\in T$ the derived module w.\ r.\ t.\ $u$, $\pu M$, of an $R$-module $M$ is an $R$-module.
\end{lemma}
\begin{pro}
 For a proof we refer to \citep{julianna}.
\end{pro}

\begin{lemma}
 Let $R$ be a monad on $\TSet$ and $(M, \sigma)$ an $R$-module. Suppose $F:\TSet\to \Set $ is a functor.
Then $F\comp M$ is an $R$-module with substitution
\begin{equation*}
 \sigma_F = F(\sigma): F\comp M\comp R\to F\comp M.
\end{equation*}
\end{lemma}
\begin{pro}
 Since $F$ is a functor, it preserves commutative diagrams.
\end{pro}

Now we have all the ingredients we need in order to give the following
\begin{definition}
 A \emph{representation} of a $T$-typed signature $\Sigma$ in a monad $R:\TSet\to\TSet$ is, for every symbol $s\in\Sigma$ with arity $a(s)=(s_0; \bar s_1,\ldots, \bar s_n)$, a morphism of modules
\begin{equation*}
 \prod_{i=1}^n R^{\bar s_i} \to R_{s_0}.							
\end{equation*}
\end{definition}


For a $T$-typed signature $\Sigma$ we define 
\begin{equation*}
 \hat \Sigma: \TSet\to\TSet
\end{equation*}
to be the functor that associates to a $T$-set $X$ of variables the set of trees which can be constructed with the constructors of $\Sigma$ and whose \emph{free} variables are contained in the typed set $X$. We do not give a formal definition of what a tree is - the intuitive idea is sufficient. In fact $\hat\Sigma$ is a monad $(\Sigma, \eta,\mu)$: the natural transformation $\eta$ creates from a variable $x_t\in X_t$ a tree $\eta_{X,t}(x_t)$ consisting only of the root. The morphism $\mu$ identifies a tree having subtrees as leaves with a big tree.  The important fact is that we can define maps recursively on the (typed) set $\hat\Sigma(X)$. We are able to do so since given a tree $E\in \hat\Sigma(X)_u$ (of type $u\in T$), we can identify the root of $E$, i.\ e.\ the last constructor which was used to build $E$. Recursive definitions are then done by \emph{pattern matching}. This will be done in the next section. 
We regard a tree as an expression of the language induced by $\Sigma$. That means that the language is in fact the monad $\hat\Sigma$ together with a set of morphisms of modules, one for each constructor $s\in \Sigma$. The role of such a morphism associated to $s\in\Sigma$ is to construct new expressions with $s$ as root and subtrees being the arguments of the morphism.
Without further explanation we mention that $\hat\Sigma$ (together with corresponding morphisms of modules) is the initial object in the category of $\Sigma$-representations.

We omit the hat `` $ \hat {~}$ '' and denote the language induced by the signature $\Sigma$ also with the letter $\Sigma$.


\begin{example}\label{ex:signature}
 The signature $\Sigma_S$ for a language suitable to build statements of set theory is as follows: the types are $T=\lbrace t, f\rbrace$ (terms and formulae). The signature is given by
\begin{align*}
 \Sigma_S=\bigl\lbrace \quad 
                      %\langle,\rangle &:(X\times Y; X,Y), \\
                      =&:\bigl(f; (t;\emptyset),(t;\emptyset)\bigr),\\
                      %app&:(Y;Y^X,X),\\
                      \in&:\bigl(f; (t;\emptyset),(t;\emptyset)\bigr),\\
                      %\lambda&:(Z^X; Z^{*_X}),\\
                      \wedge &:\bigl(f; (f;\emptyset),(f;\emptyset)\bigr),\\
                      \vee &: \bigl(f; (f;\emptyset),(f;\emptyset)\bigr),\\
                      \Rightarrow&:\bigl(f; (f;\emptyset),(f;\emptyset)\bigr),\\
                      \neg&: \bigl(f;(f;\emptyset)\bigr),\\
                      \forall&: \bigl(f; (f;t)\bigr),\\
                      \exists&: \bigl(f; (f; t)\bigr)\quad \bigr\rbrace.
\end{align*}
The morphism of modules associated to the symbol $\Rightarrow$ constructs from two formulae $P$ and $Q$ in $\hat\Sigma_S(X)_f$ a formula 
\begin{equation*}
 \Rightarrow_X(P, Q)\quad :=\quad (P\Rightarrow Q)\quad\text{in } \hat\Sigma_S(X)_f.
\end{equation*}
The morphism of modules associated to the symbol $\forall$ constructs from a formula $P\in \hat\Sigma_S(X^{*_t})_f$ a formula $\forall_X(P)\in \hat\Sigma_S(X)_f$.
\end{example}
\begin{remark} [about trees] In a text it is rather inconvenient to draw expressions as trees, for reasons of space efficiency. The tree-like structure is therefore simulated with the help of parentheses. As an example, the following element of $\hat\Sigma_S\bigl((\es,\lbrace P,Q,R\rbrace)\bigr)_f$, 
\begin{equation*}
 \begin{xy}
  \xymatrix @R=.5pc{
      &       &  \Rightarrow \ar@{-}[ld]\ar@{-}[rd]&          &  &\txt{ is written as} & & \\
       &   P  &              &   \wedge\ar@{-}[ld]\ar@{-}[rd] & & P\Rightarrow(Q\wedge R).& & \\
        &     &                    Q   & & R, & & &
}
 \end{xy}
\end{equation*}
\end{remark}

\begin{remark}\label{rem:minimality}
 For two (typed) sets $Z\leq Y$ we have $\hat\Sigma(Z)\leq\hat\Sigma(Y)$ with the usual order on families of sets. By recursion we can determine the \emph{minimal} (typed) set $X$ such that a given expression $E$ of type $t\in T$ is an element of $\hat\Sigma(X)_t$. 
\end{remark}


\subsection{Substitution}
Let $\Sigma$ be a $T$-typed signature and $(\hat\Sigma, \eta, \mu)$ the corresponding monad. For any type $u\in T$ we want to define a substitution 
\begin{equation*}
 \lbrack x:=t\rbrack: \hat\Sigma(X)\to \hat\Sigma(X)
\end{equation*}
for any $x\in X_u$ and $t\in \hat\Sigma(X)_u$. We define the substitution as the composition:
\begin{equation*}
 \begin{xy}
  \xymatrix{
      \lbrack x:=t\rbrack: & \hat\Sigma(X) \ar[rr]\ar[rd]_{\hat\Sigma(f)}& & \hat\Sigma(X). \\
                           &               & \hat\Sigma\hat\Sigma(X)\ar[ru]_\mu&     
}
 \end{xy}
\end{equation*}
Here $f=\prod f_v:X_v\to \hat\Sigma(X)_v$ is defined as
\begin{equation*}
 f_v(y):=\begin{cases}
              t, &\text{ if } y=x, \\
              \eta_{v,X_v}(y) &\text{ otherwise}.
       \end{cases}
\end{equation*}


\section{A Glance at Model Theory}

In order to give a meaning to the terms and formulae constructed in a formal language, we \emph{interpret} them in a suitable \emph{universe} consisting of the (mathematical) objects we are interested in. 

To explain what an interpretation is, we exemplify one such of the language (induced by the signature) $\Sigma_S$ of \ref{ex:signature} in a universe $M$ of sets. We do not further specify the universe, but as an example
%In \citep{manin}, the universe $M$ is taken to be a set. 
%In mathematics the use of a set-theoretic language such as $L_1Set$ and its interpretation in a universe of sets is the most common case. 
%It should be emphasized that in this case the universe $M$ itself will not be a set, in particular, the universe $M$ is not in the range of the quantifiers. 
%This is necessary in order to avoid paradoxical behaviour \`a la Russell. 
 $M$ might be taken to be the von Neumann universe as constructed in an appendix in \citep{manin}. In general, one of the main tasks of a universe is to specify the range of the quantifiers. A good explanation of the idea of a universe (of sets) is also given at the beginning of \citep{krivine}.

\subsection{Interpretation of $\Sigma_S$ in a universe of sets}

From now on we will denote by $\Omega$ the set of truth values $\Omega = \lbrace 0, 1\rbrace$.
Let $\Sigma_S$ be the signature given in \ref{ex:signature}, the set $T$ of types being $T=\lbrace t,f\rbrace$. In general, an interpretation $\phi$ for such a two-typed signature $\Sigma$ is, for every (typed) set $X=(X_t, X_f)$ in $\TSet$, two maps
\begin{align}
 \hat\Sigma(X)_t &\to \label{interpretation:t}
\Bigl( 
\bigl(\lbrace X_t\to M \rbrace\times\lbrace X_f\to\Omega \rbrace\bigr) %\notag
\to 
M
%\cup\bigcup_{n\geq 1}\lbrace M^n \to M\rbrace 
%\cup\bigcup_{n\geq 1}\mathcal{P}M^n 
%
\Bigr),
\\
 \hat\Sigma(X)_f &\to \label{interpretation:f}
\Bigl( 
\bigl(\lbrace X_t\to M \rbrace\times\lbrace X_f\to\Omega \rbrace\bigr) %\notag
\to
\Omega
\Bigr).
\end{align}
For an expression $E\in \hat\Sigma(X)_u$ we denote its interpretation $\phi$ by $|E|=|E|_{X,u}$, where $u$ is the type of $E$. Here we may or may not specify the interpretation $\phi$ by mentioning it as a subscript, according to necessity.
 
Let us start with the definition of \eqref{interpretation:t} for the language $\Sigma_S$. Let $\alpha\in \hat \Sigma_S(X)_t$ be a term. Since we do not have any constructors (operation symbols) which produce a term, we conclude that $\alpha$ must be a tree of the form $\eta_{X,t}(x_t)$, where $x_t\in X_t$, i.\ e.\ a variable $x_t$ of type \emph{term}, regarded as a tree. We define
\begin{equation*}
 |\eta_{X,t}(x_t)|_{X, t} (\xi, \omega):=\xi(x_t).
\end{equation*}

For the definition of \eqref{interpretation:f} we suppose $P\in \hat\Sigma_S(X)_f$. In case $P=\eta_{X,f}(x_f)$, where $x_f\in X_f$, we set 
\begin{equation*}
 |\eta_{X,f}(x_f)|_{X, f} (\xi, \omega):=\omega(x_f).
\end{equation*}
In case $P$ is a formula $(\alpha_1=\alpha_2)$ we define
\begin{equation}\label{eq:equality}
 |P|_{X,f}(\xi, \omega) := \begin{cases}
                        1, &\text{ if } |\alpha_1|_{X,t}(\xi, \omega)=|\alpha_2|_{X,t}(\xi, \omega),\\
                        0  &\text{ otherwise.}
                       \end{cases}
\end{equation}
Analogously for the formula $P=(\alpha_1\in\alpha_2)$ we set
\begin{equation}\label{eq:membership}
 |P|_{X,f}(\xi, \omega) := \begin{cases}
                        1, &\text{ if } |\alpha_1|_{X,t}(\xi, \omega)\in |\alpha_2|_{X,t}(\xi, \omega),\\
                        0  &\text{ otherwise.}
                       \end{cases}
\end{equation}
Observe that the symbols ``$=$" (in \eqref{eq:equality}) and ``$\in$" (in \eqref{eq:membership}) in the case switching are \emph{not} the symbols of our signature $\Sigma$, but symbols for equality and membership, respectively, in the universe $M$. We could do without these symbols outside our language $\Sigma$ by using a different language, e.\ g.\ the English language, but this would change basically nothing. We use the same symbols in the universe $M$ in an informal way in order to define formally the interpretation of these symbols as part of the language $\Sigma$. This is part of what is meant with ``circularity" in the introduction and explained at the beginning of \citep{tourlakis}. 

The rules for the logical connectives are similar; we omit the subscript $X,f$:
\begin{align}\label{interpretation:formulae}
 |Q_1\Rightarrow Q_2| &= 1 - |Q_1|+|Q_1||Q_2|,\\ 
 |Q_1\vee Q_2| &= \max(|Q_1|,|Q_2|),\notag\\   
 |Q_1\wedge Q_2| &= \min(|Q_1|,|Q_2|),\notag\\
 |\neg Q| &= 1-|Q|,\notag
\end{align}
where $1=1(\xi, \omega):\lbrace X_t\to M \rbrace\times\lbrace X_f\to\Omega \rbrace \to
\Omega$ is the function constantly equal to $1\in \Omega$.

The interpretation of the quantifiers is slightly more complicated, since these have a variable-binding effect. Let $P=\forall_X Q \in \hat\Sigma(X)_f$ be a universally quantified formula. Now the formula $Q$ is an element in $\hat\Sigma(X^{*_t})_f$. Recall that $X^{*_t}_f=X_f$ and $X^{*_t}_t = X_t\cup \lbrace \infty_{X_t}\rbrace$ by definition \ref{def:partial_star}. We define
\begin{equation*}
|\forall_X Q|_{X, f}(\xi, \omega):= \min_{\xi'\geq\xi} \bigl(|Q|_{X^{*_t}, f}(\xi', \omega)\bigr),
\end{equation*}
where the minimum ranges over all the \emph{extensions} $\xi':X^{*_t}_t\to M$ of the map $\xi: X_t\to M$ on $X^{*_t}_t= X_t\cup \lbrace \infty_{X_t}\rbrace$, i.\ e.\ all the $\xi':X^{*_t}_t\to M$ such that
\begin{equation*}
 \xi'|_{X_t}= \xi.
\end{equation*}
In other words, we vary over all the possible values $\xi'(\infty_{X_t})\in M$ for the variable $\infty_{X_t}$ which is bound by the universal quantifier. Once again the circularity: the interpretation of a quantifier is explained by using the same quantifier in the universe $M$.

The interpretation of the existential quantifier is analogous:
\begin{equation*}
|\exists_X Q|_{X, f}(\xi, \omega):= \max_{\xi'\geq\xi} \bigl(|Q|_{X^{*_t}, f}(\xi', \omega)\bigr).
\end{equation*}

In \citep{manin} the author works with a single-typed language only. Variables of type \emph{formula} are not handled there, even though they naturally appear in the definition of a \emph{tautology} (c.\ f.\ \ref{def:tautology}). From now on we will suppose that the expressions we handle do not contain free variables of type \emph{formula}, if not mentioned explicitly. (Since there is no constructor which binds variables of type \emph{formula}, such a formula does not contain any variable of type \emph{formula} at all.) For such a formula we will omit the argument $\omega$ in the future. We will also omit the subscript $X,f$ (as already done in \eqref{interpretation:formulae}), in order to simplify the notation.
				
The preceding definition may be extended to the case of several types of (super)type \emph{term} by splitting the map \eqref{interpretation:t}. If $\lbrace t_i\mid i\in I\rbrace$ is the set of types of type \emph{term}, we would use as a universe an $I$-indexed family $M=\prod_{i\in I} M_i$. Since this complicates notation, but not the underlying principle, we will omit this step and continue working with an arbitrary two-typed signature $\Sigma$ allowing the construction of terms and formulae.


\begin{definition}
 Let $(M, \phi)$ be any interpretation of $\Sigma$ in a universe $M$. The formula $P\in \hat\Sigma\bigl((X_t,\es)\bigr)_f$ (without free variables of type \emph{formula}) is called \emph{$\phi$-true} if $|P|_\phi(\xi)=1$ for all $\xi:X_t\to M$, i.\ e.\ if $|P|_\phi = 1$.
\end{definition}

\begin{definition}
 Given a set $\Gamma$ of formulae in a language $\Sigma$, then $(M,\phi)$ is called a \emph{model} for $\Gamma$ if all the formulae of $\Gamma$ are $\phi$-true.
\end{definition}

Directly from the definition we obtain the following
\begin{prop}\label{cor:1}
 Let $P$ be a \emph{closed} formula, i.\ e.\ $P\in \hat\Sigma(0_\TSet)_f$,where $0_\TSet = (\emptyset, \emptyset)$. Then the function $|P|_\phi$ is constant, that is, the truth value of $P$ is well defined.
\end{prop}


\subsection{Syntactic Properties of Truth; Tautologies}\label{def:tautology}

A tautology is a formula which is "always true"; here a precise definition:

\begin{definition}
Let $X_f=\lbrace f_1,\ldots,f_n\rbrace$ be a finite set of variables of type \emph{formula}.
 Let $P\in \hat\Sigma\bigl((\es, X_f)\bigr)_f$ be a formula containing free variables of $X_f$, which is constructed only by the use of the logical connectives. Suppose that for an interpretation $(M,\phi)$ we have $|P|_\phi(\omega)=1$ for any $\omega:X_f\to\Omega$. 
It follows that for any interpretation $(N,\psi)$ we have $|P|_\psi(\omega)=1$ for any $\omega:X_f\to\Omega$, since the interpretation rules for the logical connectives are independent of the actual interpretation. We might call such a formula a \emph{template} for a tautology.

A formula $Q\in\hat\Sigma\bigl((Y_t, \es)\bigr)_f $ is called a \emph{tautology} if $Q$ is obtained from a template $P$ by substituting the variables $f_i$ by formulae without variables of type \emph{formula}. In other words, $Q$ is a tautology if 
\begin{equation*}
Q=P\lbrack f_i:=t_i\rbrack_{i=1,\ldots,n}
\end{equation*}
for $t_i\in\hat\Sigma\bigl((Y_t, \es)\bigr)_f $.
\end{definition}


\begin{comment}

\begin{definition}\label{def:tautology1}
 Let $\Gamma$ be a set of formulae in the language $\Sigma$. A \emph{logical polynomial} over $\Gamma$ is an element of the set $LPol = LPol_\Gamma$ defined inductively as follows:
\begin{enumerate}
 \item $P\in \Gamma$ implies $P\in LPol_\Gamma$;
 \item $Q_1, Q_2\in LPol$ implies $\neg Q_1\in LPol$ and $Q_1 \star Q_2\in LPol$ ($\star$ being one of the binary logical connectives).
\end{enumerate}
\end{definition}
A sequence of formulae $P_1, \ldots, P_n$ such that for any $i=1,\ldots,n$ we have 
\begin{equation*}
 P_i\in \Gamma \quad\text{ or }\quad P_i=\neg P_j \quad\text{ or } \quad P_i=P_j\star P_k \quad\text{ with } \quad j, k<i
\end{equation*}
is called a \emph{representation} of $P_n$ as a logical polynomial over $\Gamma$.
Observe that a representation is not unique: for $\Gamma = \lbrace Q, \neg Q\rbrace$ the formula $\neg Q$ has two representations, a sequence of length $1$ and one of length $2$.

Given a map $|.|: \Gamma\to \Omega$, it can be extended to the set $LPol$ with the rules 
\begin{align*}
 |Q_1\Rightarrow Q_2| &= 1 - |Q_1|+|Q_1||Q_2|,\\ 
 |Q_1\vee Q_2| &= \max(|Q_1|,|Q_2|),\notag\\   
 |Q_1\wedge Q_2| &= \min(|Q_1|,|Q_2|),\notag\\
 |\neg Q| &= 1-|Q|.\notag
\end{align*}
Observe that here the function $|.|$ does \emph{not} denote a representation as in \eqref{interpretation:formulae}.
\begin{definition}
A \emph{tautology} $P$ is a formula $P$ such that there exists a set of formulae $\Gamma$ and a representation $s$ of $P$ as a logical polynomial in $LPol_\Gamma$ such that for every map $|.|:\Gamma \to \Omega$ we have $|P|_s=1$. Here $|.|_s$ denotes the extension of the given map to all of $LPol$. Observe that the value is dependent on the chosen representation $s$ of $P$.	\end{definition}
\end{comment}


\begin{example}
 Consider the formula $\neg P\Rightarrow(P\Rightarrow Q)$ in variables $P$ and $Q$ which is used in proposition \ref{prop:contradiction}. It is a template: 
\begin{align*}
 |\neg P \Rightarrow (P\Rightarrow Q)|&=1-|\neg P|+|\neg P||P\Rightarrow Q| = \\
                                      &=1-(1-|P|) +(1-|P|)(1-|P|+|P||Q|) \\
                                      &=|P|+1-|P|+|P||Q|-2|P|-|P||Q| \\
                                      &=1,
\end{align*}
where in the last step we used the fact that $|P|^2=|P|$. Hence the truth value of the formula is independent of the values $|P|$ and $|Q|$.
\end{example}


Let $\phi$ be an interpretation of a language $\Sigma$ and let $T_\phi \Sigma$ be the set of $\phi$-true formulae of $\Sigma$.

\begin{prop}\label{prop:goedelian}$ $
\begin{enumerate}
 \item The set $T_\phi \Sigma$ is \emph{complete}, i.\ e.\ for any closed formula $P$ either $P$ or $\neg P$ lies in $T_\phi \Sigma$. This follows from \ref{cor:1}.
 \item The set $T_\phi \Sigma$ does not contain any \emph{contradiction}, i.e. there is no formula $P$ s.t. $P$ and $\neg P$ lie in $T_\phi \Sigma$. This follows because $|\neg P|_\phi = 1 - |P|_\phi$.
 \item $T_\phi \Sigma$ is closed under the \emph{rules of deduction} $\MP$ (modus ponens) and $\Gen$ (generalization). The latter means that for $P\in\hat\Sigma(X^{*_t})$, if $P\in T_\phi\Sigma$, then also $\forall_X P\in T_\phi\Sigma$.
 \item The set $T_\phi \Sigma$ contains all the tautologies.
 \item The set $T_\phi \Sigma$ contains all the \emph{logical quantifier axioms} (c.\ f.\ definition \ref{def:log-quant-axioms}).
\end{enumerate}
\end{prop}

\begin{remark}\label{rem:inj}
 Since for a (typed) set $X\in\TSet$ we have $X\subset X^{*_t}$ (factorwise), it holds that $\hat\Sigma(X)\subset\hat\Sigma(X^{*_t})$. For $P\in \hat\Sigma(X)$ and $Q\in \hat\Sigma(X^{*_t})$ we can thus still define $(P\Rightarrow Q) \in \hat\Sigma(X^{*_t})$. This allows the following
\end{remark}


\begin{definition}\label{def:log-quant-axioms}
For a language $\Sigma$, the set of \emph{logical quantifier axioms} is the set consisting of all the formulae of the form
\begin{enumerate}
 \item $\bigl(\forall_X(P\Rightarrow Q)\bigr)\Rightarrow \bigl(P\Rightarrow (\forall_X Q)\bigr)\quad$ for $P,Q$ as in remark \ref{rem:inj};
 \item $(\forall_X \neg P) \Leftrightarrow (\neg \exists_X P)$;
 \item $(\forall_X P)\Rightarrow P \lbrack \infty_X:=t\rbrack\quad$ for $t\in \hat\Sigma(X^{*_t})$. This axiom is called \emph{axiom of specialization}.
\end{enumerate}
Here the formula $P\Leftrightarrow Q$ is an abbreviated notation for $(P\Rightarrow Q) \wedge (Q\Rightarrow P)$.
\end{definition}



\begin{comment}
Some nice tautologies are
\begin{itemize}
 \item [A0.] $P\Rightarrow P$
 \item [A1.] $P\Rightarrow(Q\Rightarrow P)$
 \item [A2.] $\bigl(P\Rightarrow (Q \Rightarrow R)\bigr)\Rightarrow \bigl((P\Rightarrow Q)\Rightarrow (P\Rightarrow R)\bigr)$
 \item [A3.] $(\neg Q \Rightarrow \neg P) \Rightarrow \bigl((\neg Q \Rightarrow P)\Rightarrow Q\bigr)$
\item [B1.] $ \neg \neg P \Rightarrow P,\quad P\Rightarrow \neg\neg P$
 \item [B2.] $\neg P \Rightarrow (P\Rightarrow Q)$
\end{itemize}
\end{comment}

\begin{definition}
For a language $\Sigma$ we define the set $\Ax \Sigma$ to be the set consisting of all the tautologies of $\Sigma$ and the logical quantifier axioms.
\end{definition}


\begin{definition}
 A set of formulae $\Gamma$ in $\Sigma$ is called \emph{G\"odelian}, if it is complete, does not contain a contradiction, is closed under the rules of deduction and contains $\Ax \Sigma$.
\end{definition}

The proposition \ref{prop:goedelian} can hence be restated as follows:

\begin{prop}
 For any language $\Sigma$ and for any interpretation $(M,\phi)$ of $\Sigma$ the set $T_\phi \Sigma$ is G\"odelian.
\end{prop}



\subsection{Deducibility - Formalization of Proofs}
Let $\Sigma$ be a language and let $\Gamma$ be a set of formulae in $\Sigma$.

\begin{definition} \label{def:deduction}
 A formula $P$ in $\Sigma$ is \emph{deducible} from $\Gamma$ if there exists a sequence $P_1,\ldots, P_n=P$ of formulae s.t. for every $i=1,\ldots,n$ it holds (at least) one of the following:
\begin{enumerate}
 \item $P_i$ is in $\Gamma$,
 \item $\exists k<i$ s.t. $P_i$ is a direct consequence of $P_k$ using $\Gen$,
 \item \label{deduction:3} $\exists j,k<i$ s.t. $P_i$ is a direct consequence of $P_j$ and $P_k$ using $\MP$.
\end{enumerate}
In symbols $\Gamma\vdash P$.
\end{definition}

An example for a proof in this style is given with the following

\begin{prop}[about contradiction]\label{prop:contradiction}
 Suppose $\Gamma$ contains all the tautologies of type $\neg P \Rightarrow (P\Rightarrow Q)$. Then the following are equivalent:
\begin{enumerate}
 \item \label{contra:1}$\Gamma \vdash P$ and $\Gamma\vdash \neg P$.
 \item \label{contra:2}$\Gamma \vdash Q$ for any formula $Q$.
\end{enumerate}
\end{prop}
\begin{pro}
 The statement \ref{contra:2} obviously implies \ref{contra:1}. Conversely, let $Q$ be any formula and suppose $\Gamma \vdash P$ and $\Gamma\vdash \neg P$. We add the formula $\neg P \Rightarrow (P\Rightarrow Q)$ (being an element of $\Gamma$) to the concatenation of the deduction of $P$ and $\neg P$. The formula $\neg P$ appearing in the so created deduction sequence, we can apply rule nr. \ref{deduction:3} of definition \ref{def:deduction} to $\neg P$ and $\neg P \Rightarrow (P\Rightarrow Q)$; this yields $P\Rightarrow Q$. Since also the formula $P$ appears in the sequence, we can again apply the same deduction rule $\MP$; this proves $\Gamma\vdash Q$.
\end{pro}

This definition of a deduction is useful for the following reason: suppose $\Gamma$ is a set of $\phi$-true formulae, i.\ e.\ $|P|_\phi=1$ for all $P\in \Gamma$. By the recursive definition of $|.|_\phi$ it follows that all the formulae $Q$ deducible from $\Gamma$ also are $\phi$-true.

Mathematicians rarely write down a proof in this way. There are several reasons for this: firstly, a proof in this style is difficult to check for a human mind, as explained in \citep[p. 36 ff]{manin}. Furthermore the details which are interesting from a mathematician's point of view tend to be hidden among a large amount of formulae.

The advantage of a proof given in this style is obvious: a machine can check the validity of the proof - it simply has to be fed with the initial data $\Gamma$. Furthermore one can, again with the help of a machine, try to reduce the set of formulae in $\Gamma$. For example one might choose to work without the tautologies of the form $\neg\neg P \Rightarrow P$ and thus change from classical to intuitionistic logic. Or one might do set theory in an axiomatic system without the axiom of choice. After deleting a formula from $\Gamma$, some sequences are not valid deductions any more - but which ones? The filtering is a perfect task for a machine. 


\begin{lemma}\label{lemded}
Let $\Gamma$ be a set of formulae and $P$ and $Q$ formulae of a language $\Sigma$.
 If $\Gamma\cup\lbrace P\rbrace\vdash Q$ then $\Gamma\vdash P\Rightarrow Q$.
\end{lemma}
A proof can be found in \citep{manin}.

\begin{definition}
 Let $\Gamma$ be a set of formulae in $L$. A formula $P$ is \emph{independent} of $\Gamma$ if neither $\Gamma \vdash P$ nor $\Gamma\vdash \neg P$.
\end{definition}

\begin{definition}
 A set of formulae $\Gamma$ is \emph{consistent} if there is no formula $P$ s.t. $\Gamma\vdash P$ and $\Gamma\vdash \neg P$.
\end{definition}

The following theorem is called \emph{G\"odel's completeness theorem}. We do not give a proof, the reader can find one in \citep{manin}.
\begin{theorem}\label{compl}$ $
\begin{enumerate}
 \item \label{goedel:1}Every G\"odelian set $T$ in $L$ is the set of $\phi$-true formulae for a suitable interpretation $(M,\phi)$ of $L$ with $|M|\leq \card(L)+\aleph_0$.
 \item Any set $\Gamma$ of formulae in $L$ which is consistent and contains $\Ax L$ can be embedded into a G\"odelian set. In particular, by pt. \ref{goedel:1},  $\Gamma$ has a model.
\end{enumerate}
\end{theorem}

\begin{cor}\label{corgoe}
 Let $\Gamma$ contain $\Ax L$.
\begin{enumerate}
 \item \label{corgoe:1}A formula $P$ is deducible from $\Gamma$ iff either $\Gamma$ is inconsistent or $P$ is $\phi$-true for all models $(M,\phi)$ of $\Gamma$.
 \item A closed formula $P$ is independent of $\Gamma$ iff both $\Gamma \cup \lbrace P\rbrace$ and $\Gamma \cup \lbrace \neg P\rbrace$ are consistent iff (by \ref{corgoe:1}) both $\Gamma \cup \lbrace P\rbrace$ and $\Gamma \cup \lbrace \neg P\rbrace$ have models.
\end{enumerate}
\end{cor}

\begin{pro}[of \ref{corgoe}]$ $
 \begin{enumerate}
  \item Let $P\in \hat\Sigma(X)_f$ be $\phi$-true for all models $(M,\phi)$ of $\Gamma$. Since $P$ contains only finitely many free variables, we can produce the \emph{closure} $\bar P$ of $P$ by applying the appropriate morphisms $\forall_{X_i}$ with decreasing sets $X_i$ to $P$.
We distinguish the following two cases:
\begin{enumerate}
\item $\Gamma \cup\lbrace \neg \bar P\rbrace$ inconsistent: then $\Gamma \cup\lbrace \neg \bar P\rbrace \vdash \bar P$ and by the deduction lemma \ref{lemded} we obtain $\Gamma\vdash \neg \bar P \Rightarrow P $. We may use the tautology $(\neg \bar P \Rightarrow \bar P)\Rightarrow \bar P$;  $\MP$ and subsequent specialization (c.\ f.\ \ref{def:log-quant-axioms}) yield $\Gamma\vdash P$.
 \item $\Gamma \cup\lbrace \neg \bar P\rbrace$ consistent: by \ref{compl} the set $\Gamma \cup\lbrace \neg \bar P\rbrace$ has a model in which $\Gamma$ is true and $P$ is false: if $P$ were true, then also $\bar P$ would be true since $\Gen$ preserves truth. So $\neg \bar P$ would be false, a contradiction.
 \end{enumerate}
\item $\Gamma\cup\lbrace P\rbrace$ consistent iff $\Gamma\cup\lbrace P\rbrace$ has a model $(M,\phi)$: one direction by is given by \ref{compl}. If conversely we had $\Gamma\cup\lbrace P\rbrace\vdash Q$ and $\Gamma\cup\lbrace P\rbrace\vdash \neg Q$, then both $Q$ and $\neg Q$ were $\phi$-true, a contradiction.

Suppose that $P$ is independent of $\Gamma$. As $\neg P$ is not deducible, by \ref{corgoe:1} there exists a model $(M_1,\phi_1)$ of $\Gamma$ in which $\neg P$ is not $\phi_1$-true, hence in which $P$ is $\phi_1$-true by the closedness of $P$. Similarly there exists a model $(M_2, \phi_2)$ in which $\neg P$ is $\phi_2$-true.

Conversely, if $\Gamma\cup\lbrace P\rbrace$ has a model, then $\neg P$ can not be deducible from $\Gamma$ and vice versa. 
\end{enumerate}
\end{pro}

\begin{comment}
\begin{lemma}
 If $\Gamma$ is consistent and complete and contains $\Ax L$, and if the alphabet of $L$ is sufficient for $\Gamma$, then $\Gamma$ has a model $(M,\phi)$ with $|M|\leq \card(L)+\aleph_0$.
\end{lemma}
\end{comment}


\section{Syntax and Semantics of a Topos}

A goal of category theory is to generalize the preceding treatment of a universe of sets $M$.  
Whereas set theory starts with a universe of objects (the sets) and a binary relation between them (denoted by $\in$), a category consists of a universe of objects and arrows between these objects, fulfilling certain axioms. We regard a category as a generalized universe of sets. In order to obtain a similar structure as in a universe of sets, we impose additional axioms on the category - this leads to the notion of \emph{topos}. The axioms defining a special topos can be shown to be equiconsistent to those of $\RZC$, restricted Zermelo set theory with axiom of choice (see section \ref{sect:last}). 

At first we give the definition of a topos and explain some of its properties which can be derived without any use of set-theoretical concepts.

Thereafter we associate to a given topos $\T$ a syntax $\Sigma_\T$ suitable to express statements of set theory. Finally we define the validity of formulae with the help of arrows of $\T$ (and hence avoid the circularity of the model-theoretic approach). 



\subsection{About Topoi}
\subsubsection{Definitions \& First Properties}

As before we presume some knowledge about category theory. In particular, for some arrows whose existence is given by universal properties we use the notation of \citep{lawvere} and \citep{sheaves}. We also use some calculational rules (e.\ g.\ for the composition of products of arrows). Proofs can be found in \citep{lambek-scott}. 


\begin{definition}\label{def:topos}
 A \emph{topos} $\T$ is a category $\T$ with 
\begin{enumerate}
 \item a pullback for every diagram $Y\to B \ot X$,
 \item a terminal object $1$,
 \item \label{topos:3}a \emph{subobject classifier} $\Omega$, i.\ e.\ an object $\Omega$ and a monic arrow $\true:1\monic \Omega$ such that for every monic $m:S\monic B$ there is a unique arrow $\phi:B\to \Omega$ in $\T$, called the \emph{characteristic map} of $m$ ($\charmap(m)$), which makes the following diagram a pullback:



\begin{equation}\label{subobject}
\begin{xy}
%(0,0)*+{B}; (10,0)*+{1} **\dir{-} ?<*\dir{)} ?>*\dir{>>}


\xymatrix{
  S \ar@{{)}->}[d]_m \ar@{->}[r] & 1 \ar@{)->}[d]^{\true}\\
  B \ar@{->}[r]^{\phi} & \Omega,
}
\end{xy}
\end{equation}

 \item \label{topos:4} for each object $B$ an object $PB$ called the \emph{power object} of $B$ and an arrow $\in_B: B\times PB\to \Omega$ such that for every arrow $f: B\times A\to\Omega$ there is a unique arrow $g:A\to PB$ which renders commutative the following diagram:
\begin{equation}\label{eq:powerdiag}
\begin{xy}
\xymatrix{A \ar[dd]^g && B\times A \ar[dd]^{1\times g} \ar[rd]^f \\
        &&&                       \Omega.\\
PB                    && B\times PB \ar[ru]_{\in_B}
} 
\end{xy}
\end{equation}
We call the arrow $f$ the \emph{transpose} of $g$ and vice versa.

\end{enumerate}

\end{definition}

It follows (c.\ f.\ \citep[ch.\ IV.2]{sheaves}) that a topos $\T$ is \emph{cartesian closed}. By definition this means that for any two objects $B$ and $C$ of $\T$ there exist an \emph{exponential} object $C^B$ and an arrow
\begin{equation}\label{eq:exponential}
 e=e_{B, C}:B\times C^B\to C
\end{equation}
with the following universal property:
for any object $A$ and any arrow $f: B\times A\to C$ there is a unique arrow $g:A\to C^B$ with $f=e(1\times g)$. This process should be called \emph{Currying}.\footnote{after Haskell Brooks Curry; * 1900 in Millis, USA; \textdied 1982 in State College, USA;}

Furthermore a topos $\T$ has all finite limits and colimits. For a proof of the latter fact we refer to \citep[ch.\ IV.4f]{sheaves}.





\begin{remark}[about subobjects]
 A subobject $m:S\monic B$ in a category $\C$ is in fact an \emph{equivalence class} of monics into $B$. Here two monics $A\monic S$ and $B\monic S$ are said to be $equivalent$ if there exists an isomorphism $A\cong B$ in $\C$. In the definition \ref{def:topos}.\ref{topos:3} this is reflected by the fact that for a given $\phi:B\to \Omega$, the pullback of $\true$ along $\phi$ is determined only up to isomorphism. In notation and language we do not make a difference between a monic and its equivalence class.

For a given object $A$ of a topos $\T$ (or in general, of a category $\C$), the collection $\Sub(A)$ of subobjects of $A$ forms a category. Its objects are equivalence classes of monics into $A$, and there is a unique arrow $(m:S\monic A)\to (k:T\monic A)$ iff $m$ factors as $m=k\comp h$ for some $h: S\to T$. In this case the arrow $h$ is necessarily monic. Since this relation fulfills the equations defining a partial order on a set, we also say $S\leq T$. 

Setting the object $A=1$ and using $B\cong B\times 1$ in the above definition yields a third description of a subobject $m:S\monic B$ by a map $s:1\to PB$.
\end{remark}

\begin{example}
 Consider the category $\Set$ of all sets, where the terminal object is the one-point set $\lbrace *\rbrace$. Here a subobject $S\monic B$ of a set $B$ is a subset $S\subset B$. We can define a characteristic map $\chi_S: B\to \lbrace 0,1\rbrace$ on $B$ by setting 
\begin{equation*}
 \chi_S(b)=
\begin{cases}
                1 \text{ if } x\in S, \\
                0 \text{ if } x\notin S.
\end{cases}
\end{equation*}
With the monic (injective) arrow
\begin{equation*}
 \true: 1=\lbrace * \rbrace \to \Omega = \lbrace 0,1\rbrace, \quad *\mapsto 1,
\end{equation*}
we indeed define a subobject classifier for the category $\Set$.

The power object for a set $B$ in $\Set$ is, as the name suggests, the power set $\mathcal{P}B=2^B$, whereas the arrow $\in_B:B\times \mathcal{P}B\to \Omega$ is given by
\begin{equation*}
 \in_B(b,S)=
\begin{cases}
         1, &\text{ if } b\in S,\\
         0 &\text{ otherwise.}
\end{cases}
\end{equation*}
For a given $f: B\times A\to \Omega$ we construct the transpose $g:A\to \mathcal{P}B$ as 
\begin{equation*}
         g:  a\longmapsto\lbrace b\in B \mid f(a,b)=1\rbrace.
\end{equation*}
The reader might convince himself that this gives indeed a 1-to-1 correspondence as in \ref{def:topos}, pt. \ref{topos:4}, and that the diagram \eqref{eq:powerdiag} commutes in the case of $\Set$.

We hence have the first example of a topos, namely the category $\Set$ of sets with morphisms being the maps between sets. This is quite reassuring, since we defined a topos in order to obtain a generalized universe of sets.
\end{example}


The following statements about pullbacks (\citep[p. 71, exercises 5, 8]{maclane}) will often be useful. 
\begin{lemma} Let $\C$ be a category (where the following pullbacks exist). It holds:
\begin{enumerate}
 \item Let $A,B,C$ be objects of $\C$. Consider the pullback diagram
\begin{equation*}
\begin{xy}
 \xymatrix{
**[l]B\times_A C \ar[r]^-q  \ar[d]_{p} &      C \ar[d]^{g}\\
    B  \ar[r]_f     &       A.
}
\end{xy}
\end{equation*}
If $f$ is monic then $q$ is as well. 
 \item If in the diagram
\begin{equation}\label{pasting}
 \begin{xy}
  \xymatrix{
%    
        A\ar[r]^r \ar[d]_s & B\ar[d]^q\ar[r]^p & C\ar[d]^g\\
        D\ar[r]_h          & E \ar[r]_f    & F
}
 \end{xy}
\end{equation}
both the left and the right square are pullbacks, then the big rectangle is a pullback as well.
\end{enumerate}

\end{lemma}
\begin{pro}
\begin{enumerate}
\item
Let $M$ be an object of $\C$ and $x,y: M \to B\times_A C$ two morphisms of $\C$. We suppose $q\circ x=q\circ y$ and we want to show $x=y$.

At first we show $px = py$ by showing $fpx = fpy$: 
$$ fpx=gqx = gqy = fpy$$
(where we use the commutation property of the diagram and the hypothesis $qx=qy$).
But $f$ is a monic and therefore $px = py$.

Now the object $M$ with the morphisms $px = py: M\to B$ and $qx=qy:M\to C$ is a cone over $B\stackrel{f}{\to}A\stackrel{g}{\leftarrow}C$ and we can use the universal property of $B\times_A C$: there exists \emph{exactly one} morphism $r: M\to B\times_A C$ which fulfills
$$p\circ r = px (=py),\qquad q\circ r = qx (=qy).$$
As both $x$ and $y$ fulfill this property, they both coincide with $r$:
$$x=r=y.$$ \halmos

\item
 Let the arrows $x$ and $y$ be as shown in the diagram
\begin{equation}
 \begin{xy}
  \xymatrix{
    M\ar@{.>}[rd]_{\exists !\beta}\ar@{.>}[rrd]^{\exists !\alpha} \ar@/^1pc/[rrrd]^x \ar@/_1pc/[ddr]^y                                      \\
     &   A\ar[r]_r \ar[d]_s & B\ar[d]^q\ar[r]_p & C\ar[d]^g\\
     &   D\ar[r]_h          & E \ar[r]_f    & F
}
 \end{xy}
\end{equation}
such that $gx=f(hy)$. The right square is a pullback, hence there is a unique arrow $\alpha$ such that 
\begin{equation*}
 x=p\alpha;\quad hy = q\alpha.
\end{equation*}
Now the left square is a pullback, so there exists a unique arrow $\beta$ such that
\begin{equation*}
 \alpha=r\beta;\quad y=s\beta.
\end{equation*}
We have $x=pr\beta$ and $y=s\beta$.

For the unicity of $\beta$ suppose $\beta'$ with $x=pr\beta'$ and $y=s\beta'$. The latter equality implies $hy=hs\beta' = q(r\beta')$. Since the right square is a pullback, we know that
% there is exactly one arrow $\alpha$ such that 
\begin{equation*}
 r\beta'= \alpha.
\end{equation*}
It follows $r\beta=\alpha=r\beta'$, since both $r\beta$ and $r\beta'$ fulfill this equality.
Now we have $r\beta'=\alpha$ and $s\beta'=y$ by hypothesis.
Using the fact that the left square is a pullback gives $\beta=\beta'$. \halmos
\end{enumerate}
\end{pro} 

\begin{remark}\label{rules-subob}
The lemma tells us that, given an arrow $k:A\to B$ and a subobject $m:S\monic B$ of $B$ (better: a representative) in a topos $\T$, then the pullback of this monic along $k$ is a subobject of $A$. Furthermore, in the correspondence between subobjects of $B$ and arrows $B\to\Omega$ of \eqref{subobject}, pullback of a subobject $m:S\monic B$ along $k:A\to B$ corresponds to multiplication of $\charmap(m)$ with $k$ on the right.

If we choose to carry out our reasoning about categories within set theory, we can hence reformulate our definition of the subobject classifier as follows: for any object $B$ of $\T$, we postulate an isomorphism of sets
\begin{equation*}
 \Sub_\T(B)\cong \Hom_\T(B,\Omega)
\end{equation*}
natural in $B$, i.\ e.\ for any arrow $k:A\to B$ the diagram 
\begin{equation*}
 \begin{xy}
  \xymatrix{
      **[l]\Sub(B)\ar@{<->}[r]^-{\cong} \ar[d]_{k^{-1}}&   **[r]\Hom(B,\Omega) \ar[d]^{\_\_\comp k}  \\
      **[l]\Sub(A) \ar@{<->}[r]^-\cong &    **[r]\Hom(A, \Omega)
}
 \end{xy}
\end{equation*}
shall commute. The same is possible for pt. \ref{topos:4} of definition \ref{def:topos} by demanding, for any object $B$ of $\T$, the existence of the power object $PB$ such that we have an isomorphism of sets
\begin{equation*}
 \Hom_\T(B\times A,\Omega)\cong \Hom_\T(A,PB)
\end{equation*}
natural in $A$. (We omit the corresponding diagram.)

\end{remark}
We make the operation $B\mapsto PB$ a contravariant functor by defining, for a given arrow $k:A\to B$,  the arrow $Pk:PB\to PA$ to be the transpose of $\in_B(k\times 1): A\times PB\to \Omega$. To check the compatibility with composition, consider an arrow $h:B\to C$ and the following diagram:
\begin{equation*}
 \begin{xy}
  \xymatrix @C = 5pc{
         A\times PC \ar[r]^{k\times 1}\ar[d]_{1\times Ph} &  B\times PC \ar[r]^-{\in_C(h\times 1)} \ar[d]^{1\times Ph} &  \Omega\ar@2{-}[d] \\
         A\times PB  \ar[r]^{k\times 1} \ar[d]_{1\times Pk}&  B\times PB \ar[r]^-{\in_B} &  \Omega\ar@2{-}[d] \\
         A\times PA  \ar[rr]_{\in_A}&              &  \Omega.
}
 \end{xy}
\end{equation*}
All the small rectangles commute, the upper left one because of the definition of the product of arrows. The upper right one and the lower one commute because of the definition of $Ph$ and $Pk$, respectively. So the big rectangle commutes. Since $(h\times 1)\comp (k\times 1)= (hk\times 1)$, this shows that $P(hk)=Pk\comp Ph$.


\begin{prop}\label{prop:isom}
In a topos $\T$
\begin{enumerate}
 \item every monic is an equalizer and
 \item every arrow both epi and monic is an isomorphism.
\end{enumerate}
\end{prop}

\begin{pro}
 \begin{enumerate}
  \item Since \eqref{subobject} is a pullback, the monic $m:S\monic B$ is the equalizer of $\charmap(m)$ and $\true_B=B\to 1\stackrel{\true}{\to}\Omega$.% (c.\ f.\ \eqref{eq:trueB}).
  \item Suppose the arrow $e$ is both monic and epi. Being a mono, $e$ is an equalizer, say, of $f$ and $g$. But then $fe = ge$ and therefore, since $f$ is epi, $f=g$. Consider the following diagram:
\begin{equation*}
 \begin{xy}
  \xymatrix{ 
      X \ar@{)->>}[rr]^e  &&  A \ar[r]^f &  B\\
      & A\ar@{.>}[lu]_{\exists !k} \ar[ru]_{1_A}
}
 \end{xy}
\end{equation*}
Now $ek=1_A$. It follows $eke=e=e\comp 1_X$ and hence also $ke=1$, since $e$ is monic. So $e$ is an isomorphism.
 \end{enumerate}

\end{pro}



\subsubsection{The Arrows $\Delta$ and $\delta$}\label{Deltadelta}
For the categorical definition of truth we need some specials arrows existing in any topos $\T$.
For an object $B$ of $\T$ let the \emph{diagonal map} $\Delta_B$ be the arrow 
\begin{equation*}
 \Delta_B=\langle 1_B,1_B\rangle: B\monic B\times B
\end{equation*}
such that $\pi_1\Delta_B = \pi_2\Delta_B=1_B$ for the projections $\pi_1, \pi_2:B\times B\to B$.
The arrow $\Delta_B$ is indeed monic: for $f, g:A\rightrightarrows B$ with $\Delta_B\comp f=\Delta_B\comp g$ we have $f = 1_B\comp f = \pi_1\comp \Delta_B\comp f=\pi_1\comp \Delta_B\comp g = g$. It follows that $\Delta_B$ has a characteristic map
\begin{equation} \label{eq:delta}
 \delta_B: B\times B\to \Omega.
\end{equation}
For any object $X$ let $\true_X$ be defined by 
\begin{equation}\label{eq:trueB}
\true_X: X\to 1 \stackrel{\true}{\longrightarrow}\Omega.
\end{equation}
We have the following 
\begin{prop}\label{equalityPred}
 Let $b$ and $b'$ two \emph{generalized elements} of the object $B$, i.\ e.\ $b,b':X\rightrightarrows B$ are two arrows in a topos $\T$. Then
\begin{equation*}
 \delta_B\comp\langle b,b'\rangle = true_X \quad \text{ iff } \quad b=b'.
\end{equation*}
 
\end{prop}
\begin{pro}
 Let $b=b'$. Then $\delta_B\comp\langle b, b\rangle = \delta_B\comp\langle 1_B, 1_B\rangle \comp b = true_B\comp b = true_X$. Conversely, if $\delta_B\comp\langle b,b'\rangle = true_X$, then the map $\langle b,b'\rangle$ factorizes through $\Delta_B:B\to B\times B$ and gives a unique arrow $t: X\to B$ such that $\Delta_B\comp t = \langle 1_B, 1_B\rangle \comp t = \langle t, t\rangle= \langle b,b'\rangle$. Applying the projections $\pi_1, \pi_2:B\times B\to B$ yields the desired result $b=t=b'$.
\end{pro}

\subsubsection{The Category of Subobjects}

\begin{prop}\label{zero-subob}
 For any object $B$ of a topos $\T$ the arrow $0\to B$ is monic. 
\end{prop}
\begin{pro}
For a proof we refer to \citep[ch.\ IV.7]{sheaves}.
\end{pro}
For any object $B$ of $\T$ we hence have $0\leq S$ for any subobject $S\monic B$.

In the category $\Set$ every morphism $k:A\to B$ between sets $A$ and $B$ factorizes as a product $k=me:A\stackrel{e}{\twoheadrightarrow}\Img(k)\stackrel{m}{\monic}B$. This holds in a general topos $\T$.

\begin{definition}\label{def:image}
 For an arrow $k$ in a topos $\T$ the \emph{image} $m=\Img(k)$ is a monic $m$ such that $k=m\comp e$ for some arrow $e$ and whenever $k$ factors through a monic $h$, then $m$ does as well. If $k:A\to B$ is an arrow in $\T$, we sometimes write $\Img(A)$ instead of $\Img(k)$, especially when talking about subobjects.
\end{definition}

\begin{prop}\label{prop:image}
 In a topos $\T$ every arrow $k$ has an image. Furthermore it factors as $k=m\comp e$ where $e$ is epi.
\end{prop}
\begin{pro}
For a proof we refer to \citep[chapter IV.6]{sheaves}.
\end{pro}

\begin{prop}\label{prop:sub-cat}
 For any object $B$ in a topos $\T$ the category $\Sub(B)$ has all finite products and coproducts. Moreover, for each arrow $k:A\to B$ the pullback operator $k^{-1}: Sub(B)\to Sub(A)$ is a functor. This functor has a left adjoint $\exists_k$, sending each subobject $U$ of $A$ to its image under $k$.
%cartesian closed category with all finite products and coproducts.
\end{prop}

\begin{pro}
In the category $\Sub(B)$ we have the terminal object $1_B:B\to B$ and the initial object $0\monic B$ (c.\ f.\ \ref{zero-subob}).
Given two subobjects $m:S\monic B$ and $n:T\monic B$ of $B$ with corresponding characteristic maps $\charmap(m), \charmap(n):B\to \Omega$, we can construct their product and coproduct as follows. The product $S \cap T$ is simply the pullback of $S\stackrel{m}{\monic}B\stackrel{n}{\leftarrowtail}T$. This object is again a subobject of $B$ and the pullback property in $\T$ coincides with the product property in $\Sub(B)$. For the pullout $S+T$ of the arrows $m$ and $n$ the yielded arrow $S+T\to B$ is not necessarily monic. We repair this defect by taking the image and obtain a subobject $S\cup T := M=\Img(S+T\to B)$ as in the following diagram:
\begin{equation*}
 \begin{xy}
  \xymatrix{
           **[l]S+T\ar[rd]          &            & T\ar[ll] \ar[dd]\\
                               &  M\ar@{)->}[rd]&                 \\
           S\ar[uu]\ar[rr]     &            & B.                    }
 \end{xy}
\end{equation*}
Since $M$ is the smallest subobject of $B$ through which $S+T\to B$ factors, it is indeed the coproduct in $\Sub(B)$.

In order to prove that $k^{-1}$ is a functor, we have to show that it preserves the partial order. Consider the following diagram
\begin{equation*}
 \begin{xy}
  \xymatrix{
           k^{-1}S\ar[rr]\ar@{.>}[rd]^{\exists !h}\ar@{)->}[rdd] &                       & S\ar@{)->}[d]\\
                                              & k^{-1}T\ar[r]\ar@{)->}[d]   & T\ar@{)->}[d]\\
                                              & A\ar[r]_k             & B,
}
 \end{xy}
\end{equation*}
where the small square in the lower right corner is a pullback, as well as the outer distorted quadrilateral. From the former it follows the existence of the desired arrow $h$.

We define $\exists_k:\Sub(A)\to \Sub(B)$ to be the operation 
\begin{equation*}
 \exists_k(n:U\monic A) := \Img(kn).
\end{equation*}
By abuse of notation we denote the source of the resulting mono by $\exists_k(U)$.
The following diagram shows that $\exists_k$ is indeed monotone, i.\ e.\ a functor:
\begin{equation*}
 \begin{xy}
  \xymatrix{
         U \ar@{)->}[r]\ar[ddrr] & V\ar@{)->}[r]\ar[dr] & A \ar[r]^k & B.\\
                                 &                      & \exists_k(V)\ar@{)->}[ru] & \\
                                 &                      & \exists_k(U)\ar@{)->}[ruu]\ar@{.>}[u] &
}
 \end{xy}
\end{equation*}
The composition in the upper line factors via $\exists_k(U)$ as well as via $\exists_k(V)$.
Since by definition $\exists_k(U)$ is the smallest subobject of $B$ through which this composition factors, we obtain the dotted arrow. Hence for $U\leq V$ as subobjects of $A$ we have $\exists_k(U)\leq \exists_k(V)$ as subobjects of $B$.

Next we show that for $n:U\monic A$ we have 
\begin{equation}\label{sub:1}
 U\leq k^{-1}\exists_k(U).
\end{equation}
 We consider the diagram
\vspace*{.3cm}
\begin{equation*}
 \begin{xy}
  \xymatrix{
           U\ar@{)->}[rd]_n \ar@/^1.5pc/[rr] \ar@{.>}[r]    & k^{-1}\exists_k(U) \ar[d] \ar[r] & \exists_k(U) \ar@{)->}[d]  \\
         & A\ar[r]^k    &    B,      
}
 \end{xy}
\end{equation*}
where at first the image $\exists_k(U)=\Img(kn)$ is constructed and then the pullback square. Since the outer quadrilateral commutes, we obtain the dotted arrow 
\begin{equation*}
 U\to k^{-1}\exists_k(U),\quad \text{i.\ e.\ }\quad U\leq k^{-1}\exists_k(U).
\end{equation*}
We have as well 
\begin{equation}\label{sub:2}
 \exists_k k^{-1}(S)\leq S
\end{equation}
 for any subobject $S$ of $B$.

It remains to prove the triangular equalities. From \eqref{sub:1} and the monotonicity of $\exists_k$ it follows $\exists_k(U)\leq \exists_k k^{-1} \exists_k(U)$. On the other hand, by \eqref{sub:2} with $S=\exists_k(U)$ we have the other inequality. The equality $k^{-1}\exists_k k^{-1}(S) = k^{-1}(S)$ for any subobject $S\monic B$ can be proved similarly.
\halmos
\end{pro}

It follows that, being a right adjoint, the functor $k^{-1}: \Sub(B)\to \Sub(A)$ preserves limits, in particular products:
\begin{equation}\label{sect-pullback}
 k^{-1}(S\cap T)=k^{-1}(S)\cap k^{-1}(T).
\end{equation}



An object $B$ of a topos $\T$ is said to be \emph{open} if $B$ is a subobject of the terminal object, or more precisely, if the unique arrow $\bigcirc_B: B\to 1$ in $\T$ is monic. The collection of open objects of $\T$ is denoted by $\Open(\T)$ and is a subcategory of $\T$. The processes of choosing a representative of an equivalence class and projecting into the equivalence class give an equivalence of categories
\begin{equation*}
 \Sub_\T(B)\stackrel{\cong}{\longleftrightarrow}\Open(\T/B).
\end{equation*}

\begin{lemma}
 An object $B$ of a topos $\T$ is open if and only if for any object $A$ of $\T$ there is at most one arrow $A\to B$.
\end{lemma}
\begin{pro}
 Suppose there are arrows $f,g:A\rightrightarrows B$. Then $ \bigcirc_Bf=\bigcirc_B g$. The object $B$ being open, we have $f=g$. I. e. if there is an arrow $A\to B$, then it is unique. If conversely there is at most one arrow $A\to B$ for any $A$, then $B\to 1$ is obviously monic.
\end{pro}



\begin{cor}\label{cor:exp-sub}
 If $V$ is an open object of the topos $\T$, then so is its exponential $V^U$ for any object $U$ of $\T$, in particular for open $U$.
\end{cor}
\begin{pro}
 For any object $X$, the arrows $X\to V^U$ correspond to the arrows $X\times U\to V$. Since $V$ is open, there exists at most one arrow of the latter type.
\end{pro}

\begin{remark}\label{rem:prod-sub}
 For the terminal object $1$ of $\T$ the product in the category $\Sub_\T(1)$ coincides with the product in $\T$. The reader might convince himself by checking again the definition of the product in $\Sub(B)$ in the proof of \ref{prop:sub-cat}
\end{remark}

\begin{cor}\label{sub1-cart}
 Given a topos $\T$, the category $\Sub_\T(1)$ has exponentials, hence is a cartesian closed category with finite products and coproducts.
\end{cor}
\begin{pro}
 Most of the work has been done in the proposition \ref{prop:sub-cat} already. It remains to show that $\Sub(1)$ has exponentials. For subobjects $U, V$ of the terminal object $1$ we define the exponential $U\Rightarrow V$ in $\Sub(1)$ to be the exponential in $\T$, i.\ e.\ 
\begin{equation}\label{eq:implication}
 U\Rightarrow V\quad :=\quad V^U.
\end{equation}
By corollary \ref{cor:exp-sub} the object $U\Rightarrow V$ is again a subobject of $1$. The remark \ref{rem:prod-sub} ensures that this object indeed fulfills the universal property of an exponential object in $\Sub(1)$.
\end{pro}


\begin{theorem}
 Let $\T$ be a topos and $B$ any object of $\T$. Then the slice category $\T/B$ is a topos.
\end{theorem}
\begin{pro}
 For a proof we refer to \citep[ch.\ IV.7]{sheaves}.
\end{pro}

\begin{theorem}\label{slice-functor}
 For any $k:A\to B$ in a topos $\T$ the pullback functor $k^*:\T/B\to \T/A$ has both a left adjoint $\Sigma_k$, given by composition with $k$, and a right adjoint $\prod_k$. Moreover $k^*$ preserves the subobject classifier and exponentials (up to isomorphism), hence is by definition a \emph{logical morphism}.
\end{theorem}
\begin{pro}
 For a proof we refer to \citep[ch.\ IV.7]{sheaves}.
\end{pro}

The following proposition is a continuation of proposition \ref{prop:sub-cat}.
\begin{prop}\label{prop:pullback-sub}
 Let $\T$ be a topos and $B$ any object of $\T$. Then $\Sub_\T(B)$ is a cartesian closed category with finite products and coproducts. Furthermore the pullback along any morphism $k:A\to B$ induces a functor $k^{-1}: \Sub(B)\to \Sub(A)$ which preserves products, coproducts and exponentials. 
\end{prop}
\begin{pro}
 The first statement follows from 
\begin{equation}\label{eq:sub1}
 \Sub_\T(B)\cong \Sub_{\T/B}(1)
\end{equation}
 together with corollary \ref{sub1-cart}. For the second statement observe that the following diagram commutes:
\begin{equation*}
 \begin{xy}
  \xymatrix{
           \Sub(B) \ar[r]^{k^{-1}}\ar[d]_{\iota_B}  &   \Sub(A)\ar[d]^{\iota_A} \\
            \T/B \ar[r]^{k^*}     &\T/A,
}
 \end{xy}
\end{equation*}
where $\iota$ denotes the corresponding inclusions. Since $k^*$ preserves all the structure by theorem \ref{slice-functor}, it follows by the correspondence \eqref{eq:sub1} that also $k^{-1}$ does so.
\end{pro}

Finally we define a \emph{negation} operator on $\Sub_\T(B)$ by setting, for a subobject $S\monic B$,
\begin{equation*}
          \neg S \quad := \quad S\Rightarrow 0.
\end{equation*}
This is again a subobject of $B$. By the definition \eqref{eq:implication} we have the property
\begin{equation}\label{eq:char-neg}
 T\leq \neg S    \quad \text{ iff } \quad T\cap S=0.
\end{equation}


\subsubsection{Internal Structures of Topoi}\label{heyting}

This section serves to describe a structure on the subobject classifier $\Omega$ of a topos $\T$, which is used for the interpretation of formulae. More precisely, $\Omega$ is an \emph{internal Heyting algebra}. A Heyting algebra in the usual sense is a partially ordered set $H$ which, seen as a category, has all finite products (denoted by $\wedge$) and coproducts (denoted by $\vee$) and is cartesian closed. The latter means that it has an exponential operator (denoted by $\Rightarrow$) as well as elements $0$ and $1$ such that $0\leq x\leq 1$ for all $x\in L$. We imitate these properties for an object $L$ of $\T$ by giving diagrammatic versions of the defining equations of a Heyting algebra.

\begin{definition}
 Let $\C$ be a category with finite limits. An \emph{internal lattice} of $\C$ is an object $L$ together with two arrows 
\begin{equation}
 \wedge,\vee: L\times L\to L
\end{equation}
such that the following diagrams commute:
\begin{equation*}
 \begin{xy}
  \xymatrix{
        L \times L \times L  \ar[r]^-{{*}\times 1} \ar[d]_{1\times {*}} &    L\times L \ar[d]^{*}
               & 
L\times L \ar[r]^\tau \ar[rd]_-{*} &   L\times L \ar[d]^{*}   
&  
L \ar[r]^-{\Delta_L} \ar@{=}[rd] &  L\times L \ar[d]^{*} 
%
\\
           L\times L \ar[r]^{*}  &    L, 
 &  
                                 &     L,
&     
                                  &    L,
}
 \end{xy}
\end{equation*}
where the arrow $*:L\times L\to L$ is one of $\wedge$ or $\vee$ and the arrow $\tau$ is the twist map defined by
\begin{equation}\label{eq:tau}
 \begin{xy}
  \xymatrix{
L\times L \ar@/_1pc/[rdd]_{\pi_2} \ar@/^1pc/[rrd]^{\pi_1} \ar@{.>}[rd]^{\tau}& &  \\   %\ar@/_1.5pc/[rr]
 &   L\times L     \ar[r]^{\pi_2} \ar[d]^{\pi_1}  &  L \ar[d]\\
   & L \ar[r] & 1.
}
 \end{xy}
\end{equation}
These diagrams are the diagrammatic version of the law of associativity, commutativity and idempotency, respectively. 
Furthermore, we impose the \emph{absorption law} by demanding the diagram
\begin{equation*}
 \begin{xy}
  \xymatrix{
        L  & & L\times L \ar[ll]_{\wedge}\\
        L\times L \ar[u]^{\pi_1}\ar[d]_{\pi_1} \ar[r]^-{\delta\times 1}&    L\times L\times L \ar[r]^-{1\times\tau} & L\times L\times L \ar[u]_{1\times \vee} \ar[d]^{\wedge\times 1} \\
        L & & L\times L \ar[ll]^{\vee}
}
 \end{xy}
\end{equation*}
to commute. The upper rectangle represents the idea of the equation $x=x\wedge (y\vee x)$, whereas the lower one represents $x=(x\wedge y)\vee x$ for elements $x$ and $y$ of a lattice $L$.
\end{definition}

\begin{definition}
 A lattice object $L$ is said to be an \emph{internal Heyting algebra} if there are arrows 
\begin{equation*}
 \veebar : 1\to L,\quad \barwedge:1\to L
\end{equation*}
which make commute
\begin{equation*}
 \begin{xy}
  \xymatrix{
     L\times 1 \ar[r]^-{1\times \veebar}\ar[rd]_{\cong} & L\times L \ar[d]^{\vee}
& \txt{and} &
        L\times 1 \ar[r]^-{1\times \barwedge}\ar[rd]_{\cong} & L\times L \ar[d]^{\wedge}   \\
          & L & &   & L
}
 \end{xy}
\end{equation*}
as well as an implication arrow $\Rightarrow : L\times L\to L$ which renders commutative the diagrams
\begin{equation*}
 \begin{xy}
  \xymatrix{
    L \ar[r]^-{\Delta_L} \ar[d]   & L\times L \ar[d]^{\Rightarrow} & 
   L\times L\times L\ar[r]^-{\Delta\times 1}\ar[dd]^{1\times \wedge} & L\times L\times L\times L \ar[r]^-{1\times \tau\times 1}& L\times L\times L\times L \ar[d]_-{\Rightarrow \times \Rightarrow}\\
     1\ar[r]^{\barwedge} & L, & & & L\times L \ar[d]_-{\wedge}
    \\
& &  L\times L\ar[rr]^-{\Rightarrow}& & L,
}
\end{xy}
\end{equation*}
\begin{equation*}
\begin{xy}
\xymatrix{
     L\times L\times L \ar[r]^-{1\times \Rightarrow}& L\times L\ar[d]^{\wedge} &
L\times L\times L \ar[r]^-{1\times \tau}& L\times L\times L \ar[r]^-{1\times \Rightarrow}&L\times L \ar[d]^-{\wedge} \\
L\times L \ar[u]^{\Delta\times 1}\ar[r]^-{\wedge}& L, & 
 L\times L \ar[rr]^{\pi_1}\ar[u]^{\Delta\times 1}& &   L.
}
 \end{xy}
\end{equation*}
\end{definition}

A partial order on a set $H$ is given by a subset $P\subset H\times H$. We want to generalize this construction to our Heyting algebra object $L$ of $\T$. For two elements $x$ and $y$ of $H$, the partial order may be expressed by the formula
\begin{equation*}
   x\leq y  \quad\text{ iff } \quad x\wedge y = x.
\end{equation*}
%
Inspired by this equation, we define the subobject $\leq_L$ of $L\times L$ to be the equalizer of $\wedge$ and $\pi_1$, as in
\begin{equation*}
 \begin{xy}
  \xymatrix{
    \leq_L \ar[r]^-{e} & L\times L \ar@<+.5ex>[r]^-{\wedge} \ar@<-.5ex>[r]_-{\pi_1}& L.
}
 \end{xy}
\end{equation*}
Now a partial order is characterized by three properties, namely reflexivity, antisymmetry and transitivity. These properties can be expressed diagrammatically, but we shall omit their description. The interested reader may find them in \citep[ch.\ IV.8]{sheaves}.

The couple $(L,\leq_L)$ is called \emph{internal partially ordered object} of $\C$.

\begin{comment}
The first property can be expressed by saying that the diagonal $\Delta_H\subset H\times H$ is contained in $P$. In terms of arrows this means that $\Delta_L$ factors as in
\begin{equation}
 \begin{xy}
  \xymatrix{
      L \ar[r]^-{\Delta_L}\ar@{.>}[rd]&  L\times L \\
    &   \leq_L.\ar[u]_{e}
}
 \end{xy}
\end{equation}
If $\geq_L$ is the subobject of $L$ with given by the monic $\tau e$ (where $\tau$ is the twist as in \eqref{eq:tau}), then antisymmetry is imposed by demanding $\leq_L\times_{(L\times L)} \geq_L$ to be contained in the diagonal, as in
\begin{equation}
 \begin{xy}
  \xymatrix{
      \leq \times_{L\times L}\geq \ar@{)->}[rr]^{}\ar@{)->}[dd]^{} \ar@{.>}[rd]&  &  \leq_L\ar@{)->}[dd]^{e} \\
  & L \ar@{)->}[rd]^{\Delta}& \\
  \geq_L \ar@{)->}[rr]^{\tau e}& & L\times L
}
 \end{xy}
\end{equation}
\end{comment}

\begin{definition}
 Let $\T$ be a topos, and let $(L, \leq_L)$ and $(L', \leq_{L'})$ be internal partially ordered objects in $\T$. Suppose $\alpha:L\to L'$ and $\beta: L'\to L$ are monotonous arrows, i.\ e.\ 
\begin{equation*}
 \begin{xy}
  \xymatrix{
         \leq_L \ar[r]^-{e_L} \ar@{.>}[rd]  & L\times L  \ar[r]^-{\alpha\times\alpha}  &L'\times L'  \\
                  &   \leq_{L'} \ar[ru]_-{e_{L'}} &
}
 \end{xy}
\end{equation*}
and similarly for $\beta$.
We say that $\alpha$ is \emph{internally left adjoint} to $\beta$ if we have factorizations as in
\begin{equation*}
 \begin{xy}
  \xymatrix@C=8ex{
      L' \ar[r]^-{\langle \alpha\beta, 1\rangle}\ar@{.>}[rd]&  L'\times L' & \txt{and}&   L\ar[r]^-{\langle 1, \beta\alpha\rangle} \ar@{.>}[rd]& L \times L \\
          &    \leq_{L'}\ar[u]   &   &   &  \leq_{L}.\ar[u]
}
 \end{xy}
\end{equation*}

\end{definition}
This definition generalizes external adjunction of two morphisms $\phi: H\to H'$ and $\psi:H'\to H$ of partially ordered sets. Here we call $\phi$ a left adjoint of $\psi$, in symbols $\phi\dashv\psi$, if for any $x\in H$ and for any $y\in H'$ it holds
\begin{equation*}
     \phi(x)\leq y \quad \text{ iff } \quad x\leq \psi(y),
\end{equation*}
and this statement is equivalent to demanding, for any $x\in H$ and $y\in H'$
\begin{equation*}
 \phi\psi(y)\leq y \quad\text{ and } \quad x\leq\psi\phi(x).
\end{equation*}

\begin{theorem}
 For any object $B$ in a topos $\T$ the power object $PB$ is an internal Heyting algebra. In particular, $\Omega = P1$ is such.\ For any $k:A\to B$ the arrow $Pk:PB\to PA$ is a morphism of internal Heyting algebras, i.\ e.\ we have
\begin{equation*} 
\wedge_{PA} \comp (Pk\times Pk) = Pk\comp \wedge_{PB}
\end{equation*} 
and similar for the other arrows of the Heyting algebra structure.
\end{theorem}

\begin{pro}
 We are mainly interested in the Heyting algebra structure of $\Omega$. As an example, we show how to construct the arrow $\wedge:\Omega\times \Omega\to \Omega$.
The essential brick for the construction is proposition \ref{prop:sub-cat} or more precisely \eqref{sect-pullback}. For the remaining maps like $\vee$ etc. the necessary information can be found in theorem \ref{prop:pullback-sub}.

Given a pair of subobjects $S\monic B$ and $T\monic B$ characterized by $ s,t:B\to \Omega$, we can define $\wedge_B(s,t):B\to\Omega$ to be the characteristic map of $S\cap T$. Let $\pi_1, \pi_2:\Omega\times\Omega\to\Omega$ denote the projections and $S_1$ and $S_2$ the subobjects of $\Omega\times \Omega$ characterized by these projections. In order to calculate the arrow $\wedge_B(s,t)$ we now use property \eqref{sect-pullback} and the following correspondences:
\begin{align*}1_{\Omega\times\Omega}\comp\langle s,t\rangle = \langle \pi_1, \pi_2\rangle\comp\langle s,t\rangle &\stackrel{(1)}{\longleftrightarrow} (\pi_1\langle s,t\rangle, \pi_2\langle s,t\rangle)=(s,t)\\&\stackrel{(2)}{\longleftrightarrow}\bigl(\langle s,t\rangle^{-1}(S_1),\langle s,t\rangle^{-1}(S_2)\bigr) \\&\stackrel{\cap}{\longrightarrow} \langle s,t\rangle^{-1}(S_1\cap S_2) \\&\stackrel{(2)}{\longleftrightarrow} \charmap(S_1 \cap S_2)\comp \langle s,t\rangle =: \wedge \comp \langle s,t\rangle,
 \end{align*}
where (1) denotes the correspondence which defines a product of two objects by its universal property and (2) denotes the correspondence of remark \ref{rules-subob}. Hence for our subobject $S\cap T$ the characteristic map is given by composition
\begin{equation}\label{eq:wedge}
 \wedge_B(s,t): = \charmap(S\cap T) = B\stackrel{\langle s,t\rangle}{\longrightarrow}\Omega\times\Omega\stackrel{\wedge}{\longrightarrow}\Omega.
\end{equation}

This result can be generalized with the help of correspondence \ref{topos:4} of definition \ref{def:topos} by regarding subobjects of a product $B\times X$. This yields, for every object $B$ in $\T$, a map
\begin{equation*}
 \wedge:PB\times PB\to PB,
\end{equation*}
called the \emph{internal meet} on $PB$.

The same construction can be done for the remaining arrows which are to be constructed. 
The fact that the arrow $Pk:PB\to PA$ is a morphism of internal Heyting algebras, follows from $k^{-1}:\Sub(B)\to \Sub(A)$ preserving all the external structure.

\halmos

\end{pro}

In particular, it follows analogously to \eqref{eq:wedge}  that if $S\monic B$ is a subobject of $B$ in the topos $\T$, then the subobject $\neg S$ is characterized by the the composition 
\begin{equation}\label{eq:negation}
 \charmap(\neg S) = B\stackrel{\charmap S}{\longrightarrow}\Omega\stackrel{\neg}{\longrightarrow}\Omega
\end{equation}
for an arrow $\neg:\Omega\to\Omega$.




\begin{comment}
Thus we can define an arrow $\false:1\to \Omega$ as the characteristic map of $0\monic 1$, i.\ e.\ such that the left of the following diagrams is a pullback. The arrow $\false:1\to \Omega$ is monic, hence has itself a characteristic map $\neg:\Omega\to\Omega$ as in the right pullback diagram:

\begin{equation}\label{false-negation}
 \begin{xy}
  \xymatrix{
    0 \ar[r]\ar@{)->}[d] & 1\ar[d]^\true  & & 
1 \ar[r]^{\id}\ar@{)->}[d]_{\false} & 1\ar[d]^\true
\\
  1 \ar[r]_-\false & \Omega   & &
\Omega \ar[r]_-\neg & \Omega.
}
 \end{xy}
\end{equation}
\end{comment}


\begin{theorem}
 For any arrow $k:A\to B$ the arrow $Pk:PB\to PA$ has an internal left adjoint $\exists_k:PA\to PB$ as well as an internal right adjoint $\forall_k: PA\to PB$.
\end{theorem}
 
\begin{pro}
 For a proof we refer to \citep[ch.\ IV.9]{sheaves}.
\end{pro}



\subsection{Syntax}

%rules of reasoning are given by the axioms for the topos 

%intuitionistic logic - boolean logic  

%topos - boolean topos

%Whereas in the first approach the rules of deduction were defined independently of the formal language, they will be determined by the topos and its given rules for the arrows.

With a topos $\T$ we now associate a \emph{formal language} $\Sigma_\T$ suitable to express set-theoretical statements. The language is \emph{typed}, not only in the sense that we distinguish between terms and formulae, but we also have terms of different types. The types are the objects of $\T$, where an expression of type $\Omega$ is a formula. 
%In the previous chapter, we interpreted our formal language in a universe $M$.

%In set theory, the \emph{membership relation} $\in$ plays the central role in the interpretation of formulae. Since we will interpret our language $L(\T)$ not in a universe of sets, but in the topos $\T$, we will replace the membership relation by properties of arrows of $\T$ for the interpretation.
%In the topos $\Set$, we can identify the elements of an object $A$, i.\ e.\ of a set $A$, with arrows $1\to A$.  



Our formal language is given by the signature
\begin{align*}
 \Sigma_\T=\lbrace \quad \langle,\rangle &:\bigl(A\times B; (A;\emptyset),(B;\emptyset)\bigr), \\
                      =&:\bigl(\Omega; (B;\emptyset),(B;\emptyset)\bigr),\\
                      app&:\bigl(B;(B^A;\emptyset),(A;\emptyset)\bigr),\\
                      \in&:\bigl(\Omega; (B;\es),(\Omega^B;\es)\bigr),\\
                      \lambda&:\bigl(B^A; (B;A)\bigr),\\
                      \wedge &:\bigl(\Omega; (\Omega;\es),(\Omega;\es)\bigr),\\
                      \vee &: \bigl(\Omega; (\Omega;\es),(\Omega;\es)\bigr),\\
                      \Rightarrow&:\bigl(\Omega; (\Omega;\es),(\Omega;\es)\bigr),\\
                      \neg&: \bigl(\Omega;(\Omega;\es)\bigr),\\
                      \forall&: \bigl(\Omega; (\Omega;B)\bigr),\\
                      \exists&: \bigl(\Omega; (\Omega;B)\bigr)\quad\rbrace,
\end{align*}
where $A$ and $B$ are arbitrary types, i.\ e.\ objects of $\T$. 
We omitted the indices $A,B$ for the type-dependent constructors, i.\ e.\ those which are not logical symbols. But of course we demand the existence of these constructors for every type and every couple of types, respectively.

The language is given by the monad 
\begin{equation*}
 \hat\Sigma_\T: \TauSet \to \TauSet,
\end{equation*}
where an object in the category $\TauSet$ is a $\T$-indexed family of sets $Z=(Z_B)_{B\in\T}$.

To every expression $E\in \hat\Sigma(Z)_A$ we now define inductively an arrow $a(E)$ in $\T$. Its task is to help determine the validity/truth of formulae. We have the following general rule for the arrow $a(E)$: its target is the type of $E$, here the object $A$. Its source is the product of the types of the variables appearing freely in the term $E$. Here we ignore multiple appearances of the same variable, but not the appearance of different variables of the same type. We suppose that $E\in \hat\Sigma(Z)_A$ implies that $Z$ is the minimal (typed) set for which this holds, according to remark \ref{rem:minimality}.  For $E\in \hat\Sigma(Z)_A$ we can then give the formula
\begin{equation}\label{eq:source}
 \source(a(E))=\prod_{\genfrac{}{}{0pt}{1}{B\in \T}{|Z_B|=i}}B^i
\end{equation}

In the sequel we will, for an expression $\sigma$, denote its interpreting arrow by $\sigma$ as well, in order to simplify notation.
Now to the pattern matching:
suppose $E$ is a

\begin{enumerate}
 \item \emph{variable} $E=\eta_{Z,A}(x)\in \hat\Sigma(Z)_A$ for $x\in Z_A$: then the interpreting arrow is the identity $1_A: A\to A$.
 \item \emph{product} $E = \langle \sigma, \tau\rangle\in\hat\Sigma(Z)_{A\times B}$ of expressions $\sigma$ and $\tau$ with interpreting arrows $\sigma:U_1\to A$ and $\tau: U_2\to B$; the product's interpreting arrow is 
\begin{equation*}
\begin{xy}
   \xymatrix @C=4.5pc{
          W \ar[r]^-{\langle \sigma_1 \pi_1, \sigma_2\pi_2\rangle}  & A\times B       
} 
\end{xy}
%\langle \sigma \pi_1, \tau\pi_2\rangle:W\to 
\end{equation*}
 where the source $W$ is calculated from the typed set $Z$ as in equation \eqref{eq:source} and $\pi_i: W \to U_i$ ($i=1,2$) are the projections.

 \item \emph{equality} $E=(\sigma_1 = \sigma_2)\in \hat\Sigma(Z)_\Omega$; from $\sigma_i: U_i\to B$ ($i=1,2$) we construct the interpreting arrow 
\begin{equation}\label{interpretation:delta}
\begin{xy}
   \xymatrix @C=4.5pc{
       (\sigma_1=\sigma_2): W \ar[r]^-{\langle \sigma_1 \pi_1, \sigma_2\pi_2\rangle}  & B\times B \ar[r]^-{\delta_B}&  \Omega,
} 
\end{xy}
%
% (\sigma_1=\sigma_2): U_1\times U_2\stackrel{\langle \sigma_1 \pi_1, \sigma_2\pi_2\rangle}{\longrightarrow} X\times X \stackrel{\delta_X}{\longrightarrow}\Omega.
\end{equation}
where $\delta_B$ is the arrow defined in \eqref{eq:delta}.
\item \emph{application} $E=\sigma(\tau)$ with terms $\sigma$ and $\tau$ having interpreting arrows $V\to B^A$ and $U\to A$ respectively; the interpreting arrow for $E$ is
\begin{equation*}
\begin{xy}
   \xymatrix @C=4.5pc{
       \sigma(\tau): W \ar[r]^-{\langle \sigma \pi_1, \tau\pi_2\rangle}  & A\times B^A \ar[r]^-{e_{A,B}}&  B,
} 
\end{xy} 
%\sigma(\tau):W\to Y^X\times X \stackrel{e}{\to} Y.
\end{equation*}
where $e_{A,B}:A\times B^A\to B$ is as in \eqref{eq:exponential}.

\item \emph{$\in$-predicate} $E=(\sigma\in\tau)$ with terms $\sigma$ and $\tau$ having interpreting arrows $\sigma:U\to B$ and $\tau:V\to \Omega^B=PB$; the interpreting arrow for $E$ is
\begin{equation*}
 \begin{xy}
   \xymatrix @C=4.5pc{
       (\sigma\in\tau): W \ar[r]^-{\langle \sigma \pi_1, \tau\pi_2\rangle}  & B\times \Omega^B \ar[r]^-{\in_B}&  \Omega,
} 
\end{xy}
\end{equation*}
where $\in_B:B\times \Omega^B\to \Omega$ is as in \eqref{eq:powerdiag}.
\item \emph{abstraction} $E=(\lambda_{A,B,Z})\sigma$, where $\sigma\in\hat\Sigma(Z^{*_A})_B$ is interpreted by $\sigma:U\times A\to B$; $E$ is interpreted by the transpose of $\sigma$,
\begin{equation*}
 (\lambda_{A,B,Z}) \sigma: U\to B^A.
\end{equation*}
Observe the change in the source of the interpreting arrow from $U\times A$ (the factor $A$ exists because of the "star of type $A$") to $U$. The abstraction has a binding effect on the corresponding variable.
\end{enumerate}

\begin{example}\label{example:delta}
 The formula
\begin{equation*}
 (\infty_{\es}=\infty_{\es})\in\hat\Sigma({0_\TauSet}^{*_B})_\Omega
\end{equation*}
is interpreted by the arrow
\begin{equation*}
 \begin{xy}
   \xymatrix @C=4.5pc{
        W=B \ar[r]^-{\langle 1, 1\rangle=\Delta_B}  & B\times B \ar[r]^-{\delta_B}&  \Omega,
} 
\end{xy}
\end{equation*}
whereas the formula 
\begin{equation*}
 (\infty_{\es}=\infty_{{\{\infty_{\es}\}}})\in\hat\Sigma({{0_\TauSet}^{*_B}}^{*_B})_\Omega
\end{equation*}
is interpreted by the arrow
\begin{equation*}
 \begin{xy}
   \xymatrix @C=4.5pc{
        W=B\times B \ar[r]^-{\langle 1 \pi_1, 1\pi_2\rangle=1 } & B\times B \ar[r]^-{\delta_B}&  \Omega.
} 
\end{xy}
\end{equation*}
Observe in particular the different sources of the arrows.
\end{example}


Terms of type $\Omega$ (i.\ e.\ terms, whose interpreting arrow has $\Omega$ as target) are also called \emph{formulae}. They can be connected by logical quantifiers; for their interpretation we use the arrows of the Heyting algebra structure of $\Omega$ (s. \ref{heyting}) in the style of \eqref{interpretation:delta}. Let $\phi$ and $\psi$ be formulae interpreted by $\phi: U\to \Omega$ and $\psi: V\to \Omega$. In omitting the details, we set
\begin{equation}\label{logical:connectives}
 \begin{xy}
  \xymatrix@C=4.5pc @R= 1ex{
     \phi\vee\psi: W \ar[r]^-{\langle \phi \pi_1, \psi\pi_2\rangle}  & \Omega\times \Omega \ar[r]^-{\vee}&  \Omega,
\\
%}
% \end{xy}
%\end{equation}
%\begin{equation}
 %\begin{xy}
 % \xymatrix@C=4.5pc{
     \phi\wedge\psi: W \ar[r]^-{\langle \phi \pi_1, \psi\pi_2\rangle}  & \Omega\times \Omega \ar[r]^-{\wedge}&  \Omega,
\\
%}
% \end{xy}
%\end{equation}
%\begin{equation}
% \begin{xy}
%  \xymatrix@C=4.5pc{
     \phi\Rightarrow\psi: W \ar[r]^-{\langle \phi \pi_1, \psi\pi_2\rangle}  & \Omega\times \Omega \ar[r]^-{\Rightarrow}&  \Omega,
\\
%}
% \end{xy}
%\end{equation}
%\begin{equation}
% \begin{xy}
%  \xymatrix@C=4.5pc{
     \neg\phi: U \ar[r]^-{\phi}  & \Omega \ar[r]^-{\neg}&  \Omega.
}
 \end{xy}
\end{equation}



Consider the formula $\phi\in \hat\Sigma(Z^{*_B})$ containing a free variable $\infty_{Z_B}$ of type $B$. The formula is hence interpreted by an arrow $\phi:B\times U\to \Omega$, where $U$ itself is a (maybe empty) product of types. The formula
\begin{equation*}
 (\forall_{B,Z}) \phi \in\hat\Sigma(Z)_\Omega
\end{equation*}
 is interpreted by the arrow 
\begin{equation*}
\begin{xy} 
\xymatrix @C=4.5pc{
       \forall_{\bigcirc_B}\comp (\lambda_{B,\Omega,Z})\phi: U \ar[r]
^-{\text{transpose}(\phi)}  
& \Omega^B \ar[r]^-{\forall_{\bigcirc_B}}&  \Omega,
} 
\end{xy}
\end{equation*}
where $\forall_{\bigcirc_B}: \Omega^B\to \Omega$ is the internal adjoint of $P(\bigcirc_B): P1\to PB$ and $\bigcirc_B:B\to 1$ is the unique arrow from $B$ to the terminal object. 
The existential quantifier is treated similarly by using the internal left adjoint $\exists_{\bigcirc_B}: \Omega^B\to \Omega$.

If $\phi\in\hat\Sigma(Z)_\Omega$ is a formula with interpreting arrow $X\to\Omega$ (i.\ e.\ the variables which appear freely in $\phi$ are of type of the factors of $X$), we write $\lbrace x\in X \mid \phi(x)\rbrace $ for the subobject of $X$ classified by the interpreting arrow $\phi$ of the formula. In other words, the following diagram shall be a pullback:
\begin{equation*}
 \begin{xy}
  \xymatrix@C=2.5pc{
      \lbrace x\in X \mid \phi(x)\rbrace  \ar[r]\ar@{)->}[d] &  1 \ar@{)->}[d]^{\true}\\
         X   \ar[r]^{\phi}                              & \Omega
}
 \end{xy}
\end{equation*}






\subsection{Validity of Formulae}

Let $\phi=\phi(x_1, \ldots, x_n)$ be a formula in $\hat\Sigma_\T(Z)_\Omega$ with free variables $x_i$ of type $X_i$ ($i=1,\ldots n$), and let $\alpha_i: U\to X_i$ be generalized elements of the $X_i$, respectively.
We obtain the formula $\phi(\alpha_1,\ldots,\alpha_n)$ as 
\begin{equation*}
 \phi(\alpha_1,\ldots,\alpha_n):=\phi(x_1, \ldots, x_n)\lbrack x_i:=\alpha_i\rbrack_{i=1,\ldots,n}.
\end{equation*}


\begin{definition}
 The formula $\phi$ is said to be \emph{true} for the $\alpha_i$ as above, written
\begin{equation*}
 U\Vdash \phi(\alpha_1,\ldots,\alpha_n),
\end{equation*}
if the arrow $\alpha=\langle \alpha_1, \ldots, \alpha_n\rangle:U\to X=\prod X_i$ factors through the subobject $\lbrace x\mid \phi(x)\rbrace$ (where we write $x$ for $(x_1, \ldots, x_n)$):
\begin{equation}\label{cat:truth}
\begin{xy}
 \xymatrix{
     &   \lbrace x\mid \phi(x)\rbrace     \ar[r] \ar@{)->}[d]^m  &  1 \ar@{)->}[d]^{\true}\\
  U \ar@{.>}[ru]^g \ar[r]_\alpha & X \ar[r]_\phi & \Omega,
}
\end{xy}
\end{equation}
in other words, if
\begin{equation*}
 \phi\comp \alpha = \true_U.
\end{equation*}

\end{definition}

As a special case, we say that the formula $\phi(x)$ with interpreting arrow $\phi:X\to\Omega$ is \emph{universally valid} if the arrow $\alpha:=1_X:X\to X$ factors through $\lbrace x\mid \phi(x)\rbrace$, or equivalently, if we have
\begin{equation*}
 \phi=true_X:X\longrightarrow 1\stackrel{\true}{\longrightarrow}\Omega.
\end{equation*}
A universally valid formula $\phi(x)$ is valid for any generalized element $\alpha: A\to X$. 

\begin{comment}
Indeed, suppose $1_X$ factors as $1=mg $ ($m, g$ as in \ref{cat:truth}). We have $\true_{\lbrace\phi(x)\rbrace}=\phi\comp m$. Composing with $g$ on the right yields $\phi=true_X$. Conversely, suppose $\phi=true_X$. We can use the pullback property to get an arrow g as in the following diagram
%
\begin{equation}\label{factorizing-diagram}
\begin{xy}
 \xymatrix{
  X\ar@2{-}@/_1pc/[rdd] \ar@/^1pc/[rrd] \ar@{.>}[rd]^g& &  \\   %\ar@/_1.5pc/[rr]
 &   \lbrace x\mid \phi(x)\rbrace     \ar[r] \ar@{)->}[d]^m  &  1 \ar@{)->}[d]^{\true}\\
   & X \ar[r]_\phi & \Omega,
}
\end{xy}
\end{equation}
with $mg=1$. It follows $mgm=m$ and since $m$ is monic, also $gm=1$. We hence also have established that in this case it holds $X\cong \lbrace x\mid \phi(x)\rbrace$.
\end{comment}

\begin{example}
 In example \ref{example:delta}, we observed that the formula $\phi(x)=(x=x)$ is interpreted by $\phi:X\stackrel{\langle 1,1\rangle}{\longrightarrow}X\times X\stackrel{\delta_X}{\longrightarrow}\Omega$. It follows directly from the definition of the arrow $\delta$ as the characteristic map of $\Delta=\langle 1,1\rangle$ (c.\ f.\ \ref{Deltadelta}) or from proposition \ref{equalityPred} that this formula is universally valid.

The universal validity of the formula $\psi(x, x')=(x=x')$ is, according to proposition \ref{equalityPred}, equivalent to imposing $\pi_1=\pi_2$. In the category $\Set$ of sets, this is true exactly for the terminal object $\lbrace *\rbrace$ consisting of one element and for the initial element $\emptyset$, i.\ e.\ if the variables $x$ and $x'$ are of type $X=0 \text{ or } 1$. And here indeed the formula $\psi$ is correct.
\end{example}

\subsection{Semantics}
This section aims to show that the interpretation we defined behaves like expected. The statements given here are known under the name ``Kripke-Joyal semantics". We will not give any proofs. They can be found in \citep[ch.\ VI.6]{sheaves} and partly in \citep{lambek-scott}. It is not surprising that the choice of the interpreting arrows is crucial for the proofs.

A generalization of proposition \ref{equalityPred} is the following 

\begin{prop}\label{equalityPred2}
 Let $\sigma$ and $\tau$ be two terms in $\hat\Sigma_\T(Z)_Y$  interpreted by arrows $\sigma, \tau: X\to Y$. Let furthermore $a: A\to X$ be a generalized element of $X$. We denote by $\sigma(a)$ the result of the substitution $\sigma(x)\lbrack x:=a \rbrack$ and analogous for $\tau$. Then
\begin{equation*}
 A\Vdash \sigma(a)=\tau(a) \quad \text{ iff } \quad \sigma a= \tau a.
\end{equation*}
 (Observe that the equality sign on the left is a symbol of our language whereas the one on the right is an "external" one.)
\end{prop}
\begin{pro}
 The proof can be copied from the one of proposition \ref{equalityPred} after remarking that $\langle \sigma, \tau\rangle\comp a = \langle \sigma a, \tau a\rangle$.
\end{pro}


Let $b: X\to B$ and $S: X\to PB$ be arrows of $\T$. Then we have 
\begin{prop}
 \begin{equation*}
  X\Vdash b\in S \quad\text{ iff } \quad \in_B\langle b,S\rangle = true_X.
 \end{equation*}

\end{prop}
This follows immediately from the definitions.

For the logical quantifiers we have
\begin{prop}\label{prop:rules-logic}
 Let $\phi$ and $\psi$ be two formulae with interpreting arrows $\phi, \psi:X\to\Omega$ and let $a: A\to X$ be a generalized element of $X$. Then
\begin{enumerate}
 \item $A\Vdash \phi(a)\wedge \psi(a)$ iff $A\Vdash \phi(a)$ and $A\Vdash \psi(a)$;
 \item \label{logic:or}$A\Vdash \phi(a)\vee \psi(a)$ iff there is an epimorphism $\lbrack k, l\rbrack:D+E\to A$ such that $D\Vdash \phi(ak)$ and $E\Vdash \psi(al)$; 
 \item $A\Vdash \phi(a)\Rightarrow \psi(a)$ iff for all $h:B\to A$, if $B\Vdash \phi(ah)$, then also $B\Vdash\psi(ah)$;
 \item \label{logic:not}$A\Vdash \neg \psi(a)$ iff for all $h:B\to A$, if $B\Vdash \phi(ah)$, then $B\cong 0$;
\end{enumerate}
where $\lbrack k,l\rbrack$ is induced by $k:D\to A$ and $l:E\to A$ via the universal property of the coproduct.
\end{prop}

\begin{prop}\label{prop:rules-quant}
 Let $\phi$ be a formula interpreted by $\phi:X\times Y\to\Omega$ and let $a:A\to X$ be a generalized element of $X$. Then
\begin{enumerate}
 \item $A\Vdash \exists y \phi(a, y)$ iff there is an epi $h:B\to A$ and a generalized element $b:B\to Y$ such that $B\Vdash \phi(ah, b)$;
 \item \label{quant:forall}$A\Vdash \forall y \phi(a, y)$ iff for any object $B$, for any arrow $h:B\to A$ and every generalized element $b:B\to Y$ it holds $B\Vdash \phi(ah, b)$.
\end{enumerate}

\end{prop}



\subsection{Booleanness \& Classical Logic}

In this subsection we want to give an example of the use of the Kripke-Joyal semantics. At the same time we show an interesting logical result: the internal logic of a topos is intuitionistic (c.\ f.\ \ref{prop:rules-logic}, pt.\ \ref{logic:or}); the provability of the law of excluded middle is equivalent to the topos being Boolean. 

\begin{definition}
 A topos $\T$ is said to be \emph{Boolean} if the negation operator $\neg:\Omega\to\Omega$ (c.\ f.\ \eqref{eq:negation}) satisfies
\begin{equation*}
 \neg\neg=id.
\end{equation*}
\end{definition}


\begin{comment}
\begin{prop}
 Let $B\T$ be a Boolean topos and $\phi(x)$ be a formula in a free variable of type $X$. For a generalized element $a:A\to X$ of $X$ we have
\begin{equation}
 A\Vdash \neg\neg\phi(x) \quad\text{ iff } \quad A\Vdash \phi(x).
\end{equation}
\end{prop}

\begin{pro}
 The interpreting arrows of $\phi(x)$ and $\neg\neg\phi(x)$ are equal according to the definition given in \ref{logical:connectives}.
\end{pro}
\end{comment}




\begin{prop}
 Let $\T$ be a topos. The following are equivalent:
\begin{enumerate}
 \item $\T$ is Boolean;
 \item for every subobject $A\monic U$ in $\T$ it holds $A\vee\neg A=U$.
\end{enumerate}
\end{prop}
\begin{pro}
 For a proof we refer to \citep[ch.\ VI.1]{sheaves}.
\end{pro}


\begin{prop}\label{prop:boolean}
 A topos $\T$ is Boolean if and only if the formula 
\begin{equation}
 \forall_\Omega(p\vee \neg p) \in\hat\Sigma(0_\TauSet)_\Omega
\end{equation}
holds in $\T$.
\end{prop}
\begin{pro}
 The variable $p$ of type $\Omega$ is a term, hence defines a subobject $\lbrace p\mid p\rbrace\monic \Omega$. The characteristic map of the subobject coincides with the interpreting arrow of $p$, i.\ e.\ with $1:\Omega\to \Omega$, as in the pullback diagram
\begin{equation}
 \begin{xy}
  \xymatrix{
    \lbrace p\mid p\rbrace \ar@{)->}[d] \ar[r]& 1\ar@{)->}[d]^{\true} \\
   \Omega \ar[r]^\id & \Omega.
}
 \end{xy}
\end{equation}
Hence $\lbrace p\mid p\rbrace$ is in fact the subobject $\true:1\to \Omega$. For a generalized element $\alpha:U\to \Omega$ characterizing a subobject $A\monic U$ as in the pullback
\begin{equation}
 \begin{xy}
  \xymatrix{
    A \ar@{)->}[d] \ar[r]&   **[r]\{p\mid p\}=1 \ar[d]^\true\\
   U \ar[r]^\alpha&   \Omega
}
 \end{xy}
\end{equation}
we have the equivalence
\begin{equation}\label{eq:factorization}
 U\Vdash \alpha\quad\text{  iff  }\quad \alpha \text{ factors through } \true\quad\text{  iff  }\quad A=U.
\end{equation}


Suppose that $1\Vdash \forall_\Omega(p\vee\neg p)$. We show that for an arbitrary subobject $A\monic U$ in $\T$ we have $A\vee \neg A = U$. Let $\alpha: U\to \Omega$ be the characteristic map of $A\monic U$. By proposition \ref{prop:rules-quant}, \ref{quant:forall}, we have $U\Vdash \alpha\vee\neg\alpha$. According to \ref{prop:rules-logic}, \ref{logic:or}, there are arrows $q: V\to U$ and $r:W\to U$ such that $\lbrack q, r\rbrack:V+W\twoheadrightarrow U$ is epi and $V\Vdash \alpha q$, $W\Vdash \alpha r$. Now $V\Vdash \alpha q$ is equivalent to $q^{-1}(A) = V$ by \ref{eq:factorization} (and the fact that two pullbacks, glued together, give a pullback), which again is equivalent to $\Img(q)\leq A$ by the definition of the image \ref{def:image}.
\begin{equation}
 \begin{xy}
  \xymatrix@!=2.5pc{
     q^{-1}(A) \ar[r]\ar@{)->}[d]& A \ar@{)->}[d] \ar[r]& 1 \ar@{)->}[d]^\true\\
          V \ar@{->>}[d] \ar[r]^q  & U \ar[r]^\alpha & \Omega\\
  \Img(q) \ar@{)->}[ur] & & 
}
 \end{xy}
\end{equation}
Also, $W\Vdash \neg(\alpha r)$, by \ref{prop:rules-logic}, \ref{logic:not}, is equivalent to:
\begin{equation}\label{hypothe}
 \text{for } s:Q\to W \text{ with } Q\Vdash \alpha r s  \text{ it follows } Q\cong 0. 
\end{equation}
 But $Q\Vdash \alpha r s$ iff $r s$ factorizes via $A$ by definition of $\Vdash$ and the fact that $A$ is characterized by $\alpha$. Since $r^{-1}A$ is a pullback, this implies that $r^{-1}A\cong 0$: indeed, suppose $r^{-1}A\not\cong 0$. Then $r^{-1}A$ itself and $s:r^{-1}A\to W$ fulfill the hypothesis of \eqref{hypothe}, but not the conclusion. Hence $\Img(r)\leq \neg A$, since $\neg A$ is the biggest subobject such that $A\cap \neg A=0$ by property \eqref{eq:char-neg}.

Furthermore the arrow $\lbrack q, r\rbrack: V+W\to U$ is epi. Since it factors via $\Img(q)\vee\Img(r)\monic U$, the latter one is also epi, hence an isomorphism by \ref{prop:isom}. Altogether we thus have $U=\Img(q)\vee\Img(r)\leq A\vee\neg A$.


%(any arrow from $0$ is an isomorphism)  //not true

Conversely, suppose $\T$ Boolean. We have to show that for an arbitrary $\alpha: U\to \Omega$ it holds $U\Vdash \alpha\vee \neg \alpha$. We use part \ref{logic:or} of \ref{prop:rules-logic}. Let $A\monic U$ be the subobject characterized by $\alpha$. Choose $p: V\to U$ as $m:A\monic U$ and $q: W\to U$ as $\neg m:\neg A\monic U$. Since $\T$ is Boolean, we have $ A\vee\neg A = U $ and hence, by definition of $\vee$ in $\Sub(U)$, the arrow 
\begin{equation}
\lbrack m, \neg m\rbrack: A+\neg A\longrightarrow A\vee\neg A = U \quad\text{ is epi.}
\end{equation}
 It remains to show that $A\Vdash \alpha m$ and $\neg A\Vdash \neg(\alpha m)$. But by \eqref{eq:factorization} this is equivalent to $\alpha m$ factorizing via $\true:1\to \Omega$, which holds since $\alpha=\charmap(m)$.
\end{pro}







%\begin{equation}
% \begin{xy}
%  \xymatrix@R=.6em{
%     & f^{-1}(S_1), f^{-1}(S_2)  & 
%} 
% \end{xy}
%\end{equation}



%\begin{equation}
 %\begin{xy}
  %(0,20)*+{S\cap T}="st"; (20,20)*+{T}="t1"; (35,20)*+{S+T}="s+t"; (55,20)*+{T}="t2";
  %                                                         (45,10)*+{M}="m";
  %(0,0)*+{S}="s";         (20,0)*+{A}="a1" ; (35,0)*+{S}="s2";     (55,0)*+{A}="a2";
  % {\ar "st";"t1"};{\ar "s+t";"t2"};{\ar "st";"s"};{\ar "t1";"a1"};{\ar "s";"a1"};
  % {\ar "s2";"s+t"}; {\ar "t2"; "s+t"}; {\ar "s2";"a2"} ; {\ar "t2";"a2"}
  % {\ar "s+t"; "m"}; {\ar "m"; "a2"}
  
 %\end{xy}
%\end{equation}



\section{Topos Theory vs.\ Set Theory}\label{sect:last}
If a theory is inconsistent, then any formula can be proven in the theory (c.\ f.\ \ref{prop:contradiction}). It is hence valuable information whether a theory is consistent or not.
Now the consistency of a sufficiently strong theory cannot be proven within the theory itself; this is stated by G\"odel's\footnote{Kurt G\"odel; * 1906 in Brno, Czech Republic; \textdied 1978 in Princeton, USA} \emph{incompleteness theorem}.

Given this, instead of outright consistency, one usually considers \emph{relative} consistency: let $\Gamma$ and $\Upsilon$ be formal theories. The theory $\Upsilon$ is called \emph{relatively consistent to} $\Gamma$ if the consistency of $\Gamma$ implies the consistency of $\Upsilon$. Two theories are \emph{equiconsistent}, if each one is consistent relative to the other.

It can now be shown that the set of axioms $\WPT$ defining a \emph{well-pointed topos} with a \emph{natural numbers object} and the \emph{axiom of choice} (c.\ f.\ \citep{sheaves, lawvere})  is equiconsistent to the theory $\RZC$, \emph{restricted Zermelo set theory with axiom of choice}. The latter is a variant of the usual set of axioms $\ZFC$ where the quantifiers do not range over the whole universe. 
\begin{comment}
The following list is taken from \citep{sheaves}:
\begin{description}
 \item [Extensionality] $x=y$ iff, for all $t$, $t\in x$ iff $t\in y$.
 \item [Null Set] There exists a set $\es$ with $x\not\in\es$ for all $x$.
 \item [Pair] For all $x$ and $y$ there exists $z$ with $t\in z$ iff $t=x$ or $t=y$.
 \item [Union] For all $x$ there is a set $u$ with $t\in u$ iff there is some $y$ with $t\in y\in x$.
\end{description}
\end{comment}
 Instead they are of the form "$\forall x\in B$" or "$\exists y\in C$" for some $B$ and $C$. The reader can find a list of the axioms of $\RZC$ in \citep[ch.\ VI.10]{sheaves}.
Here the authors also give a proof of the equiconsistency of these two theories by constructing a \emph{model} for each theory under the assumption of having a model for the other theory and vice versa. This implies equiconsistency, since by G\"odel's completeness theorem \ref{compl} a first order theory is consistent if and only if it is \emph{satisfiable}, i.\ e.\ if and only if it has a model.


\begin{comment}
 \begin{definition}
A family $\mathcal{G}$ of objects of a topos $\T$ is said to \emph{generate} $\T$ if $f\neq g:A\to B$ in $\T$ implies the existence of $G\in \mathcal{G}$ and an arrow $u:G\to A$ such that $fu\neq gu$.
A topos $\T$ is called \emph{well-pointed} if its terminal object $1$ generates $\T$.
\end{definition}

As an example, the category $\Set$ is well-pointed: if two maps $f, g:A\to B$ are not equal, then there is an element $a\in A$ such that $f(a)\neq g(a)$.


\citep{sheaves}
\citep{maclane}
\citep{harrison-form}
\citep{manin}
\citep{tourlakis}
\citep{simpson}
\citep{wiki:truth}
\citep{krivine}
\citep{lambek-scott}
\end{comment}

\newpage

\addcontentsline{toc}{section}{References}
\bibliography{literature}

\end{document}