finish chnages necessary for issue #38

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

@@ -1,12 +1,12 @@
 % Part: first-order-logic
 % Chapter: completeness
-% Section: compactness
+% Section: compactness-direct
 
 \documentclass[../../../include/open-logic-section]{subfiles}
 
 \begin{document}
 
-\olfileid{fol}{com}{dcp}
+\olfileid{fol}{com}{cpd}
 \olsection{A Direct Proof of the Compactness Theorem}
 
 We can prove the Compactness Theorem directly, without appealing to
@@ -20,140 +20,99 @@
 
 We can use the same method to show that a finitely satisfiable set of
 sentences is satisfiable. We just have to prove the corresponding
-versions of \olref[ccs]{prop:ccs} and \olref[lin]{lem:lindenbaum}
-where we replace ``consistent'' with ``finitely satisfiable.''
-
-\begin{thm}
-  \ollabel{thm:fsat-henkin}
-  Every finitely satisfiable set~$\Gamma$ can be extended to a
-  saturated finitely satisfiable set~$\Gamma'$.
-\end{thm}
-
-
-\begin{lem}
-  \ollabel{lem:fsat-lindenbaum}
-  Every finitely satisfiable set~$\Gamma$ can be extended to a
-  !!{complete} and finitely satisfiable, saturated set~$\Gamma^*$.
-\end{lem}
+versions of the results leading to the truth lemma where we replace
+``consistent'' with ``finitely satisfiable.''
 
 \begin{prop}
 \ollabel{prop:fsat-ccs}
 Suppose $\Gamma$ is !!{complete} and finitely satisfiable. Then:
 \begin{enumerate}
