\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{internal logic}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{category_theory}{}\paragraph*{{Category theory}}\label{category_theory}

[[!include category theory - contents]]

\hypertarget{topos_theory}{}\paragraph*{{Topos Theory}}\label{topos_theory}

[[!include topos theory - contents]]

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{kinds_of_internal_logics_in_different_categories}{Kinds of internal logics in different categories}\dotfill \pageref*{kinds_of_internal_logics_in_different_categories} \linebreak
\noindent\hyperlink{internal_firstorder_logic}{Internal first-order logic}\dotfill \pageref*{internal_firstorder_logic} \linebreak
\noindent\hyperlink{theories}{Theories}\dotfill \pageref*{theories} \linebreak
\noindent\hyperlink{CategoricalSemantics}{Categorical semantics}\dotfill \pageref*{CategoricalSemantics} \linebreak
\noindent\hyperlink{the_internal_logic_as_a_functor}{The internal logic as a functor}\dotfill \pageref*{the_internal_logic_as_a_functor} \linebreak
\noindent\hyperlink{soundness_and_internal_reasoning}{Soundness and internal reasoning}\dotfill \pageref*{soundness_and_internal_reasoning} \linebreak
\noindent\hyperlink{syntactic_categories}{Completeness, syntactic categories, and Morita equivalence}\dotfill \pageref*{syntactic_categories} \linebreak
\noindent\hyperlink{kripkejoyal_semantics}{Kripke--Joyal semantics}\dotfill \pageref*{kripkejoyal_semantics} \linebreak
\noindent\hyperlink{dependent_type_theory}{Dependent type theory}\dotfill \pageref*{dependent_type_theory} \linebreak
\noindent\hyperlink{higherorder_logic}{Higher-order logic}\dotfill \pageref*{higherorder_logic} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{LogicOfSet}{Internal logic in $Set$}\dotfill \pageref*{LogicOfSet} \linebreak
\noindent\hyperlink{LogicOfPresheaves}{Internal logic in a sheaf topos on open subsets}\dotfill \pageref*{LogicOfPresheaves} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak
\noindent\hyperlink{general}{General}\dotfill \pageref*{general} \linebreak
\noindent\hyperlink{Applications}{Applications}\dotfill \pageref*{Applications} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

One of the most important observations of [[category theory]] is that large parts of mathematics can be [[internalization|internalized]] in any [[category]] with sufficient structure. The most basic examples of this involve algebraic structures; for instance, a [[group]] can be defined in any category with finite products, and an [[internal category]] can be defined in any ambient category with [[pullback]]s. For such [[algebraic theory|algebraic]] (or even [[essentially algebraic theory|essentially algebraic]]) structures, which are defined by \emph{operations} with \emph{equational axioms} imposed, it suffices for the ambient category to have (usually finite) limits.

However, if we assume that the ambient category has additional structure, then much more of mathematics can be internalized, potentially including [[field]]s, [[local ring]]s, [[finite set]]s, [[topological space]]s, even the field of [[real number]]s. The idea is to exploit the fact that all mathematics can be written in the language of [[logic]], and seek a way to internalize logic in a category with sufficient structure.

The basic ideas of the internal logic induced by a given [[category]] $C$ are:

\begin{itemize}%
\item the [[object]]s $A$ of $C$ are regarded as collections of things of a given [[type]] $A$


\item the [[morphisms]] $A\to B$ of $C$ are regarded as terms of type $B$ containing a free [[variable]] of type $A$ (i.e. in a [[context]] $x:A$)


\item a [[subobject]] $\phi \hookrightarrow A$ is regarded as a \emph{proposition} ([[predicate]]): by thinking of it as the sub-collection of all those things of type $A$ for which the statement $\phi$ is [[true]]

\begin{itemize}%
\item the maximal subobject is hence the proposition that is always true; this is the logical object of [[truth]] $\top \hookrightarrow A$


\item the minimal subobject is hence the proposition that is always false; this is the logical object of [[falsity]] $\bottom \hookrightarrow A$


\item one proposition [[implication|implies]] another if as subobjects of $A$ they are connected by a morphism in the [[poset]] of subobjects: $\phi \Rightarrow \psi$ means $\phi \hookrightarrow \psi$



\end{itemize}

\item Logical operations are implemented by [[universal construction]]s on [[subobject]]s.

\begin{itemize}%
\item the conjunction [[and]] is the [[product]] of subobjects (their [[meet]])


\item the conjunction [[or]] is the [[coproduct]] of subobjects (their [[join]])



\end{itemize}


\end{itemize}
and so on.

