\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*{signature (in logic)}

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

\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{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{types}{Types}\dotfill \pageref*{types} \linebreak
\noindent\hyperlink{models}{Models}\dotfill \pageref*{models} \linebreak
\noindent\hyperlink{theories}{Theories}\dotfill \pageref*{theories} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{remarks}{Remarks}\dotfill \pageref*{remarks} \linebreak
\noindent\hyperlink{the_language_of_a_signature}{The language of a signature}\dotfill \pageref*{the_language_of_a_signature} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

In [[logic]], a \textbf{signature} is a collection of data which prescribes the `alphabet' of non-logical symbols of a logical [[theory]], saying which operations and [[predicates]] are taken to be primitive.

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

\hypertarget{types}{}\subsubsection*{{Types}}\label{types}

Formally, a \textbf{signature} $\Sigma$ consists of

\begin{itemize}%
\item A set $S$ whose elements are called \textbf{sorts} or \textbf{[[types]]} of $\Sigma$,


\item A set $Rel(\Sigma)$ whose elements are called \textbf{relation symbols}, equipped with a function $ar: Rel(\Sigma) \to S^*$ to the [[free monoid]] on $S$ which prescribes an \textbf{arity} for each relation symbol,


\item A set $Func(\Sigma)$ whose elements are called \textbf{function symbols}, equipped with a function

\begin{displaymath}
\langle dom, cod \rangle: Func(\Sigma) \to S^* \times S
\end{displaymath}
which prescribes an arity or type for each function symbol. A function symbol $f$ may be written as $dom(f) \to cod(f)$, or as $d_0(f) \to d_1(f)$, to indicate its arity.



\end{itemize}
The majority of (but far from all) mathematical concepts are described by means of a \textbf{single-sorted} signature, where $S$ consists of a single element $X$. Examples where multisorted signatures are used is the theory of [[categories]] (with an [[object]] sort and a [[morphism]] sort) and [[quiver|(multi)directed graphs]] (with a vertex sort and an edge sort). But in the single-sorted or one-sorted case, the free monoid on the one-sort set is isomorphic to $\mathbb{N}$, and the arity of a relation is a number $n$. Hence we speak of an $n$-ary relation (unary, binary, etc.). Similarly, the arity of a function symbol or operation $f$ is the number $n$ which indexes $dom(f)$ (hence we speak of unary operations, binary operations, etc.) In either the single-sorted or multisorted case, a 0-ary operation (where the domain empty) is usually called a \textbf{constant}.

A \textbf{relational} signature is where $Func(\Sigma)$ is empty, and an \textbf{equational} or \textbf{algebraic} signature is where $Rel(\Sigma)$ is empty. (In the latter case, the only relation symbol is the equality symbol, but this is typically considered a logical symbol.) Occasionally one allows a relational signature to have constants.

\hypertarget{models}{}\subsubsection*{{Models}}\label{models}

A ([[set theory|set-theoretic]]) \textbf{model} or \textbf{interpretation} $M$ of a signature consists of functions which assign

\begin{itemize}%
\item To each sort $s$ a [[set]] $M(s)$,


\item To each relation symbol $R$ of arity $\langle s_1, \ldots, s_n \rangle$ a [[subset]] $M(R) \hookrightarrow M(s_1) \times \ldots \times M(s_n)$,


\item To each function symbol $f$ of type $\langle s_1, \ldots, s_n \rangle \to s$ a [[function]] $M(f): M(s_1) \times \ldots \times M(s_n) \to M(s)$. Such a function is called an \textbf{operation} (that interprets $f$). In the case of constants of type $s$, the empty product on the left is taken to be a terminal or 1-element set $1$, whose element needs no name but is often given a generic name like `$*$'.



\end{itemize}
More generally a signature may be interpreted in other [[category|categories]] $C$ besides [[Set]]; for this it is reasonable to suppose that $C$ is at least a [[regular category]]. See also

\begin{itemize}%
\item [[categorical semantics]].

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

In terms of a signature one may formulate [[proposition]]s, [[sequents]] and then [[theories]]. See there for more details.

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

An important point to bear in mind is that \emph{essentially} the same theories (where `same' means that the categories of models are equivalent or even isomorphic) may have very different signatures. For example,

\begin{itemize}%
\item The theory of [[group]]s is usually described as a single-sorted theory whose signature has one binary operation (called `multiplication') $m$, one constant $e$ (called `identity'), and one unary operation (called `inversion') $i$. But it can also be described using a signature with just one (binary) operation $m$; there one adds in extra axioms which posit the existence of an identity and of inverse elements. Or, it can be described using a signature with a single (binary) operation $d$ (for `division'). All these are examples of equational signatures.


\item A [[Boolean ring]] is usually described as a commutative ring with identity in which multiplication is idempotent, hence the theory of Boolean rings is usually presented using the signature normally reserved for rings (with identity). A [[Boolean algebra]] may be described using a variety of signatures, for example non-equationally, involving a binary relation $\leq$ and function symbols $\wedge$, $\neg$, $\top$.


\item The theory ZFC is usually described using a single-sorted relational signature with one binary relation $\in$. However, other approaches are possible: one can also describe ZFC with a relational symbol $\subseteq$ together with a unary function symbol $sing$ (to be interpreted as taking a `set' $S$, i.e., an element of a ZFC structure, to a singleton `set' $\{S\}$).



\end{itemize}
\hypertarget{remarks}{}\subsection*{{Remarks}}\label{remarks}

The multiplicity of ways in which one can describe essentially the same class of objects is a phenomenon which in higher category theory is often referred to as [[bias]]. Often one desires to use an `unbiased' approach which includes different signatures under one roof and on the same footing. In the case of algebraic (equational) theories, this can be done using the device of [[clone]]s or [[Lawvere theory|Lawvere theories]], which does not single out certain non-logical operations as `privileged'.

There are several reasons though why one might prefer to retain some bias, for example:

\begin{itemize}%
\item Tradition, familiarity, thus ease of reference. For example, a group \emph{is} a set equipped with a binary $m$, an unary $i$, and a constant $e$, rather than a set equipped with a single division operation, or a finite product-preserving functor for that matter.


\item Mathematical intuition. That is, different signatures may invoke different intuitions or attitudes toward a subject; for example, ``Boolean rings'' may invoke a more algebraic or algebro-geometric attitude (as in [[Stone duality]]) whereas ``Boolean algebras'' may invoke a more logical attitude (propositional logic).


\item Differences in logical strength. That is, first-order logic should be thought of as coming in layers, ranging from equational logic up to [[pretopos]] logic, and different signatures may need differing levels of logical strength for them to be interpreted as intended. Equational logic may be preferred on occasion because it is a very weak logic, whereas relational signatures often require at least the strength of regular categories for them to be interpreted correctly.



\end{itemize}
\hypertarget{the_language_of_a_signature}{}\subsection*{{The language of a signature}}\label{the_language_of_a_signature}

Each signature $\Sigma$ generates a language whose elements are first-order predicates: expressions formed by using an alphabet of logical symbols together with $\Sigma$, considered as an alphabet of non-logical symbols, according to certain rules. For an account of the traditional logical syntax, see \href{https://en.wikipedia.org/wiki/First-order_logic#Syntax}{Wikipedia}.

First-order languages can also be structured categorically through the notion of [[hyperdoctrine]]. The base of the hyperdoctrine is a [[cartesian monoidal category]] $\mathbf{Term}(\Sigma)$ consisting of sorts and terms, or rather, the objects are formal (cartesian) products of sorts, written as finite lists, and the morphisms are tuples of terms generated by the function symbols of the signature. A detailed categorical description of $\mathbf{Term}(\Sigma)$ may be found \href{https://ncatlab.org/nlab/show/free%20cartesian%20category#free_cartesian_category_on_a_signature}{here}.

Given the base $\mathbf{Term}(\Sigma)$, the language itself is structured as a certain Boolean hyperdoctrine, i.e., a functor

\begin{displaymath}
Lang(\Sigma): \mathbf{Term}(\Sigma)^{op} \to Bool
\end{displaymath}
where for each morphism $f$ in the base, the morphism $f^\ast = Lang(\Sigma)(f)$ has a left adjoint $\exists_f$ and a right adjoint $\forall_f$, subject to a Beck-Chevalley condition for each pullback square in the base. To describe it with more traditional logical terminology: the functor takes each object (i.e., product of sorts) $w = s_1 s_2 \ldots s_n$ to the Boolean algebra $Pred(w)$ of predicates of arity $w$ that built up from the formal relations of the signature using first-order logic operations. The sorts $s_i$ appearing in the arity are matched bijectively with the free variables of the predicate, and are the types of those variables. Then, the functor takes each morphism $f: v \to w$, given by an $n$-tuple of terms $\tau_i: v \to s_i$, to the Boolean algebra map $f^\ast: Pred(w) \to Pred(v)$ obtained by substituting, in predicates of arity $w$, the term $\tau_i$ for the free variable $x_i$ that is matched with $s_i$, resulting in a predicate of arity $v$.

A more precise categorical description of $Lang(\Sigma)$, in terms of a universal property, is as follows. Let $S^\ast$ denote the underlying set of free monoid generated by the set of sorts $S$; regard $S^\ast$ as a discrete category. The formal relations of the signature give a functor

\begin{displaymath}
i: S^\ast \to Set
\end{displaymath}
sending each product $w = s_1 \ldots s_n$ to the set of relations $R \in Rel(\Sigma)$ that have arity $w$. Let $j: S^\ast \to \mathbf{Term}(\Sigma)$ be the obvious inclusion functor (the identity on objects). Define an \emph{interpretation} of $\Sigma$ to be a pair consisting of a Boolean hyperdoctrine $M: \mathbf{Term}(\Sigma)^{op} \to Bool$ together with a natural transformation $\phi: i \to U M j$:

\begin{displaymath}
\itexarray{
S^\ast & \stackrel{i}{\to} & Set \\ 
\mathllap{j} \downarrow & \Downarrow \mathrlap{\phi} & \uparrow \mathrlap{U} \\ 
\mathbf{Term}(\Sigma)^{op} & \underset{M}{\to} & Bool
}
\end{displaymath}
where $U: Bool \to Set$ is the underlying set functor. There is an obvious notion of morphism between interpretations $(M, \phi) \to (M', \phi')$, given by a natural transformation $M \Rightarrow M'$ compatible with the data $\phi, \phi'$.

\begin{defn}
\label{}\hypertarget{}{}
The \emph{language} $Lang(\Sigma)$ is the initial object in the category of interpretations of $\Sigma$.

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

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

\end{itemize}
[[!redirects signatures in logic]] [[!redirects signature in logic]]

[[!redirects relation symbol]] [[!redirects function symbol]] [[!redirects relation symbols]] [[!redirects function symbols]]



\end{document}