From ef39e057552e9ab5d3cf14599b832d6790471f31 Mon Sep 17 00:00:00 2001 From: Richard Zach Date: Wed, 12 Jul 2017 06:22:31 -0600 Subject: [PATCH] finish chnages necessary for issue #38 --- .../completeness/compactness-direct.tex | 183 +++++++--------- .../completeness/complete-consistent-sets.tex | 58 ++--- .../completeness/completeness-thm.tex | 14 +- .../completeness/completeness.tex | 5 +- .../completeness/construction-of-model.tex | 200 ++++++++++-------- .../completeness/henkin-expansions.tex | 186 ++++++++++------ .../completeness/identity.tex | 35 ++- .../completeness/lindenbaums-lemma.tex | 48 ++--- .../completeness/outline.tex | 43 +++- .../natural-deduction/provability.tex | 10 + .../syntax-and-semantics/assignments.tex | 13 +- 11 files changed, 441 insertions(+), 354 deletions(-) diff --git a/content/first-order-logic/completeness/compactness-direct.tex b/content/first-order-logic/completeness/compactness-direct.tex index 2714ca4c..9fe721e3 100644 --- a/content/first-order-logic/completeness/compactness-direct.tex +++ b/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} diff --git a/content/first-order-logic/completeness/complete-consistent-sets.tex b/content/first-order-logic/completeness/complete-consistent-sets.tex index a2fed2b2..cdb2b099 100755 --- a/content/first-order-logic/completeness/complete-consistent-sets.tex +++ b/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} diff --git a/content/first-order-logic/completeness/completeness-thm.tex b/content/first-order-logic/completeness/completeness-thm.tex index 6d13c286..e7d7ae3d 100644 --- a/content/first-order-logic/completeness/completeness-thm.tex +++ b/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} diff --git a/content/first-order-logic/completeness/completeness.tex b/content/first-order-logic/completeness/completeness.tex index b5c3ba76..9293cda9 100644 --- a/content/first-order-logic/completeness/completeness.tex +++ b/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} diff --git a/content/first-order-logic/completeness/construction-of-model.tex b/content/first-order-logic/completeness/construction-of-model.tex index 9805b9df..2b02fe2a 100644 --- a/content/first-order-logic/completeness/construction-of-model.tex +++ b/content/first-order-logic/completeness/construction-of-model.tex @@ -10,23 +10,31 @@ \olsection{Construction of a Model} -We will begin by showing how to construct !!a{structure} which -satisfies a -\iftag{cmplMCS}{maximally consistent,}{} -\iftag{cmplCCS}{!!{complete} and consistent,}{} -saturated set of !!{sentence}s in a language~$\Lang L$ without~$\eq$. +\begin{explain} +Right now we are not concerned about $\eq$, i.e., we only want to show +that a consistent set~$\Gamma$ of !!{sentence}s not containing~$\eq$ +is satisfiable. We first extend~$\Gamma$ to a consistent, +!!{complete}, and saturated set~$\Gamma^*$. In this case, the +definition of a model~$\Struct{M(\Gamma^*)}$ is simple: We take the +set of closed terms of~$\Lang{L'}$ as the domain. We assign every +!!{constant} to itself, and make sure that more generally, for every +closed term~$t$, $\Value{t}{M(\Gamma^*)} = t$. The !!{predicate}s are +assigned extensions in such a way that an atomic !!{sentence} is true +in $\Struct{M(\Gamma^*)}$ iff it is in~$\Gamma^*$. This will +obviously make all the atomic !!{sentence}s in~$\Gamma^*$ true in +$\Struct{M(\Gamma^*)}$. The rest are true provided the $\Gamma^*$ we +start with is consistten, complete, and saturated. +\end{explain} \begin{defn}[Term model] -\ollabel{termmodel} -Let $\Gamma^*$ be a -\iftag{cmplMCS}{maximally consistent}{} -\iftag{cmplCCS}{!!{complete} and consistent}{}, +\ollabel{defn:termmodel} +Let $\Gamma^*$ be a !!{complete} and consistent, saturated set of !!{sentence}s in a language~$\Lang L$. The \emph{term model}~$\Struct M(\Gamma^*)$ of $\Gamma^*$ is the !!{structure} defined as follows: \begin{enumerate} -\item The !!{domain}~$\Domain{M(\Gamma^*)}$ is the set of all closed terms - of~$\Lang L$. +\item The !!{domain}~$\Domain{M(\Gamma^*)}$ is the set of all closed + terms of~$\Lang L$. \item The interpretation of !!a{constant} $c$ is $c$ itself: $\Assign{c}{M(\Gamma^*)} = c$. \item The !!{function}~$f$ is assigned the function which, given as @@ -35,12 +43,76 @@ \[ \Assign{f}{M(\Gamma^*)}(t_1, \dots, t_n) = f(t_1,\dots, t_n) \] -\item If $R$ is an $n$-place !!{predicate}, then $\tuple{t_1, \dots, - t_n} \in \Assign{R}{M(\Gamma^*)}$ iff $\Atom{R}{t_1, \dots, - t_n} \in \Gamma^*$. +\item If $R$ is an $n$-place !!{predicate}, then + \[ + \tuple{t_1, \dots, + t_n} \in \Assign{R}{M(\Gamma^*)} \text{ iff } \Atom{R}{t_1, \dots, + t_n} \in \Gamma^*. + \] \end{enumerate} \end{defn} +\begin{explain} + \iftag{prvEx}{!!^a{structure}~$\Struct{M}$ may make an existentially + quantified !!{sentence}~$\lexists[x][!A(x)]$ true without there + being an instance~$!A(t)$ that it makes true.}{} + \iftag{prvAll}{!!^a{structure}~$\Struct{M}$ may make all + instances~$!A(t)$ of a universally quantified + !!{sentence}~$\lforall[x][!A(x)]$ true, without + making~$\lforall[x][!A(x)]$ true.}{} This is because in general + not every !!{element} of~$\Domain{M}$ is the value of a closed term + ($\Struct{M}$ may not be covered). This is the reason the + satisfaction relation is defined via variable assignments. However, + for our term model~$\Struct{M(\Gamma^*)}$ this wouldn't be + necessary---because it is covered. This is the content of the next + result. +\end{explain} + +\begin{prop} +\ollabel{prop:quant-termmodel} +Let $\Struct M(\Gamma^*)$ be the term model of \olref{defn:termmodel}. +\iftag{defEx,defAll}{}{\begin{enumerate}\item}% +\iftag{prvEx}{$\Sat{M(\Gamma^*)}{\lexists[x][!A(x)]}$ iff + $\Sat{M}{!A(t)}$ for at least one term~$t$.}{}% +\iftag{defEx,defAll}{}{\item}% +\iftag{prvAll}{$\Sat{M(\Gamma^*)}{\lforall[x][!A(x)]}$ iff + $\Sat{M}{!A(t)}$ for all terms~$t$.}{}% +\iftag{defEx,defAll}{}{\end{enumerate}} +\end{prop} + +\begin{proof} +\iftag{defEx,defAll}{}{\begin{enumerate}\item}% +\iftag{prvAll}{% + \iftag{probAll}{Exercise.}{By \olref[syn][ass]{prop:sat-quant}, + $\Sat{M(\Gamma^*)}{\lforall[x][!A(x)]}$ iff for every variable + assignment $s$, $\Sat{M(\Gamma^*)}{!A(x)}[s]$. Recall that + $\Domain{M(\Gamma^*)}$ consists of the closed terms of~$\Lang{L}$, + so for every closed term~$t$, $s(x) = t$ is such a variable + assignment, and for any variable assignment, $s(x)$ is some closed + term~$t$. By \olref[fol][syn][ext]{prop:ext-formulas}, + $\Sat{M(\Gamma^*)}{!A(x)}[s]$ iff $\Sat{M(\Gamma^*)}{!A(t)}[s]$, + where $s(x) = t$. By \olref[fol][syn][ass]{prop:sentence-sat-true}, + $\Sat{M(\Gamma^*)}{!A(t)}[s]$ iff $\Sat{M(\Gamma^*)}{!A(t)}$, + since $!A(t)$ is a sentence.}}{} \iftag{defAll,defEx}{}{\item} +\iftag{prvEx}{% + \iftag{probEx}{Exercise.}{By \olref[syn][ass]{prop:sat-quant}, + $\Sat{M(\Gamma^*)}{\lexists[x][!A(x)]}$ iff for at least one + variable assignment~$s$, $\Sat{M(\Gamma^*)}{!A(x)}[s]$. As + $\Domain{M(\Gamma^*)}$ consists of the closed terms of~$\Lang{L}$, + this is the case iff there is at least one closed term~$t$ such + that $s(x) = t$ and $\Sat{M(\Gamma^*)}{!A(x)}[s]$. By + \olref[fol][syn][ext]{prop:ext-formulas}, + $\Sat{M(\Gamma^*)}{!A(x)}[s]$ iff $\Sat{M(\Gamma^*)}{!A(t)}[s]$, + where $s(x) = t$. By \olref[fol][syn][ass]{prop:sentence-sat-true}, + $\Sat{M(\Gamma^*)}{!A(t)}[s]$ iff $\Sat{M(\Gamma^*)}{!A(t)}$, + since $!A(t)$ is a sentence.}}{} +\iftag{defEx,defAll}{}{\end{enumerate}} +\end{proof} + +\begin{prob} +Complete the proof of \olref[fol][com][mod]{prop:quant-termmodel}. +\end{prob} + \begin{lem}[Truth Lemma] \ollabel{lem:truth} Suppose $!A$ does not contain~$\eq$. Then $\Sat{M(\Gamma^*)}{!A}$ iff $!A \in \Gamma^*$. @@ -55,26 +127,23 @@ $\Gamma^*$ is consistent.}}{} \tagitem{prvTrue}{% - \indcase{!A}{\ltrue}{$\Sat{M(\Gamma^*)}{\ltrue}$ by definition of - satisfaction. On the other hand, $\ltrue \in \Gamma^*$ since - $\Gamma^*$ is maximally consistent and $\Gamma^* \Proves \ltrue$.}}{} + \indcase{!A}{\ltrue}{$\Sat{M(\Gamma^*)}{\ltrue}$ + by definition of satisfaction. On the other hand, $\ltrue \in + \Gamma^*$ since $\Gamma^*$ is consistent and !!{complete}, and + $\Gamma^* \Proves \ltrue$.}}{} \item \indcase{!A}{R(t_1, \dots, t_n)}{$\Sat{M(\Gamma^*)}{\Atom{R}{t_1, \dots, t_n}}$ iff $\tuple{t_1, \dots, t_n} \in \Assign{R}{M(\Gamma^*)}$ (by the definition of satisfaction) iff $R(t_1, \dots, t_n) \in \Gamma^*$ - (the construction of $\Struct M(\Gamma^*)$.} + (by the construction of $\Struct M(\Gamma^*)$).} \tagitem{prvNot}{% \indcase{!A}{\lnot !B}{$\Sat{M(\Gamma^*)}{\indfrm}$ iff $\Sat/{M(\Gamma^*)}{!B}$ (by definition of satisfaction). By induction hypothesis, $\Sat/{M(\Gamma^*)}{!B}$ iff $!B \notin - \Gamma^*$. By - \iftag{cmplMCS}{\olref[mcs]{prop:mcs}\olref[mcs]{prop:mcs-either-or},}{} - \iftag{cmplCCS}{\olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-either-or},}{} - $\lnot !B \in \Gamma^*$ if $!B \notin \Gamma^*$; and $\lnot !B - \notin \Gamma^*$ if $!B \in \Gamma^*$ since $\Gamma^*$ is - consistent.}}{} + \Gamma^*$. Since $\Gamma^*$ is consistent and !!{complete}, + $!B \notin \Gamma^*$ iff $\lnot !B \in \Gamma^*$.}}{} \tagitem{prvAnd}{% \iftag{probAnd}{% @@ -83,9 +152,8 @@ both $\Sat{M(\Gamma^*)}{!B}$ and $\Sat{M(\Gamma^*)}{!C}$ (by definition of satisfaction) iff both $!B \in \Gamma^*$ and $!C \in \Gamma^*$ (by the induction hypothesis). By - \iftag{cmplMCS}{\olref[mcs]{prop:mcs}\olref[mcs]{prop:mcs-and},}{} - \iftag{cmplCCS}{\olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-and},}{} - this is the case iff $(!B \land !C) \in \Gamma^*$.}}}{} + \olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-and}, this is the case iff + $(!B \land !C) \in \Gamma^*$.}}}{} \tagitem{prvOr}{% \iftag{probOr}{% @@ -95,8 +163,7 @@ satisfaction) iff $!B \in \Gamma^*$ or $!C \in \Gamma^*$ (by induction hypothesis). This is the case iff $(!B \lor !C) \in \Gamma^*$ (by - \iftag{cmplMCS}{\olref[mcs]{prop:mcs}\olref[mcs]{prop:mcs-or}).}{} - \iftag{cmplCCS}{\olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-or}).}{}}}}{} + \olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-or}).}}}{} \tagitem{prvIf}{% \iftag{probIf}{% @@ -106,70 +173,27 @@ of satisfaction) iff $!B \notin \Gamma^*$ or $!C \in \Gamma^*$ (by induction hypothesis). This is the case iff $(!B \lif !C) \in \Gamma^*$ (by - \iftag{cmplMCS}{\olref[mcs]{prop:mcs}\olref[mcs]{prop:mcs-if}).}{} - \iftag{cmplCCS}{\olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-if}).}{}}}}{} + \olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-if}).}}}{} \tagitem{prvAll}{% -\iftag{probAll}{% -\indcase!{!A}{\lforall[x][!B(x)]}{}}{% -\indcase{!A}{\lforall[x][!B(x)]}{Suppose that - $\Sat{M(\Gamma^*)}{\indfrm}$, then for every variable assignment $s$, - $\Sat{M(\Gamma^*)}{!B(x)}[s]$. Suppose to the contrary that - $\lforall[x][!B(x)]\notin \Gamma^*$: Then - \iftag{cmplMCS}{by \olref[mcs]{prop:mcs}\olref[mcs]{prop:mcs-either-or},}{} - \iftag{cmplCCS}{since $\Gamma^*$ is !!{complete},}{} - $\lnot\lforall[x][!B(x)] \in \Gamma^*$. By saturation, - \iftag{prvEx} - {$(\lexists[x][\lnot !B(x)] \lif \lnot !B(c)) \in \Gamma^*$} - {$(\lnot\lforall[x][!B(x)] \lif \lnot !B(c)) \in \Gamma^*$} - for some $c$, so by - \iftag{cmplMCS}{\olref[mcs]{prop:mcs}\olref[mcs]{prop:mcs-prov-in},}{} - \iftag{cmplCCS}{\olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-prov-in},}{} - $\lnot !B(c) \in \Gamma^*$. Since $\Gamma^*$ is consistent, $!B(c) - \notin \Gamma^*$. By induction hypothesis, - $\Sat/{M(\Gamma^*)}{!B(c)}$. Therefore, if $s'$ is the variable - assignment such that $s(x)=c$, then $\Sat/{M(\Gamma^*)}{!B(x)}[s']$, - contradicting the earlier result that $\Sat{M(\Gamma^*)}{!B(x)}[s]$ - for all~$s$. Thus, we have $\indfrm \in \Gamma^*$. - -Conversely, suppose that $\lforall[x][!B(x)] \in \Gamma^*$. By -\tagrefs{prfSC/{fol:seq:prv:thm:provability-quantifiers},prfND/{fol:ntd:prv:thm:provability-quantifiers}} -together with -\iftag{cmplMCS}{\olref[mcs]{prop:mcs}\olref[mcs]{prop:mcs-prov-in},}{} -\iftag{cmplCCS}{\olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-prov-in},}{} -$!B(t) \in \Gamma^*$ for every term~$t \in \Domain{M(\Gamma^*)}$. By -inductive hypothesis, $\Sat{M(\Gamma^*)}{!B(t)}$ for every term~$t \in -\Domain{M(\Gamma^*)}$. Let $s$ be the variable assigment with $s(x) = -t$. Then $\Sat{M(\Gamma^*)}{!B(x)}[s]$ for any such~$s$, hence -$\Sat{M(\Gamma^*)}{\indfrm}$.}}}{} + \iftag{probAll}{% + \indcase!{!A}{\lforall[x][!B(x)]}{}}{% + \indcase{!A}{\lforall[x][!B(x)]}{$\Sat{M(\Gamma^*)}{\indfrm}$ iff + $\Sat{M(\Gamma^*)}{!B(t)}$ for all terms~$t$ + (\olref{prop:quant-termmodel}). By induction hypothesis, this + is the case iff $!B(t) \in \Gamma^*$ for all terms~$t$, by + \olref[hen]{prop:saturated-instances}, this in turn is the case + iff $\lforall[x][!A(x)] \in \Gamma^*$.}}}{} \tagitem{prvEx}{% \iftag{probEx}{% - \indcase!{!A}{\lexists[x][!B(x)]}{}}{% - \indcase{!A}{\lexists[x][!B(x)]}{First suppose that - $\Sat{M(\Gamma^*)}{\indfrm}$. By the definition of satisfaction, - for some variable assignment $s$, - $\Sat{M(\Gamma^*)}{!B(x)}[s]$. The value $s(x)$ is some term~$t - \in \Domain{M(\Gamma^*)}$. Thus, $\Sat{M(\Gamma^*)}{!B(t)}$, and - by our induction hypothesis, $!B(t) \in \Gamma^*$. By - \tagrefs{prfSC/{fol:seq:prv:thm:provability-quantifiers},prfND/{fol:ntd:prv:thm:provability-quantifiers}} - we have $\Gamma^* \Proves \lexists[x][!B(x)]$. Then, by - \iftag{cmplMCS}{\olref[mcs]{prop:mcs}\olref[mcs]{prop:mcs-prov-in},}{} - \iftag{cmplCCS}{\olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-prov-in},}{} - we can conclude that $\indfrm \in \Gamma^*$. - - Conversely, suppose that $\lexists[x][!B(x)] \in - \Gamma^*$. Because $\Gamma^*$ is saturated, $(\lexists[x][!B(x)] - \lif !B(c)) \in \Gamma^*$. By - \tagrefs{prfSC/{fol:seq:prv:prop:provability-mp},prfND/{fol:ntd:prv:prop:provability-mp}} - together with - \iftag{cmplMCS}{\olref[mcs]{prop:mcs}\olref[mcs]{prop:mcs-prov-in},}{} - \iftag{cmplCCS}{\olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-prov-in},}{} - $!B(c) \in \Gamma^*$. By inductive hypothesis, - $\Sat{M(\Gamma^*)}{!B(c)}$. Now consider the variable assignment - with $s(x) = \Assign{c}{M(\Gamma^*)}$. Then - $\Sat{M(\Gamma^*)}{!B(x)}[s]$. By definition of satisfaction, - $\Sat{M(\Gamma^*)}{\lexists[x][!B(x)]}$.}}}{} + \indcase!{!A}{\lexists[x][!B(x)]}{}}{% + \indcase{!A}{\lexists[x][!B(x)]}{$\Sat{M(\Gamma^*)}{\indfrm}$ iff + $\Sat{M(\Gamma^*)}{!B(t)}$ for at least one term~$t$ + (\olref{prop:quant-termmodel}). By induction hypothesis, this + is the case iff $!B(t) \in \Gamma^*$ for at least one term~$t$. + By \olref[hen]{prop:saturated-instances}, this in turn is the + case iff $\lexists[x][!A(x)] \in \Gamma^*$.}}}{} \end{enumerate} \end{proof} diff --git a/content/first-order-logic/completeness/henkin-expansions.tex b/content/first-order-logic/completeness/henkin-expansions.tex index c1e6ff80..a9953666 100755 --- a/content/first-order-logic/completeness/henkin-expansions.tex +++ b/content/first-order-logic/completeness/henkin-expansions.tex @@ -12,10 +12,10 @@ \begin{explain} Part of the challenge in proving the completeness theorem is that the -model we construct from a maximally consistent set~$\Gamma$ must make +model we construct from a complete consistent set~$\Gamma$ must make all the quantified !!{formula}s in~$\Gamma$ true. In order to guarantee this, we use a trick due to Leon Henkin. In essence, the -trick consists in expanding the language by infinitely many constants +trick consists in expanding the language by infinitely many !!{constant}s and adding, for each !!{formula} with one free !!{variable} $!A(x)$ a formula of the form \iftag{prvEx} @@ -29,103 +29,110 @@ among the new constants. \end{explain} -\begin{lem} -\ollabel{defn:lang-exp} +\begin{prop} +\ollabel{prop:lang-exp} If $\Gamma$ is consistent in $\Lang L$ and $\Lang L'$ is obtained from -$\Lang L$ by adding !!a{denumerable} set of new !!{constant}s $\Obj d_1$, -$\Obj d_2$, \dots, then $\Gamma$ is consistent in~$\Lang L'$. -\end{lem} +$\Lang L$ by adding !!a{denumerable} set of new !!{constant}s $\Obj d_0$, +$\Obj d_1$, \dots, then $\Gamma$ is consistent in~$\Lang L'$. +\end{prop} \begin{defn}[Saturated set] A set $\Gamma$ of !!{formula}s of a language $\Lang {L}$ is -\emph{saturated} if and only if for each !!{formula} $!A \in \Frm[L]$ -and !!{variable}~$x$ there is a !!{constant} $c$ such that +\emph{saturated} iff for each !!{formula} $!A(x) \in \Frm[L]$ with one +free !!{variable}~$x$ there is a !!{constant}~$c \in \Lang{L}$ such +that \iftag{prvEx} - {$\lexists[x][!A] \lif !A(c) \in \Gamma$} - {$\lnot\lforall[x][!A] \lif \lnot !A(c) \in \Gamma$}. + {$\lexists[x][!A(x)] \lif !A(c) \in \Gamma$} + {$\lnot\lforall[x][!A(x)] \lif \lnot !A(c) \in \Gamma$}. \end{defn} The following definition will be used in the proof of the next theorem. \begin{defn} -Let $\Lang L'$ be as in \olref{defn:lang-exp}. Fix an enumeration -$\tuple{!A_1, x_1}$, $\tuple{!A_2, x_2}$, \dots of all -!!{formula}-!!{variable} pairs of~$\Lang L'$. We define the -!!{sentence}s~$!D_n$ by recursion on~$n$. Assuming that $!D_1$, -\dots,~$!D_n$ have already been defined, let $c_{n+1}$ be the first -new !!{constant} among the~$\Obj d_i$ that does not occur in $!D_1$, -\dots,~$!D_n$, and let $!D_{n+1}$ be the !!{formula} \iftag{prvEx} - {$\lexists[x_{n+1}][!A_{n+1}(x_{n+1})] \lif !A_{n+1}(c_{n+1})$} - {$\lnot\lforall[x_{n+1}][!A_{n+1}(x_{n+1})] \lif \lnot - !A_{n+1}(c_{n+1})$}. This includes the case where $n = 0$ and - the list of previous $!D_i$'s is empty, i.e., $!D_1$ is - \iftag{prvEx} {$\lexists[x_1][!A_1] \lif !A_1(c_1)$} - {$\lnot\lforall[x_1][!A_1] \lif \lnot !A_1(c_1)$}. +\ollabel{defn:henkin-exp} +Let $\Lang L'$ be as in \olref{prop:lang-exp}. Fix an enumeration +$!A_0(x_0)$, $!A_1(x_1)$, \dots of all !!{formula}s~$!A_i(x_i)$ +of~$\Lang L'$ in which one variable ($x_i$) occurs free. We define +the !!{sentence}s~$!D_n$ by induction on~$n$. + +Let $c_0$ be the first !!{constant} among the $\Obj d_i$ we added +to~$\Lang{L}$ which does not occur in~$!A_0(x_0)$. Assuming that +$!D_0$, \dots,~$!D_{n-1}$ have already been defined, let $c_n$ be the +first among the new !!{constant}s~$\Obj d_i$ that occurs neither in +$!D_0$, \dots,~$!D_{n-1}$ nor in~$!A_n(x_n)$. + +Now let $!D_{n}$ be the !!{formula} \iftag{prvEx} +{$\lexists[x_{n}][!A_{n}(x_{n})] \lif + !A_{n}(c_{n})$}{$\lnot\lforall[x_{n}][!A_{n}(x_{n})] \lif \lnot + !A_{n}(c_{n})$}. \end{defn} -\begin{thm} -\ollabel{thm:henkin} +\begin{lem} +\ollabel{lem:henkin} Every consistent set~$\Gamma$ can be extended to a saturated consistent set~$\Gamma'$. -\end{thm} +\end{lem} \begin{proof} Given a consistent set of sentences~$\Gamma$ in a language~$\Lang{L}$, expand the language by adding !!a{denumerable} set of new -!!{constant}s to form~$\Lang{L'}$. By the previous Lemma, $\Gamma$ is still -consistent in the richer language. Further, let $!D_i$ be as in the -previous definition: then $\Gamma \cup \{!D_1, !D_2, \dots\}$ is -saturated by construction. Let +!!{constant}s to form~$\Lang{L'}$. By \olref{prop:lang-exp}, $\Gamma$ +is still consistent in the richer language. Further, let $!D_i$ be as +in \olref{defn:henkin-exp}. Let \begin{align*} \Gamma_0 & = \Gamma \\ -\Gamma_{n+1} & = \Gamma_n \cup \{!D_{n+1} \} +\Gamma_{n+1} & = \Gamma_n \cup \{!D_n \} \end{align*} -i.e., $\Gamma_n = \Gamma \cup \{ !D_1, \dots, !D_n \}$, and let -$\Gamma' = \bigcup_{n} \Gamma_n$. To show that $\Gamma'$ is +i.e., $\Gamma_{n+1} = \Gamma \cup \{ !D_0, \dots, !D_n \}$, and let +$\Gamma' = \bigcup_{n} \Gamma_n$. $\Gamma'$ is clearly saturated. + +If $\Gamma'$ were inconsistent, then for some $n$, $\Gamma_n$ would be +inconsistent (Exercise: explain why). So to show that $\Gamma'$ is consistent it suffices to show, by induction on~$n$, that each set~$\Gamma_n$ is consistent. The induction basis is simply the claim that $\Gamma_0 = \Gamma$ is consistent, which is the hypothesis of the theorem. For the induction -step, suppose that $\Gamma_{n-1}$ is consistent but $\Gamma_n = -\Gamma_{n-1} \cup \{!D_n\}$ is inconsistent. Recall that $!D_n$~is +step, suppose that $\Gamma_{n}$ is consistent but $\Gamma_{n+1} = +\Gamma_n \cup \{!D_n\}$ is inconsistent. Recall that $!D_n$~is \iftag{prvEx} {$\lexists[x_{n}][!A_{n}(x_n)] \lif !A_{n}(c_{n})$} -{$\lnot\lforall[x_{n}][!A_{n}(x_n)] \lif \lnot !A_{n}(c_{n})$}. -where $!A(x)$ is a !!{formula} of $\Lang{L'}$ with only the -variable~$x_n$ free and not containing any !!{constant}s~$c_i$ where -$i \ge n$. +{$\lnot\lforall[x_{n}][!A_{n}(x_n)] \lif \lnot !A_{n}(c_{n})$}, +where $!A_n(x_n)$ is a !!{formula} of $\Lang{L'}$ with only the +variable~$x_n$ free. By the way we've chosen the~$c_n$ (see +\olref{defn:henkin-exp}, $c_n$ does not occur in~$A_n(x_n)$ nor +in~$\Gamma_n$. -If $\Gamma_{n-1} \cup \{!D_n\}$ is inconsistent, then $\Gamma_{n-1} +If $\Gamma_n \cup \{!D_n\}$ is inconsistent, then $\Gamma_n \Proves \lnot !D_n$, and hence both of the following hold: \iftag{prvEx}{ \[ -\Gamma_{n-1} \Proves \lexists[x_n][!A_n(x_n)] +\Gamma_n \Proves \lexists[x_n][!A_n(x_n)] \qquad -\Gamma_{n-1} \Proves \lnot !A_n(c_n) +\Gamma_n \Proves \lnot !A_n(c_n) \]}{ \[ -\Gamma_{n-1} \Proves \lnot\lforall[x_n][!A_n(x_n)] +\Gamma_n \Proves \lnot\lforall[x_n][!A_n(x_n)] \qquad -\Gamma_{n-1} \Proves !A_n(c_n) +\Gamma_n \Proves !A_n(c_n) \]} -Here $c_n$ does not occur in $\Gamma_{n-1}$ or $!A_n(x_n)$ (remember, -it was added only with~$!D_n$). By -\tagrefs{prfSC/{fol:seq:prv:thm:strong-generalization},prfND/{fol:ntd:prv:thm:strong-generalization}}, -from \iftag{prvEx} -{$\Gamma \Proves \lnot !A_n(c_n)$} -{$\Gamma \Proves !A_n(c_n)$}, +Since $c_n$ does not occur in +$\Gamma_n$ or in~$!A_n(x_n)$, +\tagrefs{prfSC/{fol:seq:prv:thm:strong-generalization},prfND/{fol:ntd:prv:thm:strong-generalization}} applies. +From \iftag{prvEx} +{$\Gamma_n \Proves \lnot !A_n(c_n)$} +{$\Gamma_n \Proves !A_n(c_n)$}, we obtain \iftag{prvEx} -{$\Gamma \Proves \lforall[x_n][\lnot !A_n(x_n)]$} -{$\Gamma \Proves \lforall[x_n][!A_n(x_n)]$}. +{$\Gamma_n \Proves \lforall[x_n][\lnot !A_n(x_n)]$} +{$\Gamma_n \Proves \lforall[x_n][!A_n(x_n)]$}. Thus we have that both \iftag{prvEx} -{$\Gamma_{n-1} \Proves \lexists[x_n][!A_n]$ and -$\Gamma_{n-1} \Proves \lforall[x_n][\lnot !A_n(x_n)]$} -{$\Gamma_{n-1} \Proves \lnot\lforall[x_n][!A_n(x_n)]$ and -$\Gamma_{n-1} \Proves \lforall[x_n][!A_n(x_n)]$}, -so $\Gamma$ itself is inconsistent. +{$\Gamma_n \Proves \lexists[x_n][!A_n]$ and +$\Gamma_n \Proves \lforall[x_n][\lnot !A_n(x_n)]$} +{$\Gamma_n \Proves \lnot\lforall[x_n][!A_n(x_n)]$ and +$\Gamma_n \Proves \lforall[x_n][!A_n(x_n)]$}, +so $\Gamma_n$ itself is inconsistent. \iftag{prvEx} {(Note that \iftag{prvAll} @@ -135,8 +142,69 @@ $\lnot\lexists[x_n][\lnot\lnot !A_n(x_n)]$ and $\lnot\lexists[x_n][\lnot\lnot !A_n(x_n)] \Proves \lnot\lexists[x_n][!A_n(x_n)]$}.)}{} -Contradiction: $\Gamma_{n-1}$ was supposed to be consistent. Hence +Contradiction: $\Gamma_n$ was supposed to be consistent. Hence $\Gamma_n \cup \{ !D_n\}$ is consistent. \end{proof} +\begin{explain} +We'll now show that \emph{complete}, consistent sets which are +saturated have the property that \iftag{prvAll}{it contains a + universally quantified !!{sentence} iff it contains all its + instances}{}\iftag{defAll,defEx}{}{ and }\iftag{prvAll}{it contains an + existentially quantified !!{sentence} iff it contains at least one + instance}{}. We'll use this to show that the !!{structure} we'll +generate from a complete, consistent, saturated set makes all its +quantified sentences true. +\end{explain} + +\begin{prop}\ollabel{prop:saturated-instances} +Suppose $\Gamma$ is complete, consistent, 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}{$\lexists[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{proof} + \iftag{defAll,defEx}{}{\begin{enumerate}\item} + \iftag{prvAll}{% + \iftag{probAll}{Exercise.}{Suppose that $!A(t) \in \Gamma$ for + all closed terms~$t$. By way of contradiction, assume + $\lforall[x][!A(x)] \notin \Gamma$. Since $\Gamma$ is complete, + $\lnot\lforall[x][!A(x)] \in \Gamma$. By saturation, + \iftag{prvEx}{$(\lexists[x][\lnot !A(x)] \lif \lnot !A(c)) \in + \Gamma$}{$(\lnot\lforall[x][!A(x)] \lif \lnot !A(c)) \in + \Gamma$} for some !!{constant}~$c$. By assumption, since $c$ + is a closed term, $!A(c) \in \Gamma$. But this would make + $\Gamma$ inconsistent. (Exercise: give the derivation that shows + \[ + \lnot \lforall[x][!A(x)], + \iftag{prvEx}{\lexists[x][\lnot !A(x)] \lif \lnot + !A(c)}{\lnot\lforall[x][!A(x)] \lif \lnot + !A(c)}, !A(c) \Proves \lfalse.) + \] + + For the reverse direction, we do not need saturation: Suppose + $\lforall[x][!A(x)] \in \Gamma$. Since $\lforall[x][!A(x)] + \Proves !A(t)$, $!A(t) \in \Gamma$ by \olref[ccs]{prop:ccs}.}}{} + \iftag{defAll,defEx}{}{\item} + \iftag{prvEx}{% + \iftag{probEx}{Exercise.}{First suppose that $\lexists[x][!A(x)] + \in \Gamma$. Because $\Gamma$ is saturated, + $(\lexists[x][!A(x)] \lif !A(c)) \in \Gamma$ for some + !!{constant}~$c$. By + \tagrefs{prfSC/{fol:seq:prv:prop:provability-mp},prfND/{fol:ntd:prv:prop:provability-mp}} + and \olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-prov-in}, $!A(c) + \in \Gamma$. + + For the other direction, satisfaction is not necessary: Suppose + $!A(t) \in \Gamma$. Then $!A(t) \Proves \lexists[x][!A(x)]$ and by + \olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-prov-in}, + $\lexists[x][!A(x)] \in \Gamma$.}}{} + + \iftag{defAll,defEx}{}{\end{enumerate}} +\end{proof} \end{document} diff --git a/content/first-order-logic/completeness/identity.tex b/content/first-order-logic/completeness/identity.tex index 78467572..be76111b 100644 --- a/content/first-order-logic/completeness/identity.tex +++ b/content/first-order-logic/completeness/identity.tex @@ -24,11 +24,9 @@ \end{explain} \begin{defn} - Let $\Gamma^*$ be a - \iftag{cmplMCS}{maximally consistent}{} - \iftag{cmplCCS}{consistent and !!{complete}}{} - set of sentences in~$\Lang L$. We define the relation $\approx$ on - the set of closed terms of~$\Lang L$ by + Let $\Gamma^*$ be a consistent and !!{complete} set of sentences + in~$\Lang L$. We define the relation $\approx$ on the set of closed + terms of~$\Lang L$ by \[ t \approx t' \text{\quad iff \quad} \eq[t][t'] \in \Gamma^* \] @@ -57,11 +55,9 @@ \end{prop} \begin{proof} - Since $\Gamma^*$ is - \iftag{cmplMCS}{maximally consistent,}{} - \iftag{cmplCCS}{consistent and complete,}{} - $\eq[t][t'] \in \Gamma^*$ iff $\Gamma^* \Proves \eq[t][t']$. Thus - it is enough to show the following: +Since $\Gamma^*$ is consistent and !!{complete}, $\eq[t][t'] \in +\Gamma^*$ iff $\Gamma^* \Proves \eq[t][t']$. Thus it is enough to +show the following: \begin{enumerate} \item $\Gamma^* \Proves \eq[t][t]$ for all terms~$t$. \item If $\Gamma^* \Proves \eq[t][t']$ then $\Gamma^* \Proves \eq[t'][t]$. @@ -88,11 +84,9 @@ \end{prob} \begin{defn} - Suppose $\Gamma^*$ is a - \iftag{cmplMCS}{maximally consistent}{} - \iftag{cmplCCS}{consistent and !!{complete}}{} - set in a language~$\Lang -L$, $t$ is a term, and $\approx$ as in the previous definition. Then: +Suppose $\Gamma^*$ is a consistent and !!{complete} set in a +language~$\Lang L$, $t$ is a term, and $\approx$ as in the previous +definition. Then: \[ [t]_\approx = \Setabs{t'}{t'\in \Trm[L], t \approx t'} \] @@ -101,8 +95,9 @@ \begin{defn} \ollabel{defn:term-model-factor} -Let $\Struct M = \Struct M(\Gamma^*)$ be the term model for~$\Gamma^*$. Then -$\Struct M/_\approx$ is the following !!{structure}: +Let $\Struct M = \Struct M(\Gamma^*)$ be the term model +for~$\Gamma^*$. Then $\Struct M/_\approx$ is the following +!!{structure}: \begin{enumerate} \item $\Domain{M/_\approx} = \Trm[L]/_\approx$. \item $\Assign{c}{M/_\approx} = [c]_\approx$ @@ -126,9 +121,9 @@ $[t]_\approx \in \Assign{R}{M/_\approx}$ iff $\Sat{M}{\Atom{R}{t}}$. If for some other term~$t'$ with $t \approx t'$, $\Sat/{M}{\Atom{R}{t}}$, then the definition would require -$[t']_\approx \notin \Assign{R}{M/_\approx}$. If $t \approx t'$, -then $[t]_\approx = [t']_\approx$, but we can't have both $[t]_\approx -\in \Assign{R}{M/_\approx}$ and $[t]_\approx \notin +$[t']_\approx \notin \Assign{R}{M/_\approx}$. If $t \approx t'$, then +$[t]_\approx = [t']_\approx$, but we can't have both $[t]_\approx \in +\Assign{R}{M/_\approx}$ and $[t]_\approx \notin \Assign{R}{M/_\approx}$. However, \olref{prop:approx-equiv} guarantees that this cannot happen. \end{explain} diff --git a/content/first-order-logic/completeness/lindenbaums-lemma.tex b/content/first-order-logic/completeness/lindenbaums-lemma.tex index 0457c592..370e3328 100755 --- a/content/first-order-logic/completeness/lindenbaums-lemma.tex +++ b/content/first-order-logic/completeness/lindenbaums-lemma.tex @@ -11,26 +11,21 @@ We now prove a lemma that shows that any consistent set of !!{sentence}s is contained in some set of sentences which is not just -consistent, but -\iftag{cmplMCS}{maximally consistent}{} -\iftag{cmplCCS}{also !!{complete}}{}, and moreover, is saturated. The proof -works by first extending the set to a saturated set, and then adding -one sentence at a time, guaranteeing at each step -that the set remains consistent. The union of all stages in that -construction then contains, for each !!{sentence}~$!A$, either it or -its negation~$\lnot !A$, is saturated, and is also consistent. +consistent, but also !!{complete}, and moreover, is saturated. The +proof works by first extending the set to a saturated set, and then +adding one sentence at a time, guaranteeing at each step that the set +remains consistent. The union of all stages in that construction then +contains, for each !!{sentence}~$!A$, either it or its negation~$\lnot +!A$, is saturated, and is also consistent. \begin{lem}[Lindenbaum's Lemma] -\ollabel{lem:lindenbaum} -Every consistent set~$\Gamma$ can be extended to a -\iftag{cmplMCS}{maximally consistent}{} -\iftag{cmplCCS}{!!{complete} and consistent}{}, -saturated set~$\Gamma^*$. +\ollabel{lem:lindenbaum} Every consistent set~$\Gamma$ can be extended +to a !!{complete}, consistent, and saturated set~$\Gamma^*$. \end{lem} \begin{proof} Let $\Gamma$ be consistent, and let $\Gamma'$ be as in the proof of -\olref[hen]{thm:henkin}: we proved there that $\Gamma'$ +\olref[hen]{lem:henkin}: we proved there that $\Gamma'$ is a consistent saturated set in the richer language $\Lang L'$ (with the !!{denumerable} set of new constants). Let $!A_0$, $!A_1$, \dots{} be an enumeration of all the !!{formula}s of~$\Lang L'$. Define @@ -52,22 +47,19 @@ {$\lnot\lforall[x][!A] \lif \lnot !A(c)$} and thus is saturated. -Each $\Gamma_n$ is consistent: $\Gamma_0$ is consistent by -definition. If $\Gamma_{n+1} = \Gamma_n \cup \{!A\}$, this is because -the latter is consistent. If it isn't, $\Gamma_{n+1} = \Gamma_n \cup -\{!\lnot !A\}$, which must be consistent. If it weren't, i.e., both -$\Gamma_n \cup \{!A\}$ and $\Gamma_n \cup \{\lnot !A\}$ are -inconsistent, then $\Gamma_n \Proves \lnot !A$ and $\Gamma_n \Proves -!A$, so $\Gamma_n$ would be inconsistent contrary to the induction -hypothesis. +Each $\Gamma_n$ is consistent: $\Gamma_0$ is consistent by definition. +If $\Gamma_{n+1} = \Gamma_n \cup \{!A_n\}$, this is because the latter +is consistent. If it isn't, $\Gamma_{n+1} = \Gamma_n \cup \{\lnot +!A_n\}$. We have to verify that $\Gamma_n \cup \{\lnot !A_n\}$ is +consistent. Suppose it's not. Then \emph{both} $\Gamma_n \cup \{!A_n\}$ +and $\Gamma_n \cup \{\lnot !A_n\}$ are inconsistent. So $\Gamma_n +\Proves \lnot !A_n$ and $\Gamma_n \Proves !A_n$, and $\Gamma_n$ would be +inconsistent contrary to the induction hypothesis. -Every !!{formula} of $\Frm[L']$ appears on the list used to +Every !!{sentence} of $\Frm[L']$ appears on the list used to define~$\Gamma^*$. If $!A_n \notin \Gamma^*$, then that is because -$\Gamma_n \cup \{!A_n\}$ was inconsistent. -\iftag{cmplMCS}{But that means that $\Gamma^*$ is maximally - consistent.} -\iftag{cmplCCS}{But then $\lnot !A_n \notin \Gamma^*$, so $\Gamma^*$ - is !!{complete}.} +$\Gamma_n \cup \{!A_n\}$ was inconsistent. But then $\lnot !A_n +\in \Gamma^*$, so $\Gamma^*$ is !!{complete}. \end{proof} \end{document} diff --git a/content/first-order-logic/completeness/outline.tex b/content/first-order-logic/completeness/outline.tex index 2c99e995..5781fdec 100644 --- a/content/first-order-logic/completeness/outline.tex +++ b/content/first-order-logic/completeness/outline.tex @@ -53,14 +53,17 @@ This suggests the following idea: we add additional sentences to $\Gamma$ so as to (a) keep the resulting set consistent and (b) make sure that for every possible atomic sentence $!A$, either $!A$ is in -the resulting set, or $\lnot !A$, and (c) such that, whenever $!A \land -!B$ is in the set, so are both $!A$ and $!B$, if $!A \lor !B$ is in -the set, at least one of $!A$ or $!B$ is also, etc. We keep doing this -(potentially forever). Call the set of all sentences so +the resulting set, or $\lnot !A$, and (c) such that, whenever $!A +\land !B$ is in the set, so are both $!A$ and $!B$, if $!A \lor !B$ is +in the set, at least one of $!A$ or $!B$ is also, etc. We keep doing +this (potentially forever). Call the set of all sentences so added~$\Gamma^*$. Then our construction above would provide us with a structure for which we could prove, by induction, that all sentences in~$\Gamma^*$ are true in~$\Struct M$, and hence also all sentence -in~$\Gamma$ since $\Gamma \subseteq \Gamma^*$. +in~$\Gamma$ since $\Gamma \subseteq \Gamma^*$. It turns out that +guaranteeing (a) is enough. A set of sentences for which (a) holds is +called \emph{complete}. So our task will be to extend the consistent +set~$\Gamma$ to a consistent and complete set~$\Gamma^*$. There is one wrinkle in this plan: if $\lexists[x][!A(x)] \in \Gamma$ we would hope to be able to pick some !!{constant}~$c$ and add $!A(c)$ @@ -114,4 +117,34 @@ $\eq[(\Obj 0+ \Obj 0)][\Obj 0]$ will be true in this revised !!{structure}. +So here's what we'll do. First we investigate the properties of +!!{complete} consistent sets, in particular we prove that +!!a{complete} consistent set contains $!A \land !B$ iff it contains +both $!A$ and~$!B$, $!A \lor !B$ iff it contains at least one of them, +etc. (\olref[ccs]{prop:ccs}). Then we define and investigate +``saturated'' sets of sentences. A saturated set is one which contains +conditionals that link each quantified !!{sentence} to instances of it +(\olref[hen]{defn:henkin-exp}). We show that any consistent +set~$\Gamma$ can always be extended to a saturated set~$\Gamma'$ +(\olref[hen]{lem:henkin}). If a set is consistent, saturated, and +!!{complete} it also has the property that it contains +\iftag{prvEx}{$\lexists[x][!A(x)]$ iff it contains $!A(t)$ for some + closed term~$t$}{}\iftag{defEx,defAll}{}{ and +}\iftag{prvAll}{$\lforall[x][!A(x)]$ iff it contains $!A(t)$ for all + closed terms~$t$}{} (\olref[hen]{prop:saturated-instances}). We'll +then take the saturated consistent set~$\Gamma'$ and show that it can +be extended to a saturated, consistent, and !!{complete} +set~$\Gamma^*$ (\olref[lin]{lem:lindenbaum}). This set $\Gamma^*$ is +what we'll use to define our term model~$\Struct{M(\Gamma^*)}$. The +term model has the set of closed terms as its domain, and the +interpretation of its !!{predicate}s is given by the atomic +!!{sentence}s in~$\Gamma^*$ (\olref[mod]{defn:termmodel}). We'll use +the properties of consistent, complete, saturated sets to show that +indeed $\Sat{M(\Gamma^*)}{!A}$ iff $!A \in \Gamma^*$ +(\olref[mod]{lem:truth}), and thus in particular, +$\Sat{M(\Gamma^*)}{\Gamma}$. Finally, we'll consider how to define a +term model if $\Gamma$ contains~$\eq$ as well +(\olref[ide]{defn:term-model-factor}) and show that it +satisfies~$\Gamma^*$ (\olref[ide]{lem:truth}). + \end{document} diff --git a/content/first-order-logic/natural-deduction/provability.tex b/content/first-order-logic/natural-deduction/provability.tex index fa6cc45c..3e63f63a 100644 --- a/content/first-order-logic/natural-deduction/provability.tex +++ b/content/first-order-logic/natural-deduction/provability.tex @@ -73,6 +73,16 @@ \] \end{proof} +\begin{prop} + \ollabel{prop:explicit-inc} If $\Gamma \Proves !A$ and + $\Gamma \Proves \lnot !A$, then $\Gamma$ is inconsistent. +\end{prop} + +\begin{proof} + This is a simple application of the $\Intro{\lfalse}$ rule. +\end{proof} + + \begin{prop} \ollabel{prop:provability-exhaustive} If $\Gamma \cup \{!A\} \Proves \lfalse$ and $\Gamma \cup \{\lnot !A\} \Proves \lfalse$, then $\Gamma diff --git a/content/first-order-logic/syntax-and-semantics/assignments.tex b/content/first-order-logic/syntax-and-semantics/assignments.tex index ae68a613..8b204f7c 100644 --- a/content/first-order-logic/syntax-and-semantics/assignments.tex +++ b/content/first-order-logic/syntax-and-semantics/assignments.tex @@ -229,9 +229,18 @@ If $\Sat{M}{!A}$, we also simply say that \emph{$!A$ is true in~$\Struct{M}$.} +\begin{prop} +\ollabel{prop:sentence-sat-true} +Let $!A$ be a sentence, and $s$ a variable assignment. +$\Sat{M}{!A}$ iff $\Sat{M}{!A}[s]$. +\end{prop} + +\begin{proof} +Exercise. +\end{proof} + \begin{prob} -Show that if $!A$ is a sentence, $\Sat{M}{!A}$ iff \emph{there is} a -!!{variable} assignment~$s$ so that $\Sat{M}{!A}[s]$. +Prove \olref[fol][syn][ass]{prop:sentence-sat-true} \end{prob} \begin{prop}