\begin{itemize}%
\item A [[dependent type]] over an object $A$ of $C$ may be interpreted as a morphism $B\to A$ whose ``fibers'' represent the types $B(x)$ for $x:A$. This morphism might be restricted to be a [[display map]] or a [[fibration]].

\end{itemize}
Once we formalize the notion of ``logical [[theory]]'', the construction of the internal logic can be interpreted as a [[functor]] $Lang$ from suitably structured categories to theories. The morphisms of theories are ``interpretations'', and so an internalization of some theory $T$ (such as the ``theory of groups'') into a category $C$ is a morphism of theories $T\to Lang(C)$.

Moreover, the functor $Lang$ has a left [[adjoint functor]]: the [[syntactic category]] $Syn$ of a theory. Thus, a model of $T$ in $C$ is equally well a functor $Syn(T)\to C$. Frequently, this adjunction is even an [[equivalence of categories]]; see [[relation between type theory and category theory]].

\hypertarget{kinds_of_internal_logics_in_different_categories}{}\subsubsection*{{Kinds of internal logics in different categories}}\label{kinds_of_internal_logics_in_different_categories}

There are many different kinds of of ``logical theories'', each of which corresponds to a type of category in which such theories can be internalized (and yields a corresponding adjunction $Syn \dashv Lang$).

\newline |[[geometric logic|geometric]]| |[[coherent category|infinitary coherent category]] (aka [[geometric category]])| |[[first-order logic|first-order]]| |[[Heyting category]]| |[[dependent types]]| |[[locally cartesian closed category]]| |[[higher order logic|higher order]]| |[[topos|elementary topos]]| [[linear logic]]| |[[symmetric monoidal category]]|

Each type of logic up to and including ``geometric'' can also be described in terms of [[sketch|sketches]]. Not coincidentally, the corresponding types of category up to and including ``geometric'' fit into the framework of [[familial regularity and exactness]]. Sketches can also describe theories applicable to categories not even having finite products, such as finite sum sketches, but the type-theoretic approach taken on this page requires at least finite products (or else something closely akin, such as a [[cartesian multicategory]]).

However, there are other sorts of [[internalization]] that do not fit in this framework. For instance, to describe a [[monoid]] internal to a [[monoidal category]], one needs an internal [[linear logic]]. See [[internalization]] for a discussion of the more general notion in the context of [[doctrine]]s.

\hypertarget{internal_firstorder_logic}{}\subsection*{{Internal first-order logic}}\label{internal_firstorder_logic}

We begin with the interpretation of internal first-order logic, which is the most used in [[toposes]] and related categories.

\hypertarget{theories}{}\subsubsection*{{Theories}}\label{theories}

In this section, what we mean by a \emph{theory} is a \emph{[[type theory]]} without dependent types, but with a dependent logic. This entails the following.

\begin{itemize}%
\item The [[signature (in logic)|signature]] of the theory consists of

\begin{itemize}%
\item Various \emph{[[types]]} $A,B,C$. For example, the theory of a group has only one type (group elements), but the theory of a-ring-and-a-module has two types (ring elements and module elements). There are also generally \emph{type constructors} that build new types from basic ones, such as product types $A\times B$ and the unit type $1$.


\item The theory will also generally contain \emph{[[function symbol]]s} such as $f:A\to B$, each with a source and target that are types. For example, the theory of a monoid has one type $M$, one function symbol $m:M\times M\to M$, and one function symbol $e:1\to M$. Function symbols of source $1$ are also called \emph{constants}.


\item The theory may also contain \emph{[[relation symbol]]s} $R:A$, each equipped with a type. For example, the theory of a [[partial order|poset]] has one type $P$ and one relation $\le:P\times P$. The most basic relation symbol, which most theories contain, is \emph{[[equality]]} $=_A:A\times A$ on a type $A$.



\end{itemize}

\item Finally the theory may contain \emph{logical [[axiom]]s} of the form $\Gamma | \varphi  \vdash \psi$. Here $\varphi$ and $\psi$ are first-order formulas built up from terms and relation symbols using logical connectives and quantifiers such as $\top,\bot,\wedge,\vee,\Rightarrow,\neg,\forall,\exists$, and $\Gamma$ is a \emph{[[context]]} which declares the type of every variable occurring in $\varphi$ and $\psi$.



\end{itemize}
For example, the theory of a group has one type $G$, three function symbols $m:G\times G\to G$, $i:G\to G$, and $e:1\to G$, and axioms

\begin{displaymath}
\itexarray{
  x:G,y:G,z:G |  \top \vdash m(m(x,y),z) = m(x,m(y,z))\\
  x:G | \top \vdash m(x,i(x)) = e \;\wedge\; m(i(x),x) = e\\
  x:G | \top \vdash m(x,e) = x \;\wedge\; m(e,x) = x.
}
\end{displaymath}
This is an \emph{[[equational theory]]}, meaning that each axiom is just one or more equations between terms that must hold in a given context. For a different sort of example, the theory of a poset has one type $P$, one relation $\le:P\times P$, and axioms

