%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % unify facon d'ecriture: good or bad composition % % % % % % talk to hirscho about the source of interpreting arrows: must be minimal! % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \documentclass{beamer} \usepackage{amsmath, amssymb, amsfonts, amsthm} \usepackage[all,2cell]{xy} \UseAllTwocells \SilentMatrices \SelectTips{cm}{10} \usepackage{color} \usepackage{verbatim} \usetheme{Warsaw} %\usetheme{Frankfurt} \usecolortheme{seahorse} \title{What is truth?} \author{Benedikt Ahrens} \date{\today} \newcommand{\beq}{\begin{equation*}} %ohne Nummerierung \newcommand{\eeq}{\end{equation*}} \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} \newcommand{\comp}{\circ} \newcommand{\halmos}{\quad\hfill\mbox{$\Box$}} % Beweisendezeichen \newcommand{\C}{\mathbf{C}} \newcommand{\D}{\mathbf{D}} \newcommand{\T}{\mathcal{T}} \newcommand{\NN}{\mathbb{N}} \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} \DeclareMathOperator{\target}{target} \DeclareMathOperator{\source}{source} \DeclareMathOperator{\WPT}{WPT} \DeclareMathOperator{\RZC}{RZC} \DeclareMathOperator{\ZFC}{ZFC} \begin{document} \begin{frame} \titlepage \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{Contents} \tableofcontents \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{The tasks} \begin{block}{Syntax - formal language} \begin{itemize} \item express statements unambiguously \item make statements understandable for machines \item for us: at least two \alert{types} of expressions \begin{itemize} \item terms \item formulae (whose truth is to be defined) \end{itemize} \end{itemize} \end{block}\pause \begin{block}{Semantics} \begin{itemize} \item connection: language $\longrightarrow$ universe of objects \item determine validity/truth of formulae \end{itemize} \end{block} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{What we are going to learn today} \begin{itemize} \item Syntax - the language \begin{itemize} \item how to handle types \item how to handle the binding effect of quantifiers \item example: language $\Sigma_\T$ of a topos $\T$ - \alert{suitable for set theory} \end{itemize} \item Topos - categorical universe of sets \item Semantics - interpretation of the topos language \begin{itemize} \item arrows of $\T$ as little helpers for interpretation \item validity of formulae of $\Sigma_\T$ \end{itemize} \end{itemize} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{What is a formal language?} %%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{first thoughts about a language for mathematics} \begin{block}{Goals:} \begin{itemize} \item avoid ambiguity \item internationality \item machine aid \end{itemize} \end{block} \begin{block}{What we need} \begin{itemize} \item alphabet: suitable for expressing mathematical ideas \begin{itemize} \item logical symbols $\Rightarrow, \wedge, \vee, \neg$ \item quantifiers $\forall, \exists$ \item theory-specific symbols (e.g. $\in$, $+$) \end{itemize} \item grammar rules \begin{itemize} \item number of arguments \item \alert{type} of arguments \end{itemize} \end{itemize} \end{block} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{two phenomena: types \& bound variables} %\begin{block}{example I - types} % constructor \emph{if\_then\_else\_} in some programming language %\begin{itemize} % \item takes 3 arguments of type (\emph{bool, nat, nat}), returns type \emph{nat} % \item \alert{arity} (\emph{nat}; \emph{bool, nat, nat}) %\end{itemize} %\end{block} \begin{block}{example - types \& binding effect} constructor $\forall_\NN$ \begin{itemize} \item takes a \emph{formula} containing a free variable $n$ of type $\NN$, e.g. $n\geq 5$ \item returns a formula where the variable is bound, $\forall_\NN n\geq 5$ \end{itemize} \end{block} We will work with a set of types $T$. \pause \begin{definition}[category $\TSet$] \begin{itemize} \item objects: $T$-indexed families of sets \item morphisms: $T$-indexed families of morphisms of sets \end{itemize} \end{definition} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%55 \begin{frame} \frametitle{$T$-signature} \begin{definition}[$T$-typed signature] \begin{itemize} \item set $\Sigma$ of symbols \item function $a$, called \alert{arity}, assigning to each symbol $s$ of $S$ a tuple $a(s)=(s_0; \bar s_1, \ldots, \bar s_n)$ \end{itemize} 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}\pause \begin{block}{Example} Types $T=\lbrace \Omega \text{ (formula)}, \NN\rbrace$ \begin{itemize} \item $\forall:(\Omega; (\Omega;\NN))$ \begin{itemize} \item argument: a formula with a free variable of type $\NN$ \item result: a formula where the variable is bound \end{itemize} \item $\Rightarrow:(\Omega; (\Omega;\es),(\Omega;\es))$ \begin{itemize} \item two formulae as arguments, no variable-binding \end{itemize} \end{itemize} \end{block} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{Expressions $=$ Trees} \begin{itemize} \item mathematical structure for expressions: trees! \item signature $=$ rules for number and type of sons \end{itemize} \begin{definition} \begin{itemize} \item $X = (X_t)_{t\in T}$ element of $\TSet$ \item $\Sigma$ a $T$-typed signature \end{itemize} \alert{$\hat\Sigma X = ((\hat\Sigma X)_t)_{t\in T}$} the \alert{typed set of trees} constructible from symbols of $\Sigma$ and the typed set $X$ of \alert{variables} as leaves. \end{definition}\pause %\begin{block}{Example} \begin{columns} \column{.5\textwidth} \begin{itemize} \item $T = \lbrace \Omega ,\ldots \rbrace$ \item $\Sigma$ contains logical symbols with usual arity \item $P, Q, R\in X_\Omega$ variables of type formula \end{itemize} \column{.5\textwidth} \begin{equation*} \begin{xy} \xymatrix @R=.5pc{ & \Rightarrow \ar@{-}[ld]\ar@{-}[rd] & & \\ P & & \wedge\ar@{-}[ld]\ar@{-}[rd] & \\ & Q & & R } \end{xy} \end{equation*} \end{columns} %\end{block} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{adding a new element to a (typed) set of variables} \begin{definition} \begin{itemize} \item \begin{equation*} X^*:=X \coprod \lbrace \infty_X \rbrace \end{equation*} \item $u\in T$ and $X=(X_t)_{t\in T}$ in $\TSet$; we define $\quad X^{*_u} \quad$ s.t. \begin{itemize} \item $(X^{*_u})_t=X_t\quad$ for all $t\neq u$ \item $(X^{*_u})_u=(X_u)^*$ \end{itemize} \end{itemize} \end{definition}\pause \begin{definition} \begin{itemize} \item $\bar s = (s_0; s_1,\ldots,s_n)$ nonempty finite sequence of types \item $X$ in $\TSet$ a typed set of variables \end{itemize} We define \begin{equation*} \hat\Sigma^{\bar s}X:= (\hat\Sigma(X^{*_{s_1}*_{s_2}\ldots *_{s_n}}))_{s_0} \end{equation*} \end{definition} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{in the end we have a lot of structure} $X=(X_t)_{t\in T}, Y$ objects in $\TSet$, $\quad f:X\to Y$ in $\TSet$ \begin{itemize} %\item $X\hat\Sigma$ trees built according to a given grammar $=$ \alert{signature}. \item $\hat\Sigma f:\hat\Sigma X\to \hat\Sigma Y$ \alert{renaming} of variables. \item $\eta_X: X\to \hat\Sigma X$ : variable as a tree \item $\mu_X : \hat\Sigma\hat\Sigma X\to \hat\Sigma X$ \item for each $s\in \Sigma$ with arity $a(s)=(s_0; \bar s_1, \ldots, \bar s_n)$ a mapping \begin{equation*} s:\prod \hat\Sigma^{\bar s_i}X \to (\hat\Sigma X)_{s_0} \end{equation*} which builds trees with root $s$, arguments $=$ subtrees \end{itemize} %The language will be a \alert{monad} $\hat\Sigma: \TSet\to\TSet$ (definition later). \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{comment} \begin{frame} \frametitle{Monads} \begin{definition}[Monad] Triple $(R, \eta, \mu)$ consisting of \begin{itemize} \item functor $R:\TSet \to \TSet$ \item natural transformations \begin{itemize} \item $\eta : \Id \xrap R$ \item $\mu:R^2 \xrap R$ \end{itemize} \end{itemize} which render commutative, for any typed set $X$ of $\TSet$,: \begin{equation*} \begin{xy} \xymatrix{ XR \ar[r]^{X\eta R} \ar@2{-}[rd] & X R^2 \ar[d]|{X\mu} \ar@{}[ld] \ar@{}[rd] & XR \ar[l]_{XR\eta} \ar@2{-}[dl] & X R^3 \ar[r]^{ XR\mu} \ar[d]_{X\mu R} & X R^2 \ar[d]^{X\mu} \\ & X R & & X R^2 \ar[r]_{X \mu} & X R } \end{xy} \end{equation*} \end{definition} \end{frame} \end{comment} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{comment} \begin{frame} \frametitle{Modules} \begin{definition}[$R$-Module] $R$ a monad. A {\em module} $(M,\sigma)$ over $R$ consists of \begin{itemize} \item a functor $M:\TSet\to\C$ \item a natural transformation $\sigma : RM \xrap M$, called {\em substitution} \end{itemize} such that the following diagram commutes for any typed set $X$: \begin{equation*} \begin{xy} \xymatrix{ XRRM \ar[r]^{XR\sigma} \ar[d]_{X\mu M} & XRM \ar[d]^{X\sigma} \\ XRM \ar[r]_{ X\sigma} & XM} \end{xy} \end{equation*} \end{definition} Let $(M,\si^{(M)})$ and $(N,\si^{(N)})$ be two $R$--modules. The cartesian product $M \times N$ is again an $R$--module. \end{frame} \end{comment} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%% \begin{comment} \begin{frame} \frametitle{derived module} \begin{definition}[\& proposition] $R$ a monad and $M$ an $R$--module. The {\em derived module $\pu M$ with respect to} $u \in T$ of $M$ is, for any $X$ of $\TSet$: \begin{equation*} X(\pu M) := X^{*_u}M \end{equation*} and for any morphism $h$ in $\TSet$: \begin{equation*} h(\pu M) := h^{*_u}M. \end{equation*} This defines indeed an $R$--module. \end{definition} \begin{lemma} If $R$ is a monad, then for any $u\in T$ the operation $X\mapsto (XR)_u$ can be turned into an $R$-module. \end{lemma} \end{frame} \end{comment} %%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{comment} \begin{frame} \frametitle{representation of an arity in a monad} \begin{definition} $R$ a monad. For $\bar s=(s_0; s)$ with \begin{itemize} \item $s_0\in T$ \item $s=(s_1, \ldots, s_n)$ an (empty?) finite sequence of elements in $T$ \end{itemize} we define $R^{\bar s}:\TSet\to\Set$ as the $R$-module \begin{equation*} XR^{\bar s}= \bigl(X(\partial_{s_1}\ldots\partial_{s_n}R)\bigr)_{s_0}. \end{equation*} \end{definition} \begin{definition}[representation of an arity] Given the arity $s=(s_0; \bar s_1, \ldots, \bar s_n)$, we define a \alert{representation of $s$} in a monad $R$ as a morphism of modules \begin{equation*} \prod_{i=1}^n R^{\bar s_i} \to R_{s_0}. \end{equation*} \end{definition} \end{frame} \end{comment} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{example for representation in $\hat\Sigma$} \begin{block}{Example} \begin{itemize} \item $T=\lbrace \Omega, \ldots\rbrace$ \item $\Rightarrow :(\Omega; (\Omega;\es),(\Omega;\es))$ \end{itemize} \begin{align*} \Rightarrow_X:(\hat\Sigma X)_\Omega\times (\hat\Sigma X)_\Omega & \to (\hat\Sigma X)_\Omega, \\ (P, Q) & \mapsto (P\Rightarrow Q) \end{align*} \end{block} %\begin{block}{Remark} % For (typed) sets $Z\leq Y$ we have $Z\hat\Sigma\leq Y\hat\Sigma$ (usual order on families of sets). We can determine the \alert{minimal} (typed) set $X$ such that a given expression $E$ of type $t\in T$ is an element of $X\hat\Sigma_t$. %\end{block} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{What is a topos?} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{creating a universe of sets within category theory} \begin{block}{universe of sets} \begin{itemize} \item collection of sets \item maps between sets \begin{itemize} \item composition of maps (with associativity) \item identity map \end{itemize} \end{itemize} is realized in a \alert{category} \end{block}\pause \begin{block}{special sets and maps} \begin{itemize} \item power set $\mathcal{P}B$, hom set $B^A$, truth values $\Omega=\lbrace 0,1\rbrace$ \item characteristic function of $S\subset B$ \end{itemize} \end{block} \begin{block}{Goal: imitate a universe of sets with categorical means} \begin{itemize} \item describe special sets by \alert{universal properties} \end{itemize} \end{block} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{comment} \begin{frame} \frametitle{definition: category $\C$} \begin{block}{consists of} \begin{itemize} \item collection of objects $\C_0$ \item collection of arrows $\C_1$ with maps \begin{itemize} \item source:$\C_1 \to \C_0$ \item target:$\C_1 \to \C_0$ \end{itemize} Notation: $f: A\to B$ \end{itemize} \end{block}\pause \begin{block}{structure} \begin{itemize} \item \emph{composition} of \alert{composable} arrows \item for each object an \emph{identity} arrow, left and right neutral under composition \item associativity of composition \end{itemize} \end{block} \end{frame} \end{comment} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{comment} \begin{frame} \frametitle{examples of categories} \begin{block}{vector spaces over fixed $K$} \begin{itemize} \item objects: vector spaces over $K$ \item arrows: $K$-linear maps \end{itemize} \end{block}\pause \begin{block}{monoid $M$} \begin{itemize} \item one object \item arrows: the elements of $M$ \item composition of arrows $\longleftrightarrow$ multiplication in $M$ \end{itemize} \end{block}\pause \begin{block}{partially ordered set $P$} \begin{itemize} \item objects: the elements of $P$ \item arrows: \begin{itemize} \item identity arrows \item additionally exactly one arrow $a\to b$ iff $a\leq b$ in $P$ \end{itemize} \end{itemize} \end{block} \end{frame} \end{comment} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{comment} \begin{frame} \frametitle{generalization of properties of maps} \begin{definition}[injectivity] $f:B\to C$ injective if for all $b, b'\in B$ it holds \begin{equation*} (b)f=(b')f \Longrightarrow b = b' \end{equation*} \end{definition}\pause \begin{lemma} $f:B\to C$ injective iff\\ $\forall A$, $\forall g_1, g_2:A\to B$ we have \begin{equation*} g_1f=g_2f \Longrightarrow g_1=g_2 \end{equation*} \end{lemma}\pause \begin{definition}[mono, epi] An arrow $f:A\to B$ in a category $\C$ is \alert{monic/epi} if it is \alert{right/left cancellable}. \end{definition} \end{frame} \end{comment} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{comment} \begin{frame} \frametitle{properties of arrows in a category} \begin{definition}[epi] An arrow $f:A\to B$ in a category $\C$ is \alert{epi} if it is \alert{right cancellable}. \end{definition} \end{frame} \end{comment} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{Universal properties of $\Omega$ and $\mathcal{P}B$} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5 \begin{comment} \begin{frame} \frametitle{generalization of characteristic function} \begin{definition}[subobject] Suppose that the collection of monos $S\monic B$ in $\C$ is a set ($\C$ a small category).\\ A \alert{subobject $S$ of $B$} in the category $\C$ is an \alert{equivalence class of monos $S\monic B$}, where \begin{equation*} (s:S\monic B) \equiv (t:T\monic B) \end{equation*} iff \begin{equation*} S\cong T \text{ in }\C. \end{equation*} \end{definition} %In $\Set$ every subobject has an indicator function. %How to define an indicator function for $S\monic B$ in a category $\C$? %\begin{definition}[pullback] %\begin{columns} % \column{.4\textwidth} % $C\times_A B$ the \alert{pullback} of $f$ and $g$ if for any $x,y$ such that $xf=yg$ there is exactly one $\beta$ which renders commutative the emerging triangles. %\column{.4\textwidth} %\begin{equation*} % \begin{xy} % \xymatrix{ % M\ar@{.>}[rd]_{\exists !\beta}\ar@/^1pc/[rrd]^{x} \ar@/_1pc/[ddr]_y 5 \\ % & C\times_A B\ar[r]_r \ar[d]_s & B\ar[d]^f \\ % & C\ar[r]_g & A %} % \end{xy} %\end{equation*} %\end{columns} %\end{definition} %\begin{block}{Notation in $\Set$} % \begin{itemize} % \item set of truth values $\Omega=\{0,1\}$ % \item map $\true:1_\Set=\{*\} \to \Omega$, $*\mapsto 1$ % \item $\chi_{S,B}$ the indicator function for $S\subset B$ % \end{itemize} %\end{block} \end{frame} \end{comment} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{comment} \begin{frame} \frametitle{diagrammatic property of indicator functions} \begin{columns} \column{.4\textwidth} The following diagram commutes: \begin{equation*} \begin{xy} \xymatrix @!=2pc { S \ar@{{)}->}[d]_i \ar@{->}[r] & 1 \ar@{)->}[d]^{\true}\\ B \ar@{->}[r]^{\chi} & \Omega } \end{xy} \end{equation*}\pause \column{.6\textwidth} Suppose $f:T\to B$ s.t. the outer quadrilateral commutes: \vspace*{.5cm} \begin{equation*} \begin{xy} \xymatrix @!=2pc { T \ar@/^2pc/[rr] \ar[rd]_f & S \ar@{{)}->}[d]_i \ar@{->}[r] & 1 \ar@{)->}[d]^{\true}\\ & B \ar@{->}[r]^{\chi} & \Omega } \end{xy} \end{equation*}\pause Then $f(T)$ is contained in $i(S)\cong S$. \end{columns} \end{frame} \end{comment} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%55 \begin{comment} \begin{frame} \frametitle{diagrammatic property of indicator functions II} \begin{columns} \column{.6\textwidth} \begin{equation*} \begin{xy} \xymatrix @!=2pc { T \ar@/^2pc/[rr] \ar[rd]_f \ar@{.>}[r]_g& S \ar@{{)}->}[d]_i \ar@{->}[r] & 1 \ar@{)->}[d]^{\true}\\ & B \ar@{->}[r]^{\chi} & \Omega } \end{xy} \end{equation*} \column{.4\textwidth} There exists exactly one map $g:T\to S$ such that $ gi = f$. The upper part of the diagram also commutes. \end{columns}\pause \begin{definition}[pullback] \begin{columns} \column{.4\textwidth} $C\times_A B$ the \alert{pullback} of $f$ and $g$ if for any $x,y$ such that $xf=yg$ there is exactly one $\beta$ which renders commutative the emerging triangles. \column{.4\textwidth} \begin{equation*} \begin{xy} \xymatrix{ M\ar@{.>}[rd]_{\exists !\beta}\ar@/^1pc/[rrd]^{x} \ar@/_1pc/[ddr]_y \\ & C\times_A B\ar[r]_r \ar[d]_s & B\ar[d]^f \\ & C\ar[r]_g & A } \end{xy} \end{equation*} \end{columns} \end{definition} \end{frame} \end{comment} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{comment} \begin{frame} \frametitle{diagrammatic property of indicator functions III} \begin{definition} $S$ is called the \alert{pullback} of $B\stackrel{\chi}{\to}\Omega \stackrel{\true}{\leftarrow}1$ \end{definition} \end{frame} \end{comment} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{definition of a subobject classifier} \begin{definition}[subobject classifier] A \alert{subobject classifier} in a category $\C$ (w.\ fib. products and $1$) consists of \begin{itemize} \item an object $\Omega$ of $\C$ \item a monic $\true:1\to\Omega$ \end{itemize} s.\ t.\ for any mono $S\monic B$ there exists a unique \alert{char. function} $\phi:B\to\Omega$, i.\ e.\ a unique $\phi$ giving a fibered product: \begin{equation*} \begin{xy} \xymatrix{ S \ar@{{)}->}[d]_m \ar@{->}[r] & 1 \ar@{)->}[d]^{\true}\\ B \ar@{->}[r]^{\phi} & \Omega. } \end{xy} \end{equation*} \end{definition} Example in $\Set$: $\quad \Omega=\lbrace 0,1\rbrace$, $\quad\true:*\mapsto 1$, $\quad\phi = \chi_{(S,B)}$ % \begin{equation*} % \Sub(B)\cong \Hom(B,\Omega) \text{ natural in } B % \end{equation*} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{universal property of $\mathcal{P}B$ - power object in $\Set$ and $\C$} \begin{block}{membership predicate in $\Set$} \begin{equation*} \in_B: B\times \mathcal{P}B\to \Omega, \quad (b,S)\mapsto \begin{cases} 1, &\text{ if } b\in S,\\ 0 &\text{ otherwise.} \end{cases} \end{equation*} \end{block} \begin{block}{universal property of $(\mathcal{P}B, \in_B)$} \begin{columns} \column{.4\textwidth} For any $f: B\times A\to\Omega$ there is a unique arrow $g:A\to \mathcal{P}B$ which makes commute: \column{.4\textwidth} \begin{equation*} \begin{xy} \xymatrix{ B\times A \ar[d]_{1\times g} \ar[rd]^f \\ B\times \mathcal{P}B \ar[r]_-{\in_B} & \Omega. } \end{xy} \end{equation*} \end{columns} \end{block} In the same way we can postulate the existence of a power object $(PB, \in_B)$ in \alert{any} category $\C$ with products and $\Omega$! \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{Definition of a topos and important properties} %%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{Definition of a topos} \begin{definition}[elementary topos $\T$] A topos is a category $\T$ with \begin{itemize} \item a fibered product for every diagram $X\to B \leftarrow Y$; \item a terminal object $1$; \item a subobject classifier $(\Omega, \true: 1\to \Omega)$; \item for every object $B$ a power object $PB$ with $\in_B:B\times PB\to\Omega$. \end{itemize} \end{definition} \begin{theorem}[$\T$ has exponentials] \begin{columns} \column{.6\textwidth} For any $B$ and $C$ there is an object $C^B$ and $e=e_{B,C}: B\times C^B\to C$ s.t. for any $f:B\times A\to C$ there is a unique $g:A\to C^B$ which makes commute \column{.3\textwidth} \begin{equation*} \begin{xy} \xymatrix{ B\times A \ar[rd]^f \ar[d]_{1\times g}& \\ B\times C^B \ar[r]_-{e} & C } \end{xy} \end{equation*} \end{columns} \end{theorem} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{some important arrows of $\T$} \begin{block}{$P:B\mapsto PB$ can be made a contravariant functor} Consider $k:A\to B$ in $\T$. Define $Pk:PB\to PA$ as the \alert{transpose} of $\in_B \circ (k\times 1)$: \begin{equation*} \begin{xy} \xymatrix{ 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*} This makes $P:\T\to\T$ a contravariant functor. \end{block} %\begin{itemize} % \item $B\mapsto PB$ can be made into a contravariant functor % \item $Pk:PB\to PA$ has \alert{internal} left and right adjoint %\begin{equation*} % \exists_k,\forall_k: PA\to PB %\end{equation*} %\end{itemize} %\begin{block}{$\Omega$ is an internal Heyting algebra - we have} % \begin{align*} % \wedge, \vee, \Rightarrow&: \Omega\times \Omega\to\Omega \\ % \neg&:\Omega\to\Omega \\ % 0, 1&: 1_\T\to\Omega %(for the elements $0$ and $1$) %\end{align*} %which make commute the diagrams given by the equations defining a Heyting algebra. %\end{block} %\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} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{Definition Heyting algebra} \begin{itemize} \item A \alert{lattice} $L$ is a set with two elements $0\neq 1$ and two binary operations $\wedge$ and $\vee$ which satisfy \begin{itemize} \item commutativity, associativity \item $x\wedge x=x$, $\quad x\vee x=x$,$\qquad 1\wedge x =x $, $\quad 0\vee x=x$, \item $x\wedge (y\vee x)=x= (x\wedge y)\vee x$. \end{itemize} Induces a partial order by $\quad x\leq y$ iff $x\wedge y = x$. \item A lattice $H$ is a \alert{Heyting algebra} if for $x,y\in H$ we have an \alert{exponential} $(x\Rightarrow y)$ s.t. \begin{equation*} z\leq (x\Rightarrow y) \quad\text{ iff }\quad z\wedge x\leq y. \end{equation*} \item In a Heyting algebra H we define a \alert{negation operator} \begin{equation*} \neg x := (x \Rightarrow 0). \end{equation*} \end{itemize} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{Equations in $H$ and diagrammatic version} \begin{lemma}[Equations holding in Heyting algebra $H$] For $x, y,z \in H$ we have \begin{align*} (x\Rightarrow &x)=1\\ x\wedge (x\Rightarrow y) = x\wedge y&, \qquad y\wedge (x\Rightarrow y)=y\\ x\Rightarrow (y\wedge z) = &(x\Rightarrow y)\wedge (x\Rightarrow z) \end{align*} \end{lemma}\pause \begin{block}{Example for diagrammatic version of $x\wedge (x\Rightarrow y)= x\wedge y$} \begin{equation*} \begin{xy} \xymatrix{ H\times H\times H \ar[r]^-{1\times \Rightarrow}& H\times H\ar[d]^{\wedge} \\ H\times H \ar[u]^{\Delta\times 1}\ar[r]^-{\wedge}& H } \end{xy} \end{equation*} \end{block} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{comment} \begin{frame} \frametitle{$\Omega$ as internal Heyting algebra I} \begin{itemize} \begin{definition}[Heyting algebra] A \alert{lattice} $L$ is a set with two distinguished elements $0$ and $1$ and two binary operations $\wedge$ and $\vee$ which are both commutative and associative and which satisfy \begin{itemize} \item $x\wedge x=x$, $\quad x\vee x=x$,$\qquad 1\wedge x =x $, $\quad 0\vee x=0$, \item $x\wedge (y\vee x)=x= (x\wedge y)\vee x$. \end{itemize} \end{definition} \begin{block}{Example: diagrammatic version of associativity} \begin{columns} \column{.4\textwidth} \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]^{*} & L } \end{xy} \end{equation*} \column{.4\textwidth} where $*$ is one of the operations $\wedge$ or $\vee$ \end{columns} \end{block} \end{frame} \end{comment} %%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{$PB$ is an internal Heyting algebra} %\begin{definition}[Heyting algebra] %A lattice $H$ is a \alert{Heyting algebra} if it has a to each pair of elements $x$ and $y$ an \emph{exponential} $x\Rightarrow y$ s.t. %\begin{equation*} % z\leq (x\Rightarrow y) \text{ iff } z\wedge x\leq y. %\end{equation*} % \end{definition} \begin{theorem} For any $B$ in $\T$ the power object $PB$ is an \alert{internal Heyting algebra}, i.e. there are arrows \begin{itemize} \item $\wedge, \vee, \Rightarrow: PB\times PB\to PB$ \item $\neg: PB\to PB$ \item $0, 1: 1_\T\to PB$ (for the elements $0$ and $1$) \end{itemize} which make commute the diagrams given by the preceding equations of a Heyting algebra. \begin{center} In particular, $\Omega = P1$ is such. \end{center} \end{theorem} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%5 \begin{frame} \frametitle{Internal partial order of a Heyting algebra object} \begin{itemize} \item $H$ an internal Heyting algebra of $\T$. The object $\leq_H$ shall be the equalizer of $\wedge, \pi_1:H\times H\to H$ as in \begin{equation*} \begin{xy} \xymatrix{ \leq_H \ar[r] \ar[d]_e & H \ar[d]^{\Delta_H} \\ H\times H \ar[r]_{\langle \wedge, \pi_1\rangle} & H\times H. } \end{xy} % %\begin{xy} % \xymatrix{ % \leq_H \ar[r]^-{e} & H\times H \ar@<+.5ex>[r]^-{\wedge} \ar@<-.5ex>[r]_-{\pi_1}& H. %} % \end{xy} \end{equation*} \item Properties reflexivity, transitivity, antisymmetry can be expressed diagrammatically. Example: reflexivity \begin{equation*} \begin{xy} \xymatrix{ H \ar[r]^-{\Delta_H}\ar@{.>}[rd]& H\times H \\ & \leq_H.\ar[u]_{e} } \end{xy} \end{equation*} \end{itemize} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{Def: internal adjunction} %of $(H, \leq_H)$ and $(H', \leq_{H'})$ $(H, \leq_H)$ and $(H', \leq_{H'})$ \alert{internal partially ordered objects} in $\T$. Suppose $\alpha:H\to H'$ and $\beta: H'\to H$ are monotonous arrows, i.\ e.\ \begin{equation*} \begin{xy} \xymatrix{ \leq_H \ar[r]^-{e_H} \ar@{.>}[rd] & H\times H \ar[r]^-{\alpha\times\alpha} &H'\times H' \\ & \leq_{H'} \ar[ru]_-{e_{H'}} & } \end{xy} \end{equation*} and similarly for $\beta$.\\ $\alpha$ is \alert{internally left adjoint} to $\beta$ if we have factorizations as in \begin{equation*} \begin{xy} \xymatrix@C=8ex{ H' \ar[r]^-{\langle \alpha\beta, 1\rangle}\ar@{.>}[rd]& H'\times H' & \txt{and}& H\ar[r]^-{\langle 1, \beta\alpha\rangle} \ar@{.>}[rd]& H \times H \\ & \leq_{H'}\ar[u] & & & \leq_{H}.\ar[u] } \end{xy} \end{equation*} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{$Pk$ has internal adjoints} \begin{theorem} For any arrow $k:A\to B$ the arrow $Pk:PB\to PA$ has an \begin{itemize} \item internal left adjoint $\exists_k:PA\to PB$; \item internal right adjoint $\forall_k: PA\to PB$. \end{itemize} \end{theorem} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{Arrow $\delta$ as equality predicate} \begin{definition}[arrows $\delta_B$ and $\true_X$] \begin{itemize} \item $\Delta_B=\langle 1_B,1_B\rangle: B\monic B\times B$ has a characteristic map \begin{equation*} \delta_B: B\times B\to \Omega. \end{equation*} \item For any object $X$ let be defined by \begin{equation*} \true_X: X\to 1 \stackrel{\true}{\longrightarrow}\Omega. \end{equation*} \end{itemize} \end{definition}\pause \begin{lemma} 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\langle b,b'\rangle = true_X \quad \text{ iff } \quad b=b'. \end{equation*} \end{lemma} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Interpretation in a topos} \subsection{Syntax of the language of a topos} %%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{The signature $\Sigma=\Sigma_\T$} \begin{columns} \column{.3\textwidth} \begin{itemize} \item types $=$ objects of $\T$ \item formulae $=$ expressions of type $\Omega$ \item we omit indices $A$, $B$ for the constructors \end{itemize}\pause \column{.6\textwidth} \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*} \end{columns} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{An arrow for every expression} %%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{Arrows as helpers for interpretation} \begin{block}{An arrow for every expression} \begin{itemize} \item $Z$ an object of $\TauSet$ \item define for every expression $E\in (\hat\Sigma Z)_B$ an arrow $a(E)$ of $\T$ \begin{itemize} \item $\target(a(E)) = B =$ type of $E$ \item \begin{equation*} \source(a(E))=\prod_{\genfrac{}{}{0pt}{1}{B\in \T}{|Z_B|=i}}B^i \end{equation*} where we suppose that $|Z_B|< \infty$ and only finitely many $Z_B\neq \es$ \end{itemize} \end{itemize} \end{block} \begin{itemize} \item variable $b$ of type $B$ interpreted by $1_B:B\to B$ \item $\phi(a, b, b')\in \hat\Sigma({0_\TauSet}^{*_A*_B*_B})_\Omega$ interpreted by an arrow \begin{equation*} A\times B\times B \to \Omega \end{equation*} \end{itemize} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{Expanding the set of free variables by combining expressions} \begin{block}{Constructors with several arguments} \begin{itemize} \item for $Z \leq Y$ we have $\hat\Sigma Z \leq \hat\Sigma Y$ \item necessity of adjusting the source of interpreting arrow %%\end{equation*} \end{itemize} \end{block}\pause \begin{definition}[enlarging the source of an interpreting arrow] \begin{itemize} \item expression $\sigma$ interpreted by $\sigma: U \to B$ \item $\sigma$ is also interpreted by \begin{equation*} \sigma\circ \pi_1: U \times A \to B \end{equation*} \end{itemize} \end{definition} Given two expressions, we can hence suppose that the sources of their interpreting arrows coincide. \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{Recursive definition of the interpreting arrow I} \begin{itemize} \item variable $b$ of type $B$ interpreted by $1_B:B\to B$ \item interpreting arrow for an equality predicate \begin{itemize} \item $E$ a formula $(\sigma = \tau)\in \hat\Sigma Z_\Omega$ \item $\sigma$ and $\tau$ of type $B$ interpreted by $\sigma, \tau: U \to B$ \end{itemize} $E$ is interpreted by \begin{equation*} \begin{xy} \xymatrix @C=4.5pc{ (\sigma=\tau): U \ar[r]^-{\langle \sigma , \tau\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*} \item $E$ a formula $\phi\Rightarrow \psi$,\\ $\phi$ and $\psi$ formulae interpreted by $\phi,\psi: U\to \Omega$ \begin{equation*} \begin{xy} \xymatrix @C=4.5pc{ \phi\Rightarrow\psi: U \ar[r]^-{\langle \phi , \psi\rangle} & \Omega\times \Omega \ar[r]^-{\Rightarrow}& \Omega } \end{xy} \end{equation*} \end{itemize} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \begin{block}{Example} \begin{itemize} \item $(b=b)$ a formula in $\hat\Sigma({0_\TauSet}^{*_B})_\Omega$ interpreted by arrow \begin{equation*} \begin{xy} \xymatrix @C=4.5pc{ B \ar[r]^-{\langle 1, 1\rangle=\Delta_B} & B\times B \ar[r]^-{\delta_B}& \Omega } \end{xy} \end{equation*} \item $(b=b')$ in $\hat\Sigma({0_\TauSet}^{*_B*_B})_\Omega$ \begin{itemize} \item we regard $b, b'$ as elements in $\hat\Sigma({0_\TauSet}^{*_B*_B})_B$ \item $b$ interpreted by $1_B\circ \pi_1:B\times B\to B$ \item $b'$ interpreted by $1_B\circ \pi_2:B\times B\to B$ \end{itemize} $(b=b')$ interpreted by the arrow \begin{equation*} \begin{xy} \xymatrix @C=4.5pc{ B\times B \ar[r]^-{\langle \pi_1, \pi_2\rangle=1 } & B\times B \ar[r]^-{\delta_B}& \Omega. } \end{xy} \end{equation*} \end{itemize} \end{block} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{Recursive definition of the interpreting arrow II} variable $b$ of type $B$ interpreted by $1_B:B\to B$ \begin{equation*} \begin{xy} \xymatrix@C=4.5pc @R= 1ex{ % \langle \sigma, \tau\rangle: U \ar[r]^-{\langle \sigma , \tau\rangle} & A\times B & \\ \sigma(\tau): U \ar[r]^-{\langle \sigma , \tau\rangle} & A\times B^A \ar[r]^-{e_{A,B}}& B \\ (\sigma\in\tau): U \ar[r]^-{\langle \sigma , \tau\rangle} & B\times \Omega^B \ar[r]^-{\in_B}& \Omega\\ (\lambda_{A,B,Z}) \sigma: U \ar[r]^-{\txt{ transpose } (\sigma)}& B^A & \\ % \phi\vee\psi: U \ar[r]^-{\langle \phi , \psi\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\\ \forall_{B} (\lambda_{B,\Omega,Z})\phi: U \ar[r] ^-{\text{transpose}(\phi)} & \Omega^B \ar[r]^-{\forall_{(\bullet_B)}}& \Omega } \end{xy} \end{equation*} where $\bullet_B:B\to 1$ %In general recursive definition, using e.g. \alert{Heyting algebra arrows of $\Omega$} and \alert{internal adjoints} $\exists_k, \forall_k:PA\to PB$. \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5 \subsection{Definition of the validity of formulae} %%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{How a formula defines an object} \begin{definition}[object defined by a formula] \begin{itemize} \item $\quad\phi\in Z\hat\Sigma_\Omega\quad$ a formula \item in free variables $x_i$ of type $X_i$ \item interpreting arrow $ \phi: X = \prod X_i \to\Omega$ \end{itemize} %If with (i.\ e.\ the variables which appear freely in $\phi$ are of type of the factors of $X$), we write %\begin{equation*} The object \begin{center} $\lbrace x\in X \mid \phi(x)\rbrace $ \end{center} %\end{equation*} is defined to be the fibered product \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*} \end{definition} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{Validity of a formula} \begin{itemize} \item $\phi=\phi(x_1, \ldots, x_n)$ a formula in $Z\hat\Sigma_\Omega$ with free variables $x_i$ of type $X_i$ ($i=1,\ldots n$) \item $\alpha_i: U\to X_i$ generalized elements of the $X_i$ \end{itemize} %\begin{definition} $\phi$ is \alert{true} for the $\alpha_i$, \begin{equation*} U\Vdash \phi(\alpha_1,\ldots,\alpha_n), \end{equation*} if $\alpha=\langle \alpha_1, \ldots, \alpha_n\rangle : U\to X=\prod X_i$ factors through $\lbrace x\mid \phi(x)\rbrace$ \begin{equation*} \begin{xy} \xymatrix{ & \lbrace x\mid \phi(x)\rbrace \ar[r] \ar@{)->}[d]^m & 1 \ar@{)->}[d]^{\true}& &\txt{iff}\\ U \ar@{.>}[ru]^g \ar[r]_\alpha & X \ar[r]_\phi & \Omega & &\phi\circ\alpha=true_U . } \end{xy} \end{equation*} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{Special case: universal validity} \begin{itemize} \item $\phi(x)$ a formula with interpreting arrow $\phi:X\to\Omega$ \end{itemize} is \alert{universally valid} if one of the following equivalent holds: \begin{align} \alpha:=1_X:X\to X &\text { factors through } \lbrace x\mid \phi(x)\rbrace \\ \phi=true_X:&X\longrightarrow 1\stackrel{\true}{\longrightarrow}\Omega \\ \lbrace x\mid \phi(x&)\rbrace \cong X %\end{center} \end{align}\pause \begin{block}{Example} The formula $(b=b)$ in $({0_\TauSet}^{*_B})\hat\Sigma_\Omega$ interpreted by arrow \begin{equation*} \begin{xy} \xymatrix @C=4.5pc{ B \ar[r]^-{\langle 1, 1\rangle=\Delta_B} & B\times B \ar[r]^-{\delta_B}& \Omega } \end{xy} \end{equation*} is universally valid by def. of the arrow $\delta_B$ as char. map of $\Delta_B$. \end{block} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame} \frametitle{Why the strange choice of arrows?} The \alert{Beth-Kripke-Joyal theorem} tells us that the validity we defined behaves as we would expect. Examples: \begin{itemize} \item $A\Vdash \phi(a)\wedge \psi(a)$ iff $A\Vdash \phi(a)$ and $A\Vdash \psi(a)$ \item $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{itemize} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%5 \begin{frame} \frametitle{What was this good for?} \begin{itemize} \item equiconsistency $\WPT \longleftrightarrow \RZC$ (c.f. \cite{sheaves}) \begin{itemize} \item $\WPT$ the axioms defining a \alert{well-pointed topos} (terminal object generates the topos) \item $\RZC$ the axioms of \alert{restricted Zermelo set theory} \end{itemize} \item form instead of substance (c.f. \cite{lawvere}) \begin{itemize} \item set theory based on isomorphism-invariant structure (e.g. universal properties) instead of membership relation \end{itemize} \end{itemize} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{thebibliography}{99} \begin{frame} \frametitle{References} \bibitem[Law05]{lawvere} Lawvere, F. William. {\sl An elementary theory of the category of sets (long version) with commentary}, Reprinted and expanded from Proc. Nat. Acad. Sci. U.S.A. {\bf 52} (1964) \bibitem[MLM92]{sheaves} Mac Lane, Saunders and Moerdijk, Ieke. {\sl Sheaves in geometry and logic}, Springer-Verlag, New York, 1992 %\begin{thebibliography}{99} % \bibitem [FPT99]{fpt} M. Fiore, G. Plotkin, D. Turi. {\sl Abstract syntax with variable binding}, Proc. 14th Annual Symposium on Logic and Computer Science, p. 193 -- 202, 1999 % \bibitem [HM07]{HM} A. Hirschowitz, M. Maggesi. {\sl The algebraicity of the lambda calcus}, preprint 2007, arXiv:0704.2900 %\end{thebibliography} \end{frame} \end{thebibliography} %%%%%%%%%%%%%%%%%%%%%%%%%%%%% \end{document}