\documentclass[12pt]{amsart}
\usepackage{amsmath, amsthm, amssymb, amsfonts}
\usepackage{enumerate}
\usepackage{graphicx}
\usepackage{verbatim}
%\numberwithin{equation}{section}

%%%Document Configuration
\pagestyle{headings}
%\addtolength{\topmargin}{-.5in}
\textwidth = 6in 
\oddsidemargin = .25in
\evensidemargin = .25in
\voffset = -1in
\textheight = 9.5 in
%\textwidth = 6in
%\parindent = 0in
%\headsep = 0in
\relpenalty = 9999
\binoppenalty = 9999
%linespacing
\renewcommand{\baselinestretch}{1.25}
\reversemarginpar
%%%

%%%Theorem Configuration
\theoremstyle{plain}
\newtheorem{thm}{Theorem}[section]
\newtheorem{cor}[thm]{Corollary}
\newtheorem{dfn}{Definition}[section]
\newtheorem{exer}[thm]{Exercise}
\newtheorem{ex}[thm]{Example}
\newtheorem{fact}[thm]{Fact}
\newtheorem{hw}[section]{}
\newtheorem{lem}[thm]{Lemma}
\newtheorem*{main}{Main~Theorem}
\newtheorem{prop}[thm]{Proposition}
\newtheorem{remark}[thm]{Remark}
%\newtheorem{hw}[section]{HW}
%%%

%%%Bibliography Configuration
\bibliographystyle{plain}
%%%

