compactness example (#346)

* Removed \div as function on rationals.

* A tiny bit more explanation in the changes for the infinitesimal example

---------

Co-authored-by: Richard Zach <[email protected]>

content/first-order-logic/completeness/compactness.tex

@@ -121,22 +121,30 @@
 \end{ex}
 
 \begin{ex}
-Consider a language $\Lang{L}$ containing the !!{predicate}~$<$,
-!!{constant}s $\Obj{0}$, $\Obj{1}$, and !!{function}s $+$, $\times$,
-$-$, $\div$. Let $\Gamma$ be the set of all !!{sentence}s in this
-language true in $\Struct{Q}$ with domain $\Rat$ and the obvious
-interpretations.  $\Gamma$ is the set of all !!{sentence}s
-of~$\Lang{L}$ true about the rational numbers. Of course, in $\Rat$
-(and even in $\Real$), there are no numbers which are greater than~$0$
+Consider !!a{language} $\Lang{L}$ containing the !!{predicate}~$<$,
+!!{constant}s $\Obj{0}$, $\Obj{1}$, and !!{function}s $+$, $\times$, and
+$-$. Let $\Gamma$ be the set of all !!{sentence}s in this
+!!{language} true in the !!{structure}~$\Struct{Q}$ with domain~$\Rat$ and the obvious
+interpretations.  $\Gamma$~is the set of all !!{sentence}s
+of~$\Lang{L}$ true about the rational numbers. Of course, in~$\Rat$
+(and even in~$\Real$), there are no numbers~$r$ which are greater than~$0$
 but less than $1/k$ for all $k \in \PosInt$.  Such a number, if it
 existed, would be an \emph{infinitesimal:} non-zero, but infinitely
-small.  The compactness theorem shows that there are models
-of~$\Gamma$ in which infinitesimals exist: Let $\Delta$ be $\{0<c\}
-\cup \Setabs{c < (\Obj{1} \div \num{k})}{k \in \PosInt}$ (where
+small.  The compactness theorem can be used to show that there are 
+models of~$\Gamma$ in which infinitesimals exist. We do not have 
+!!a{function} for division in our language (division by zero is 
+undefined, and !!{function}s have to be interpreted by total functions).
+However, we can still express that $r < 1/k$, since this is the case iff
+$r \cdot k < 1$. Now let $c$ be a new !!{constant} and let $\Delta$ be 
+\[
+\{0<c\}
+\cup \Setabs{ c \times \num k < \Obj{1} }{k \in \PosInt}
+\]
+(where
 $\num{k} = (\Obj{1} + (\Obj{1} + \dots + (\Obj{1} + \Obj{1})\dots))$
-with $k$ $\Obj{1}$'s). For any finite subset~$\Delta_0$ of~$\Delta$
-there is a $K$ such that all the !!{sentence}s $c < (\Obj{1} \div \num{k})$ in
-$\Delta_0$ have $k < K$. If we expand $\Struct{Q}$ to $\Struct{Q'}$
+with $k$~$\Obj{1}$'s). For any finite subset~$\Delta_0$ of~$\Delta$
+there is a~$K$ such that for all the !!{sentence}s $c \times \num{k} < \Obj{1}$ 
+in~$\Delta_0$ have $k < K$. If we expand $\Struct{Q}$ to~$\Struct{Q'}$
 with $\Assign{c}{Q'} = 1/K$ we have that $\Sat{Q'}{\Gamma \cup
   \Delta_0}$, and so $\Gamma \cup \Delta$ is finitely satisfiable
 (Exercise: prove this in detail). By compactness, $\Gamma \cup \Delta$