\begin{displaymath}
\itexarray{
  x:P | \top \vdash x\le x\\
  x:P,y:P | x\le y \;\wedge\; y\le x \vdash x=y\\
  x:P,y:P,z:P | x\le y \;\wedge\; y\le z \vdash x\le z.
}
\end{displaymath}
\hypertarget{CategoricalSemantics}{}\subsubsection*{{Categorical semantics}}\label{CategoricalSemantics}

Now suppose that we have a category $C$ with [[finite limit]]s and we want to interpret such a theory internally in $C$. We identify the aspects of the theory with structures in the category by what is called [[categorical semantics]]:

First, for each \emph{type} in the theory we choose an [[object]] of $C$. Then for each \emph{function symbol} in the theory we choose a [[morphism]] in $C$. And finally, for each \emph{relation} in the theory we choose a [[subobject]] in $C$. (We always interpret the relation of \emph{equality} on a type $A$ by the diagonal $A\hookrightarrow A\times A$ in $C$.) Thus, for example, to interpret the theory of a group in $C$ we must choose an object $G$ and morphisms $m:G\times G\to G$, $i:G\to G$, and $e:1\to G$, while to interpret the theory of a poset, we must choose an object $P$ and a subobject $[\le] \hookrightarrow P\times P$.

Of course, this is not enough; we need to say somehow that \emph{the axioms are satisfied}. We first define, inductively, an interpretation of every \emph{term} that can be constructed from the theory by a morphism in $C$. For example, given an object $G$ and a morphism $m:G\times G\to G$, there are two evident morphisms $G\times G\times G \to G$ which are the interpretations of the two terms $m(m(x,y),z)$ and $m(x,m(y,z))$.

We then define, inductively, an interpretation of every \emph{[[logical formula]]} that can be constructed from the theory by a \emph{subobject} in $C$. The idea is that if $x:A$ is a variable of type $A$ and $\varphi(x)$ is a formula with $x$ as its free variable, then the interpretation of $\varphi(x)$ should be the ``subset'' $\{x\in A | \varphi(x)\}$ of $A$. The base case of this induction is that if $t$ is a term interpreted by a morphism $A\to B$ and $R:B$ is a relation symbol, then $R(t)$ is interpreted by the pullback of the chosen subobject $R\hookrightarrow B$ representing $R$ along the morphism $t:A\to B$. The building blocks of logical formulas then correspond to operations on the posets $Sub(A)$ of subobjects in $C$, as follows.

