Model theory

Models of Arithmetic

content/model-theory/models-of-arithmetic/models-of-arithmetic.tex

% Part: model-theory% Chapter: models-of-arithmetic\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{mod}{mar}{Models of Arithmetic}\olimport{introduction}\olimport{standard-models}\olimport{non-standard-models}\olimport{models-of-q}\olimport{models-of-pa}\olimport{computable-models}\OLEndChapterHook\end{document}

content/model-theory/models-of-arithmetic/introduction.tex

% Part: model-theory% Chapter: models-of-arithmetic% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mod}{mar}{int}\section{Introduction}The \emph{standard model} of arithmetic is the!!{structure}~$\Struct{N}$ with $\Domain{N} = \Nat$ in which$\Obj{0}$, $\prime$, $+$, $\times$, and $<$ are interpreted as youwould expect. That is, $\Obj{0}$ is $0$, $\prime$ is the successorfunction, $+$ is interpreted as addition and $\times$ as multiplicationof the numbers in~$\Nat$. Specifically,\begin{align*}  \Assign{\Obj{0}}{N} & = 0\\  \Assign{\prime}{N}(n) & = n + 1\\  \Assign{+}{N}(n, m) & = n + m\\  \Assign{\times}{N}(n, m) & = nm\end{align*}Of course, there are structures for $\Lang{L_A}$ that have domainsother than~$\Nat$. For instance, we can take $\Struct{M}$ with domain$\Domain{M} = \{a\}^*$ (the finite sequences of the singlesymbol~$a$, i.e., $\emptyset$, $a$, $aa$, $aaa$, \dots), andinterpretations\begin{align*}  \Assign{\Obj{0}}{M} & = \emptyset\\  \Assign{\prime}{M}(s) & = s \concat a\\  \Assign{+}{M}(n, m) & = a^{n + m}\\  \Assign{\times}{M}(n, m) & = a^{nm}\end{align*}These two structures are ``essentially the same'' in the sense thatthe only difference is the !!{element}s of the !!{domain}s but not howthe !!{element}s of the !!{domain}s are related among each other bythe interpretation functions. We say that the two !!{structure}s are\emph{isomorphic}.It is an easy consequence of the compactness theorem that any theorytrue in~$\Struct{N}$ also has models that are not isomorphicto~$\Struct{N}$.  Such structures are called \emph{non-standard}.  Theinteresting thing about them is that while the !!{element}s of astandard model (i.e., $\Struct{N}$, but also all !!{structure}sisomorphic to it) are exhausted by the values of the standardnumerals~$\num{n}$, i.e.,\[\Domain{N} = \Setabs{\Value{\num{n}}{N}}{n \in \Nat}\]that isn't the case in non-standard models: if $\Struct{M}$ isnon-standard, then there is at least one $x \in \Domain{M}$ such that$x \neq \Value{\num{n}}{M}$ for all~$n$.These non-standard elements are pretty neat: they are ``infinitenatural numbers.'' But their existence also explains, in a sense, theincompleteness phenomena.  Consider an example, e.g., the consistencystatement for Peano arithmetic, $\OCon[\Th{PA}]$, i.e., $\lnot\lexists[x][\OPrf[\Th{PA}](x, \gn{\lfalse})]$. Since $\Th{PA}$ neitherproves $\OCon[\Th{PA}]$ nor $\lnot \OCon[\Th{PA}]$, either can beconsistently added to $\Th{PA}$. Since $\Th{PA}$ is consistent,$\Sat{N}{\OCon[\Th{PA}]}$, and consequently $\Sat/{N}{\lnot  \OCon[\Th{PA}]}$.  So $\Struct{N}$ is \emph{not} a model of $\Th{PA}\cup \{\lnot \OCon[\Th{PA}]\}$, and all its models must benonstandard. Models of $\Th{PA} \cup \{\lnot \OCon[\Th{PA}]\}$ mustcontain some !!{element} that serves as the witness that makes$\lexists[x][\OPrf[\Th{PA}](\gn{\lfalse})]$ true, i.e., a G\"odelnumber of !!a{derivation} of a contradiction from~$\Th{PA}$.  Such!!a{element} can't be standard---since $\Th{PA} \Proves \lnot\OPrf[\Th{PA}](\num{n}, \gn{\lfalse})$ for every~$n$.\end{document}

content/model-theory/models-of-arithmetic/standard-models.tex