-\item \ollabel{prop:complete-prov-in} If $\Gamma \Proves !A$, then $!A \in
-  \Gamma$.
-
-\tagitem{prvAnd}{\ollabel{prop:complete-and} $(!A \land !B) \in \Gamma$
+\tagitem{prvAnd}{$(!A \land !B) \in \Gamma$
   iff both $!A \in \Gamma$ and $!B \in \Gamma$.}{}
 
-\tagitem{prvOr}{\ollabel{prop:complete-or} $(!A \lor !B) \in \Gamma$ iff
+\tagitem{prvOr}{$(!A \lor !B) \in \Gamma$ iff
   either $!A \in \Gamma$ or $!B \in \Gamma$.}{}
 
-\tagitem{prvIf}{\ollabel{prop:complete-if} $(!A \lif !B) \in \Gamma$ iff
+\tagitem{prvIf}{$(!A \lif !B) \in \Gamma$ iff
   either $!A \notin \Gamma$ or $!B \in \Gamma$.}{}
 \end{enumerate}
 \end{prop}
 
+\begin{prop}
+Prove \olref[fol][com][cpd]{prop:fsat-ccs}. Avoid the use of $\Proves$.
+\end{prop}
+
+\begin{lem}
+\ollabel{lem:fsat-henkin} Every finitely satisfiable set~$\Gamma$ can
+be extended to a saturated finitely satisfiable set~$\Gamma'$.
+\end{lem}
 
-\begin{thm}[Compactness Theorem]
-\ollabel{thm:compactness}
-The following hold for any sentences $\Gamma$ and $!A$:
-\begin{enumerate}
-  \item $\Gamma \Entails !A$ iff there is a finite $\Gamma_0
-    \subseteq \Gamma$ such that $\Gamma_0 \Entails !A$.
-  \item $\Gamma$ is satisfiable if and only if it is finitely
-    satisfiable.
-\end{enumerate}
+\begin{prob}
+Prove \olref[fol][com][cpd]{lem:fsat-henkin}. (Hint: The crucial step
+is to show that if $\Gamma_n$ is finitely satisfiable, so is $\Gamma_n
+\cup \{!D_n\}$, without any appeal to !!{derivation}s or consistency.)
+\end{prob}
+
+\begin{prop}\ollabel{prop:fsat-instances}
+Suppose $\Gamma$ is complete, finitely satisfiable, and saturated.
+\iftag{defAll,defEx}{}{\begin{enumerate}\item}
+\iftag{prvAll}{$\lforall[x][!A(x)] \in \Gamma$ iff $!A(t) \in \Gamma$
+  for all closed terms~$t$.}{}
+\iftag{defAll,defEx}{}{\item}
+\iftag{prvEx}{$\lforall[x][!A(x)] \in \Gamma$ iff $!A(t) \in \Gamma$
+  for at least one closed term~$t$.}{}
+\iftag{defAll,defEx}{}{\end{enumerate}}
+\end{prop}
+
+\begin{prob}
+Prove \olref[fol][com][cpd]{lem:fsat-henkin}. (Hint: The crucial step
+is to show that if $\Gamma_n$ is finitely satisfiable, so is
+$\Gamma_{n+1}$, without any appeal to !!{derivation}s or consistency.)
+\end{prob}
+
+\begin{lem}
+\ollabel{lem:fsat-lindenbaum} Every finitely satisfiable set~$\Gamma$
+can be extended to a !!{complete} and finitely satisfiable, saturated
+set~$\Gamma^*$.
+\end{lem}
+
+\begin{prob}
+Prove \olref[fol][com][cpd]{lem:fsat-lindenbaum}.  (Hint: the crucial
+step is to show that if $\Gamma_n$ is finitely satisfiable, then
+either $\Gamma_n \cup \{!A_n\}$ or $\Gamma_n \cup \{\lnot !A_n\}$ is
+finitely satisfiable.)
+\end{prob}
+
+\begin{thm}
+\ollabel{thm:compactness-direct} $\Gamma$ is satisfiable if and only
+if it is finitely satisfiable.
 \end{thm}
 
 \begin{proof}
-We prove (2).  If $\Gamma$ is satisfiable, then there is a
+If $\Gamma$ is satisfiable, then there is a
 !!{structure}~$\Struct{M}$ such that $\Sat{M}{!A}$ for all $!A \in
 \Gamma$.  Of course, this $\Struct M$ also satisfies every finite
 subset of~$\Gamma$, so $\Gamma$ is finitely satisfiable.
 
-Now suppose that $\Gamma$ is finitely satisfiable.  Then every finite
-subset~$\Gamma_0 \subseteq \Gamma$ is satisfiable.  By soundness,
-every finite subset is consistent.  Then $\Gamma$ itself must be
-consistent.  For assume it is not, i.e., $\Gamma \Proves \bot$.  But
-!!{derivation}s are finite, and so already some finite
-subset~$\Gamma_0 \subseteq \Gamma$ must be inconsistent
-(cf.\ \tagrefs{prfSC/{fol:seq:ptn:prop:proves-compact},prfND/{fol:ntd:ptn:prop:proves-compact}}).
-But we just showed they are all consistent, a contradiction.  Now by
-completeness, since $\Gamma$ is consistent, it is satisfiable.
+Now suppose that $\Gamma$ is finitely satisfiable. By
+\olref{lem:fsat-henkin}, there is a finitely satisfiable, saturated
+set $\Gamma' \supseteq \Gamma$. By \olref{lem:fsat-lindenbaum},
+$\Gamma'$ can be extended to a !!{complete}, finitely satisfiable,
+saturated set~$\Gamma^*$. Construct the term
+model~$\Struct{M(\Gamma^*)}$ as in \olref[mod]{defn:termmodel}.  Note
+that \olref[mod]{prop:quant-termmodel} did not rely on the fact that
+$\Gamma^*$ is consistent (or !!{complete} or saturated, for that
+matter), but just on the fact that $\Struct{M(\Gamma^*)}$ is covered.
+The proof of the Truth Lemma (\olref[mod]{lem:truth}) goes through if
+we replace references to \olref[ccs]{prop:ccs} and
+\olref[hen]{prop:saturated-instances} by references to
+\olref{prop:fsat-ccs} and \olref{prop:fsat-instances}.
 \end{proof}
 
 \begin{prob}
-Prove (1) of \olref[fol][com][com]{thm:compactness}.
-\end{prob}
-
-\begin{ex}
-In every model~$\Struct{M}$ of a theory~$\Gamma$, each term~$t$ of
-course picks out !!a{element} of~$\Domain{M}$. Can we guarantee that
-it is also true that every !!{element} of~$\Domain{M}$ is picked out
-by some term or other? In other words, are there theories~$\Gamma$ all
-models of which are covered?  The compactness theorem shows that this
-is not the case if $\Gamma$ has infinite models. Here's how to see
-this: Let $\Struct{M}$ be an infinite model of~$\Gamma$, and let $c$
-be !!a{constant} not in the language of~$\Gamma$. Let $\Delta$ be the
-set of all sentences $\eq/[c][t]$ for $t$ a term in the
-language~$\Lang{L}$ of~$\Gamma$, i.e.,
-  \[
-  \Delta = \Setabs{\eq/[c][t]}{t \in \Trm[L]}.
-  \]
-A finite subset of $\Gamma \cup \Delta$ can be written as $\Gamma'
-\cup \Delta'$, with $\Gamma' \subseteq \Gamma$ and $\Delta' \subseteq
-\Delta$. Since $\Delta'$ is finite, it can contain only finitely many
-terms. Let $a \in \Domain{M}$ be !!a{element} of $\Domain{M}$ not
-picked out by any of them, and let $\Struct{M'}$ be the !!{structure}
-that is just like $\Struct{M}$, but also $\Assign{c}{M'} = a$. Since
-$a \neq \Value{t}{M}$ for all~$t$ occuring in~$\Delta'$,
-$\Sat{M'}{\Delta'}$. Since $\Sat{M}{\Gamma}$, $\Gamma' \subseteq
-\Gamma$, and $c$ does not occur in~$\Gamma$, also
-$\Sat{M'}{\Gamma'}$. Together, $\Sat{M'}{\Gamma' \cup \Delta'}$ for
-every finite subset $\Gamma' \cup \Delta'$ of $\Gamma \cup \Delta$. So
-every finite subset of $\Gamma \cup \Delta$ is satisfiable. By
-compactness, $\Gamma \cup \Delta$ itself is satisfiable. So there are
-models~$\Sat{M}{\Gamma \cup \Delta}$. Every such $\Struct{M}$ is a
-model of~$\Gamma$, but is not covered, since $\Value{c}{M} \neq
-\Value{t}{M}$ for all terms~$t$ of~$\Lang{L}$.
-\end{ex}
-
-\begin{prob}
-Use the compactness theorem to show that any set of sentences in the
-language of arithmetic which are true in the standard model of
-arithmetic $\Struct{N}$ are also true in !!a{structure}~$\Struct{N'}$
-that contains an element greater than all natural
-numbers~$\Assign{\num{n}}{N'}$ ($\num{n}$ is
-$\Obj{0}^{\prime\dots\prime}$ with $n$ $\prime$'s).
+Write out the complete proof of the Truth Lemma
+(\olref[fol][com][mod]{lem:truth}) in the version required for the
+proof of \olref[fol][com][cpd]{thm:compactness-direct}.
 \end{prob}
 
-\begin{ex}
-We know that first-order logic with !!{identity} can express that the
-size of the !!{domain} must have some minimal size: The
-sentence~$!A_{\ge n}$ (which says ``there are at least $n$ distinct
-objects'') is true only in structures where $\Domain{M}$ has at
-least~$n$ objects. So if we take
-  \[
-  \Delta = \Setabs{!A_{\ge n}}{n \ge 1}
-  \]
-then any model of $\Delta$ must be infinite. Thus, we can guarantee
-that a theory only has infinite models by adding~$\Delta$ to it: the
-models of $\Gamma \cup \Delta$ are all and only the infinite models
-of~$\Gamma$.
-
-So first-order logic can express infinitude. The compactness theorem
-shows that it cannot express finitude, however. For suppose some set
-of sentences $\Lambda$ were satisfied in all and only finite
-!!{structure}s. Then $\Delta \cup \Lambda$ is finitely
-satisfiable. Why? Suppose $\Delta' \cup \Lambda' \subseteq \Delta \cup
-\Lambda$ is finite with $\Delta' \subseteq \Delta$ and $\Lambda'
-\subseteq \Lambda$. Let $n$ be the largest number such that $A_{\ge n}
-\in \Delta'$. $\Lambda$, being satisfied in all finite structures, has
-a model~$\Struct{M}$ with finitely many but $\ge n$ !!{element}s. But
-then $\Sat{M}{\Delta' \cup \Lambda'}$.  By compactness, $\Delta \cup
-\Lambda$ has an infinite model, contradicting the assumption that
-$\Lambda$ is satisfied only in finite !!{structure}s.
-\end{ex}
-
 \end{document}

content/first-order-logic/completeness/complete-consistent-sets.tex

@@ -20,44 +20,44 @@
 \end{defn}
 
 \begin{explain}
-  !!^{complete} sets of sentences leave no questions unanswered. For any
-  !!{sentence}~$A$, $\Gamma$ ``says'' if $!A$ is true or false.  The
-  importance of !!{complete} sets extends beyond the proof of the
-  completeness theorem. A theory which is !!{complete} and
-  axiomatizable, for instance, is always decidable.
+!!^{complete} sets of sentences leave no questions unanswered. For
+any !!{sentence}~$A$, $\Gamma$ ``says'' if $!A$ is true or false.  The
+importance of !!{complete} sets extends beyond the proof of the
+completeness theorem. A theory which is !!{complete} and
+axiomatizable, for instance, is always decidable.
 \end{explain}
 
 \begin{explain}
-  !!^{complete} consistent sets are important in the completeness proof
-  since we can guarantee that every consistent set of
-  !!{sentence}s~$\Gamma$ is contained in a !!{complete} consistent
-  set~$\Gamma^*$.  !!a{complete} consistent set contains, for
-  each !!{sentence}~$!A$, either $!A$ or its negation $\lnot !A$, but
-  not both. This is true in particular for atomic !!{sentence}s, so
-  from !!a{complete} consistent set in a language suitably expanded by
-  !!{constant}s, we can construct a !!{structure} where the
-  interpretation of !!{predicate}s is defined according to which
-  atomic !!{sentence}s are in~$\Gamma^*$. This !!{structure} can then
-  be shown to make all !!{sentence}s in~$\Gamma^*$ (and hence also in
-  $\Gamma$) true. The proof of this latter fact requires that $\lnot
-  !A \in \Gamma^*$ iff $!A \notin \Gamma^*$, $(!A \lor !B) \in
-  \Gamma^*$ iff $!A \in \Gamma^*$ or $!B \in \Gamma^*$, etc.
+!!^{complete} consistent sets are important in the completeness proof
+since we can guarantee that every consistent set of
+!!{sentence}s~$\Gamma$ is contained in a !!{complete} consistent
+set~$\Gamma^*$.  !!^a{complete} consistent set contains, for each
+!!{sentence}~$!A$, either $!A$ or its negation $\lnot !A$, but not
+both. This is true in particular for atomic !!{sentence}s, so from
+!!a{complete} consistent set in a language suitably expanded by
+!!{constant}s, we can construct a !!{structure} where the
+interpretation of !!{predicate}s is defined according to which atomic
+!!{sentence}s are in~$\Gamma^*$. This !!{structure} can then be shown
+to make all !!{sentence}s in~$\Gamma^*$ (and hence also all those
+in~$\Gamma$) true. The proof of this latter fact requires that $\lnot
+!A \in \Gamma^*$ iff $!A \notin \Gamma^*$, $(!A \lor !B) \in \Gamma^*$
+iff $!A \in \Gamma^*$ or $!B \in \Gamma^*$, etc.
 \end{explain}
 
 \begin{prop}
 \ollabel{prop:ccs}
 Suppose $\Gamma$ is !!{complete} and consistent. Then:
 \begin{enumerate}
-\item \ollabel{prop:complete-prov-in} If $\Gamma \Proves !A$, then $!A \in
+\item \ollabel{prop:ccs-prov-in} If $\Gamma \Proves !A$, then $!A \in
   \Gamma$.
 
-\tagitem{prvAnd}{\ollabel{prop:complete-and} $(!A \land !B) \in \Gamma$
+\tagitem{prvAnd}{\ollabel{prop:ccs-and} $(!A \land !B) \in \Gamma$
   iff both $!A \in \Gamma$ and $!B \in \Gamma$.}{}
 
-\tagitem{prvOr}{\ollabel{prop:complete-or} $(!A \lor !B) \in \Gamma$ iff
+\tagitem{prvOr}{\ollabel{prop:ccs-or} $(!A \lor !B) \in \Gamma$ iff
   either $!A \in \Gamma$ or $!B \in \Gamma$.}{}
 
-\tagitem{prvIf}{\ollabel{prop:complete-if} $(!A \lif !B) \in \Gamma$ iff
+\tagitem{prvIf}{\ollabel{prop:ccs-if} $(!A \lif !B) \in \Gamma$ iff
   either $!A \notin \Gamma$ or $!B \in \Gamma$.}{}
 \end{enumerate}
 \end{prop}
@@ -84,13 +84,13 @@
 $\Gamma \Proves !A \land !B$. By
 \tagrefs{prfSC/{fol:seq:prv:prop:provability-land-left},prfND/{fol:ntd:prv:prop:provability-land-left}},
 $\Gamma \Proves !A$ and $\Gamma \Proves !B$. By
-\olref{prop:complete-prov-in}, $!A \in \Gamma$ and $!B \in \Gamma$, as
+\olref{prop:ccs-prov-in}, $!A \in \Gamma$ and $!B \in \Gamma$, as
 required.
 
 For the reverse direction, let $!A \in \Gamma$ and $!B \in
 \Gamma$. Then $\Gamma \Proves !A$ and $\Gamma \Proves !B$. By
 \tagrefs{prfSC/{fol:seq:prv:prop:provability-land-right},prfND/{fol:ntd:prv:prop:provability-land-right}},
-$\Gamma \Proves !A \land !B$. By \olref{prop:complete-prov-in}, $(!A \land
+$\Gamma \Proves !A \land !B$. By \olref{prop:ccs-prov-in}, $(!A \land
 !B) \in \Gamma$.}}
 
 \tagitem{defOr}{}{%
@@ -111,7 +111,7 @@
 For the reverse direction, suppose that $!A \in \Gamma$ or $!B \in
 \Gamma$. Then $\Gamma \Proves !A$ or $\Gamma \Proves !B$. By
 \tagrefs{prfSC/{fol:seq:prv:prop:provability-lor-right},prfND/{fol:ntd:prv:prop:provability-lor-right}},
-$\Gamma \Proves !A \lor !B$. By \olref{prop:complete-prov-in}, $(!A \lor
+$\Gamma \Proves !A \lor !B$. By \olref{prop:ccs-prov-in}, $(!A \lor
 !B) \in \Gamma$, as required.}}
 
 \tagitem{defIf}{}{%
@@ -122,20 +122,20 @@
 to the contrary that $!A \in \Gamma$ and $!B \notin \Gamma$. On these
 assumptions, $\Gamma \Proves !A \lif !B$ and $\Gamma \Proves !A$. By
 \tagrefs{prfSC/{fol:seq:prv:prop:provability-mp},prfND/{fol:ntd:prv:prop:provability-mp}},
-$\Gamma \Proves !B$. But then by \olref{prop:complete-prov-in}, $!B \in
+$\Gamma \Proves !B$. But then by \olref{prop:ccs-prov-in}, $!B \in
 \Gamma$, contradicting the assumption that $!B \notin \Gamma$.
 
 For the reverse direction, first consider the case where $!A \notin
 \Gamma$. Since $\Gamma$ is !!{complete}, $\lnot !A \in \Gamma$ and
 hence $\Gamma \Proves \lnot !A$. By
 \tagrefs{prfSC/{fol:seq:prv:prop:provability-lif},prfND/{fol:ntd:prv:prop:provability-lif}},
-$\Gamma \Proves !A \lif !B$. Again by \olref{prop:complete-prov-in}, we get
+$\Gamma \Proves !A \lif !B$. Again by \olref{prop:ccs-prov-in}, we get
 that $(!A \lif !B) \in \Gamma$, as required.
 
 Now consider the case where $!B \in \Gamma$. Then $\Gamma \Proves !B$
 and by
 \tagrefs{prfSC/{fol:seq:prv:prop:provability-lif},prfND/{fol:ntd:prv:prop:provability-lif}},
-$\Gamma \Proves !A \lif !B$. By \olref{prop:complete-prov-in}, $(!A \lif
+$\Gamma \Proves !A \lif !B$. By \olref{prop:ccs-prov-in}, $(!A \lif
 !B) \in \Gamma$.}}
 \end{enumerate}
 \end{proof}

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

@@ -13,16 +13,14 @@
 
 \begin{thm}[Completeness Theorem]
 \ollabel{thm:completeness}
-Let $\Gamma$ be a set of !!{sentence}s.  If
-$\Gamma$ is consistent, it is satisfiable.
+Let $\Gamma$ be a set of !!{sentence}s.  If $\Gamma$ is consistent, it
+is satisfiable.
 \end{thm}
 
 \begin{proof}
 Suppose $\Gamma$ is consistent.  By \olref[lin]{lem:lindenbaum}, there
-is a $\Gamma^* \supseteq \Gamma$ which is
-\iftag{cmplMCS}{maximally consistent}{}
-\iftag{cmplCCS}{consistent, !!{complete},}{} and
-saturated.  If $\Gamma$ does not contain~$\eq$, then by
+is a $\Gamma^* \supseteq \Gamma$ which is consistent, !!{complete},
+and saturated.  If $\Gamma$ does not contain~$\eq$, then by
 \olref[mod]{lem:truth}, $\Sat{M(\Gamma^*)}{!A}$ iff $!A \in \Gamma^*$.
 From this it follows in particular that for all $!A \in \Gamma$,
 $\Sat{M(\Gamma^*)}{!A}$, so $\Gamma$ is satisfiable.  If $\Gamma$ does
@@ -65,10 +63,10 @@
 \begin{prob}
 In order for a !!{derivation} system to be complete, its rules must be
 strong enough to prove every unsatisfiable set inconsistent.  Which of
-the rules of $\Log{LK}$ were necessary to prove completeness?  Are any
+the rules of !!{derivation} were necessary to prove completeness?  Are any
 of these rules not used anywhere in the proof?  In order to answer
 these questions, make a list or diagram that shows which of the rules
-of $\Log{LK}$ were used in which results that lead up to the proof of
+of !!{derivation} were used in which results that lead up to the proof of
 \olref[fol][com][cth]{thm:completeness}.  Be sure to note any tacit
 uses of rules in these proofs.
 \end{prob}

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

@@ -11,8 +11,7 @@ \chapter{The Completeness Theorem}
 
 \olimport{outline}
 
-\iftag{cmplMCS}{\olimport{maximally-consistent-sets}}{}
-\iftag{cmplCCS}{\olimport{complete-consistent-sets}}
+\olimport{complete-consistent-sets}
 
 \olimport{henkin-expansions}
 
@@ -26,7 +25,7 @@ \chapter{The Completeness Theorem}
 
 \olimport{compactness}
 
-\iftag{cmplCCS}{\olimport{compactness-direct}}
+\olimport{compactness-direct}
 
 \olimport{downward-ls}