%%%semantic definitions
\DeclareMathOperator*{\acl}{acl}
\DeclareMathOperator*{\Aut}{Aut}
\DeclareMathOperator*{\Dom}{Dom}
\DeclareMathOperator*{\Mod}{Mod}
\DeclareMathOperator*{\Th}{Th}
\DeclareMathOperator*{\tp}{tp}
\renewcommand{\div}{\mid}
\renewcommand{\emptyset}{\varnothing}
\renewcommand{\implies}{\Rightarrow}
\renewcommand{\natural}{\mathbb{N}}
\newcommand{\Acl}[1]{\obar{#1}}
\newcommand{\assign}{\leftarrow}
\newcommand{\caseif}{\Rightarrow}
\newcommand{\caseonlyif}{\Leftarrow}
\newcommand{\cantprove}{\nvdash}
\newcommand{\complex}{\mathbb{C}}
\newcommand{\field}{\mathbb{F}}
\newcommand{\minus}{\setminus}
\newcommand{\power}[1]{{\mathcal{P}}({#1})}
\newcommand{\nonnegative}{\mathbb{N}}
\newcommand{\integer}{\mathbb{Z}}
\newcommand{\intersect}{\cap}
\newcommand{\isomorphic}{\simeq}
\newcommand{\obar}[1]{\overline{#1}}
\newcommand{\proves}{\vdash}
\newcommand{\rational}{\mathbb{Q}}
\newcommand{\real}{\mathbb{R}}
\newcommand{\union}{\cup}
\newcommand{\units}[1]{{\left(#1\right)}^{\times}}
%%%

%%%local definitions
\newcommand{\eleq}{\equiv}
\newcommand{\elleq}{\preccurlyeq}
\newcommand{\lang}[1]{{\mathcal{#1}}}
\newcommand{\Los}{{\L o\'s}}
\newcommand{\LS}{{L\"{o}wenheim-Skolem }}
\newcommand{\mathscr}[1]{{\mathcal{#1}}}
\newcommand{\st}[1]{{\mathcal{#1}}}
\newcommand{\structure}[1]{{\mathcal{#1}}}
\newcommand{\struct}[1]{\left\langle#1\right\rangle}
\newcommand{\subst}{\preceq}
\newcommand{\symAnd}{\mathop{\bigwedge}}
\newcommand{\symand}{\wedge}
\newcommand{\symimply}{\rightarrow}
\newcommand{\symiff}{\leftrightarrow}
\newcommand{\symnot}{\neg}
\newcommand{\symor}{\vee}
\newcommand{\tuple}[1]{\obar{#1}}
\newcommand{\WFF}{well-formed formula}
\newcommand{\0}{\textbf{0}}
\newcommand{\suc}{\textbf{S}}
\newcommand{\A}{\mathfrak{A}}
\newcommand{\B}{\mathfrak{B}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\NNN}{\mathfrak{N}}
\newcommand{\E}{\textbf{E}}
\newcommand{\Cn}{\textrm{Cn}}
\newcommand{\res}{\upharpoonright}


%figures
\newcommand{\graph}{\fbox{\includegraphics{graph.pdf}}}
\newcommand{\tzero}{\parbox{17px}{\raisebox{-4px}{\includegraphics{t0.pdf}}}}
\newcommand{\tone}{\parbox{17px}{\raisebox{-4px}{\includegraphics{t1.pdf}}}}
\newcommand{\ttwo}{\parbox{17px}{\raisebox{-4px}{\includegraphics{t2.pdf}}}}
\newcommand{\tthree}{\parbox{19px}{\raisebox{-4px}{\includegraphics{t3.pdf}}}}
\newcommand{\tfour}{\parbox{19px}{\raisebox{-4px}{\includegraphics{t4.pdf}}}}
\newcommand{\tfive}{\parbox{19px}{\raisebox{-4px}{\includegraphics{t5.pdf}}}}
\newcommand{\tphi}{\parbox{17px}{\raisebox{-4px}{\includegraphics{phi.pdf}}}}
\newcommand{\tpsi}{\parbox{19px}{\raisebox{-4px}{\includegraphics{psi.pdf}}}}
\newcommand{\tbigphi}{
\fboxsep 0px
\fboxrule 0px
\fbox{\includegraphics{bigphi.pdf}}
\framebox[-100px][c]{\raisebox{98px}{
$a$
}}
\framebox[-70px][c]{\raisebox{50px}{
$x_1^{a,b}$
}}
\framebox[-10px][c]{\raisebox{13px}{
$x_3^{a,b}$
}}
\framebox[-176px][c]{\raisebox{13px}{
$x_2^{a,b}$
}}
}
\newcommand{\tbigpsi}{
\fboxsep 0px
\fboxrule 0px
{\fbox{\includegraphics{bigpsi.pdf}}}
\framebox[-100px][c]{\raisebox{54px}{
$y^{a,b}_2$
}}
\framebox[-150px][c]{\raisebox{34px}{
$y^{a,b}_1$
}}
\framebox[-100px][c]{\raisebox{10px}{
$y^{a,b}_3$
}}
\framebox[-184px][c]{\raisebox{13px}{
$a$
}}
\framebox[-16px][c]{\raisebox{13px}{
$b$
}}
}
%%%

\begin{document}

\title{Interpretability}
\author{Dakota Blair}
\maketitle

\begin{dfn}[Interpretation]
Let $L$ and $K$ be languages.
Let $\st{M}$ be an $L$-structure and $\st{N}$ be a $K$-structure.
If $\st{M}^*$ is an $L^*$-structure, where $K \subset L^*$ such that
there is a map ${\cdot~}^* : L \to L^*$ such that
$\st{M} \models \varphi \iff \st{M}^* \models \varphi^*$
then $\st{M}^*$ and every structure isomorphic to it is an
\textbf{interpretation} of $\st{M}$ in $\st{N}$.
\end{dfn}

\begin{remark}
By the interpretation lemma, to define the map ${\cdot}^*$ it suffices to show that
every constant, function and relation of $L$ is definable in $K$.
\end{remark}

\begin{ex}
Interpreting $\complex = (\complex, 0, 1, +, -, \cdot)$ in $\real$ as a
$(\real, 0, 1, +, -, \cdot)$ structure.
\end{ex}

Given $x \in \real$ denote by $x^{-1}$ the unique real number $y$
such that $xy = 1$.
Note that addition ($+(z,u,v)$), $0$, multiplication ($\cdot(z,u,v)$), $1$
and inverses are definable,
in particular, if $0^* = (0,0)$ and $1^* = (1,0)$ then
\begin{align*}
+(z,u,v) & \mathop{\longmapsto}^*
\varsigma(x,y,a,b,c,d) \iff (x = a + c) \symand (y = b + d)\\ 
\cdot(z,u,v) & \mathop{\longmapsto}^*
\mu(x,y,a,b,c,d) \iff (x = ac-bd) \symand (y = ad + bc)\\
\exists^{=1} z' (zz' = 1) & \mathop{\longmapsto}^*
\iota(x,y,a,b) \iff \exists^{=1}xy(x = a(aa+bb)^{-1}) \symand (y = -b(aa+bb)^{-1}).\\
\end{align*}
We therefore may use the following abbreviations for these operations,
understanding $(a, b)$ to be $a+bi$:
\begin{align*}
(a,b) + (c,d) & = (a + c , b + d)\\
(a,b)(c,d) & = (ac - bd , ad + bc)\\% = (x,y)
(a,b)^{-1} & = (a(aa+bb)^{-1} , -b(aa+bb)^{-1}).\\% = (x,y)
\end{align*}

\begin{ex}
Interpreting linear orders in graphs as $\{R\}$-structures.
\end{ex}

Let $\tpsi(x,y,u,v,w)$
be the formula asserting that $x, y, u, v$ and $w$ are distinct,
there are edges $(x,u), (u,v), (u,w)$ and $(v,y)$
and these are the only edges involving vertices $u, v$ and $w$.
Define $\tphi(x,y,u,v)$ in a similar fashion.
Now define $\tzero(z)$ as $\exists uvw \tphi(z,u,v,w)$
and $\tone(z), \ttwo(z), \tthree(z), \tfour(z), \tfive(z)$ analagously.
Finally, let $S = \{ \tzero, \tone, \ttwo, \tthree, \tfour, \tfive \}$.

If $(A, <)$ is a linear order
then define a graph $G_A$ such that for each $(a, b) \in A^2$
\[
\tbigphi
\raisebox{50px}{ and (if $a < b$) \hspace{1pc}}
%\raisebox{25px}{\fboxsep 0px 
\tbigpsi
%}
\]
are subgraphs of $G_A$.
Further construct $G_A$ so that these are the only edges which involve any
$x^a_i$ or $y^{a,b}_i$.

\begin{lem}
If $(A, <)$ is a linear order then for all verticies $x \in G_A$
there is exactly one $\varphi(x) \in S$ such that $G_A \models \varphi(x)$.
\end{lem}

Let $T$ be the theory in the language of graphs with the following axioms:
\begin{enumerate}
\item $R$ is symmetric and irreflexive
\item Exactly one $\varphi \in S$ is true for every $x$.
\item If $\tzero(x)$ and $\tzero(y)$ then $\symnot R(x,y)$.
\item If $\exists uvw \tpsi(x,y,u,v,w)$
      then $\forall u_1 v_1 w_1 \symnot \tpsi(y,x,u_1,v_1,w_1)$.
\item If $\exists uvw \tpsi(x,y,u,v,w)$
       and $\exists u_1 v_1 w_1 \tpsi(y,z,u_1,v_1,w_1)$ \\
      then $\exists u_2 v_2 w_2 \tpsi(x,z,u_2,v_2,w_2)$.
\item If $\tzero(x)$ and $\tzero(y)$ then either $x = y$,\\
       $\exists uvw \tpsi(x,y,u,v,w)$
       or $\exists uvw \tpsi(y,x,u,v,w)$
\item If $\tphi(x,u,v,w) \symand \tphi(x,u_1,v_1,w_1)$
      then $u = u_1$ and
       $v = v_1 \symand w = w_1$ or $v = w_1 \symand w = v_1$.
\item If $\tpsi(x,y,u,v,w) \symand \tpsi(x,y,u_1,v_1,w_1)$
      then $u = u_1, v = v_1$ and $w = w_1$.
\end{enumerate}

\begin{remark}
If $(A, <)$ is a linear order then $G_A \models T$.
\end{remark}

\begin{remark}
We may also interpret other common order-related axioms in this language.
Using the interpretation map above we see that density
($\forall xy (x < y)  \symimply \exists z (x<z \symand z<y)$)
becomes:
\begin{align*}
& \forall xy \tzero(x) \symand \tzero(y) \symand \exists uvw \tpsi (x,y,u,v,w) \symimply\\
& \hspace{1 in}
  \exists z \tzero(z) \symand\\
& \hspace{1 in}
  \exists u_x v_x w_x \tthree(u_x) \symand \tfour(v_x) \symand \tfive(w_x)
   \symand \tpsi (x,z,u_x,v_x,w_x) \symand\\
& \hspace{1 in}
  \exists u_y v_y w_y \tthree(u_y) \symand \tfour(v_y) \symand \tfive(w_y)
   \symand \tpsi (z,y,u_y,v_y,w_y).
\end{align*}
\end{remark}
\end{document}
\begin{comment}
%field axioms
Now we may list the field axioms and their interpretations:
\begin{align}
\tag{$0 \neq 1$}
(0, 0) \neq (1, 0)\\
\tag{$\forall z (0 + z = z)$}
\forall ab (0,0) + (a,b) = (a,b) \\
\tag{$\forall z (1z = z)$}
\forall ab (1,0)(a,b) = (a,b)\\
\tag{$\forall z (-z + z = 0)$}
\forall ab (-a,-b) + (a,b) = (0,0) \\
\tag{$\forall z\exists z^{-1} (z \neq 0 \symimply zz^{-1} = 1)$}
\forall ab \exists a^{-1},b^{-1}(a + b) \neq (0, 0) \symimply (a,b)(a, b)^{-1} = (1,0)\\
\tag{$\forall zw(z + w = w+ z)$}
\forall abcd (a, b) + (c,d) = (c,d) + (a,b)\\
\tag{$\forall zw(zw = wz)$}
\forall abcd (a,b)(c,d) = (c,d)(a,b)\\
\tag{$\forall zwv((z+w)+v = z+(w+v))$}
 \forall abcdef ((a,b) + (c,d)) + (e,f) = (a,b) + ((c,d) + (e,f))\\
\tag{$\forall zwv((zw)v = z(wv))$}
\forall abcdef ((a,b)(c,d))(e,f) = (a,b)((c,d)(e,f))\\
\tag{$\forall zwv(z(w + v) = zw + zv))$}
 \forall abcdef (a,b)((c,d) + (e,f)) = (a,b)(c,d) + (a,b)(e,f)
\end{align}
\end{comment}