% Part: model-theory% Chapter: models-of-arithmetic% Section: standard-models\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mod}{mar}{stm}\olsection{Standard Models of Arithmetic}The language of arithmetic~$\Lang{L_A}$ is obviously intended to beabout numbers, specifically, about natural numbers. So, ``the''standard model~$\Struct{N}$ is special: it is the model we want totalk about. But in logic, we are often just interested in structuralproperties, and any two !!{structure}s that are isomorphic sharethose.  So we can be a bit more liberal, and consider any!!{structure} that is isomorphic to~$\Struct{N}$ ``standard.''\begin{defn}A !!{structure} for $\Lang{L_A}$ is \emph{standard} if it isisomorphic to~$\Struct{N}$.\end{defn}\begin{prop}\ollabel{prop:standard-domain} If !!a{structure}~$\Struct{M}$ is standard,then its domain is the set of values of the standard numerals, i.e.,\[\Domain{M} = \Setabs{\Value{\num{n}}{M}}{n \in \Nat}\]\end{prop}\begin{proof}Clearly, every $\Value{\num{n}}{M} \in \Domain{M}$. We just have toshow that every $x \in \Domain{M}$ is equal to $\Value{\num{n}}{M}$for some~$n$.  Since $\Struct{M}$ is standard, it is isomorphicto~$\Struct{N}$. Suppose $g\colon \Nat \to \Domain{M}$ is anisomorphism. Then $g(n) = g(\Value{\num{n}}{N}) =\Value{\num{n}}{M}$. But for every $x \in \Domain{M}$, there is an~$n\in \Nat$ such that $g(n) = x$, since $g$ is !!{surjective}.\end{proof}\begin{explain}If a structure~$\Struct{M}$ for $\Lang{L_A}$ is standard, the elementsof its !!{domain} can all be named by the standard numerals $\num{0}$,$\num{1}$, $\num{2}$, \dots, i.e., the terms $\Obj{0}$, $\Obj{0}'$,$\Obj{0}''$, etc. Of course, this does not mean that the !!{element}sof $\Domain{M}$ \emph{are} the numbers, just that we can pick them outthe same way we can pick out the numbers in~$\Domain{N}$.\end{explain}\begin{prob}Show that the converse of \olref[mod][mar][stm]{prop:standard-domain}is false, i.e., give an example of !!a{structure}~$\Struct{M}$ with$\Domain{M} = \Setabs{\Value{\num{n}}{M}}{n \in \Nat}$ that is notisomorphic to~$\Struct{N}$.\end{prob}\begin{prop}\ollabel{prop:thq-standard}If $\Sat{M}{\Th{Q}}$, and $\Domain{M} = \Setabs{\Value{\num{n}}{M}}{n  \in \Nat}$, then $\Struct{M}$ is standard.\end{prop}\begin{proof}We have to show that $\Struct{M}$ is isomorphicto~$\Struct{N}$. Consider the function $g\colon \Nat \to \Domain{M}$defined by $g(n) = \Value{\num{n}}{M}$. By the hypothesis, $g$ is!!{surjective}.  It is also !!{injective}: $\Th{Q} \Proves\eq/[\num{n}][\num{m}]$ whenever $n \neq m$. Thus, since$\Sat{M}{\Th{Q}}$, $\Sat{M}{\eq/[\num{n}][\num{m}]}$, whenever $n \neqm$. Thus, if $n \neq m$, then $\Value{\num{n}}{M} \neq\Value{\num{m}}{M}$, i.e., $g(n) \neq g(m)$.We also have to verify that $g$ is an isomorphism.\begin{enumerate}\item We have $g(\Assign{\Obj{0}}{N}) = g(0)$ since,  $\Assign{\Obj{0}}{N} = 0$. By definition of~$g$, $g(0) =  \Value{\num{0}}{M}$. But $\num{0}$ is just $\Obj{0}$, and the value  of a term which happens to be !!a{constant} is given by what the  !!{structure} assigns to that !!{constant}, i.e.,  $\Value{\Obj{0}}{M} = \Assign{\Obj{0}}{M}$. So we have  $g(\Assign{\Obj{0}}{N}) = \Assign{\Obj{0}}{M}$ as required.\item $g(\Assign{\prime}{N}(n)) = g(n+1)$, since $\prime$ in  $\Struct{N}$ is the successor function on~$\Nat$. Then, $g(n+1) =  \Value{\num{n+1}}{M}$ by definition of~$g$. But $\num{n+1}$ is the  same term as $\num{n}'$, so $\Value{\num{n+1}}{M} =  \Value{\num{n}'}{M}$. By the definition of the value function, this  is $= \Assign{\prime}{M}(\Value{\num{n}}{M})$. Since    $\Value{\num{n}}{M} = g(n)$ we get $g(\Assign{\prime}{N}(n)) =  \Assign{\prime}{M}(g(n))$.\item $g(\Assign{+}{N}(n,m)) = g(n+m)$, since $+$ in $\Struct{N}$ is  the addition function on~$\Nat$. Then, $g(n+m) =  \Value{\num{n+m}}{M}$ by definition of~$g$. But $\Th{Q} \Proves  \num{n+m} = (\num{n} + \num{m})$, so $\Value{\num{n+m}}{M} =  \Value{\num{n}+\num{m}}{M}$. By the definition of the value  function, this is $=  \Assign{+}{M}(\Value{\num{n}}{M},\Value{\num{m}}{M})$. Since    $\Value{\num{n}}{M} = g(n)$ and $\Value{\num{m}}{M} = g(m)$, we    get $g(\Assign{+}{N}(n, m)) = \Assign{+}{M}(g(n), g(m))$.\item $g(\Assign{\times}{N}(n, m)) = \Assign{\times}{M}(g(n), g(m))$:  Exercise.\item $\tuple{n,m} \in \Assign{<}{N}$ iff $n < m$. If $n < m$, then  $\Th{Q} \Proves \num{n} < \num{m}$, and also $\Sat{M}{\num{n} <  \num{m}}$. Thus $\tuple{\Value{\num{n}}{M}, \Value{\num{m}}{M}} \in  \Assign{<}{M}$, i.e., $\tuple{g(n), g(m)} \in \Assign{<}{M}$. If $n  \not< m$, then $\Th{Q} \Proves \lnot \num{n} < \num{m}$, and  consequently $\Sat/{M}{\num{n} < \num{m}}$. Thus, as before,  $\tuple{g(n), g(m)} \notin \Assign{<}{M}$. Together, we get:  $\tuple{n,m} \in \Assign{<}{N}$ iff $\tuple{g(n), g(m)} \in  \Assign{<}{M}$.\end{enumerate}\end{proof}\begin{explain}The function~$g$ is the most obvious way of defining a mapping from$\Nat$ to the domain of any other !!{structure}~$\Struct{M}$ for$\Lang{L_A}$, since every such $\Struct{M}$ contains !!{element}s namedby $\num{0}$, $\num{1}$, $\num{2}$, etc. So it isn't surprising thatif $\Struct{M}$ makes at least some basic statements about the$\num{n}$'s true in the same way that~$\Struct{N}$ does, and $g$ isalso bijective, then $g$ will turn into an isomorphism.  In fact, if$\Domain{M}$ contains no !!{element}s other than what the $\num{n}$'sname, it's the only one.\end{explain}\begin{prop}\ollabel{prop:thq-unique-iso} If $\Struct{M}$ is standard, then $g$ fromthe proof of \olref{prop:thq-standard} is the only isomorphism from $\Struct{N}$ to~$\Struct{M}$.\end{prop}\begin{proof}Suppose $h\colon \Nat \to \Domain{M}$ is an isomorphism between$\Struct{N}$ and~$\Struct{M}$. We show that $g = h$ by inductionon~$n$. If $n = 0$, then $g(0) = \Assign{\Obj{0}}{M}$ by definitionof~$g$. But since $h$ is an isomorphism, $h(0) =h(\Assign{\Obj{0}}{N}) =\Assign{\Obj{0}}{M}$, so $g(0) = h(0)$.Now consider the case for $n+1$. We have\begin{align*}  g(n+1) & = \Value{\num{n+1}}{M} \text{ by definition of~$g$}\\  & = \Value{\num{n}'}{M} \text{ since $\num{n+1}\ident \num{n}'$}\\  & = \Assign{\prime}{M}(\Value{\num{n}}{M})     \text{ by definition of $\Value{t'}{M}$}\\  & = \Assign{\prime}{M}(g(n))  \text{ by definition of~$g$}\\  & = \Assign{\prime}{M}(h(n)) \text{ by induction hypothesis}\\  & = h(\Assign{\prime}{N}(n)) \text{ since $h$ is an isomorphism}\\  & = h(n+1)\end{align*}\end{proof}\begin{explain}For any !!{denumerable} set~$M$, there's !!a{bijection} between$\Nat$ and $M$, so every such set~$M$ is potentially the !!{domain} ofa standard model~$\Struct{M}$. In fact, once you pick an object $z \inM$ and a suitable function $s$ as $\Assign{\Obj{0}}{M}$ and$\Assign{\prime}{M}$, the interpretations of $+$, $\times$, and $<$ isalready fixed.  Only functions~$s\colon M \to M \setminus \{z\}$ thatare both !!{injective} and !!{surjective} are suitable in a standardmodel as~$\Assign{\prime}{M}$.  The range of $s$ cannot contain~$z$,since otherwise $\lforall[x][\eq/[\Obj 0][x']]$ would be false. That!!{sentence} is true in~$\Struct{N}$, and so $\Struct{M}$ also has tomake it true. The function~$s$ has to be !!{injective}, since thesuccessor function~$\Assign{\prime}{N}$ in~$\Struct{N}$ is, and that$\Assign{\prime}{N}$ is !!{injective} is expressed by !!a{sentence}true in~$\Struct{N}$. It has to be !!{surjective} because otherwisethere would be some $x \in M \setminus \{z\}$ not in the domainof~$s$, i.e., the !!{sentence} $\lforall[x][(\eq[x][\Obj 0] \lor\lexists[y][\eq[y'][x]])]$ would be false in~$\Struct{M}$---but it istrue in~$\Struct{N}$.\end{explain}\end{document}

content/model-theory/models-of-arithmetic/non-standard-models.tex

% Part: model-theory% Chapter: models-of-arithmetic% Section: non-standard-models\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mod}{mar}{nst}\section{Non-Standard Models}\begin{explain}We call !!a{structure} for $\Lang{L_A}$ standard if it is isomorphicto~$\Struct{N}$. If !!a{structure} isn't isomorphic to~$\Struct{N}$,it is called non-standard.\end{explain}\begin{defn}A !!{structure}~$\Struct{M}$ for $\Lang{L_A}$ is \emph{non-standard}if it is not isomorphic to~$\Struct{N}$. The !!{element}s $x \in\Domain{M}$ which are equal to $\Value{\num{n}}{M}$ for some $n \in\Nat$ are called \emph{standard numbers} (of $\Struct{M}$), and thosenot, \emph{non-standard numbers}.\end{defn}\begin{explain}By \olref[stm]{prop:standard-domain}, any standard !!{structure}for~$\Lang{L_A}$ contains only standard !!{element}s. Consequently, anon-standard !!{structure} must contain at least one non-standardelement. In fact, the existence of a non-standard !!{element}guarantees that the !!{structure} is non-standard.\end{explain}\begin{prop}If !!a{structure}~$\Struct{M}$ for $\Lang{L_A}$ contains anon-standard number, $\Struct{M}$ is non-standard.\end{prop}\begin{proof}Suppose not, i.e., suppose $\Struct{M}$ standard but contains anon-standard number~$x$. Let $g\colon \Nat \to \Domain{M}$ be anisomorphism. It is easy to see (by induction on~$n$) that$g(\Value{\num{n}}{N}) = \Value{\num{n}}{M}$. In other words, $g$ mapsstandard numbers of~$\Struct{N}$ to standard numbersof~$\Struct{M}$. If $\Struct{M}$ contains a non-standard number, $g$cannot be !!{surjective}, contrary to hypothesis.\end{proof}\begin{prob}Recall that $\Th{Q}$ contains the axioms\begin{align*}& \lforall[x][\lforall[y][(\eq[x'][y'] \lif \eq[x][y])]] \tag{$!Q_1$}\\& \lforall[x][\eq/[\Obj 0][x']] \tag{$!Q_2$}\\& \lforall[x][(\eq[x][\Obj 0] \lor \lexists[y][\eq[x][y']])] \tag{$!Q_3$}\end{align*}Give !!{structure}s~$\Struct{M_1}$, $\Struct{M_2}$, $\Struct{M_3}$ such that\begin{enumerate}\item $\Sat{M_1}{!Q_1}$, $\Sat{M_1}{!Q_2}$, $\Sat/{M_1}{!Q_3}$;\item $\Sat{M_2}{!Q_1}$, $\Sat/{M_2}{!Q_2}$, $\Sat{M_2}{!Q_3}$; and\item $\Sat/{M_3}{!Q_1}$, $\Sat{M_3}{!Q_2}$, $\Sat{M_3}{!Q_3}$;\end{enumerate}Obviously, you just have to specify~$\Assign{\Obj{0}}{M_i}$ and$\Assign{\prime}{M_i}$ for each.\end{prob}\begin{explain}It is easy enough to specify non-standard !!{structure}s for$\Lang{L_A}$. For instance, take the structure with !!{domain}~$\Int$and interpret all non-logical symbols as usual. Since negative numbersare not values of $\num{n}$ for any~$n$, this structure isnon-standard. Of course, it will not be a \emph{model} of arithmeticin the sense that it makes the same sentences trueas~$\Struct{N}$. For instance, $\lforall[x][\eq/[x'][\Obj{0}]]$ isfalse.  However, we can prove that non-standard models of arithmeticexist easily enough, using the compactness theorem.\end{explain}\begin{prop}Let $\Th{TA} = \Setabs{!A}{\Sat{N}{!A}}$ be the theoryof~$\Struct{N}$. $\Th{TA}$ has !!a{enumerable} non-standard model.\end{prop}\begin{proof}Expand $\Lang{L_A}$ by a new !!{constant}~$c$ and consider the set of!!{sentence}s\[\Gamma = \Th{TA} \cup \{\eq/[c][\num{0}], \eq/[c][\num{1}],\eq/[c][\num{2}], \dots\}\]Any model~$\Struct{M^c}$ of~$\Gamma$ would contain !!a{element}~$x =\Assign{c}{M}$ which is non-standard, since $x \neq\Value{\num{n}}{M}$ for all $n \in \Nat$. Also, obviously,$\Sat{M^c}{\Th{TA}}$, since $\Th{TA} \subseteq \Gamma$. If we turn$\Struct{M^c}$ into !!a{structure}~$\Struct{M}$ for $\Lang{L_A}$simply by forgetting about~$c$, its domain still contains thenon-standard~$x$, and also~$\Sat{M}{\Th{TA}}$. The latter isguaranteed since $c$ does not occur in~$\Th{TA}$. So, it suffices toshow that $\Gamma$ has a model.We use the compactness theorem to show that~$\Gamma$ has a model. Ifevery finite subset of~$\Gamma$ is satisfiable, sois~$\Gamma$. Consider any finite subset $\Gamma_0 \subseteq\Gamma$. $\Gamma_0$ includes some !!{sentence}s of~$\Th{TA}$ and someof the form~$\eq/[c][\num{n}]$, but only finitely many. Suppose $k$ isthe largest number so that $\eq/[c][\num{k}] \in \Gamma_0$. Define$\Struct{N_k}$ by expanding~$\Struct{N}$ to include theinterpretation~$\Assign{c}{N_k} = k+1$. $\Sat{N_k}{\Gamma_0}$: if $!A\in \Th{TA}$, $\Sat{N_k}{!A}$ since $\Struct{N_k}$ is justlike~$\Struct{N}$ in all respects except~$c$, and $c$ does not occurin~$!A$. And $\Sat{N_k}{\eq/[c][\num{n}]}$, since $n \le k$, and$\Value{c}{N_k} = k+1$. Thus, every finite subset of~$\Gamma$ issatisfiable.\end{proof}\end{document}

content/model-theory/models-of-arithmetic/models-of-q.tex

% Part: model-theory% Chapter: models-of-arithmetic% Section: non-standard-models\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mod}{mar}{mdq}\section{Models of $\Th{Q}$}\begin{explain}We know that there are non-standard !!{structure}s that make the same!!{sentence}s true as~$\Struct{N}$ does, i.e., is a modelof~$\Th{TA}$. Since $\Sat{N}{\Th{Q}}$, any model of~$\Th{TA}$ is alsoa model of~$\Th{Q}$. $\Th{Q}$ is much weaker than~$\Th{TA}$, e.g.,$\Th{Q} \Proves/ \lforall[x][\lforall[y][\eq[(x +      y)][(y+x)]]]$. Weaker theories are easier to satisfy: they havemore models. E.g., $\Th{Q}$ has models which make$\lforall[x][\lforall[y][\eq[(x + y)][(y+x)]]]$ false, but thosecannot also be models of~$\Th{TA}$, or $\Th{PA}$ for that matter.Models of $\Th{Q}$ are also relatively simple: we can specify themexplicitly.\end{explain}\begin{ex}\ollabel{ex:model-K-of-Q}Consider the !!{structure}~$\Struct{K}$ with domain $\Domain{K} = \Nat\cup \{a\}$ and interpretations\begin{align*}  \Assign{\Obj{0}}{K} & = 0\\  \Assign{\prime}{K}(x) & =  \begin{cases}    x+1 & \text{if $x\in \Nat$}\\    a & \text{if $x = a$}  \end{cases}\\  \Assign{+}{K}(x, y) & =  \begin{cases}    x+y & \text{if $x$, $y \in\Nat$}\\    a & \text{otherwise}  \end{cases}\\  \Assign{\times}{K}(x, y) & =  \begin{cases}    xy & \text{if $x$, $y \in\Nat$}\\    0 & \text{if $x = 0$ or $y = 0$}\\    a & \text{otherwise}\\  \end{cases}\\  \Assign{<}{K} & =  \Setabs{\tuple{x,y}}{x, y \in \Nat \text{ and } x<y} \cup  \Setabs{\tuple{x,a}}{x \in \Domain{K}}\end{align*}To show that $\Sat{K}{\Th{Q}}$ we have to verify that all axiomsof~$\Th{Q}$ are true in~$\Struct{K}$.  For convenience, let's write$x^\nssucc$ for $\Assign{\prime}{K}(x)$ (the ``successor'' of $x$in~$\Struct{K}$), $x \nsplus y$ for $\Assign{+}{K}(x, y)$ (the ``sum''of $x$ and $y$ in~$\Struct{K}$, $x \nstimes y$ for$\Assign{\times}{K}(x, y)$ (the ``product'' of $x$ and~$y$in~$\Struct{K}$), and $x \nsless y$ for $\tuple{x,y} \in\Assign{<}{K}$. With these abbreviations, we can give the operationsin~$\Struct{K}$ more perspicuously as\[\begin{array}{c|c}  x & x^\nssucc \\  \hline  n & n+1 \\  a & a\end{array}\qquad\begin{array}{c|ccc}  x \nsplus y & 0 & m & a \\  \hline  0 & 0 & m & a \\  n & n & n+m & a \\  a & a & a & a \\\end{array}\qquad\begin{array}{c|ccc}  x \nstimes y & 0 & m & a \\  \hline  0 & 0 & 0 & 0 \\  n & 0 & nm & a \\  a & 0 & a & a \\\end{array}\]We have $n \nsless m$ iff $n<m$ for $n$, $m \in \Nat$ and $x \nslessa$ for all~$x \in \Domain{K}$.$\Sat{K}{\lforall[x][\lforall[y][(\eq[x'][y'] \lif \eq[x][y])]]}$since $\nssucc$ is !!{injective}. $\Sat{K}{\lforall[x][\eq/[\Obj0][x']]}$ since $0$~is not a $\nssucc$-successor in~$\Struct{K}$.$\Sat{K}{\lforall[x][(\eq[x][\Obj 0] \lor \lexists[y][\eq[x][y']])]}$since for every $n>0$, $n = (n-1)^\nssucc$, and $a = a^\nssucc$.$\Sat{K}{\lforall[x][\eq[(x + \Obj 0)][x]]}$ since $n \nsplus 0 = n+0= n$, and $a\nsplus 0 = a$ by definition of~$\nsplus$.$\Sat{K}{\lforall[x][\lforall[y][\eq[(x + y')][(x + y)']]]}$ is a bittrickier.  If $n$, $m$ are both standard, we have:\begin{align*}(n \nsplus m^\nssucc) & = (n+(m+1)) = (n+m)+1 = (n \nsplus m)^\nssucc  \intertext{since $\nsplus$ and $^\nssucc$ agree with $+$ and $\prime$ on  standard numbers.  Now suppose $x \in \Domain{K}$. Then}(x \nsplus a^\nssucc) & = (x \nsplus a) = a = a^\nssucc = (x \nsplus a)^\nssucc\intertext{The remaining case is if $y \in \Domain{K}$ but $x =  a$. Here we also have to distinguish cases according to whether $y =  n$ is standard or $y = b$:}(a \nsplus n^\nssucc) & = (a \nsplus (n+1)) = a = a^\nssucc = (a \nsplus n)^\nssucc\\(a \nsplus a^\nssucc) & = (a \nsplus a) = a = a^\nssucc = (a \nsplus a)^\nssucc\end{align*}This is of course a bit more detailed than needed. For instance, since$a \nsplus z = a$ whatever $z$ is, we can immediately conclude $a \nsplusa^\nssucc = a$. The remaining axioms can be verified the same way.$\Struct{K}$ is thus a model of~$\Th{Q}$. Its ``addition''~$\nsplus$is also commutative. But there are other sentences truein~$\Struct{N}$ but false in~$\Struct{K}$, and vice versa. Forinstance, $a \nsless a$, so $\Sat{K}{\lexists[x][x < x]}$ and$\Sat/{K}{\lforall[x][\lnot x<x]}$. This shows that $\Th{Q} \Proves/\lforall[x][\lnot x < x]$.\end{ex}\begin{prob}Prove that $\Struct{K}$ from \olref[mod][mar][mdq]{ex:model-K-of-Q}satisfies the remaining axioms of~$\Th{Q}$,\begin{align*}  & \lforall[x][\eq[(x \times \Obj 0)][\Obj 0]] \tag{$!Q_6$}\\  & \lforall[x][\lforall[y][\eq[(x \times y')][((x \times y) + x)]]] \tag{$!Q_7$}\\  & \lforall[x][\lforall[y][(x < y \liff \lexists[z][\eq[(z' + x)][y]])]] \tag{$!Q_8$}\end{align*}Find !!a{sentence} only involving~$\prime$ true in~$\Struct{N}$ butfalse in~$\Struct{K}$.\end{prob}\begin{ex}\ollabel{ex:model-L-of-Q} Consider the !!{structure}~$\Struct{L}$ withdomain $\Domain{L} = \Nat \cup \{a, b\}$ and interpretations$\Assign{\prime}{L} = \nssucc$, $\Assign{+}{L} = \nsplus$ given by\[\begin{array}{c|c}  x & x^\nssucc \\  \hline  n & n+1 \\  a & a\\  b & b\end{array}\qquad\begin{array}{c|ccc}  x \nsplus y & m & a & b\\  \hline  n & n+m & b & a\\  a & a & b & a\\  b & b & b & a\end{array}\]Since $\nssucc$ is !!{injective}, $0$ is not in its range, and every$x \in \Domain{L}$ other than~$0$ is, axioms $!Q_1$--$!Q_3$ are truein~$\Struct{L}$. For any $x$, $x \nsplus 0 = x$, so $!Q_4$ is true aswell.  For $!Q_5$, consider $x \nsplus y^\nssucc$ and $(x \nsplusy)^\nssucc$. They are equal if $x$ and $y$ are both standard, sincethen $\nssucc$ and $\nsplus$ agree with $\prime$ and $+$. If $x$ isnon-standard, and $y$ is standard, we have $x \nsplus y^\nssucc = x =x^\nssucc = (x \nsplus y)^\nssucc$. If $x$ and $y$ are bothnon-standard, we have four cases:\begin{align*}&  a \nsplus a^\nssucc  = b = b^\nssucc = (a \nsplus a)^\nssucc\\&  b \nsplus b^\nssucc  = a = a^\nssucc = (b \nsplus b)^\nssucc\\&  b \nsplus a^\nssucc  = b = b^\nssucc = (b \nsplus y)^\nssucc\\&  a \nsplus b^\nssucc  = a = a^\nssucc = (a \nsplus b)^\nssucc\\\intertext{If $x$ is standard, but $y$ is non-standard, we have}&  n \nsplus a^\nssucc  = n \nsplus a = b = b^\nssucc = (n \nsplus a)^\nssucc\\&  n \nsplus b^\nssucc  = n \nsplus b = a = a^\nssucc = (n \nsplus b)^\nssucc\end{align*}So, $\Sat{L}{!Q_5}$. However, $a \nsplus 0 \neq 0 \nsplus a$, so$\Sat/{L}{\lforall[x][\lforall[y][\eq[(x+y)][(y+x)]]]}$.\end{ex}\begin{prob}Expand $\Struct{L}$ of \olref[mod][mar][mdq]{ex:model-L-of-Q} toinclude $\nstimes$ and $\nsless$ that interpret~$\times$ and $<$. Showthat your structure satisfies the remaining axioms of~$\Th{Q}$,\begin{align*}& \lforall[x][\eq[(x \times \Obj 0)][\Obj 0]] \tag{$!Q_6$}\\ &  \lforall[x][\lforall[y][\eq[(x \times y')][((x \times y) + x)]]]  \tag{$!Q_7$}\\ & \lforall[x][\lforall[y][(x < y \liff \lexists[z][\eq[(z'+x)][y]])]] \tag{$!Q_8$}\end{align*}\end{prob}\begin{prob}In $\Struct{L}$ of \olref[mod][mar][mdq]{ex:model-L-of-Q}, $a^\nssucc= a$ and $b^\nssucc = b$. Is there a model of~$\Th{Q}$ in which$a^\nssucc = b$ and $b^\nssucc = a$?\end{prob}\begin{explain}We've explicitly constructed models of~$\Th{Q}$ in which thenon-standard !!{element}s live ``beyond'' the standard elements. Infact, that much is required by the axioms. A non-standard!!{element}~$x$ cannot be ${} \nsless 0$, since $\Th{Q} \Proves\lforall[x][\lnot x<0]$ (see \olref[inc][req][min]{lem:less-zero}).Also, for every $n$, $\Th{Q} \Proves \lforall[x][(x < \num{n}' \lif(\eq[x][\num{0}] \lor \eq[x][\num{1}] \lor \dots \lor\eq[x][\num{n}]))]$ (\olref[inc][req][min]{lem:less-nsucc}), so wecan't have $a \nsless n$ for any~$n>0$.\end{explain}\end{document}

content/model-theory/models-of-arithmetic/models-of-pa.tex

% Part: first-order-logic% Chapter: models-of-arithmetic% Section: models-of-pa\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mod}{mar}{mpa}\section{Models of $\Th{PA}$}\begin{explain}Any non-standard model of~$\Th{TA}$ is also one of~$\Th{PA}$. We knowthat non-standard models of~$\Th{TA}$ and hence of~$\Th{PA}$ exist. Wealso know that such non-standard models contain non-standard``numbers,'' i.e., !!{element}s of the domain that are ``beyond'' allthe standard ``numbers.''  But how are they arranged? How many arethere? We've seen that models of the weaker theory~$\Th{Q}$ cancontain as few as a single non-standard number. But these simple!!{structure}s are not models of $\Th{PA}$ or $\Th{TA}$.The key to understanding the structure of models of $\Th{PA}$ or$\Th{TA}$ is to see what facts are !!{derivable} in these theories.For instance, already $\Th{PA}$ proves that $\lforall[x][\eq/[x][x']]$and $\lforall[x][\lforall[y][\eq[(x+y)][(y+x)]]]$, so this rules outsimple structures (in which these !!{sentence}s are false) as modelsof~$\Th{PA}$.Suppose~$\Struct{M}$ is a model of~$\Th{PA}$. Then if $\Th{PA} \Proves!A$, $\Sat{M}{!A}$.  Let's again use $\nszero$ for$\Assign{\Obj{0}}{M}$, $\nssucc$ for $\Assign{\prime}{M}$, $\nsplus$for $\Assign{+}{M}$, $\nstimes$ for $\Assign{\times}{M}$, and$\nsless$ for $\Assign{<}{M}$. Any !!{sentence}~$!A$ then states somecondition about $\nszero$, $\nssucc$, $\nsplus$, $\nstimes$, and$\nsless$, and if $\Sat{M}{!A}$ that condition must be satisfied. Forinstance, if $\Sat{M}{!Q_1}$, i.e.,$\Sat{M}{\lforall[x][\lforall[y][(\eq[x'][y'] \lif \eq[x][y])]]}$,then $\nssucc$ must be !!{injective}.\end{explain}\begin{prop}In $\Struct{M}$, $\nsless$ is a linear strict order, i.e., itsatisfies:\begin{enumerate}\item Not $x \nsless x$ for any~$x \in \Domain{M}$.\item If $x \nsless y$ and $y \nsless z$ then $x \nsless z$.\item For any $x \neq y$, $x \nsless y$ or $y \nsless x$\end{enumerate}\end{prop}\begin{proof}$\Th{PA}$ proves:\begin{enumerate}\item $\lforall[x][\lnot x < x]$\item $\lforall[x][\lforall[y][\lforall[z][((x < y \land y < z) \lif x < z)]]]$\item $\lforall[x][\lforall[y][((x < y \lor y < x) \lor \eq[x][y]))]]$\end{enumerate}\end{proof}\begin{prop}\ollabel{prop:M-discrete} $\nszero$ is the least !!{element}of~$\Domain{M}$ in the $\nsless$-ordering. For any $x$, $x \nslessx^\nssucc$, and $x^\nssucc$ is the $\nsless$-least !!{element} withthat property.  For any $x$, there is a unique $y$ such that$y^\nssucc = x$. (We call $y$ the ``predecessor'' of~$x$in~$\Struct{M}$, and denote it by~$^\nssucc x$.)\end{prop}\begin{proof}Exercise.  \end{proof}\begin{prob}Find !!{sentence}s in~$\Lang{L_A}$ !!{derivable} in~$\Th{PA}$ (andhence true in~$\Struct{N}$) which guarantee the properties of$\nszero$, $\nssucc$, and $\nsless$ in\olref[mod][mar][mpa]{prop:M-discrete}\end{prob}\begin{prop}All standard !!{element}s of~$\Struct{M}$ are less than (accordingto~$\nsless$) all non-standard !!{element}s.\end{prop}\begin{proof}We'll use $n$ as short for $\Value{\num{n}}{M}$, a standard!!{element} of~$\Struct{M}$.  Already $\Th{Q}$ proves that, for any~$n\in \Nat$, $\lforall[x][(x < \num{n}' \lif (\eq[x][\num{0}] \lor  \eq[x][\num{1}] \lor \dots \lor \eq[x][\num{n}]))]$. There are no!!{element}s that are $\nsless \nszero$. So if $n$ is standard and $x$is non-standard, we cannot have $x \nsless n$. By definition, anon-standard element is one that isn't $\Value{\num{n}}{M}$ for any~$n\in \Nat$, so $x \neq n$ as well. Since $\nsless$ is a linear order,we must have $n \nsless x$.\end{proof}\begin{prop}Every nonstandard !!{element}~$x$ of~$\Domain{M}$ is an element of the subset\[\dots ^{\nssucc\nssucc\nssucc}x \nsless ^{\nssucc\nssucc}x \nsless^{\nssucc}x \nsless x \nsless x^{\nssucc} \nsless x^{\nssucc\nssucc}\nsless x^{\nssucc\nssucc\nssucc} \nsless \dots\]We call this subset the \emph{block of~$x$} and write it as $[x]$. Ithas no least and no greatest !!{element}. It can be characterized asthe set of those $y \in \Domain{M}$ such that, for some standard~$n$,$x \nsplus n = y$ or $y \nsplus n = x$.\end{prop}\begin{proof}Clearly, such a set~$[x]$ always exists since every !!{element}~$y$ of$\Domain{M}$ has a unique successor~$y^\nssucc$ and uniquepredecessor~$^\nssucc y$. For successive !!{element}s $y$, $y^\nssucc$we have $y \nsless y^\nssucc$ and $y^\nssucc$ is the $\nsless$-least!!{element} of~$\Domain{M}$ such that $y$ is $\nsless$-less than it.Since always $^\nssucc y \nsless y$ and $y \nsless y^\nssucc$, $[x]$has no least or greatest !!{element}. If $y \in [x]$ then $x \in [y]$,for then either $y^{\nssucc\dots\nssucc} = x$ or$x^{\nssucc\dots\nssucc} = y$.  If $y^{\nssucc\dots\nssucc} = x$ (with$n$ $\nssucc$'s), then $y \nsplus n = x$ and conversely, since$\Th{PA} \Proves \lforall[x][\eq[x^{\prime\dots\prime}][(x +    \num{n})]]$ (if $n$ is the number of~$\prime$'s).\end{proof}\begin{prop}If $[x] \neq [y]$ and $x \nsless y$, then for any $u \in [x]$ and any$v \in [y]$, $u \nsless v$.\end{prop}\begin{proof}Note that $\Th{PA} \Proves \lforall[x][\lforall[y][(x < y \lif (x' < y    \lor x' = y))]]$. Thus, if $u \nsless v$, we also have $u \nsplusn^\nssucc \nsless v$ for any~$n$ if $[u] \neq [v]$.Any $u \in [x]$ is $\nsless y$: $x \nsless y$ by assumption. If $u\nsless x$, $u \nsless y$ by transitivity. And if $x \nsless u$ but $u\in [x]$, we have $u = x\nsplus n^\nssucc$ for some~$n$, and so $u\nsless y$ by the fact just proved.  Now suppose that $v \in [y]$ is $\nsless y$, i.e., $v \nsplusm^\nssucc = y$ for some standard~$m$. This rules out $v \nsless x$,otherwise $y = v \nsplus m^\nssucc \nsless x$. Clearly also, $x \neqv$, otherwise $x \nsplus m^\nssucc = v \nsplus m^\nssucc = y$ and wewould have $[x] = [y]$. So, $x \nsless v$. But then also $x \nsplusn^\nssucc \nsless v$ for any~$n$. Hence, if $x \nsless u$ and $u \in[x]$, we have $u \nsless v$. If $u \nsless x$ then $u \nsless v$ bytransitivity.Lastly, if $y \nsless v$, $u \nsless v$ since, as we've shown, $u\nsless y$ and $y \nsless v$.\end{proof}\begin{cor}If $[x] \neq [y]$, $[x] \cap [y] = \emptyset$.\end{cor}\begin{proof}Suppose $z \in [x]$ and $x \nsless y$. Then $z \nsless u$ for all $u\in [y]$. If $z \in [y]$, we would have $z \nsless z$. Similarly if $y\nsless x$.\end{proof}\begin{explain}This means that the blocks themselves can be ordered in a way thatrespects $\nsless$: $[x] \nsless [y]$ iff $x \nsless y$, or,equivalently, if $u \nsless v$ for any $u \in [x]$ and $v \in [y]$.Clearly, the standard block $[0]$ is the least block. It intersectswith no non-standard block, and no two non-standard blocks intersecteither. Specifically, you cannot ``reach'' a different block by takingrepeated successors or predecessors.\end{explain}\begin{prop}If $x$ and $y$ are non-standard, then $x \nsless x \nsplus y$ and $x\nsplus y \notin [x]$.\end{prop}\begin{proof}If $y$ is nonstandard, then $y \neq \nszero$. $\Th{PA} \Proves\lforall[x][(y \neq \Obj{0} \lif x < (x+y))]$.  Now suppose $x\nsplus y \in [x]$. Since $x \nsless x \nsplus y$, we would have $x\nsplus n^\nssucc = x \nsplus y$. But $\Th{PA} \Proves\lforall[x][\lforall[y][\lforall[z][(\eq[(x+y)][(x+z)] \lif y = z)]]]$(the cancellation law for addition). This would mean $y = n^\nssucc$for some standard~$n$; but $y$ is assumed to be non-standard.\end{proof}\begin{prop}There is no least non-standard block.\end{prop}\begin{proof}$\Th{PA} \Proves \lforall[x][\lexists[y][(\eq[(y+y)][x] \lor      \eq[(y+y)'][x])]]$, i.e., that every $x$ is divisible by~$2$  (possibly with remainder~$1$). If $x$ is non-standard, so is~$y$. By  the preceding proposition, $y \nsless y \nsplus y$ and $y \nsplus y  \notin [y]$. Then also $y \nsless (y \nsplus y)^\nssucc$ and $(y  \nsplus y)^\nssucc \notin [y]$. But $x = y \nsplus y$ or $x = (y  \nsplus y)^\nssucc$, so $y \nsless x$ and $y \notin [x]$.\end{proof}\begin{prop}There is no largest block.\end{prop}\begin{proof}Exercise.\end{proof}\begin{prob}Show that in a non-standard model of~$\Th{PA}$, there is no largestblock.\end{prob}\begin{prop}\ollabel{prop:blocks-dense}The ordering of the blocks is dense. That is, if $x \nsless y$ and$[x] \neq [y]$, then there is a block $[z]$ distinct from both that isbetween them.\end{prop}\begin{proof}Suppose $x \nsless y$. As before, $x \nsplus y$ is divisible by two(possibly with remainder): there is a $z \in \Domain{M}$ such thateither $x \oplus y = z \oplus z$ or $x \oplus y = (z \oplusz)^\nssucc$. The element $z$ is the ``average'' of $x$ and~$y$, and $x\nsless z$ and $z \nsless y$.\end{proof}\begin{prob}Write out a detailed proof of\olref[mod][mar][mpa]{prop:blocks-dense}. Which !!{sentence} must$\Th{PA}$ !!{derive} in order to guarantee the existence of~$z$? Whyis $x \nsless z$ and $z \nsless y$, and why is $[x] \neq [z]$ and $[z]\neq [y]$?\end{prob}\begin{explain}The non-standard blocks are therefore ordered like the rationals: theyform !!a{denumerable} dense linear ordering without endpoints.  One can showthat any two such !!{denumerable} orderings are isomorphic. It followsthat for any two !!{enumerable} non-standard models $\Struct{M}_1$ and$\Struct{M_2}$ of true arithmetic, their reducts to the languagecontaining $<$ and $=$ only are isomorphic. Indeed, an isomorphism $h$can be defined as follows: the standard parts of $\Struct{M_1}$ and$\Struct{M_2}$ are isomorphic to the standard model $\Struct{N}$ andhence to each other. The blocks making up the non-standard part arethemselves ordered like the rationals and therefore isomorphic; anisomorphism of the blocks can be extended to an isomorphism\emph{within} the blocks by matching up arbitrary elements in each,and then taking the image of the successor of $x$ in $\Struct{M_1}$ tobe the successor of the image of $x$ in $\Struct{M_2}$. Note that itdoes \emph{not} follow that $\mathfrak{M}_1$ and $\mathfrak{M}_2$ areisomorphic in the full language of arithmetic (indeed, isomorphism isalways relative to !!a{language}), as there are non-isomorphic ways todefine addition and multiplication over $\Domain{M_1}$ and$\Domain{M_2}$. (This also follows from a famous theorem due to Vaughtthat the number of countable models of a complete theory cannot be~2.)\end{explain}\end{document}

content/model-theory/models-of-arithmetic/computable-models.tex

% Part: model-theory% Chapter: models-of-arithmetic% Section: computable-models\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{mod}{mar}{cmp}\section{Computable Models of Arithmetic}\begin{explain}The standard model~$\Struct{N}$ has two nice features. Its domain isthe natural numbers~$\Nat$, i.e., its elements are just the kinds ofthings we want to talk about using the language of arithmetic, and thestandard numeral~$\num{n}$ actually picks out~$n$. The other nicefeature is that the interpretations of the non-logical symbolsof~$\Lang{L_A}$ are all \emph{computable}. The successor, addition,and multiplication functions which serve as $\Assign{\prime}{N}$,$\Assign{+}{N}$, and $\Assign{\times}{N}$ are computable functions ofnumbers. (Computable by Turing machines, or definable by primitiverecursion, say.) And the less-than relation on~$\Struct{N}$, i.e.,$\Assign{<}{N}$, is decidable.Non-standard models of arithmetical theories such as $\Th{Q}$ and$\Th{PA}$ must contain non-standard elements. Thus their domainstypically include !!{element}s in addition to~$\Nat$. However, anycountable !!{structure} can be built on any !!{denumerable} set,including~$\Nat$. So there are also non-standard models withdomain~$\Nat$. In such models~$\Struct{M}$, of course, at least somenumbers cannot play the roles they usually play, since some~$k$ mustbe different from~$\Value{\num{n}}{M}$ for all~$n \in \Nat$.\end{explain}\begin{defn}!!^a{structure}~$\Struct{M}$ for $\Lang{L_A}$ is \emph{computable} iff  $\Domain{M} = \Nat$ and $\Assign{\prime}{M}$, $\Assign{+}{M}$,  $\Assign{\times}{M}$ are computable functions and $\Assign{<}{M}$ is  a decidable relation.\end{defn}\begin{ex}\ollabel{ex:comp-model-q}Recall the structure $\Struct{K}$ from \olref[mdq]{ex:model-K-of-Q}.Its domain was $\Domain{K} = \Nat\cup \{a\}$ and interpretations\begin{align*}  \Assign{\Obj{0}}{K} & = 0\\  \Assign{\prime}{K}(x) & =  \begin{cases}    x+1 & \text{if $x\in \Nat$}\\    a & \text{if $x = a$}  \end{cases}\\  \Assign{+}{K}(x, y) & =  \begin{cases}    x+y & \text{if $x$, $y \in\Nat$}\\    a & \text{otherwise}  \end{cases}\\  \Assign{\times}{K}(x, y) & =  \begin{cases}    xy & \text{if $x$, $y \in\Nat$}\\    0 & \text{if $x=0$ or $y=0$}\\    a & \text{otherwise}\\  \end{cases}\\  \Assign{<}{K} & =  \Setabs{\tuple{x,y}}{x, y \in \Nat \text{ and } x<y} \cup  \Setabs{\tuple{x,a}}{n \in \Domain{K}}\end{align*}But $\Domain{K}$ is !!{denumerable} and so is equinumerouswith~$\Nat$. For instance, $g\colon \Nat \to \Domain{K}$ with $g(0) =a$ and $g(n) = n+1$ for $n>0$ is !!a{bijection}.  We can turn it intoan isomorphism between a new model~$\Struct{K'}$ of~$\Th{Q}$ and$\Struct{K}$.  In $\Struct{K'}$, we have to assign different functionsand relations to the symbols of~$\Lang{L_A}$, since different!!{element}s of~$\Nat$ play the roles of standard and non-standardnumbers.Specifically, $0$ now plays the role of~$a$, not of the smalleststandard number. The smallest standard number is now~$1$. So we assign$\Assign{\Obj{0}}{K'} = 1$. The successor function is also differentnow: given a standard number, i.e., an $n > 0$, it still returns$n+1$. But $0$ now plays the role of~$a$, which is its ownsuccessor. So $\Assign{\prime}{K'}(0) = 0$.  For addition andmultiplication we likewise have\begin{align*}\Assign{+}{K'}(x, y) & =  \begin{cases}    x+y-1 & \text{if $x$, $y >0$}\\    0 & \text{otherwise}  \end{cases}\\  \Assign{\times}{K'}(x, y) & =  \begin{cases}    1 & \text{if $x = 1$ or $y = 1$}\\    xy - x - y + 2 & \text{if $x$, $y > 1$}\\    0 & \text{otherwise}\\  \end{cases}\end{align*}And we have $\tuple{x, y} \in \Assign{<}{K'}$ iff $x < y$ and $x > 0$and $y > 0$, or if $y = 0$.All of these functions are computable functions of natural numbers and$\Assign{<}{K'}$ is a decidable relation on~$\Nat$---but they are notthe same functions as successor, addition, and multiplicationon~$\Nat$, and $\Assign{<}{K'}$ is not the same relation as~$<$on~$\Nat$.\end{ex}\begin{prob}Give !!a{structure}~$\Struct{L'}$ with $\Domain{L'} = \Nat$ isomorphicto~$\Struct{L}$ of \olref[mod][mar][mdq]{ex:model-L-of-Q}.\end{prob}\begin{explain}\Olref{ex:comp-model-q} shows that $\Th{Q}$ has computablenon-standard models with domain~$\Nat$.  However, the following resultshows that this is not true for models of~$\Th{PA}$ (and thus also formodels of~$\Th{TA}$).\end{explain}\begin{thm}[Tennenbaum's Theorem]$\Struct{N}$ is the only computable model of~$\Th{PA}$.\end{thm}  \end{document}