\begin{tabular}{l|l|l}
Logical operator&&Operation on $Sub(A)$\\
\hline 
[[logical conjunction&conjunction]]: $\wedge$&\\
[[truth]]: $\top$&&[[top element]] ($A$ itself)\\
[[disjunction]]: $\vee$&&[[union]]\\
[[falsity]]: $\bot$&&[[bottom element]] ([[initial object\\
[[implication]]: $\Rightarrow$&&[[Heyting algebra\\
[[existential quantification]]: $\exists$&&[[left adjoint]] to [[pullback]]\\
[[universal quantification]]: $\forall$&&[[right adjoint]] to [[pullback]]\\
\end{tabular}

The fact that existential and universal quantifiers can be interpreted as left and right adjoints to pullbacks was first realized by [[Bill Lawvere]]. One way to realize that it makes sense is to notice that in [[Set]], the image of a subset $R\subset A$ under a function $f:A\to B$ can be defined as

\begin{displaymath}
\{b\in B | (\exists a\in A)(a\in R \;\wedge\; f(a)=b)\},
\end{displaymath}
while its ``dual image'' (the right adjoint to pullback) can be defined as

\begin{displaymath}
\{b\in B | (\forall a \in A)(f(a)=b \Rightarrow a\in R)\}.
\end{displaymath}
Of course, not in all finitely complete categories $C$ do all these operations on subobjects exist. Moreover, in order for the relationship with logic to be well-behaved, any of the operations we make use of must be \emph{[[pullback stability|stable]] under} (preserved by) pullbacks. (Pullbacks of subobjects correspond to ``innocuous'' logical operations such as adding extra unused variables, duplicating variables, and so on, so they should definitely not affect the meaning of the logical connectives. However, in [[linear logic]] such operations become less innocuous.)

In any category with finite limits, the posets $Sub(A)$ always have finite intersections (given by pullback), including a top element (given by $A$ itself). Thus in any such category, we can interpret logical theories that use only the connectives $\wedge$ and $\top$. This includes both the theories of groups and posets considered above.\newline In a [[regular category]], the existence of pullback-stable [[image]]s implies that the [[base change]] functor $f^*:Sub(B)\to Sub(A)$ along any map $f:A\to B$ has a left adjoint, usually written $\exists_f$, and that these adjoints ``commute with pullbacks'' in an appropriate sense (given by the [[Beck-Chevalley condition]]. Thus, in a regular category we can interpret any theory in so-called \emph{[[regular logic]]}, which uses only $\wedge$, $\top$, and $\exists$.

Actually, some instances of $\exists$ can be interpreted in any category with finite limits: if $f$ is itself a monomorphism, then $f^*$ always has a left adjoint, given simply by composition with $f$. On the logical side, this means that we can interpret ``provably unique existence'' in any category with finite limits. Logic with $\wedge$, $\top$, and ``provably unique existence'' is called \emph{cartesian logic} or \emph{finite-limit logic}.

A [[coherent category]] is basically defined to be a [[regular category]] in which the subobject posets additionally have pullback-stable finite unions. Thus, in a coherent category we can interpret so-called \emph{coherent logic}, which adds $\vee$ and $\bot$ to [[regular logic]]. Likewise, in an infinitary-coherent (or ``geometric'') category we can interpret \emph{geometric logic}, which adds infinitary disjunctions $\bigvee_i \varphi_i$ to coherent logic. Geometric logic is especially important because it is preserved by the inverse image parts of [[geometric morphism]]s, and because any geometric theory has a [[classifying topos]].

On the other hand, in a [[extensive category|lextensive category]], we do not have images or all unions, but if we have two subobjects of $A$ which are \emph{disjoint} (their intersection is initial), then their coproduct is also their union in $Sub(A)$. Therefore, in a lextensive category we can interpret \emph{disjunctive logic}, which is cartesian logic plus $\bot$ and ``provably disjoint disjunction.'' Likewise, in an infinitary-lextensive category we can interpret ``infinitary-disjunctive logic.''

Finally, in a [[Heyting category]] the base change functors $f^*:Sub(B)\to Sub(A)$ also have right adjoints, usually written $\forall_f$, and it is easy to see that this implies that each $Sub(A)$ is also a [[Heyting algebra]], hence has an ``implication'' $\Rightarrow$ as well. (We define ``negation'' by $\neg \varphi \equiv \varphi \Rightarrow \bot$.) Thus, in a Heyting category we can interpret all of (finitary, first-order) [[intuitionistic logic]].

Now that we know how to interpret logic, we can say that a \textbf{model} of a given theory in $C$ consists of a choice of objects, morphisms, and subobjects for the types, function symbols, and relation symbols as above, such that for each axiom $\Gamma | \varphi \vdash \psi$, we have $[\varphi]\le [\psi]$ in $Sub([\Gamma])$. Here, $[\Gamma]$ is the product of the objects that correspond to the types of the variables in $\Gamma$, $[\varphi]$ and $[\psi]$ are the interpretations of the formulas $\varphi$ and $\psi$ as subobjects of $[\Gamma]$, and $\leq$ is the relation of subobject inclusion.

It is easy to verify that a model of the theory of a group in $C$ is precisely an internal [[group]] object in $C$, as usually defined. For instance, the validity of the axiom

\begin{displaymath}
x:G,y:G,z:G | \top \vdash m(m(x,y),z) = m(x,m(y,z))
\end{displaymath}
means that the [[equalizer]] of the two morphisms $G\times G\times G \to G$ must be all of $G\times G\times G$, or equivalently that those two morphisms must be equal. The same happens in most other cases.

\hypertarget{the_internal_logic_as_a_functor}{}\subsubsection*{{The internal logic as a functor}}\label{the_internal_logic_as_a_functor}

As described above, a model of a given theory $T$ in a category $C$ consists of an assignment

\begin{tabular}{l|l|l}
&&\\
\hline 
types of $T$&$\to$&objects of $C$\\
function symbols of $T$&$\to$&morphisms of $C$\\
relation symbols of $T$&$\to$&subobjects in $C$\\
axioms of $T$&$\to$&containments in $C$\\
\end{tabular}

This is a sort of [[heteromorphism]] in that it changes the name of things as it operates on them. We can describe it more simply as a ``translation of theories'' as follows.

Given a category $C$ (which may be regular, coherent, geometric, Heyting, etc.), we define its \textbf{internal type theory (with first-order logic)} $Lang(C)$ to be the theory whose

\begin{itemize}%
\item types are the objects of $C$;
\item function symbols are the morphisms on $C$;
\item relation symbols are the subobjects in $C$;
\item axioms are the containments in $C$.

\end{itemize}
Now a model of $T$ in $C$ can be described simply as a morphism of theories (a ``translation'' or ``interpretation'')

\begin{displaymath}
T \to Lang(C).
\end{displaymath}
The functor $Lang : Categories \to Theories$ has a left adjoint, the [[syntactic category]] of a theory. Thus we have a chain of natural isomorphisms

\begin{displaymath}
Theories(T,Lang(C)) \cong Models(T,C) \cong Categories(Syn(T),C)).
\end{displaymath}
\hypertarget{soundness_and_internal_reasoning}{}\subsection*{{Soundness and internal reasoning}}\label{soundness_and_internal_reasoning}

Internal logic is not just a way to concisely describe internal structures in a category, but also gives us a way to \emph{prove} things about them by ``internal reasoning.'' We simply need to verify that the ``usual'' methods of logical reasoning (for example, from $\varphi\vdash \psi$ and $\psi\vdash \chi$ deduce $\varphi\vdash\chi$) are \emph{internally valid}, in the sense that if the premises are satisfied in some model $C$ (in the example, if $[\varphi]\le [\psi]$ and $[\psi]\le [\chi]$) then so is the conclusion (in the example, $[\varphi]\le [\chi]$). This is called the \emph{Soundness Theorem}.

It then follows that if we start from the axioms of a theory and ``reason normally'' within type theory, which in practice amounts to pretending that the types are sets, the function symbols are functions, and the relation symbols are subsets, then anything we prove will still be true when the theory is interpreted in an \emph{arbitrary} category, not just [[Set]]. For example, by easy equational reasoning from the theory of a group, we can prove that inverses are unique, which is expressed by the logical sequent

\begin{displaymath}
x:G,y:G,z:G | m(x,y)=e \;\wedge\; m(x,z)=e \vdash y=z.
\end{displaymath}
It follows that this is also true, suitably interpreted, as a statement about internal group objects in \emph{any} category.

There are (at least) three caveats. Firstly, we must take care to use only the rules appropriate to the fragment of logic that is valid in the particular categories we are interested in. For example, if we want our conclusions to be valid in any [[regular category]], we must restrict ourselves to reasoning ``within regular logic.'' Most mathematicians are not familiar with making such distinctions in their reasoning, but in practice most things one would want to say about a regular theory turn out to be provable in regular logic. (We will not spell out the details of what this means.) And once we are in a Heyting category, and in particular in a topos, this problem goes away and we can use full first-order logic.

The second, more important, caveat is that the internal logic of all these categories is, in general, [[constructive mathematics|constructive]]. This means that, among other things, the interpretation of $\neg\neg\varphi$ is, in general, distinct from that of $\varphi$, and that $\varphi\vee \neg\varphi$ is not always valid. So even if we believe that [[classical logic]] (including the principle of [[excluded middle]] and even the [[axiom of choice]]) is ``true,'' as many mathematicians do, there is still a reason to look for proofs that are constructively acceptable, since it is only these which are valid in the internal logic of most categories. If the category is [[Boolean category|Boolean]] and/or satisfies the internal [[axiom of choice]], however, then this problem goes away, but these fail in many categories in which one wants to internalize (such as many [[Grothendieck topos]]es).

The third caveat is that one must take care to distinguish the \emph{internal} logic of a category from what is \emph{externally} true about it. In general, internal validity is ``local'' truth, meaning things which become true ``after passing to a [[cover]].'' This is particularly important for formulas involving \emph{disjunction} and \emph{existence}. For example, an object's being [[projective object|projective]] in the category $C$ is a different statement from its being \emph{internally} projective, meaning that ``$X$ is projective'' is true in the internal logic. Another good example can be found in the different notions of [[finite object]] in a topos. This problem goes away if the ambient category is [[well-pointed topos|well-pointed]], but well-pointed categories are even rarer than Boolean ones satisfying choice; the only well-pointed Grothendieck topos is [[Set]] itself.

\hypertarget{syntactic_categories}{}\subsection*{{Completeness, syntactic categories, and Morita equivalence}}\label{syntactic_categories}

The converse of the Soundness Theorem is called the \emph{Completeness Theorem}, and states that if a sequent $\varphi\vdash\psi$ is valid in every model of a theory, then it is \emph{provable} from that theory. This is noticeably less trivial. In classical first-order logic, where the only models considered are set-valued ones, the completeness theorem is usually proven using [[ultraproduct]]s. However, in categorical logic there is a more elegant approach (which additionally no longer depends on any form of the [[axiom of choice]]).

The \textbf{[[syntactic category]]} $C_T = Syn(T)$ of a theory $T$ was mentioned above, as the left adjoint to the ``internal logic functor'' $Lang$. By the [[Yoneda lemma]], the syntactic category $C_T$ contains a ``generic'' model of the theory. Moreover, by the construction of $C_T$ (see [[syntactic category]]), the valid sequents in this model are \emph{precisely} those provable from the theory. Therefore, if a sequent is valid in all models, it is in particular valid in the generic model in $C_T$, and hence provable from $T$.

The universal property of $C_T$ is also sometimes useful for semantic conclusions. For instance, sometimes one can prove something about the generic model and then carry it over to all models.

Furthermore, if $T$ lives in a sub-fragment of geometric logic (such as regular, coherent, lextensive, or geometric logic), then the [[Grothendieck topos]] of [[sheaf|sheaves]] on $C_T$ for its appropriate (regular, coherent, extensive, or geometric) [[coverage]] contains a $T$-model which is generic for models in Grothendieck toposes: any $T$-model in a Grothendieck topos is its image under the inverse image of a unique [[geometric morphism]]. This topos is called the \textbf{[[classifying topos]]} of the theory.

The [[syntactic category]] of a theory can be considered as the ``extensional essence'' of that theory, since functors out of $C_T$ completely determine the $T$-models in any category $D$ with suitable structure. It therefore makes sense, in some contexts, to define a \emph{morphism} of theories to be a functor between their [[syntactic categories]], and an \emph{equivalence} of theories (sometimes called a \emph{Morita equivalence}) to be an equivalence between their syntactic categories.

A morphism $T\to T'$ between theories, in this sense, induces a functor from $T'$-models in $D$ to $T$-models in $D$, for any category $D$ with suitable structure, in a way which is natural in $D$. In particular, theories which are ``Morita equivalent'' in this sense have naturally equivalent categories of models in all categories $D$ with suitable structure; so they have the same ``meaning'' even though they may be presented quite differently. (Note that this is a much stronger sort of equivalence than merely having equivalent categories of models in some particular category, such as $Set$.) Moreover, the fact that the syntactic category is defined ``syntactically'' means that a morphism $T\to T'$ actually induces a ``translation'' of the types, functions, and relations of $T$ into those of $T'$.

By first applying various ``completion'' processes to syntactic categories before asking about equivalence, we obtain coarser notions of equivalence, which only induce equivalences of models in more restricted sorts of categories. For instance, if we compare the [[exact completion]]s of syntactic categories of regular theories, we obtain a notion of equivalence that induces equivalences of categories of models in all exact categories (not necessarily all regular ones). Likewise for coherent theories and [[pretopos]]es, and for geometric theories and infinitary pretoposes. Note, though, that the infinitary-pretopos completion of a (small) geometric theory is in fact already a (Grothendieck) topos, and coincides with the classifying topos considered above. Thus, passage to classifying toposes is also an instance of this construction, and an equivalence of classifying toposes means that two theories have equivalent categories of models in all toposes. (This is still much stronger than just having equivalent categories of models in $Set$.)

\hypertarget{kripkejoyal_semantics}{}\subsection*{{Kripke--Joyal semantics}}\label{kripkejoyal_semantics}

To be written, but see [[Kripke-Joyal semantics]].

\hypertarget{dependent_type_theory}{}\subsection*{{Dependent type theory}}\label{dependent_type_theory}

We now consider the internal language of a [[locally cartesian closed category]] as a [[dependent type theory]].

Material to be moved here from [[relation between type theory and category theory]].

\hypertarget{higherorder_logic}{}\subsection*{{Higher-order logic}}\label{higherorder_logic}

To be written, but see [[Mitchell–Bénabou language]] for the version in a [[topos]].

\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

\hypertarget{LogicOfSet}{}\subsubsection*{{Internal logic in $Set$}}\label{LogicOfSet}

The [[topos]] [[Set]] in [[classical mathematics]] of course has as its internal logic the ``ordinary'' logic. This is reproduced by following the abstract nonsense as follows:

the [[terminal object]] of [[Set]] is [[generalized the|the]] one-element set ${*}$, the [[subobject classifier]] in [[Set]] is the two-element set $\Omega = \{true, false\}$ equipped with the map

\begin{displaymath}
T : {*} \to \Omega
\end{displaymath}
that picks the element $true$ in $\Omega$. The [[Heyting algebra]] of [[subobject]]s of the [[terminal object]] is the [[poset]]

\begin{displaymath}
L = \{  \emptyset \hookrightarrow {*} \}
\end{displaymath}
consisting only of the two trivial subobjects of $*$, the point itself and the empty set, and the unique inclusion morphism between them. These are classified, respectively, by the [[truth value]]s ${*} \stackrel{true}{\to} \Omega$ and ${*} \stackrel{false}{\to} \Omega$, so that we can also write our [[poset]] of [[subobject]]s of the [[terminal object]] as

\begin{displaymath}
L = \{  false \to true \}
  \,.
\end{displaymath}
The logical operation $\wedge = AND$ is the [[product]] in the [[poset]] $L$. Indeed we find pullback diagrams in $L$

\begin{displaymath}
\itexarray{
    true \times \true = true &\to& true
    \\
    \downarrow
    \\
    true
  }
  \;\;\;
  \;\;\;
  \;\;\;
  \itexarray{
    true \times false = false &\to& false
    \\
    \downarrow
    \\
    true
  }
  \;\;\;
  \;\;\;
  \;\;\;
  \itexarray{
    false \times false = false &\to& false
    \\
    \downarrow
    \\
    false
  }
  \,.
\end{displaymath}
The logical operation $\vee = OR$ is the [[coproduct]] in the [[poset]] $L$. Indeed we find [[pushout]] diagrams in $L$

\begin{displaymath}
\itexarray{
    && true
    \\
    && \downarrow
    \\
    true
    &\to&
    true \coprod \true = true   
  }
  \;\;\;\;
  \;\;\;
  \;\;\;
   \itexarray{
    && false
    \\
    && \downarrow
    \\
    true
    &\to&
    true \coprod false = true
  }
  \;\;\;\;
  \;\;\;
  \;\;\;
   \itexarray{
    && false
    \\
    && \downarrow
    \\
    false
    &\to&
    false \coprod false = false
  }
 \,.
\end{displaymath}
The logical operation $\not = NOT$ is given by the [[internal hom]] into the [[initial object]] in $L$:

\begin{displaymath}
\not = hom(-, false) : L^{op} \to L
  \,.
\end{displaymath}
We find the value of the [[internal hom]] by its defining [[adjunction]]. For $hom(true,false)$ we have

\begin{displaymath}
Hom_L(true, hom(true,false)) \simeq Hom_L(true \times true, false) = Hom_L(true, false) = \emptyset
\end{displaymath}
and

\begin{displaymath}
Hom_L(false, hom(true,false)) \simeq Hom_L(false \times true, false) = Hom_L(false, false) = {*}
\end{displaymath}
from which we deduce that

\begin{displaymath}
hom(true,false) = false\,.
\end{displaymath}
Similarly for $hom(false,false)$ we have

\begin{displaymath}
Hom_L(true, hom(false,false)) \simeq 
  Hom_L(true \times false, false)
  = Hom_L(false, false) = {*}
\end{displaymath}
and

\begin{displaymath}
Hom_L(false, hom(false,false)) \simeq 
  Hom_L(false \times false, false)
  = Hom_L(false, false) = {*}
\end{displaymath}
from which we deduce that

\begin{displaymath}
hom(false,false) = true
  \,.
\end{displaymath}
This way all the familiar logical operations are recovered from the internal logic of the [[topos]] [[Set]].

\hypertarget{LogicOfPresheaves}{}\subsubsection*{{Internal logic in a sheaf topos on open subsets}}\label{LogicOfPresheaves}

Let $X$ be a [[topological space]] and $Op(X)$ its [[category of open subsets]] and $Sh(X) := Sh(Op(X))$ the [[Grothendieck topos]] of [[category of sheaves|of sheaves]] on $X$.

We discuss the internal logic of this sheaf topos (originally \hyperlink{Tarski}{Tarski, 1938}).

The [[terminal object]] is the sheaf [[representable functor|represented by]] $X$: the one that is constant on the one-element set

\begin{displaymath}
X : U \mapsto {*}
  \,.
\end{displaymath}
The [[subobject]]s of this object are the [[representable functor|representable presheaves]]

\begin{displaymath}
hom(-,V) : U \mapsto
  \left\{
    \itexarray{
      {*} & | if U \subset V
      \\
      \emptyset & otherwise
    }
  \right.
\end{displaymath}
for $V \in Op(X)$.

\begin{remark}
\label{}\hypertarget{}{}
In the \emph{[[presheaf]]} topos $PSh(Op(X))= Func(Op(X)^{op},Set)$, the subobjects of $1$ are arbitrary [[sieves]] in $Op(X)$, not just representables. For instance, for any two open sets $U$ and $V$ there is a sieve consisting of all open sets contained in either $U$ or $V$, which doesn't necessarily contain $U\cup V$. It's only in the \emph{sheaf} topos $Sh(X)$ that the representables are precisely the subobjects of $1$.

\end{remark}
The [[poset]] of [[subobject]]s formed by these is just the [[category of open subsets]] itself:

\begin{displaymath}
L = Op(X)
  \,.
\end{displaymath}
\begin{itemize}%
\item The logical operation $AND$ is the [[product]] in $Op(X)$: this is the \textbf{intersection} of open subsets.


\item The logical operation $OR$ is the [[coproduct]] in $Op(X)$: this is the \textbf{union} of open subsets.


\item The [[internal hom]] in $Op(X)$ is given by

\begin{displaymath}
hom(U,V) = (U^c \vee V)^\circ
\end{displaymath}
(the interior of the union of the complement of $U$ with V).

So \textbf{negation} is given by sending an open subset to the interior of its complement:

\begin{displaymath}
\not U = hom(U,\emptyset)
  = (U^c \vee \emptyset)^\circ = (U^c)^\circ
  \,.
\end{displaymath}


\end{itemize}
In particular we find that in the internal logic of $PSh(X)$ the law of the [[excluded middle]] fails in general, as in general we do not have that

\begin{displaymath}
(\not U) \vee U = true
\end{displaymath}
because $\not U \vee U = (U^c)^\circ \cup U = X \backslash \partial U$ is the total space $X$ without the boundary (frontier) of $U$, and not $true = X$, all of the total space.

Thus, the internal logic of this [[Grothendieck topos|sheaf topos]] is (in general) [[intuitionistic logic]]. As remarked above, this is the case in many toposes.

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[type theory]], [[homotopy type theory]]


\item [[relation between category theory and type theory]]



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\hypertarget{general}{}\subsubsection*{{General}}\label{general}

Most books on topos theory develop some internal logic, at least in the context of a topos. For example:

\begin{itemize}%
\item [[Saunders Mac Lane]] [[Ieke Moerdijk]], \emph{[[Sheaves in Geometry and Logic]]}


\item Goldblatt, \emph{Topoi: the categorial analysis of logic}



\end{itemize}
Part D of

\begin{itemize}%
\item [[Peter Johnstone]], \emph{[[Sketches of an Elephant]]}

\end{itemize}
is comprehensive.

Phoa has a presentation of the internal logic of a topos over a dependent type theory, as opposed to other systems which use simple type theory. This is system is not minimal, but close to what is used in practice \href{http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/ECS-LFCS-92-208.ps.gz}{PS}.

The book

\begin{itemize}%
\item [[Bart Jacobs]], \emph{Categorical Logic and Type Theory}

\end{itemize}
works in the even more general context of [[Grothendieck fibration|fibrations]], allowing us to associate to each object $A$ an arbitrary poset instead of $Sub(A)$.

The book

\begin{itemize}%
\item [[Paul Taylor]], \emph{[[Practical Foundations of Mathematics]]}

\end{itemize}
is arguably all about this subject (although you wouldn't know it until about Chapter VIII), but from a different perspective. In particular, Taylor allows us to replace having \emph{all} pullbacks with pullbacks along a pullback-stable class of [[display morphisms]].

A discussion of [[dependent type theory]] as the [[internal language]] of [[locally cartesian closed categories]] is in

\begin{itemize}%
\item R. A. G. Seely, \emph{Locally cartesian closed categories and type theory}, Math. Proc. Camb. Phil. Soc. (1984) 95 (\href{http://www.math.mcgill.ca/rags/LCCC/LCCC.pdf}{pdf})

\end{itemize}
The observation that the poset of open subsets of a topological space serve as a model for [[intuitionistic logic]] is apparently originally due to

\begin{itemize}%
\item [[Alfred Tarski]], \emph{Der Aussagenkalk\"u{}l und die Topologie}, Fundamenta Mathemeticae 31 (1938), pp. 103--134.

\end{itemize}
\hypertarget{Applications}{}\subsubsection*{{Applications}}\label{Applications}

Discussion of fundamental constructions of [[algebraic geometry]] from the perspective of the internal logic of the [[sheaf topos]] over a [[scheme]] ([[Zariski topos]], [[etale topos]]) is in

\begin{itemize}%
\item [[Ingo Blechschmidt]], \emph{Using the internal language of toposes in algebraic geometry}, talk at \href{https://indico.math.cnrs.fr/event/747/}{Toposes at IHES}, November 2015 (\href{https://github.com/iblech/internal-methods/blob/master/slides-ihes2015.pdf}{pdf}, \href{https://www.youtube.com/watch?v=7S8--bIKaWQ}{recording})


\item [[Ingo Blechschmidt]], \emph{Using the internal language of toposes in algebraic geometry}, thesis (\href{http://rawgit.com/iblech/internal-methods/master/notes.pdf}{pdf})


\item [[Ingo Blechschmidt]], \emph{Internal methods} \href{https://github.com/iblech/internal-methods}{github repository}



\end{itemize}
[[!redirects internal logic]] [[!redirects internal logics]] [[!redirects internal language]] [[!redirects internal languages]]



\end{document}