The Open Logic Text — accessible offline edition

The Completeness Theorem — Source and provenance

The Completeness Theorem

Source and provenance

All 12 authority files and 1854 lines are shown exactly. The projected chapter slice is byte-checked at SHA-256 3f6186470ab3bfacdaabb2268f9e16150a039bf6c8144d5d2f40d7c8567a3794. AI production model: OpenAI Codex gpt-5.6-sol, Ultra. Source authorship remains with the credited Open Logic Project contributors.

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

42 lines; SHA-256 35cbcfc7f12046ceabc5c4407c43817d71d3907e9e9d57a1b5928fcbe10c672c. Open preserved source.

  1. % Part: first-order-logic
  2. % Chapter: completeness
  4. \documentclass[../../../include/open-logic-chapter]{subfiles}
  6. \begin{document}
  8. \iftag{FOL}
  9. {\olchapter{fol}{com}{The Completeness Theorem}}
  10. {\olchapter{pl}{com}{The Completeness Theorem}}
  12. \olimport{introduction}
  14. \olimport{outline}
  16. \olimport{complete-consistent-sets}
  18. \iftag{FOL}{%
  19. \olimport{henkin-expansions}
  20. }{}
  22. \olimport{lindenbaums-lemma}
  24. \olimport{construction-of-model}
  26. \iftag{FOL}{%
  27. \olimport{identity}
  28. }{}
  30. \olimport{completeness-thm}
  32. \olimport{compactness}
  34. \olimport{compactness-direct}
  36. \iftag{FOL}{%
  37. \olimport{downward-ls}
  38. }{}
  40. \OLEndChapterHook
  42. \end{document}

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

75 lines; SHA-256 40a994a78343dccb102c8347722a6eb85fd3a12dd4c6565a37960f7b24673500. Open preserved source.

  1. % Part: first-order-logic
  2. % Chapter: completeness
  3. % Section: introduction
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{com}{int}}
  11. {\olfileid{pl}{com}{int}}
  13. \olsection{Introduction}
  15. The completeness theorem is one of the most fundamental results about
  16. logic. It comes in two formulations, the equivalence of which we'll
  17. prove. In its first formulation it says something fundamental about
  18. the relationship between semantic consequence and our !!{derivation}
  19. system: if !!a{sentence}~$!A$ follows from some !!{sentence}s
  20. $\Gamma$, then there is also !!a{derivation} that establishes $\Gamma
  21. \Proves !A$. Thus, the !!{derivation} system is as strong as it can
  22. possibly be without proving things that don't actually follow.
  24. In its second formulation, it can be stated as a model existence
  25. result: every consistent set of !!{sentence}s is satisfiable.
  26. Consistency is a proof-theoretic notion: it says that our
  27. !!{derivation} system is unable to produce certain !!{derivation}s.
  28. But who's to say that just because there are no !!{derivation}s of a
  29. certain sort from~$\Gamma$, it's guaranteed that there is
  30. \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!{valuation}{~$\pAssign{v}$}
  31. with $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$}? Before the
  32. completeness theorem was first proved---in fact before we had the
  33. !!{derivation} systems we now do---the great German mathematician
  34. David Hilbert held the view that consistency of mathematical theories
  35. guarantees the existence of the objects they are about. He put it as
  36. follows in a letter to Gottlob Frege:
  37. \begin{quote}
  38. If the arbitrarily given axioms do not contradict one another with
  39. all their consequences, then they are true and the things defined by
  40. the axioms exist. This is for me the criterion of truth and
  41. existence.
  42. \end{quote}
  43. Frege vehemently disagreed. The second formulation of the completeness
  44. theorem shows that Hilbert was right in at least the sense that if the
  45. axioms are consistent, then \emph{some}
  46. \iftag{FOL}{!!{structure}}{!!{valuation}} exists that makes them all
  47. true.
  49. These aren't the only reasons the completeness theorem---or rather,
  50. its proof---is important. It has a number of important consequences,
  51. some of which we'll discuss separately. For instance, since any
  52. !!{derivation} that shows $\Gamma \Proves !A$ is finite and so can
  53. only use finitely many of the !!{sentence}s in~$\Gamma$, it follows by
  54. the completeness theorem that if $!A$ is a consequence of~$\Gamma$, it
  55. is already a consequence of a finite subset of~$\Gamma$. This is
  56. called \emph{compactness}. Equivalently, if every finite subset of
  57. $\Gamma$ is consistent, then $\Gamma$ itself must be consistent.
  59. Although the compactness theorem follows from the completeness theorem
  60. via the detour through !!{derivation}s, it is also possible to use the
  61. \emph{the proof of} the completeness theorem to establish it
  62. directly. For what the proof does is take a set of !!{sentence}s with
  63. a certain property---consistency---and constructs !!a{structure} out
  64. of this set that has certain properties (in this case, that it
  65. satisfies the set). Almost the very same construction can be used to
  66. directly establish compactness, by starting from ``finitely
  67. satisfiable'' sets of !!{sentence}s instead of consistent ones.
  68. \iftag{FOL}{The construction also yields other consequences, e.g.,
  69. that any satisfiable set of !!{sentence}s has a finite or
  70. !!{denumerable}s model. (This result is called the
  71. L\"owenheim--Skolem theorem.) In general, the construction of
  72. !!{structure}s from sets of !!{sentence}s is used often in logic,
  73. and sometimes even in philosophy.}{}
  75. \end{document}

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

170 lines; SHA-256 e86bb4893ff5da65af4fa5b8b7eebec5807e0b4aa0562ca5388fac369aec642e. Open preserved source.

  1. % Part: first-order-logic
  2. % Chapter: completeness
  3. % Section: outline
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{com}{out}}
  11. {\olfileid{pl}{com}{out}}
  13. \olsection{Outline of the Proof}
  15. The proof of the completeness theorem is a bit complex, and upon first
  16. reading it, it is easy to get lost. So let us outline the proof. The
  17. first step is a shift of perspective, that allows us to see a route to
  18. a proof. When completeness is thought of as ``whenever $\Gamma
  19. \Entails !A$ then $\Gamma \Proves !A$,'' it may be hard to even come
  20. up with an idea: for to show that $\Gamma \Proves !A$ we have to find
  21. !!a{derivation}, and it does not look like the hypothesis that
  22. $\Gamma \Entails !A$ helps us for this in any way. For some proof
  23. systems it is possible to directly construct !!a{derivation}, but we
  24. will take a slightly different approach. The shift in perspective
  25. required is this: completeness can also be formulated as: ``if
  26. $\Gamma$ is consistent, it is satisfiable.'' Perhaps we can use the
  27. information in~$\Gamma$ together with the hypothesis that it is
  28. consistent to construct \iftag{FOL}{!!a{structure}}{!!a{valuation}}
  29. that satisfies every \iftag{FOL}{!!{sentence}}{!!{formula}}
  30. in~$\Gamma$. After all, we know
  31. what kind of \iftag{FOL}{!!{structure}}{!!{valuation}} we are looking
  32. for: one that is as $\Gamma$ describes it!{}
  34. If $\Gamma$ contains only \iftag{FOL}{atomic
  35. !!{sentence}s}{!!{propositional variable}s}, it is easy to construct
  36. a model for it.\iftag{FOL}{ Suppose the atomic !!{sentence}s are all
  37. of the form $\Atom{P}{a_1,\dots,a_n}$ where the $a_i$ are
  38. !!{constant}s.}{} All we have to do is come up with
  39. \iftag{FOL}{%
  40. !!a{domain}~$\Domain{M}$ and an assignment for~$P$ so that
  41. $\Sat{M}{\Atom{P}{a_1,\ldots,a_n}}$. But that's not very hard:
  42. put $\Domain{M} = \Nat$, $\Assign{\Obj c_i}{M} = i$, and for every
  43. $\Atom{P}{a_1,\ldots,a_n} \in \Gamma$, put the tuple $\tuple{k_1,
  44. \dots, k_n}$ into $\Assign{P}{M}$, where $k_i$ is the index of the
  45. constant symbol~$a_i$ (i.e., $a_i \ident \Obj c_{k_i}$).}{%
  46. !!a{valuation}~$\pAssign{v}$ such that $\pSat{v}{p}$ for all $p \in
  47. \Gamma$. Well, let $\pAssign{v}(p) = \True$ iff $p \in \Gamma$.}
  49. Now suppose $\Gamma$ contains some !!{formula}~$\lnot !B$, with $!B$
  50. atomic. We might worry that the construction of
  51. $\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ interferes with the possibility
  52. of making $\lnot !B$ true. But here's where the consistency
  53. of~$\Gamma$ comes in: if $\lnot !B \in \Gamma$, then $!B \notin
  54. \Gamma$, or else $\Gamma$ would be inconsistent. And if $!B \notin
  55. \Gamma$, then according to our construction
  56. of~$\iftag{FOL}{\Struct{M}}{\pAssign{v}}$,
  57. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B}$, so
  58. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\lnot !B}$. So far so good.
  60. What if $\Gamma$ contains complex, non-atomic formulas? Say it
  61. contains $!A \land !B$. To make that true, we should proceed as if
  62. both $!A$ and $!B$ were in~$\Gamma$. And if $!A \lor !B \in \Gamma$,
  63. then we will have to make at least one of them true, i.e., proceed as
  64. if one of them was in~$\Gamma$.
  66. This suggests the following idea: we add additional !!{formula}s
  67. to~$\Gamma$ so as to (a)~keep the resulting set consistent and
  68. (b)~make sure that for every possible atomic !!{sentence}~$!A$, either
  69. $!A$ is in the resulting set, or $\lnot !A$ is, and (c)~such that,
  70. whenever $!A \land !B$ is in the set, so are both $!A$ and $!B$, if
  71. $!A \lor !B$ is in the set, at least one of $!A$ or $!B$ is also, etc.
  72. We keep doing this (potentially forever). Call the set of all
  73. !!{formula}s so added~$\Gamma^*$. Then our construction above would
  74. provide us with \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}
  75. for which we could prove, by induction, that it satisfies all sentences
  76. in~$\Gamma^*$, and hence also all sentence in~$\Gamma$
  77. since $\Gamma \subseteq \Gamma^*$. It turns out that guaranteeing (a)
  78. and~(b) is enough. A set of sentences for which (b) holds is called
  79. \emph{complete}. So our task will be to extend the consistent
  80. set~$\Gamma$ to a consistent and complete set~$\Gamma^*$.
  82. \iftag{FOL}{%
  83. There is one wrinkle in this plan: if $\lexists[x][!A(x)] \in \Gamma$
  84. we would hope to be able to pick some !!{constant}~$c$ and add $!A(c)$
  85. in this process. But how do we know we can always do that? Perhaps we
  86. only have a few !!{constant}s in our language, and for each one of
  87. them we have $\lnot !A(c) \in \Gamma$. We can't also add $!A(c)$,
  88. since this would make the set inconsistent, and we wouldn't know
  89. whether $\Struct{M}$ has to make $!A(c)$ or $\lnot !A(c)$ true.
  90. Moreover, it might happen that $\Gamma$ contains only sentences in a
  91. language that has no constant symbols at all (e.g., the language of
  92. set theory).
  94. The solution to this problem is to simply add infinitely many
  95. constants at the beginning, plus sentences that connect them with the
  96. quantifiers in the right way. (Of course, we have to verify that this
  97. cannot introduce an inconsistency.)
  99. Our original construction works well if we only have !!{constant}s in
  100. the atomic sentences. But the language might also contain
  101. !!{function}s. In that case, it might be tricky to find the right
  102. functions on~$\Nat$ to assign to these !!{function}s to make
  103. everything work. So here's another trick: instead of using $i$ to
  104. interpret $\Obj c_i$, just take the set of !!{constant}s itself as the
  105. domain. Then $\Struct M$ can assign every !!{constant} to itself:
  106. $\Assign{\Obj c_i}{M} = \Obj c_i$. But why not go all the way: let
  107. $\Domain{M}$ be all \emph{terms} of the language!{} If we do this,
  108. there is an obvious assignment of functions (that take terms as
  109. arguments and have terms as values) to !!{function}s: we assign to the
  110. !!{function}~$\Obj f^n_i$ the function which, given $n$ terms $t_1$,
  111. \dots,~$t_n$ as input, produces the term $\Obj f^n_i(t_1, \dots, t_n)$
  112. as value.
  114. The last piece of the puzzle is what to do with~$\eq$. The
  115. !!{predicate}~$\eq$ has a fixed interpretation: $\Sat{M}{\eq[t][t']}$
  116. iff $\Value{t}{M} = \Value{t'}{M}$. Now if we set things up so that the
  117. !!{value} of a term~$t$ is $t$ itself, then this !!{structure}
  118. will make \emph{no} sentence of the form $\eq[t][t']$ true
  119. unless $t$ and $t'$ are one and the same term. And of
  120. course this is a problem, since basically every interesting theory in
  121. a language with !!{function}s will have as theorems sentences
  122. $\eq[t][t']$ where $t$ and $t'$ are not the same term (e.g., in
  123. theories of arithmetic: $\eq[(\Obj 0+ \Obj 0)][\Obj 0]$). To solve
  124. this problem, we change the domain of~$\Struct M$: instead of using terms as
  125. the objects in~$\Domain{M}$, we use sets of terms, and each set is so
  126. that it contains all those terms which the sentences in~$\Gamma$
  127. require to be equal. So, e.g., if $\Gamma$ is a theory of arithmetic,
  128. one of these sets will contain: $\Obj 0$, $(\Obj 0 + \Obj 0)$, $(\Obj
  129. 0 \times \Obj 0)$, etc. This will be the set we assign to $\Obj 0$,
  130. and it will turn out that this set is also the value of all the terms
  131. in it, e.g., also of $(\Obj 0 + \Obj 0)$. Therefore, the sentence
  132. $\eq[(\Obj 0+ \Obj 0)][\Obj 0]$ will be true in this revised
  133. !!{structure}.}{}
  135. So here's what we'll do. First we investigate the properties of
  136. !!{complete} consistent sets, in particular we prove that
  137. !!a{complete} consistent set contains $!A \land !B$ iff it contains
  138. both $!A$ and~$!B$, $!A \lor !B$ iff it contains at least one of them,
  139. etc. (\olref[ccs]{prop:ccs}).\iftag{FOL}{ Then we define and
  140. investigate ``saturated'' sets of sentences. A saturated set is one
  141. which contains conditionals that link each quantified !!{sentence}
  142. to instances of it (\olref[hen]{defn:henkin-exp}). We show that any
  143. consistent set~$\Gamma$ can always be extended to a saturated
  144. set~$\Gamma'$ (\olref[hen]{lem:henkin}). If a set is consistent,
  145. saturated, and !!{complete} it also has the property that it
  146. contains \iftag{prvEx}{$\lexists[x][!A(x)]$ iff it contains $!A(t)$
  147. for some closed term~$t$}{}\iftag{defEx,defAll}{}{ and
  148. }\iftag{prvAll}{$\lforall[x][!A(x)]$ iff it contains $!A(t)$ for all
  149. closed terms~$t$}{} (\olref[hen]{prop:saturated-instances}).}{}
  150. We'll then take the\iftag{FOL}{ saturated}{} consistent
  151. set~$\iftag{FOL}{\Gamma'}{\Gamma}$ and show that it can be extended
  152. to a \iftag{FOL}{saturated, consistent, and}{consistent and}
  153. !!{complete} set~$\Gamma^*$ (\olref[lin]{lem:lindenbaum}). This set
  154. $\Gamma^*$ is what we'll use to define our \iftag{FOL}{term
  155. model~$\Struct M(\Gamma^*)$}{!!{valuation}~$\pAssign v(\Gamma^*)$}.
  156. \iftag{FOL}{The term model has the set of closed terms as its domain,
  157. and the interpretation of its !!{predicate}s is given by the atomic
  158. !!{sentence}s}{The valuation is determined by the !!{propositional
  159. variable}s} in~$\Gamma^*$ (\olref[mod]{defn:termmodel}). We'll
  160. use the properties of\iftag{FOL}{ saturated,}{} complete consistent
  161. sets to show that indeed
  162. $\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{!A}$ iff $!A \in
  163. \Gamma^*$ (\olref[mod]{lem:truth}), and thus in particular,
  164. $\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{\Gamma}$.
  165. \iftag{FOL}{Finally, we'll consider how to define a term model if
  166. $\Gamma$ contains~$\eq$ as well
  167. (\olref[ide]{defn:term-model-factor}) and show that it
  168. satisfies~$\Gamma^*$ (\olref[ide]{lem:truth}).}{}
  170. \end{document}

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

223 lines; SHA-256 cf7d517de5d2d257492c66f2cf16347fce490f2d932681a3f6ebd2386e9b1ffd. Open preserved source.

  1. % Part: first-order-logic
  2. % Chapter: completeness
  3. % Section: complete-sets
  5. % Definition of complete consistent sets. Properties of complete sets required
  6. % for completeness proved are in provability.tex in the
  7. % chapter on the proof system used.
  9. \documentclass[../../../include/open-logic-section]{subfiles}
  11. \begin{document}
  13. \iftag{FOL}
  14. {\olfileid{fol}{com}{ccs}}
  15. {\olfileid{pl}{com}{ccs}}
  17. \olsection{Complete Consistent Sets of \usetoken{P}{sentence}}
  19. \begin{defn}[Complete set]
  20. \ollabel{def:complete-set} A set~$\Gamma$ of !!{sentence}s is
  21. \emph{!!{complete}} iff for any !!{sentence}~$!A$, either $!A \in
  22. \Gamma$ or $\lnot !A \in \Gamma$.
  23. \end{defn}
  25. \begin{explain}
  26. !!^{complete} sets of sentences leave no questions unanswered. For
  27. any !!{sentence}~$!A$, $\Gamma$ ``says'' if $!A$ is true or false. The
  28. importance of !!{complete} sets extends beyond the proof of the
  29. completeness theorem. A theory which is !!{complete} and
  30. axiomatizable, for instance, is always decidable.
  31. \end{explain}
  33. \begin{explain}
  34. !!^{complete} consistent sets are important in the completeness proof
  35. since we can guarantee that every consistent set of
  36. !!{sentence}s~$\Gamma$ is contained in !!a{complete} consistent
  37. set~$\Gamma^*$. !!^a{complete} consistent set contains, for each
  38. !!{sentence}~$!A$, either $!A$ or its negation $\lnot !A$, but not
  39. both. This is true in particular for \iftag{FOL}{atomic
  40. !!{sentence}s}{propositional variables}, so from !!a{complete}
  41. consistent set\iftag{FOL}{ in a language suitably expanded by
  42. !!{constant}s}{}, we can construct
  43. \iftag{FOL}{!!a{structure}}{!!a{valuation}} where the
  44. \iftag{FOL}{interpretation of !!{predicate}s}{truth value assigned to
  45. propositional variables} is defined according to which
  46. \iftag{FOL}{atomic !!{sentence}s}{!!{propositional variable}s} are
  47. in~$\Gamma^*$. This \iftag{FOL}{!!{structure}}{!!{valuation}} can then
  48. be shown to make all !!{sentence}s in~$\Gamma^*$ (and hence also all
  49. those in~$\Gamma$) true. The proof of this latter fact requires that
  50. $\lnot !A \in \Gamma^*$ iff $!A \notin \Gamma^*$, $(!A \lor !B) \in
  51. \Gamma^*$ iff $!A \in \Gamma^*$ or $!B \in \Gamma^*$, etc.
  52. \end{explain}
  54. In what follows, we will often tacitly use the properties of
  55. reflexivity, monotonicity, and transitivity of $\Proves$ (see
  56. \iftag{FOL}{%
  57. \tagrefs{prfSC/{fol:seq:ptn:sec},prfND/{fol:ntd:ptn:sec},prfAX/{fol:axd:ptn:sec},prfTab/{fol:tab:ptn:sec}}}{%
  58. \tagrefs{prfSC/{pl:seq:ptn:sec},prfND/{pl:ntd:ptn:sec},prfAX/{pl:axd:ptn:sec},prfTab/{pl:tab:ptn:sec}}}).
  60. \begin{prop}
  61. \ollabel{prop:ccs}
  62. Suppose $\Gamma$ is !!{complete} and consistent. Then:
  63. \begin{enumerate}
  64. \item \ollabel{prop:ccs-prov-in} If $\Gamma \Proves !A$, then $!A \in
  65. \Gamma$.
  67. \tagitem{prvAnd}{\ollabel{prop:ccs-and} $!A \land !B \in \Gamma$
  68. iff both $!A \in \Gamma$ and $!B \in \Gamma$.}{}
  70. \tagitem{prvOr}{\ollabel{prop:ccs-or} $!A \lor !B \in \Gamma$ iff
  71. either $!A \in \Gamma$ or $!B \in \Gamma$.}{}
  73. \tagitem{prvIf}{\ollabel{prop:ccs-if} $!A \lif !B \in \Gamma$ iff
  74. either $!A \notin \Gamma$ or $!B \in \Gamma$.}{}
  75. \end{enumerate}
  76. \end{prop}
  78. \begin{proof}
  79. Let us suppose for all of the following that $\Gamma$ is !!{complete} and
  80. consistent.
  81. \begin{enumerate}
  82. \item If $\Gamma \Proves !A$, then $!A \in \Gamma$.
  84. Suppose that $\Gamma \Proves !A$. Suppose to the contrary that $!A
  85. \notin \Gamma$. Since $\Gamma$ is !!{complete}, $\lnot !A \in \Gamma$.
  86. By
  87. \iftag{FOL}{%
  88. \tagrefs{prfSC/{fol:seq:prv:prop:explicit-inc},
  89. prfND/{fol:ntd:prv:prop:explicit-inc},
  90. prfAX/{fol:axd:prv:prop:explicit-inc},
  91. prfTab/{fol:tab:prv:prop:explicit-inc}}}{%
  92. \tagrefs{prfSC/{pl:seq:prv:prop:explicit-inc},
  93. prfND/{pl:ntd:prv:prop:explicit-inc},
  94. prfAX/{pl:axd:prv:prop:explicit-inc},
  95. prfTab/{pl:tab:prv:prop:explicit-inc}}},
  96. $\Gamma$ is inconsistent. This contradicts the assumption that
  97. $\Gamma$ is consistent. Hence, it cannot be the case that $!A \notin
  98. \Gamma$, so $!A \in \Gamma$.
  100. \tagitem{defAnd}{}{%
  101. \iftag{probAnd}{Exercise.}{%
  102. $!A \land !B \in \Gamma$ iff both $!A \in \Gamma$ and $!B \in \Gamma$:
  104. For the forward direction, suppose $!A \land !B \in \Gamma$. Then
  105. by
  106. \iftag{FOL}{%
  107. \tagrefs{prfSC/{fol:seq:ppr:prop:provability-land},
  108. prfND/{fol:ntd:ppr:prop:provability-land},
  109. prfAX/{fol:axd:ppr:prop:provability-land},
  110. prfTab/{fol:tab:ppr:prop:provability-land}}}{%
  111. \tagrefs{prfSC/{pl:seq:ppr:prop:provability-land},
  112. prfND/{pl:ntd:ppr:prop:provability-land},
  113. prfAX/{pl:axd:ppr:prop:provability-land},
  114. prfTab/{pl:tab:ppr:prop:provability-land}}}, item~(1),
  115. $\Gamma \Proves !A$ and $\Gamma \Proves !B$. By
  116. \olref{prop:ccs-prov-in}, $!A \in \Gamma$ and $!B \in \Gamma$, as
  117. required.
  119. For the reverse direction, let $!A \in \Gamma$ and $!B \in
  120. \Gamma$. By
  121. \iftag{FOL}{%
  122. \tagrefs{prfSC/{fol:seq:ppr:prop:provability-land},
  123. prfND/{fol:ntd:ppr:prop:provability-land},
  124. prfAX/{fol:axd:ppr:prop:provability-land},
  125. prfTab/{fol:tab:ppr:prop:provability-land}}}{%
  126. \tagrefs{prfSC/{pl:seq:ppr:prop:provability-land},
  127. prfND/{pl:ntd:ppr:prop:provability-land},
  128. prfAX/{pl:axd:ppr:prop:provability-land},
  129. prfTab/{pl:tab:ppr:prop:provability-land}}}, item~(2),
  130. $\Gamma \Proves !A \land !B$. By \olref{prop:ccs-prov-in}, $!A \land
  131. !B \in \Gamma$.}}
  133. \tagitem{defOr}{}{%
  134. \iftag{probOr}{Exercise.}{%
  135. First we show that if $!A \lor !B \in \Gamma$, then either $!A \in
  136. \Gamma$ or $!B \in \Gamma$. Suppose $!A \lor !B \in \Gamma$ but $!A
  137. \notin \Gamma$ and $!B \notin \Gamma$. Since $\Gamma$ is
  138. !!{complete}, $\lnot !A \in \Gamma$ and $\lnot !B \in \Gamma$. By
  139. \iftag{FOL}{%
  140. \tagrefs{prfSC/{fol:seq:ppr:prop:provability-lor},
  141. prfND/{fol:ntd:ppr:prop:provability-lor},
  142. prfAX/{fol:axd:ppr:prop:provability-lor},
  143. prfTab/{fol:tab:ppr:prop:provability-lor}}}{%
  144. \tagrefs{prfSC/{pl:seq:ppr:prop:provability-lor},
  145. prfND/{pl:ntd:ppr:prop:provability-lor},
  146. prfAX/{pl:axd:ppr:prop:provability-lor},
  147. prfTab/{pl:tab:ppr:prop:provability-lor}}},
  148. item (1), $\Gamma$ is inconsistent, a contradiction. Hence, either $!A
  149. \in \Gamma$ or $!B \in \Gamma$.
  151. For the reverse direction, suppose that $!A \in \Gamma$ or $!B \in
  152. \Gamma$. By
  153. \iftag{FOL}{%
  154. \tagrefs{prfSC/{fol:seq:ppr:prop:provability-lor},
  155. prfND/{fol:ntd:ppr:prop:provability-lor},
  156. prfAX/{fol:axd:ppr:prop:provability-lor},
  157. prfTab/{fol:tab:ppr:prop:provability-lor}}}{%
  158. \tagrefs{prfSC/{pl:seq:ppr:prop:provability-lor},
  159. prfND/{pl:ntd:ppr:prop:provability-lor},
  160. prfAX/{pl:axd:ppr:prop:provability-lor},
  161. prfTab/{pl:tab:ppr:prop:provability-lor}}}, item (2),
  162. $\Gamma \Proves !A \lor !B$. By \olref{prop:ccs-prov-in}, $!A \lor
  163. !B \in \Gamma$, as required.}}
  165. \tagitem{defIf}{}{%
  166. \iftag{probIf}{Exercise.}{%
  167. For the forward direction, suppose $!A \lif !B \in \Gamma$, and suppose
  168. to the contrary that $!A \in \Gamma$ and $!B \notin \Gamma$. On these
  169. assumptions, $!A \lif !B \in \Gamma$ and $!A \in \Gamma$. By
  170. \iftag{FOL}{%
  171. \tagrefs{prfSC/{fol:seq:ppr:prop:provability-lif},
  172. prfND/{fol:ntd:ppr:prop:provability-lif},
  173. prfAX/{fol:axd:ppr:prop:provability-lif},
  174. prfTab/{fol:tab:ppr:prop:provability-lif}}}{%
  175. \tagrefs{prfSC/{pl:seq:ppr:prop:provability-lif},
  176. prfND/{pl:ntd:ppr:prop:provability-lif},
  177. prfAX/{pl:axd:ppr:prop:provability-lif},
  178. prfTab/{pl:tab:ppr:prop:provability-lif}}}, item (1),
  179. $\Gamma \Proves !B$. But then by \olref{prop:ccs-prov-in}, $!B \in
  180. \Gamma$, contradicting the assumption that $!B \notin \Gamma$.
  182. For the reverse direction, first consider the case where $!A \notin
  183. \Gamma$. Since $\Gamma$ is !!{complete}, $\lnot !A \in \Gamma$. By
  184. \iftag{FOL}{%
  185. \tagrefs{prfSC/{fol:seq:ppr:prop:provability-lif},
  186. prfND/{fol:ntd:ppr:prop:provability-lif},
  187. prfAX/{fol:axd:ppr:prop:provability-lif},
  188. prfTab/{fol:tab:ppr:prop:provability-lif}}}{%
  189. \tagrefs{prfSC/{pl:seq:ppr:prop:provability-lif},
  190. prfND/{pl:ntd:ppr:prop:provability-lif},
  191. prfAX/{pl:axd:ppr:prop:provability-lif},
  192. prfTab/{pl:tab:ppr:prop:provability-lif}}}, item (2),
  193. $\Gamma \Proves !A \lif !B$. Again by \olref{prop:ccs-prov-in}, we get
  194. that $!A \lif !B \in \Gamma$, as required.
  196. Now consider the case where $!B \in \Gamma$. By
  197. \iftag{FOL}{%
  198. \tagrefs{prfSC/{fol:seq:ppr:prop:provability-lif},
  199. prfND/{fol:ntd:ppr:prop:provability-lif},
  200. prfTab/{fol:tab:ppr:prop:provability-lif},
  201. prfAX/{fol:axd:ppr:prop:provability-lif}}}{%
  202. \tagrefs{prfSC/{pl:seq:ppr:prop:provability-lif},
  203. prfND/{pl:ntd:ppr:prop:provability-lif},
  204. prfTab/{pl:tab:ppr:prop:provability-lif},
  205. prfAX/{pl:axd:ppr:prop:provability-lif}}},
  206. item (2) again, $\Gamma \Proves !A \lif !B$. By
  207. \olref{prop:ccs-prov-in}, $!A \lif !B \in \Gamma$.}}
  208. \end{enumerate}
  209. \end{proof}
  211. \tagprob{FOL}
  212. \begin{prob}
  213. Complete the proof of \olref[fol][com][ccs]{prop:ccs}.
  214. \end{prob}
  215. \tagendprob
  217. \tagprob{notFOL}
  218. \begin{prob}
  219. Complete the proof of \olref[pl][com][ccs]{prop:ccs}.
  220. \end{prob}
  221. \tagendprob
  223. \end{document}

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

213 lines; SHA-256 a42f0551e062db3102c47f082be24cd4f8506504989a0008df4b87564e1f9335. Open preserved source.

  1. % Part: first-order-logic
  2. % Chapter: completeness
  3. % Section: henkin-expansion
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{com}{hen}
  11. \olsection{Henkin Expansion}
  13. \begin{explain}
  14. Part of the challenge in proving the completeness theorem is that the
  15. model we construct from a complete consistent set~$\Gamma$ must make
  16. all the quantified !!{formula}s in~$\Gamma$ true. In order to
  17. guarantee this, we use a trick due to Leon Henkin. In essence, the
  18. trick consists in expanding the language by infinitely many !!{constant}s
  19. and adding, for each !!{formula} with one free !!{variable} $!A(x)$ a
  20. formula of the form
  21. \iftag{prvEx}
  22. {$\lexists[x][!A(x)] \lif !A(c)$}
  23. {$\lnot\lforall[x][!A(x)] \lif \lnot !A(c)$},
  24. where $c$ is one of the new !!{constant}s. When we construct the
  25. !!{structure} satisfying~$\Gamma$, this will guarantee that each
  26. \iftag{prvEx}
  27. {true existential sentence has a witness}
  28. {false universal sentence has a counterexample}
  29. among the new constants.
  30. \end{explain}
  32. \begin{prop}
  33. \ollabel{prop:lang-exp}
  34. If $\Gamma$ is consistent in $\Lang L$ and $\Lang L'$ is obtained from
  35. $\Lang L$ by adding !!a{denumerable} set of new !!{constant}s $\Obj d_0$,
  36. $\Obj d_1$, \dots, then $\Gamma$ is consistent in~$\Lang L'$.
  37. \end{prop}
  39. \begin{defn}[Saturated set]
  40. A set $\Gamma$ of !!{formula}s of a language $\Lang {L}$ is
  41. \emph{saturated} iff for each !!{formula}~$!A(x) \in \Frm[L]$ with one
  42. free !!{variable}~$x$ there is !!a{constant}~$c \in \Lang{L}$ such
  43. that
  44. \iftag{prvEx}
  45. {$\lexists[x][!A(x)] \lif !A(c) \in \Gamma$}
  46. {$\lnot\lforall[x][!A(x)] \lif \lnot !A(c) \in \Gamma$}.
  47. \end{defn}
  49. The following definition will be used in the proof of the next theorem.
  51. \begin{defn}
  52. \ollabel{defn:henkin-exp}
  53. Let $\Lang L'$ be as in \olref{prop:lang-exp}. Fix an enumeration
  54. $!A_0(x_0)$, $!A_1(x_1)$, \dots of all !!{formula}s~$!A_i(x_i)$
  55. of~$\Lang L'$ in which one variable ($x_i$) occurs free. We define
  56. the !!{sentence}s~$!D_n$ by induction on~$n$.
  58. Let $c_0$ be the first !!{constant} among the $\Obj d_i$ we added
  59. to~$\Lang{L}$ which does not occur in~$!A_0(x_0)$. Assuming that
  60. $!D_0$, \dots,~$!D_{n-1}$ have already been defined, let $c_n$ be the
  61. first among the new !!{constant}s~$\Obj d_i$ that occurs neither in
  62. $!D_0$, \dots,~$!D_{n-1}$ nor in~$!A_n(x_n)$.
  64. Now let $!D_{n}$ be the !!{formula} \iftag{prvEx}
  65. {$\lexists[x_{n}][!A_{n}(x_{n})] \lif
  66. !A_{n}(c_{n})$}{$\lnot\lforall[x_{n}][!A_{n}(x_{n})] \lif \lnot
  67. !A_{n}(c_{n})$}.
  68. \end{defn}
  70. \begin{lem}
  71. \ollabel{lem:henkin}
  72. Every consistent set~$\Gamma$ can be extended to a saturated
  73. consistent set~$\Gamma'$.
  74. \end{lem}
  76. \begin{proof}
  77. Given a consistent set of sentences~$\Gamma$ in a language~$\Lang{L}$,
  78. expand the language by adding !!a{denumerable} set of new
  79. !!{constant}s to form~$\Lang{L'}$. By \olref{prop:lang-exp}, $\Gamma$
  80. is still consistent in the richer language. Further, let $!D_i$ be as
  81. in \olref{defn:henkin-exp}. Let
  82. \begin{align*}
  83. \Gamma_0 & = \Gamma \\
  84. \Gamma_{n+1} & = \Gamma_n \cup \{!D_n \}
  85. \end{align*}
  86. i.e., $\Gamma_{n+1} = \Gamma \cup \{ !D_0, \dots, !D_n \}$, and let
  87. $\Gamma' = \bigcup_{n} \Gamma_n$. $\Gamma'$ is clearly saturated.
  89. If $\Gamma'$ were inconsistent, then for some $n$, $\Gamma_n$ would be
  90. inconsistent (Exercise: explain why). So to show that $\Gamma'$ is
  91. consistent it suffices to show, by induction on~$n$, that each
  92. set~$\Gamma_n$ is consistent.
  94. The induction basis is simply the claim that $\Gamma_0 = \Gamma$ is
  95. consistent, which is the hypothesis of the theorem. For the induction
  96. step, suppose that $\Gamma_{n}$ is consistent but $\Gamma_{n+1} =
  97. \Gamma_n \cup \{!D_n\}$ is inconsistent. Recall that $!D_n$~is
  98. \iftag{prvEx}
  99. {$\lexists[x_{n}][!A_{n}(x_n)] \lif !A_{n}(c_{n})$}
  100. {$\lnot\lforall[x_{n}][!A_{n}(x_n)] \lif \lnot !A_{n}(c_{n})$},
  101. where $!A_n(x_n)$ is !!a{formula} of $\Lang{L'}$ with only the
  102. variable~$x_n$ free. By the way we've chosen the~$c_n$ (see
  103. \olref{defn:henkin-exp}), $c_n$ does not occur in~$!A_n(x_n)$ nor
  104. in~$\Gamma_n$.
  106. If $\Gamma_n \cup \{!D_n\}$ is inconsistent, then $\Gamma_n
  107. \Proves \lnot !D_n$, and hence both of the following hold:
  108. \iftag{prvEx}{
  109. \[
  110. \Gamma_n \Proves \lexists[x_n][!A_n(x_n)]
  111. \qquad
  112. \Gamma_n \Proves \lnot !A_n(c_n)
  113. \]}{
  114. \[
  115. \Gamma_n \Proves \lnot\lforall[x_n][!A_n(x_n)]
  116. \qquad
  117. \Gamma_n \Proves !A_n(c_n)
  118. \]}
  119. Since $c_n$ does not occur in
  120. $\Gamma_n$ or in~$!A_n(x_n)$,
  121. \tagrefs{prfAX/{fol:axd:qpr:thm:strong-generalization},prfSC/{fol:seq:qpr:thm:strong-generalization},prfND/{fol:ntd:qpr:thm:strong-generalization},prfTab/{fol:tab:qpr:thm:strong-generalization}} applies.
  122. From \iftag{prvEx}
  123. {$\Gamma_n \Proves \lnot !A_n(c_n)$}
  124. {$\Gamma_n \Proves !A_n(c_n)$},
  125. we obtain
  126. \iftag{prvEx}
  127. {$\Gamma_n \Proves \lforall[x_n][\lnot !A_n(x_n)]$}
  128. {$\Gamma_n \Proves \lforall[x_n][!A_n(x_n)]$}.
  129. Thus we have that both
  130. \iftag{prvEx}
  131. {$\Gamma_n \Proves \lexists[x_n][!A_n(x_n)]$ and
  132. $\Gamma_n \Proves \lforall[x_n][\lnot !A_n(x_n)]$}
  133. {$\Gamma_n \Proves \lnot\lforall[x_n][!A_n(x_n)]$ and
  134. $\Gamma_n \Proves \lforall[x_n][!A_n(x_n)]$},
  135. so $\Gamma_n$ itself is inconsistent.
  136. \iftag{prvEx}
  137. {(Note that
  138. \iftag{prvAll}
  139. {$\lforall[x_n][\lnot !A_n(x_n)] \Proves
  140. \lnot\lexists[x_n][!A_n(x_n)]$}
  141. {$\lforall[x_n][\lnot !A_n]$ is defined as
  142. $\lnot\lexists[x_n][\lnot\lnot !A_n(x_n)]$ and
  143. $\lnot\lexists[x_n][\lnot\lnot !A_n(x_n)] \Proves
  144. \lnot\lexists[x_n][!A_n(x_n)]$}.)}{}
  145. Contradiction: $\Gamma_n$ was supposed to be consistent. Hence
  146. $\Gamma_n \cup \{ !D_n\}$ is consistent.
  147. \end{proof}
  149. \begin{explain}
  150. We'll now show that \emph{complete}, consistent sets which are
  151. saturated have the property that \iftag{prvAll}{it contains a
  152. universally quantified !!{sentence} iff it contains all its
  153. instances}{}\iftag{defAll,defEx}{}{ and }\iftag{prvAll}{it contains an
  154. existentially quantified !!{sentence} iff it contains at least one
  155. instance}{}. We'll use this to show that the !!{structure} we'll
  156. generate from a complete, consistent, saturated set makes all its
  157. quantified sentences true.
  158. \end{explain}
  160. \begin{prop}\ollabel{prop:saturated-instances}
  161. Suppose $\Gamma$ is complete, consistent, and saturated.
  162. \begin{tagenumerate}{prvEx,prvAll}
  163. \tagitem{prvEx}{$\lexists[x][!A(x)] \in \Gamma$ iff $!A(t) \in \Gamma$
  164. for at least one closed term~$t$.}{}
  165. \tagitem{prvAll}{$\lforall[x][!A(x)] \in \Gamma$ iff $!A(t) \in \Gamma$
  166. for all closed terms~$t$.}{}
  167. \end{tagenumerate}
  168. \end{prop}
  170. \begin{proof}
  171. \begin{tagenumerate}{prvEx,prvAll}
  172. \tagitem{prvEx}{%
  173. \iftag{probEx}{Exercise.}{First suppose that $\lexists[x][!A(x)]
  174. \in \Gamma$. Because $\Gamma$ is saturated,
  175. $(\lexists[x][!A(x)] \lif !A(c)) \in \Gamma$ for some
  176. !!{constant}~$c$. By
  177. \tagrefs{prfAX/{fol:axd:ppr:prop:provability-lif},prfSC/{fol:seq:ppr:prop:provability-lif},prfND/{fol:ntd:ppr:prop:provability-lif},prfTab/{fol:tab:ppr:prop:provability-lif}}, item~(1),
  178. and \olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-prov-in}, $!A(c)
  179. \in \Gamma$.
  181. For the other direction, saturation is not necessary: Suppose
  182. $!A(t) \in \Gamma$. Then $\Gamma \Proves \lexists[x][!A(x)]$ by
  183. \tagrefs{prfAX/{fol:axd:qpr:prop:provability-quantifiers},prfSC/{fol:seq:qpr:prop:provability-quantifiers},prfND/{fol:ntd:qpr:prop:provability-quantifiers},prfTab/{fol:tab:qpr:prop:provability-quantifiers}}, item~(1). By
  184. \olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-prov-in},
  185. $\lexists[x][!A(x)] \in \Gamma$.}}{}
  186. \tagitem{prvAll}{%
  187. \iftag{probAll}{Exercise.}{Suppose that $!A(t) \in \Gamma$ for
  188. all closed terms~$t$. By way of contradiction, assume
  189. $\lforall[x][!A(x)] \notin \Gamma$. Since $\Gamma$ is complete,
  190. $\lnot\lforall[x][!A(x)] \in \Gamma$. By saturation,
  191. \iftag{prvEx}{$(\lexists[x][\lnot !A(x)] \lif \lnot !A(c)) \in
  192. \Gamma$}{$(\lnot\lforall[x][!A(x)] \lif \lnot !A(c)) \in
  193. \Gamma$} for some !!{constant}~$c$. By assumption, since $c$
  194. is a closed term, $!A(c) \in \Gamma$. But this would make
  195. $\Gamma$ inconsistent. (Exercise: give the !!{derivation} that shows
  196. \[
  197. \lnot \lforall[x][!A(x)],
  198. \iftag{prvEx}{\lexists[x][\lnot !A(x)] \lif \lnot
  199. !A(c)}{\lnot\lforall[x][!A(x)] \lif \lnot
  200. !A(c)}, !A(c)
  201. \]
  202. is inconsistent.)
  204. For the reverse direction, we do not need saturation: Suppose
  205. $\lforall[x][!A(x)] \in \Gamma$. Then $\Gamma \Proves !A(t)$
  206. by
  207. \tagrefs{prfAX/{fol:axd:qpr:prop:provability-quantifiers},prfSC/{fol:seq:qpr:prop:provability-quantifiers},prfND/{fol:ntd:qpr:prop:provability-quantifiers},prfTab/{fol:tab:qpr:prop:provability-quantifiers}},
  208. item~(2). We get $!A(t) \in \Gamma$ by
  209. \olref[ccs]{prop:ccs}.}}{}
  210. \end{tagenumerate}
  211. \end{proof}
  213. \end{document}

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

99 lines; SHA-256 1ee3d9dd14df1c3368c3e7a12d68e4d6627b9e92030a00820270b75ceb4bdf78. Open preserved source.

  1. % Part: first-order-logic
  2. % Chapter: completeness
  3. % Section: lindenbaums-lemma
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{com}{lin}}
  11. {\olfileid{pl}{com}{lin}}
  13. \olsection{Lindenbaum's Lemma}
  15. \begin{explain}
  16. We now prove a lemma that shows that any consistent set of
  17. !!{sentence}s is contained in some set of sentences which is not just
  18. consistent, but also !!{complete}. The proof works by adding one
  19. !!{sentence} at a time, guaranteeing at each step that the set remains
  20. consistent. We do this so that for every $!A$, either $!A$ or $\lnot
  21. !A$ gets added at some stage. The union of all stages in that
  22. construction then contains either $!A$ or its negation~$\lnot !A$ and
  23. is thus complete. It is also consistent, since we make sure at each
  24. stage not to introduce an inconsistency.
  25. \end{explain}
  27. \begin{lem}[Lindenbaum's Lemma]
  28. \ollabel{lem:lindenbaum} Every consistent
  29. set~$\Gamma$ in a language~$\Lang{L}$ can be
  30. extended to !!a{complete} and consistent set~$\Gamma^*$.
  31. \end{lem}
  33. \begin{proof}
  34. Let $\Gamma$ be consistent. Let $!A_0$, $!A_1$,
  35. \dots{} be an enumeration of all the !!{sentence}s of~$\Lang L$.
  36. Define $\Gamma_0 = \Gamma$, and
  37. \[
  38. \Gamma_{n+1} =
  39. \begin{cases}
  40. \Gamma_n \cup \{ !A_n \} & \textrm{if $\Gamma_n \cup \{!A_n\}$ is
  41. consistent;} \\
  42. \Gamma_n \cup \{ \lnot !A_n \} & \textrm{otherwise.}
  43. \end{cases}
  44. \]
  45. Let $\Gamma^* = \bigcup_{n \geq 0} \Gamma_n$.
  47. Each $\Gamma_n$ is consistent: $\Gamma_0$ is consistent by definition.
  48. If $\Gamma_{n+1} = \Gamma_n \cup \{!A_n\}$, this is because the latter
  49. is consistent. If it isn't, $\Gamma_{n+1} = \Gamma_n \cup \{\lnot
  50. !A_n\}$. We have to verify that $\Gamma_n \cup \{\lnot !A_n\}$ is
  51. consistent. Suppose it's not. Then \emph{both} $\Gamma_n \cup
  52. \{!A_n\}$ and $\Gamma_n \cup \{\lnot !A_n\}$ are inconsistent. This
  53. means that $\Gamma_n$ would be inconsistent by
  54. \iftag{FOL}{%
  55. \tagrefs{prfAX/{fol:axd:prv:prop:provability-exhaustive},
  56. prfSC/{fol:seq:prv:prop:provability-exhaustive},
  57. prfND/{fol:ntd:prv:prop:provability-exhaustive},
  58. prfTab/{fol:tab:prv:prop:provability-exhaustive}}}{%
  59. \tagrefs{prfAX/{pl:axd:prv:prop:provability-exhaustive},
  60. prfSC/{pl:seq:prv:prop:provability-exhaustive},
  61. prfND/{pl:ntd:prv:prop:provability-exhaustive},
  62. prfTab/{pl:tab:prv:prop:provability-exhaustive}}},
  63. contrary to the induction hypothesis.
  65. For every~$n$ and every $i < n$, $\Gamma_i \subseteq \Gamma_n$. This
  66. follows by a simple induction on~$n$. For $n=0$, there are no $i < 0$,
  67. so the claim holds automatically. For the inductive step, suppose it
  68. is true for~$n$. We show that if $i < n+1$ then $\Gamma_i \subseteq
  69. \Gamma_{n+1}$. We have $\Gamma_{n+1} = \Gamma_n \cup \{!A_n\}$ or $=
  70. \Gamma_n \cup \{\lnot !A_n\}$ by construction. So $\Gamma_n \subseteq
  71. \Gamma_{n+1}$. If $i < n+1$, then $\Gamma_i \subseteq \Gamma_n$ by
  72. inductive hypothesis (if $i < n$) or the trivial fact that $\Gamma_n
  73. \subseteq \Gamma_n$ (if $i = n$). We get that $\Gamma_i \subseteq
  74. \Gamma_{n+1}$ by transitivity of~$\subseteq$.
  76. From this it follows that $\Gamma^*$ is consistent. Here's why: Let
  77. $\Gamma' \subseteq \Gamma^*$ be finite. Each $!B \in \Gamma'$ is also
  78. in~$\Gamma_i$ for some~$i$. Let $n$ be the largest of these. Since
  79. $\Gamma_i \subseteq \Gamma_n$ if $i \le n$, every $!B \in \Gamma'$ is
  80. also $\in \Gamma_n$, i.e., $\Gamma' \subseteq \Gamma_n$, and
  81. $\Gamma_n$~is consistent. So, every finite subset $\Gamma' \subseteq
  82. \Gamma^*$ is consistent. By \iftag{FOL}{%
  83. \tagrefs{prfAX/{fol:axd:ptn:prop:proves-compact},
  84. prfSC/{fol:seq:ptn:prop:proves-compact},
  85. prfND/{fol:ntd:ptn:prop:proves-compact},
  86. prfTab/{fol:tab:ptn:prop:proves-compact}}}{%
  87. \tagrefs{prfAX/{pl:axd:ptn:prop:proves-compact},
  88. prfSC/{pl:seq:ptn:prop:proves-compact},
  89. prfND/{pl:ntd:ptn:prop:proves-compact},
  90. prfTab/{pl:tab:ptn:prop:proves-compact}}}, $\Gamma^*$ is
  91. consistent.
  93. Every !!{sentence} of $\Frm[L]$ appears on the list used to
  94. define~$\Gamma^*$. If $!A_n \notin \Gamma^*$, then that is because
  95. $\Gamma_n \cup \{!A_n\}$ was inconsistent. But then $\lnot !A_n
  96. \in \Gamma^*$, so $\Gamma^*$ is !!{complete}.
  97. \end{proof}
  99. \end{document}

content/first-order-logic/completeness/construction-of-model.tex

279 lines; SHA-256 e8f3c25a2b378ac1996cc9cebb1192b2bdc2527df547e922008dad3822d29969. Open preserved source.

  1. % Part: first-order-logic
  2. % Chapter: completeness
  3. % Section: construction-of-model
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{com}{mod}}
  11. {\olfileid{pl}{com}{mod}}
  13. \olsection{Construction of a Model}
  15. \begin{explain}
  16. \iftag{FOL}{Right now we are not concerned about $\eq$, i.e., we only
  17. want to show that a consistent set~$\Gamma$ of !!{sentence}s not
  18. containing~$\eq$ is satisfiable. We first extend~$\Gamma$ to a
  19. consistent, !!{complete}, and saturated set~$\Gamma^*$. In this
  20. case, the definition of a model~$\Struct{M(\Gamma^*)}$ is simple: We
  21. take the set of closed terms of~$\Lang{L'}$ as the domain. We assign
  22. every !!{constant} to itself, and make sure that more generally, for
  23. every closed term~$t$, $\Value{t}{M(\Gamma^*)} = t$. The
  24. !!{predicate}s are assigned extensions in such a way that an atomic
  25. !!{sentence} is true in $\Struct{M(\Gamma^*)}$ iff it is
  26. in~$\Gamma^*$. This will obviously make all the atomic
  27. !!{sentence}s in~$\Gamma^*$ true in $\Struct{M(\Gamma^*)}$. The rest
  28. are true provided the $\Gamma^*$ we start with is consistent,
  29. complete, and saturated.}{We are now ready to define !!a{valuation}
  30. that makes all $!A \in \Gamma$ true. To do this, we first apply
  31. Lindenbaum's Lemma: we get a complete consistent $\Gamma^* \supseteq
  32. \Gamma$. We let the !!{propositional variable}s in~$\Gamma^*$
  33. determine~$\pAssign v(\Gamma^*)$.}
  34. \end{explain}
  36. \iftag{FOL}{%
  37. \begin{defn}[Term model]
  38. \ollabel{defn:termmodel}
  39. Let $\Gamma^*$ be !!a{complete} and consistent,
  40. saturated set of !!{sentence}s in a language~$\Lang L$. The \emph{term
  41. model}~$\Struct M(\Gamma^*)$ of $\Gamma^*$ is the !!{structure}
  42. defined as follows:
  43. \begin{enumerate}
  44. \item The !!{domain}~$\Domain{M(\Gamma^*)}$ is the set of all closed
  45. terms of~$\Lang L$.
  46. \item The interpretation of !!a{constant} $c$ is $c$ itself:
  47. $\Assign{c}{M(\Gamma^*)} = c$.
  48. \item The !!{function}~$f$ is assigned the function which, given as
  49. arguments the closed terms $t_1$, \dots, $t_n$, has as value the
  50. closed term $f(t_1, \dots, t_n)$:
  51. \[
  52. \Assign{f}{M(\Gamma^*)}(t_1, \dots, t_n) = f(t_1,\dots, t_n)
  53. \]
  54. \item If $R$ is an $n$-place !!{predicate}, then
  55. \[
  56. \tuple{t_1, \dots,
  57. t_n} \in \Assign{R}{M(\Gamma^*)} \text{ iff } \Atom{R}{t_1, \dots,
  58. t_n} \in \Gamma^*.
  59. \]
  60. \end{enumerate}
  61. \end{defn}
  62. }{%
  63. \begin{defn}
  64. \ollabel{defn:termmodel}
  65. Suppose $\Gamma^*$ is a complete consistent set of !!{formula}s. Then we let
  66. \[
  67. \pAssign v(\Gamma^*)(p) = \begin{cases}
  68. \True & \text{if $p \in \Gamma^*$}\\
  69. \False & \text{if $p \notin \Gamma^*$}
  70. \end{cases}
  71. \]
  72. \end{defn}
  73. }
  75. \iftag{FOL}{%
  76. We will now check that we indeed have $\Value{t}{M(\Gamma^*)} = t$.
  78. \begin{lem}
  79. \ollabel{lem:val-in-termmodel} Let $\Struct M(\Gamma^*)$ be the term model
  80. of \olref{defn:termmodel}, then $\Value{t}{M(\Gamma^*)} = t$.
  81. \end{lem}
  82. \begin{proof}
  83. The proof is by induction on $t$, where the base case, when $t$
  84. is !!a{constant}, follows directly from the definition of the term
  85. model. For the induction step assume $t_1, \ldots, t_n$ are closed terms
  86. such that $\Value{t_i}{M(\Gamma^*)} = t_i$ and that $f$ is an $n$-ary
  87. !!{function}. Then
  88. \begin{align*}
  89. \Value{f(t_1,\ldots,t_n)}{M(\Gamma^*)} &= \Assign{f}{M(\Gamma^*)}(\Value{t_1}
  90. {M(\Gamma^*)},
  91. \ldots, \Value{t_n}{M(\Gamma^*)}) \\
  92. &= \Assign{f}{M(\Gamma^*)}(t_1, \dots, t_n) \\
  93. &= f(t_1,\dots, t_n),
  94. \end{align*}
  95. and so by induction this holds for every closed term~$t$.
  96. \end{proof}
  97. }
  99. \iftag{FOL}{%
  100. \begin{explain}
  101. \iftag{prvEx}{!!^a{structure}~$\Struct{M}$ may make an existentially
  102. quantified !!{sentence}~$\lexists[x][!A(x)]$ true without there
  103. being an instance~$!A(t)$ that it makes true.}{}
  104. \iftag{prvAll}{!!^a{structure}~$\Struct{M}$ may make all
  105. instances~$!A(t)$ of a universally quantified
  106. !!{sentence}~$\lforall[x][!A(x)]$ true, without
  107. making~$\lforall[x][!A(x)]$ true.}{} This is because in general
  108. not every !!{element} of~$\Domain{M}$ is the value of a closed term
  109. ($\Struct{M}$ may not be covered). This is the reason the
  110. satisfaction relation is defined via variable assignments. However,
  111. for our term model~$\Struct{M(\Gamma^*)}$ this wouldn't be
  112. necessary---because it is covered. This is the content of the next
  113. result.
  114. \end{explain}
  116. \begin{prop}
  117. \ollabel{prop:quant-termmodel}
  118. Let $\Struct M(\Gamma^*)$ be the term model of \olref{defn:termmodel}.
  119. \begin{tagenumerate}{prvEx,prvAll}
  120. \tagitem{prvEx}{$\Sat{M(\Gamma^*)}{\lexists[x][!A(x)]}$ iff
  121. $\Sat{M(\Gamma^*)}{!A(t)}$ for at least one closed term~$t$.}{}
  122. \tagitem{prvAll}{$\Sat{M(\Gamma^*)}{\lforall[x][!A(x)]}$ iff
  123. $\Sat{M(\Gamma^*)}{!A(t)}$ for all closed terms~$t$.}{}
  124. \end{tagenumerate}
  125. \end{prop}
  127. \begin{proof}
  128. \begin{tagenumerate}{prvEx,prvAll}
  129. \tagitem{prvEx}{%
  130. \iftag{probEx}{Exercise.}{By \olref[syn][ass]{prop:sat-quant},
  131. $\Sat{M(\Gamma^*)}{\lexists[x][!A(x)]}$ iff for at least one
  132. variable assignment~$s$, $\Sat{M(\Gamma^*)}{!A(x)}[s]$. As
  133. $\Domain{M(\Gamma^*)}$ consists of the closed terms of~$\Lang{L}$,
  134. this is the case iff there is at least one closed term~$t$ such
  135. that $s(x) = t$ and $\Sat{M(\Gamma^*)}{!A(x)}[s]$. By
  136. \olref[fol][syn][ext]{prop:ext-formulas},
  137. $\Sat{M(\Gamma^*)}{!A(x)}[s]$ iff $\Sat{M(\Gamma^*)}{!A(t)}[s]$,
  138. where $s(x) = t$. By \olref[fol][syn][ass]{prop:sentence-sat-true},
  139. $\Sat{M(\Gamma^*)}{!A(t)}[s]$ iff $\Sat{M(\Gamma^*)}{!A(t)}$,
  140. since $!A(t)$ is a sentence.}}{}
  141. \tagitem{prvAll}{%
  142. \iftag{probAll}{Exercise.}{By \olref[syn][ass]{prop:sat-quant},
  143. $\Sat{M(\Gamma^*)}{\lforall[x][!A(x)]}$ iff for every variable
  144. assignment $s$, $\Sat{M(\Gamma^*)}{!A(x)}[s]$. Recall that
  145. $\Domain{M(\Gamma^*)}$ consists of the closed terms of~$\Lang{L}$,
  146. so for every closed term~$t$, $s(x) = t$ is such a variable
  147. assignment, and for any variable assignment, $s(x)$ is some closed
  148. term~$t$. By \olref[fol][syn][ext]{prop:ext-formulas},
  149. $\Sat{M(\Gamma^*)}{!A(x)}[s]$ iff $\Sat{M(\Gamma^*)}{!A(t)}[s]$,
  150. where $s(x) = t$. By \olref[fol][syn][ass]{prop:sentence-sat-true},
  151. $\Sat{M(\Gamma^*)}{!A(t)}[s]$ iff $\Sat{M(\Gamma^*)}{!A(t)}$,
  152. since $!A(t)$ is a sentence.}}{}
  153. \end{tagenumerate}
  154. \end{proof}
  155. }{}
  157. \tagprob[FOL]{probEx,probAll}
  158. \begin{prob}
  159. Complete the proof of \olref[fol][com][mod]{prop:quant-termmodel}.
  160. \end{prob}
  161. \tagendprob
  163. \begin{lem}[Truth Lemma]
  164. \ollabel{lem:truth} \iftag{FOL}{Suppose $!A$ does not contain~$\eq$. Then}{}
  165. $\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{!A}$ iff $!A \in \Gamma^*$.
  166. \end{lem}
  168. \begin{proof}
  169. We prove both directions simultaneously, and by induction on $!A$.
  170. \begin{enumerate}
  171. \tagitem{prvFalse}{\indcase{!A}{\lfalse}
  172. {$\iftag{FOL}{\Sat/{M(\Gamma^*)}{\lfalse}}{\pSat/{v(\Gamma^*)}{\lfalse}}$
  173. by definition of satisfaction. On the other hand, $\lfalse \notin
  174. \Gamma^*$ since $\Gamma^*$ is consistent.}}{}
  176. \tagitem{prvTrue}{\indcase{!A}{\ltrue}
  177. {$\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{\ltrue}$
  178. by definition of satisfaction. On the other hand, $\ltrue \in
  179. \Gamma^*$ since $\Gamma^*$ is consistent and !!{complete}, and
  180. $\Gamma^* \Proves \ltrue$.}}{}
  182. \tagitem{FOL}{\indcase{!A}{R(t_1, \dots, t_n)}
  183. {$\Sat{M(\Gamma^*)}{\Atom{R}{t_1, \dots, t_n}}$ iff $\tuple{t_1,
  184. \dots, t_n} \in \Assign{R}{M(\Gamma^*)}$ (by the definition of
  185. satisfaction) iff $R(t_1, \dots, t_n) \in \Gamma^*$ (by the
  186. construction of $\Struct
  187. M(\Gamma^*)$).}}{\indcase{!A}{p}{$\pSat{v(\Gamma^*)}{p}$ iff
  188. $\pAssign v(\Gamma^*)(p) = \True$ (by the definition of
  189. satisfaction) iff $p \in \Gamma^*$ (by the construction of
  190. $\pAssign v(\Gamma^*)$).}}
  192. \tagitem{prvNot}{%
  193. \indcase{!A}{\lnot !B}
  194. {$\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{\indfrm}$ iff
  195. $\iftag{FOL}{\Sat/{M(\Gamma^*)}{!B}}{\pSat/{v(\Gamma^*)}{!B}}$ (by
  196. definition of satisfaction). By induction hypothesis,
  197. $\iftag{FOL}{\Sat/{M(\Gamma^*)}{!B}}{\pSat/{v(\Gamma^*)}{!B}}$ iff
  198. $!B \notin \Gamma^*$. Since $\Gamma^*$ is consistent and
  199. !!{complete}, $!B
  200. \notin \Gamma^*$ iff $\lnot !B \in \Gamma^*$.}}{}
  202. \tagitem{prvAnd}{%
  203. \iftag{probAnd}{%
  204. \indcase!{!A}{!B \land !C}{}}{%
  205. \indcase{!A}{!B \land
  206. !C}{$\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{\indfrm}$
  207. iff we have both
  208. $\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{!B}$ and
  209. $\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{!C}$ (by
  210. definition of satisfaction) iff both $!B \in \Gamma^*$ and $!C \in
  211. \Gamma^*$ (by the induction hypothesis). By
  212. \olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-and}, this is the case
  213. iff $(!B \land !C) \in \Gamma^*$.}}}{}
  215. \tagitem{prvOr}{%
  216. \iftag{probOr}{%
  217. \indcase!{!A}{!B \lor !C}{}}{%
  218. \indcase{!A}{!B \lor !C}
  219. {$\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{\indfrm}$
  220. iff $\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{!B}$ or
  221. $\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{!C}$ (by
  222. definition of satisfaction) iff $!B \in \Gamma^*$ or $!C \in
  223. \Gamma^*$ (by induction hypothesis). This is the case iff $(!B
  224. \lor !C) \in \Gamma^*$ (by
  225. \olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-or}).}}}{}
  227. \tagitem{prvIf}{%
  228. \iftag{probIf}{%
  229. \indcase!{!A}{!B \lif !C}{}}{%
  230. \indcase{!A}{!B \lif !C}
  231. {$\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{\indfrm}$
  232. iff $\iftag{FOL}{\Sat/{M(\Gamma^*)}}{\pSat/{v(\Gamma^*)}}{!B}$ or $\iftag{FOL}{\Sat{M (\Gamma^*)}}{\pSat{v(\Gamma^*)}}{!C}$ (by
  233. definition of satisfaction) iff $!B \notin \Gamma^*$ or $!C \in
  234. \Gamma^*$ (by induction hypothesis). This is the case iff $(!B
  235. \lif !C) \in \Gamma^*$ (by
  236. \olref[ccs]{prop:ccs}\olref[ccs]{prop:ccs-if}).}}}{}
  238. \iftag{FOL}{%
  239. \tagitem{prvAll}{%
  240. \iftag{probAll}{%
  241. \indcase!{!A}{\lforall[x][!B(x)]}{}}{%
  242. \indcase{!A}{\lforall[x][!B(x)]}{$\Sat{M(\Gamma^*)}{\indfrm}$ iff
  243. $\Sat{M(\Gamma^*)}{!B(t)}$ for all terms~$t$
  244. (\olref{prop:quant-termmodel}). By induction hypothesis, this
  245. is the case iff $!B(t) \in \Gamma^*$ for all terms~$t$, by
  246. \olref[hen]{prop:saturated-instances}, this in turn is the case
  247. iff $\lforall[x][!A(x)] \in \Gamma^*$.}}}{}
  249. \tagitem{prvEx}{%
  250. \iftag{probEx}{%
  251. \indcase!{!A}{\lexists[x][!B(x)]}{}}{%
  252. \indcase{!A}{\lexists[x][!B(x)]}{$\Sat{M(\Gamma^*)}{\indfrm}$ iff
  253. $\Sat{M(\Gamma^*)}{!B(t)}$ for at least one term~$t$
  254. (\olref{prop:quant-termmodel}). By induction hypothesis, this
  255. is the case iff $!B(t) \in \Gamma^*$ for at least one term~$t$.
  256. By \olref[hen]{prop:saturated-instances}, this in turn is the
  257. case iff $\lexists[x][!B(x)] \in \Gamma^*$.}}}{}
  258. }{}
  259. \end{enumerate}
  260. \end{proof}
  263. \tagprob[FOL]{probOr,probAnd,probIf,probEx,probAll}
  265. \begin{prob}
  266. Complete the proof of \olref[fol][com][mod]{lem:truth}.
  267. \end{prob}
  269. \tagendprob
  271. \tagprob[notFOL]{probOr,probAnd,probIf}
  273. \begin{prob}
  274. Complete the proof of \olref[pl][com][mod]{lem:truth}.
  275. \end{prob}
  277. \tagendprob
  279. \end{document}

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

205 lines; SHA-256 2b497ead07aad76f2db101bd56768abd9bc71df7c819164edf0183656d148e7d. Open preserved source.

  1. % Part: first-order-logic
  2. % Chapter: completeness
  3. % Section: identity
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{com}{ide}
  10. \olsection{Identity}
  12. \begin{explain}
  13. The construction of the term model given in the preceding section is
  14. enough to establish completeness for first-order logic for
  15. sets~$\Gamma$ that do not contain~$\eq$. The term model satisfies
  16. every $!A \in \Gamma^*$ which does not contain~$\eq$ (and hence all
  17. $!A \in \Gamma$). It does not work, however, if $\eq$ is present.
  18. The reason is that $\Gamma^*$ then may contain
  19. !!a{sentence}~$\eq[t][t']$, but in the term model the value of any
  20. term is that term itself. Hence, if $t$ and $t'$ are different terms,
  21. their values in the term model---i.e., $t$ and $t'$,
  22. respectively---are different, and so $\eq[t][t']$ is false. We can
  23. fix this, however, using a construction known as ``factoring.''
  24. \end{explain}
  26. \begin{defn}
  27. Let $\Gamma^*$ be a consistent and !!{complete} set of sentences
  28. in~$\Lang L$. We define the relation $\approx$ on the set of closed
  29. terms of~$\Lang L$ by
  30. \[
  31. t \approx t' \text{\quad iff \quad} \eq[t][t'] \in \Gamma^*
  32. \]
  33. \end{defn}
  35. \begin{prop}
  36. \ollabel{prop:approx-equiv}
  37. The relation $\approx$ has the following properties:
  38. \begin{enumerate}
  39. \item $\approx$ is reflexive.
  40. \item $\approx$ is symmetric.
  41. \item $\approx$ is transitive.
  42. \item If $t \approx t'$, $f$ is !!a{function}, and $t_1$, \dots,
  43. $t_{i-1}$, $t_{i+1}$, \dots, $t_n$ are closed terms, then
  44. \[
  45. \Atom{f}{t_1,\dots, t_{i-1}, t, t_{i+1}, \dots, t_n} \approx
  46. \Atom{f}{t_1,\dots, t_{i-1}, t', t_{i+1}, \dots, t_n}.
  47. \]
  48. \item If $t \approx t'$, $R$ is !!a{predicate}, and $t_1$, \dots,
  49. $t_{i-1}$, $t_{i+1}$, \dots, $t_n$ are closed terms, then
  50. \begin{multline*}
  51. \Atom{R}{t_1,\dots, t_{i-1}, t, t_{i+1}, \dots, t_n} \in \Gamma^* \text{ iff } \\
  52. \Atom{R}{t_1,\dots, t_{i-1}, t', t_{i+1}, \dots, t_n} \in \Gamma^*.
  53. \end{multline*}
  54. \end{enumerate}
  55. \end{prop}
  57. \begin{proof}
  58. Since $\Gamma^*$ is consistent and !!{complete}, $\eq[t][t'] \in
  59. \Gamma^*$ iff $\Gamma^* \Proves \eq[t][t']$. Thus it is enough to
  60. show the following:
  61. \begin{enumerate}
  62. \item $\Gamma^* \Proves \eq[t][t]$ for all closed terms~$t$.
  63. \item If $\Gamma^* \Proves \eq[t][t']$ then $\Gamma^* \Proves \eq[t'][t]$.
  64. \item If $\Gamma^* \Proves \eq[t][t']$ and $\Gamma^* \Proves
  65. \eq[t'][t'']$, then $\Gamma^* \Proves \eq[t][t'']$.
  66. \item If $\Gamma^* \Proves \eq[t][t']$, then
  67. \[
  68. \Gamma^* \Proves
  69. \eq[\Atom{f}{t_1,\dots,t_{i-1},t,t_{i+1},,\dots,t_n}][\Atom{f}{t_1,\dots,t_{i-1},t',t_{i+1},\dots,t_n}]
  70. \]
  71. for every $n$-place !!{function}~$f$ and closed terms $t_1$, \dots,
  72. $t_{i-1}$, $t_{i+1}$, \dots,~$t_n$.
  73. \item If $\Gamma^* \Proves \eq[t][t']$ and
  74. $\Gamma^* \Proves
  75. \Atom{R}{t_1,\dots,t_{i-1},t,t_{i+1},\dots,t_n}$, then
  76. $\Gamma^* \Proves \Atom{R}{t_1,\dots,t_{i-1},t',t_{i+1},\dots,t_n}$
  77. for every $n$-place !!{predicate}~$R$ and closed terms $t_1$, \dots,
  78. $t_{i-1}$, $t_{i+1}$, \dots,~$t_n$.
  79. \end{enumerate}
  80. \end{proof}
  82. \begin{prob}
  83. Complete the proof of~\olref[fol][com][ide]{prop:approx-equiv}.
  84. \end{prob}
  86. \begin{defn}
  87. Suppose $\Gamma^*$ is a consistent and !!{complete} set in a
  88. language~$\Lang L$, $t$ is a closed term, and $\approx$ as in the
  89. previous definition. Then:
  90. \[
  91. \equivrep{t}{\approx} = \Setabs{t'}{t'\in \Trm[L], t \approx t'}
  92. \]
  93. and $\equivclass{\Trm[L]}{\approx} = \Setabs{\equivrep{t}{\approx}}{t \in \Trm[L]}$.
  94. \end{defn}
  96. \begin{defn}
  97. \ollabel{defn:term-model-factor}
  98. Let $\Struct M = \Struct M(\Gamma^*)$ be the term model
  99. for~$\Gamma^*$ from \olref[mod]{defn:termmodel}. Then $\Struct{\equivclass{M}{\approx}}$ is the following
  100. !!{structure}:
  101. \begin{enumerate}
  102. \item $\Domain{\equivclass{M}{\approx}} = \equivclass{\Trm[L]}{\approx}$.
  103. \item $\Assign{c}{\equivclass{M}{\approx}} = \equivrep{c}{\approx}$
  104. \item $\Assign{f}{\equivclass{M}{\approx}}(\equivrep{t_1}{\approx}, \dots,
  105. \equivrep{t_n}{\approx}) = \equivrep{\Atom{f}{t_1,\dots, t_n}}{\approx}$
  106. \item $\tuple{\equivrep{t_1}{\approx}, \dots, \equivrep{t_n}{\approx}} \in
  107. \Assign{R}{\equivclass{M}{\approx}}$ iff
  108. $\Sat{M}{\Atom{R}{t_1,\dots, t_n}}$, i.e., iff $\Atom{R}{t_1,\dots,
  109. t_n} \in \Gamma^*$.
  110. \end{enumerate}
  111. \end{defn}
  113. \begin{explain}
  114. Note that we have defined $\Assign{f}{\equivclass{M}{\approx}}$ and
  115. $\Assign{R}{\equivclass{M}{\approx}}$ for elements of
  116. $\equivclass{\Trm[L]}{\approx}$ by referring to them as
  117. $\equivrep{t}{\approx}$, i.e., via \emph{representatives}~$t \in
  118. \equivrep{t}{\approx}$. We have to make sure that these definitions
  119. do not depend on the choice of these representatives, i.e., that for
  120. some other choices~$t'$ which determine the same equivalence classes
  121. ($\equivrep{t}{\approx} = \equivrep{t'}{\approx}$), the definitions
  122. yield the same result. For instance, if $R$ is a one-place
  123. !!{predicate}, the last clause of the definition says that
  124. $\equivrep{t}{\approx} \in \Assign{R}{\equivclass{M}{\approx}}$ iff
  125. $\Sat{M}{\Atom{R}{t}}$. If for some other term~$t'$ with $t \approx
  126. t'$, $\Sat/{M}{\Atom{R}{t}}$, then the definition would require
  127. $\equivrep{t'}{\approx} \notin \Assign{R}{\equivclass{M}{\approx}}$.
  128. If $t \approx t'$, then $\equivrep{t}{\approx} =
  129. \equivrep{t'}{\approx}$, but we can't have both $\equivrep{t}{\approx}
  130. \in \Assign{R}{\equivclass{M}{\approx}}$ and $\equivrep{t}{\approx}
  131. \notin \Assign{R}{\equivclass{M}{\approx}}$. However,
  132. \olref{prop:approx-equiv} guarantees that this cannot happen.
  133. \end{explain}
  135. \begin{prop}
  136. $\Struct{\equivclass{M}{\approx}}$ is well defined, i.e., if $t_1$,
  137. \dots, $t_n$, $t_1'$, \dots, $t_n'$ are closed terms,
  138. and $t_i \approx t_i'$ then
  139. \begin{enumerate}
  140. \item $\equivrep{\Atom{f}{t_1,\dots, t_n}}{\approx} =
  141. \equivrep{\Atom{f}{t_1',\dots, t_n'}}{\approx}$, i.e.,
  142. \[
  143. \Atom{f}{t_1,\dots, t_n} \approx \Atom{f}{t_1',\dots, t_n'}
  144. \]
  145. and
  146. \item $\Sat{M}{\Atom{R}{t_1,\dots, t_n}}$ iff
  147. $\Sat{M}{\Atom{R}{t_1',\dots, t_n'}}$, i.e.,
  148. \[
  149. \Atom{R}{t_1,\dots, t_n} \in \Gamma^* \text{ iff }
  150. \Atom{R}{t_1',\dots, t_n'} \in \Gamma^*.
  151. \]
  152. \end{enumerate}
  153. \end{prop}
  155. \begin{proof}
  156. Follows from \olref{prop:approx-equiv} by induction on~$n$.
  157. \end{proof}
  159. As in the case of the term model, before proving the truth lemma we need the
  160. following lemma.
  162. \begin{lem}
  163. \ollabel{lem:val-in-termmodel-factored} Let $\Struct M = \Struct M
  164. (\Gamma^*)$, then $\Value{t}{\equivclass{M}{\approx}} = \equivrep{t}
  165. {\approx}$.
  166. \end{lem}
  167. \begin{proof}
  168. The proof is similar to that of \olref[mod]{lem:val-in-termmodel}.
  169. \end{proof}
  171. \begin{prob}
  172. Complete the proof of~\olref[fol][com][ide]{lem:val-in-termmodel-factored}.
  173. \end{prob}
  175. \begin{lem}
  176. \ollabel{lem:truth}
  177. $\Sat{\equivclass{M}{\approx}}{!A}$ iff $!A \in \Gamma^*$ for all
  178. sentences~$!A$.
  179. \end{lem}
  181. \begin{proof}
  182. By induction on~$!A$, just as in the proof of \olref[mod]{lem:truth}.
  183. The only case that needs additional attention is when $!A \ident
  184. \eq[t][t']$.
  185. \begin{align*}
  186. \Sat{\equivclass{M}{\approx}}{\eq[t][t']} & \text{ iff } \equivrep{t}{\approx} = \equivrep{t'}{\approx}
  187. \text{ (by definition of $\Struct{\equivclass{M}{\approx}}$)}\\
  188. & \text{ iff } t \approx t' \text{ (by definition of $\equivrep{t}{\approx}$)}\\
  189. & \text{ iff } \eq[t][t'] \in \Gamma^* \text{ (by definition of $\approx$).}
  190. \end{align*}
  191. \end{proof}
  193. \begin{digress}
  194. Note that while $\Struct{M(\Gamma^*)}$ is always !!{enumerable} and
  195. infinite, $\Struct{\equivclass{M}{\approx}}$ may be finite, since it
  196. may turn out that there are only finitely many classes
  197. $\equivrep{t}{\approx}$. This is to be expected, since $\Gamma$ may
  198. contain !!{sentence}s which require any !!{structure} in which they
  199. are true to be finite. For instance, $\lforall[x][\lforall[y][x =
  200. y]]$ is a consistent !!{sentence}, but is satisfied only in
  201. !!{structure}s with !!a{domain} that contains exactly one
  202. !!{element}.
  203. \end{digress}
  205. \end{document}

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

125 lines; SHA-256 5510644c6a3ff18e97d5e97a928d00cb0b091506e8c10bafa504c1b2c38b242b. Open preserved source.

  1. % Part: first-order-logic
  2. % Chapter: completeness
  3. % Section: completeness-theorem
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{com}{cth}}
  11. {\olfileid{pl}{com}{cth}}
  13. \olsection{The Completeness Theorem}
  15. \begin{explain}
  16. Let's combine our results: we arrive at the completeness theorem.
  17. \end{explain}
  19. \begin{thm}[Completeness Theorem]
  20. \ollabel{thm:completeness}
  21. Let $\Gamma$ be a set of !!{sentence}s. If $\Gamma$ is consistent, it
  22. is satisfiable.
  23. \end{thm}
  25. \begin{proof}
  26. Suppose $\Gamma$ is consistent.\iftag{FOL}{ By
  27. \olref[hen]{lem:henkin}, there is a saturated consistent set
  28. $\Gamma' \supseteq \Gamma$.}{} By \olref[lin]{lem:lindenbaum}, there
  29. is a $\Gamma^* \supseteq \iftag{FOL}{\Gamma'}{\Gamma}$ which is
  30. consistent and !!{complete}.
  31. \iftag{FOL}{
  32. Since $\Gamma' \subseteq \Gamma^*$, for each
  33. !!{formula}~$!A(x)$, $\Gamma^*$ contains !!a{sentence} of the form
  34. \iftag{prvEx}
  35. {$\lexists[x][!A(x)] \lif !A(c)$}
  36. {$\lnot\lforall[x][!A(x)] \lif \lnot !A(c)$}
  37. and so $\Gamma^*$ is saturated. If $\Gamma$
  38. does not contain~$\eq$, then by}{By}
  39. \olref[mod]{lem:truth},
  40. $\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{!A}$ iff $!A \in
  41. \Gamma^*$. From this it follows in particular that for all $!A \in
  42. \Gamma$, $\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{!A}$, so
  43. $\Gamma$ is satisfiable.\iftag{FOL}{
  44. If $\Gamma$ does contain~$\eq$,
  45. then by \olref[ide]{lem:truth}, for all !!{sentence}s~$!A$,
  46. $\Sat{\equivclass{M}{\approx}}{!A}$ iff $!A \in \Gamma^*$. In
  47. particular, $\Sat{\equivclass{M}{\approx}}{!A}$ for all $!A \in
  48. \Gamma$, so $\Gamma$ is satisfiable.}{}
  49. \end{proof}
  51. \begin{cor}[Completeness Theorem, Second Version]
  52. \ollabel{cor:completeness}
  53. For all $\Gamma$ and !!{sentence}s~$!A$: if $\Gamma \Entails !A$ then
  54. $\Gamma \Proves !A$.
  55. \end{cor}
  57. \begin{proof}
  58. Note that the $\Gamma$'s in \olref{cor:completeness} and
  59. \olref{thm:completeness} are universally quantified. To make sure we
  60. do not confuse ourselves, let us restate \olref{thm:completeness}
  61. using a different variable: for any set of !!{sentence}s~$\Delta$, if
  62. $\Delta$ is consistent, it is satisfiable. By contraposition, if
  63. $\Delta$ is not satisfiable, then $\Delta$ is inconsistent. We will
  64. use this to prove the corollary.
  66. Suppose that $\Gamma \Entails !A$. Then $\Gamma \cup \{\lnot !A\}$ is
  67. unsatisfiable by \olref[syn][sem]{prop:entails-unsat}. Taking $\Gamma
  68. \cup \{\lnot !A\}$ as our $\Delta$, the previous version of
  69. \olref{thm:completeness} gives us that $\Gamma \cup \{\lnot !A\}$ is
  70. inconsistent. By
  71. \iftag{FOL}{%
  72. \tagrefs{prfAX/{fol:axd:prv:prop:prov-incons},
  73. prfSC/{fol:seq:prv:prop:prov-incons},
  74. prfND/{fol:ntd:prv:prop:prov-incons},
  75. prfTab/{fol:tab:prv:prop:prov-incons}}}{%
  76. \tagrefs{prfAX/{pl:axd:prv:prop:prov-incons},
  77. prfSC/{pl:seq:prv:prop:prov-incons},
  78. prfND/{pl:ntd:prv:prop:prov-incons},
  79. prfTab/{pl:tab:prv:prop:prov-incons}}},
  80. $\Gamma \Proves !A$.
  81. \end{proof}
  83. \tagprob{FOL}
  84. \begin{prob}
  85. Use \olref[fol][com][cth]{cor:completeness} to prove
  86. \olref[fol][com][cth]{thm:completeness}, thus showing that the two
  87. formulations of the completeness theorem are equivalent.
  88. \end{prob}
  89. \tagendprob
  91. \tagprob{notFOL}
  92. \begin{prob}
  93. Use \olref[pl][com][cth]{cor:completeness} to prove
  94. \olref[pl][com][cth]{thm:completeness}, thus showing that the two
  95. formulations of the completeness theorem are equivalent.
  96. \end{prob}
  97. \tagendprob
  99. \tagprob{FOL}
  100. \begin{prob}
  101. In order for !!a{derivation} system to be complete, its rules must be
  102. strong enough to prove every unsatisfiable set inconsistent. Which of
  103. the rules of !!{derivation} were necessary to prove completeness? Are any
  104. of these rules not used anywhere in the proof? In order to answer
  105. these questions, make a list or diagram that shows which of the rules
  106. of !!{derivation} were used in which results that lead up to the proof of
  107. \olref[fol][com][cth]{thm:completeness}. Be sure to note any tacit
  108. uses of rules in these proofs.
  109. \end{prob}
  110. \tagendprob
  112. \tagprob{notFOL}
  113. \begin{prob}
  114. In order for !!a{derivation} system to be complete, its rules must be
  115. strong enough to prove every unsatisfiable set inconsistent. Which of
  116. the rules of !!{derivation} were necessary to prove completeness? Are any
  117. of these rules not used anywhere in the proof? In order to answer
  118. these questions, make a list or diagram that shows which of the rules
  119. of !!{derivation} were used in which results that lead up to the proof of
  120. \olref[pl][com][cth]{thm:completeness}. Be sure to note any tacit
  121. uses of rules in these proofs.
  122. \end{prob}
  123. \tagendprob
  125. \end{document}

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

199 lines; SHA-256 a872b7018576b26eb53179792e27b5b0af3338b5220712086e1be7d928b3d65c. Open preserved source.

  1. % Part: first-order-logic
  2. % Chapter: completeness
  3. % Section: compactness
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{com}{com}}
  11. {\olfileid{pl}{com}{com}}
  13. \olsection{The Compactness Theorem}
  15. One important consequence of the completeness theorem is the
  16. compactness theorem. The compactness theorem states that if each
  17. \emph{finite} subset of a set of !!{sentence}s is satisfiable, the
  18. entire set is satisfiable---even if the set itself is infinite. This
  19. is far from obvious. There is nothing that seems to rule out, at first
  20. glance at least, the possibility of there being infinite sets of
  21. !!{sentence}s which are contradictory, but the contradiction only
  22. arises, so to speak, from the infinite number. The compactness
  23. theorem says that such a scenario can be ruled out: there are no
  24. unsatisfiable infinite sets of !!{sentence}s each finite subset of
  25. which is satisfiable. Like the completeness theorem, it has a version
  26. related to entailment: if an infinite set of !!{sentence}s entails
  27. something, already a finite subset does.
  29. \begin{defn}
  30. A set $\Gamma$ of !!{formula}s is \emph{finitely satisfiable} iff every finite $\Gamma_0 \subseteq \Gamma$ is satisfiable.
  31. \end{defn}
  33. \begin{thm}[Compactness Theorem]
  34. \ollabel{thm:compactness}
  35. The following hold for any sentences $\Gamma$ and $!A$:
  36. \begin{enumerate}
  37. \item $\Gamma \Entails !A$ iff there is a finite $\Gamma_0
  38. \subseteq \Gamma$ such that $\Gamma_0 \Entails !A$.
  39. \item $\Gamma$ is satisfiable iff it is finitely
  40. satisfiable.
  41. \end{enumerate}
  42. \end{thm}
  44. \begin{proof}
  45. We prove (2). If $\Gamma$ is satisfiable, then there is
  46. \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}
  47. such that $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ for all $!A \in
  48. \Gamma$. Of course, this $\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ also
  49. satisfies every finite subset of~$\Gamma$, so $\Gamma$ is finitely
  50. satisfiable.
  52. Now suppose that $\Gamma$ is finitely satisfiable. Then every finite
  53. subset~$\Gamma_0 \subseteq \Gamma$ is satisfiable. By soundness
  54. (\iftag{FOL}{%
  55. \tagrefs{prfAX/{fol:axd:sou:cor:consistency-soundness},
  56. prfSC/{fol:seq:sou:cor:consistency-soundness},
  57. prfND/{fol:ntd:sou:cor:consistency-soundness},
  58. prfTab/{fol:tab:sou:cor:consistency-soundness}}}{%
  59. \tagrefs{prfAX/{pl:axd:sou:cor:consistency-soundness},
  60. prfSC/{pl:seq:sou:cor:consistency-soundness},
  61. prfND/{pl:ntd:sou:cor:consistency-soundness},
  62. prfTab/{pl:tab:sou:cor:consistency-soundness}}}),
  63. every finite subset is consistent. Then $\Gamma$ itself must be
  64. consistent by
  65. \iftag{FOL}{%
  66. \tagrefs{prfAX/{fol:axd:ptn:prop:proves-compact},
  67. prfSC/{fol:seq:ptn:prop:proves-compact},
  68. prfND/{fol:ntd:ptn:prop:proves-compact},
  69. prfTab/{fol:tab:ptn:prop:proves-compact}}}{%
  70. \tagrefs{prfAX/{pl:axd:ptn:prop:proves-compact},
  71. prfSC/{pl:seq:ptn:prop:proves-compact},
  72. prfND/{pl:ntd:ptn:prop:proves-compact},
  73. prfTab/{pl:tab:ptn:prop:proves-compact}}}.
  74. By completeness (\olref[cth]{thm:completeness}), since $\Gamma$~is
  75. consistent, it is satisfiable.
  76. \end{proof}
  78. \tagprob{FOL}
  79. \begin{prob}
  80. Prove (1) of \olref[fol][com][com]{thm:compactness}.
  81. \end{prob}
  82. \tagendprob
  84. \tagprob{notFOL}
  85. \begin{prob}
  86. Prove (1) of \olref[pl][com][com]{thm:compactness}.
  87. \end{prob}
  88. \tagendprob
  90. \iftag{FOL}{%
  91. \begin{ex}
  92. In every model~$\Struct{M}$ of a theory~$\Gamma$, each term~$t$ of
  93. course picks out !!a{element} of~$\Domain{M}$. Can we guarantee that
  94. it is also true that every !!{element} of~$\Domain{M}$ is picked out
  95. by some term or other? In other words, are there theories~$\Gamma$ all
  96. models of which are covered? The compactness theorem shows that this
  97. is not the case if $\Gamma$ has infinite models. Here's how to see
  98. this: Let $\Struct{M}$ be an infinite model of~$\Gamma$, and let $c$
  99. be !!a{constant} not in the language of~$\Gamma$. Let $\Delta$ be the
  100. set of all sentences $\eq/[c][t]$ for $t$ a term in the
  101. language~$\Lang{L}$ of~$\Gamma$, i.e.,
  102. \[
  103. \Delta = \Setabs{\eq/[c][t]}{t \in \Trm[L]}.
  104. \]
  105. A finite subset of $\Gamma \cup \Delta$ can be written as $\Gamma'
  106. \cup \Delta'$, with $\Gamma' \subseteq \Gamma$ and $\Delta' \subseteq
  107. \Delta$. Since $\Delta'$ is finite, it can contain only finitely many
  108. terms. Let $a \in \Domain{M}$ be !!a{element} of $\Domain{M}$ not
  109. picked out by any of them, and let $\Struct{M'}$ be the !!{structure}
  110. that is just like $\Struct{M}$, but also $\Assign{c}{M'} = a$. Since
  111. $a \neq \Value{t}{M}$ for all~$t$ occurring in~$\Delta'$,
  112. $\Sat{M'}{\Delta'}$. Since $\Sat{M}{\Gamma}$, $\Gamma' \subseteq
  113. \Gamma$, and $c$ does not occur in~$\Gamma$, also
  114. $\Sat{M'}{\Gamma'}$. Together, $\Sat{M'}{\Gamma' \cup \Delta'}$ for
  115. every finite subset $\Gamma' \cup \Delta'$ of $\Gamma \cup \Delta$. So
  116. every finite subset of $\Gamma \cup \Delta$ is satisfiable. By
  117. compactness, $\Gamma \cup \Delta$ itself is satisfiable. So there are
  118. models~$\Sat{M}{\Gamma \cup \Delta}$. Every such $\Struct{M}$ is a
  119. model of~$\Gamma$, but is not covered, since $\Value{c}{M} \neq
  120. \Value{t}{M}$ for all terms~$t$ of~$\Lang{L}$.
  121. \end{ex}
  123. \begin{ex}
  124. Consider !!a{language} $\Lang{L}$ containing the !!{predicate}~$<$,
  125. !!{constant}s $\Obj{0}$, $\Obj{1}$, and !!{function}s $+$, $\times$, and
  126. $-$. Let $\Gamma$ be the set of all !!{sentence}s in this
  127. !!{language} true in the !!{structure}~$\Struct{Q}$ with domain~$\Rat$ and the obvious
  128. interpretations. $\Gamma$~is the set of all !!{sentence}s
  129. of~$\Lang{L}$ true about the rational numbers. Of course, in~$\Rat$
  130. (and even in~$\Real$), there are no numbers~$r$ which are greater than~$0$
  131. but less than $1/k$ for all $k \in \PosInt$. Such a number, if it
  132. existed, would be an \emph{infinitesimal:} non-zero, but infinitely
  133. small. The compactness theorem can be used to show that there are
  134. models of~$\Gamma$ in which infinitesimals exist. We do not have
  135. !!a{function} for division in our language (division by zero is
  136. undefined, and !!{function}s have to be interpreted by total functions).
  137. However, we can still express that $r < 1/k$, since this is the case iff
  138. $r \cdot k < 1$. Now let $c$ be a new !!{constant} and let $\Delta$ be
  139. \[
  140. \{\Obj{0} < c\}
  141. \cup \Setabs{ c \times \num k < \Obj{1} }{k \in \PosInt}
  142. \]
  143. (where $\num{k} = (\Obj{1} + (\Obj{1} + \dots + (\Obj{1} +
  144. \Obj{1})\dots))$ with $k$~$\Obj{1}$'s). For any finite
  145. subset~$\Delta_0$ of~$\Delta$ there is a~$K$ such that for all the
  146. !!{sentence}s $c \times \num{k} < \Obj{1}$ in~$\Delta_0$ have $k < K$.
  147. If we expand $\Struct{Q}$ to~$\Struct{Q'}$ with $\Assign{c}{Q'} = 1/K$
  148. we have that $\Sat{Q'}{\Gamma_0 \cup \Delta_0}$ for any finite
  149. $\Gamma_0 \subseteq \Gamma$, and so $\Gamma \cup \Delta$ is finitely
  150. satisfiable (Exercise: prove this in detail). By compactness, $\Gamma
  151. \cup \Delta$ is satisfiable. Any model~$\Struct{S}$ of $\Gamma \cup
  152. \Delta$ contains an infinitesimal, namely~$\Assign{c}{S}$.
  153. \end{ex}
  154. }{}
  156. \tagprob{FOL}
  157. \begin{prob}
  158. In the standard model of arithmetic~$\Struct{N}$, there is no
  159. !!{element}~$k \in \Domain{N}$ which satisfies every formula~$\num{n}
  160. < x$ (where $\num{n}$ is $\Obj{0}^{\prime\dots\prime}$ with $n$
  161. $\prime$'s). Use the compactness theorem to show that the set of
  162. !!{sentence}s in the language of arithmetic which are true in the standard
  163. model of arithmetic $\Struct{N}$ are also true in
  164. !!a{structure}~$\Struct{N'}$ that contains !!a{element} which
  165. \emph{does} satisfy every formula $\num{n} < x$.
  166. \end{prob}
  167. \tagendprob
  169. \iftag{FOL}{
  170. \begin{ex}
  171. We know that first-order logic with !!{identity} can express that the
  172. size of the !!{domain} must have some minimal size: The
  173. sentence~$!A_{\ge n}$ (which says ``there are at least $n$ distinct
  174. objects'') is true only in structures where $\Domain{M}$ has at
  175. least~$n$ objects. So if we take
  176. \[
  177. \Delta = \Setabs{!A_{\ge n}}{n \ge 1}
  178. \]
  179. then any model of $\Delta$ must be infinite. Thus, we can guarantee
  180. that a theory only has infinite models by adding~$\Delta$ to it: the
  181. models of $\Gamma \cup \Delta$ are all and only the infinite models
  182. of~$\Gamma$.
  184. So first-order logic can express infinitude. The compactness theorem
  185. shows that it cannot express finitude, however. For suppose some set
  186. of sentences $\Lambda$ were satisfied in all and only finite
  187. !!{structure}s. Then $\Delta \cup \Lambda$ is finitely
  188. satisfiable. Why? Suppose $\Delta' \cup \Lambda' \subseteq \Delta \cup
  189. \Lambda$ is finite with $\Delta' \subseteq \Delta$ and $\Lambda'
  190. \subseteq \Lambda$. Let $n$ be the largest number such that $!A_{\ge n}
  191. \in \Delta'$. $\Lambda$, being satisfied in all finite structures, has
  192. a model~$\Struct{M}$ with finitely many but $\ge n$ !!{element}s. But
  193. then $\Sat{M}{\Delta' \cup \Lambda'}$. By compactness, $\Delta \cup
  194. \Lambda$ has an infinite model, contradicting the assumption that
  195. $\Lambda$ is satisfied only in finite !!{structure}s.
  196. \end{ex}
  197. }{}
  199. \end{document}

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

161 lines; SHA-256 e6398fcc96ac7a2e787c5128d1b2dbf8f515dbd0e780004831abcfd0c3f327d8. Open preserved source.

  1. % Part: first-order-logic
  2. % Chapter: completeness
  3. % Section: compactness-direct
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{com}{cpd}}
  11. {\olfileid{pl}{com}{cpd}}
  13. \olsection{A Direct Proof of the Compactness Theorem}
  15. We can prove the Compactness Theorem directly, without appealing to
  16. the Completeness Theorem, using the same ideas as in the proof of the
  17. completeness theorem. In the proof of the Completeness Theorem we
  18. started with a consistent set~$\Gamma$ of !!{sentence}s, expanded it
  19. to a consistent\iftag{FOL}{, saturated,}{} and !!{complete}
  20. set~$\Gamma^*$ of !!{sentence}s, and then showed that in the
  21. \iftag{FOL}{term
  22. model~$\Struct{M(\Gamma^*)}$}{!!{valuation}~$\pAssign{v(\Gamma^*)}$}
  23. constructed from $\Gamma^*$, all !!{sentence}s of~$\Gamma$ are true,
  24. so $\Gamma$ is satisfiable.
  26. We can use the same method to show that a finitely satisfiable set of
  27. sentences is satisfiable. We just have to prove the corresponding
  28. versions of the results leading to the truth lemma where we replace
  29. ``consistent'' with ``finitely satisfiable.''
  31. \begin{prop}
  32. \ollabel{prop:fsat-ccs}
  33. Suppose $\Gamma$ is !!{complete} and finitely satisfiable. Then:
  34. \begin{enumerate}
  35. \tagitem{prvAnd}{$(!A \land !B) \in \Gamma$
  36. iff both $!A \in \Gamma$ and $!B \in \Gamma$.}{}
  38. \tagitem{prvOr}{$(!A \lor !B) \in \Gamma$ iff
  39. either $!A \in \Gamma$ or $!B \in \Gamma$.}{}
  41. \tagitem{prvIf}{$(!A \lif !B) \in \Gamma$ iff
  42. either $!A \notin \Gamma$ or $!B \in \Gamma$.}{}
  43. \end{enumerate}
  44. \end{prop}
  46. \tagprob{FOL}
  47. \begin{prob}
  48. Prove \olref[fol][com][cpd]{prop:fsat-ccs}. Avoid the use of $\Proves$.
  49. \end{prob}
  50. \tagendprob
  52. \tagprob{notFOL}
  53. \begin{prob}
  54. Prove \olref[pl][com][cpd]{prop:fsat-ccs}. Avoid the use of $\Proves$.
  55. \end{prob}
  56. \tagendprob
  58. \iftag{FOL}{%
  59. \begin{lem}
  60. \ollabel{lem:fsat-henkin} Every finitely satisfiable set~$\Gamma$ can
  61. be extended to a saturated finitely satisfiable set~$\Gamma'$.
  62. \end{lem}
  63. }{}
  65. \tagprob{FOL}
  66. \begin{prob}
  67. Prove \olref[fol][com][cpd]{lem:fsat-henkin}. (Hint: The crucial step
  68. is to show that if $\Gamma_n$ is finitely satisfiable, so is $\Gamma_n
  69. \cup \{!D_n\}$, without any appeal to !!{derivation}s or consistency.)
  70. \end{prob}
  71. \tagendprob
  73. \iftag{FOL}{
  74. \begin{prop}\ollabel{prop:fsat-instances}
  75. Suppose $\Gamma$ is complete, finitely satisfiable, and saturated.
  76. \begin{tagenumerate}{prvEx,prvAll}
  77. \tagitem{prvEx}{$\lexists[x][!A(x)] \in \Gamma$ iff $!A(t) \in \Gamma$
  78. for at least one closed term~$t$.}{}
  79. \tagitem{prvAll}{$\lforall[x][!A(x)] \in \Gamma$ iff $!A(t) \in \Gamma$
  80. for all closed terms~$t$.}{}
  81. \end{tagenumerate}
  82. \end{prop}
  83. }{}
  85. \tagprob{FOL}
  86. \begin{prob}
  87. Prove \olref[fol][com][cpd]{prop:fsat-instances}.
  88. \end{prob}
  89. \tagendprob
  91. \begin{lem}
  92. \ollabel{lem:fsat-lindenbaum} Every finitely satisfiable set~$\Gamma$
  93. can be extended to !!a{complete} and finitely satisfiable
  94. set~$\Gamma^*$.
  95. \end{lem}
  97. \tagprob{FOL}
  98. \begin{prob}
  99. Prove \olref[fol][com][cpd]{lem:fsat-lindenbaum}. (Hint: the crucial
  100. step is to show that if $\Gamma_n$ is finitely satisfiable, then
  101. either $\Gamma_n \cup \{!A_n\}$ or $\Gamma_n \cup \{\lnot !A_n\}$ is
  102. finitely satisfiable.)
  103. \end{prob}
  104. \tagendprob
  106. \tagprob{notFOL}
  107. \begin{prob}
  108. Prove \olref[pl][com][cpd]{lem:fsat-lindenbaum}. (Hint: the crucial
  109. step is to show that if $\Gamma_n$ is finitely satisfiable, then
  110. either $\Gamma_n \cup \{!A_n\}$ or $\Gamma_n \cup \{\lnot !A_n\}$ is
  111. finitely satisfiable.)
  112. \end{prob}
  113. \tagendprob
  115. \begin{thm}[Compactness]
  116. \ollabel{thm:compactness-direct} $\Gamma$ is satisfiable if and only
  117. if it is finitely satisfiable.
  118. \end{thm}
  120. \begin{proof}
  121. If $\Gamma$ is satisfiable, then there is
  122. \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}
  123. such that $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ for all $!A \in \Gamma$.
  124. Of course, this \iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} also
  125. satisfies every finite subset of~$\Gamma$, so $\Gamma$ is finitely
  126. satisfiable.
  128. Now suppose that $\Gamma$ is finitely satisfiable.\iftag{FOL}{ By
  129. \olref{lem:fsat-henkin}, there is a finitely satisfiable, saturated
  130. set $\Gamma' \supseteq \Gamma$.}{} By \olref{lem:fsat-lindenbaum},
  131. $\iftag{FOL}{\Gamma'}{\Gamma}$ can be extended to !!a{complete} and
  132. finitely satisfiable set~$\Gamma^*$\iftag{FOL}{, and $\Gamma^*$ is
  133. still saturated}{}. Construct the \iftag{FOL}{term
  134. model~$\Struct{M(\Gamma^*)}$}{!!{valuation}~$\pAssign{v(\Gamma^*)}$}
  135. as in \olref[mod]{defn:termmodel}.\iftag{FOL}{ Note that
  136. \olref[mod]{prop:quant-termmodel} did not rely on the fact that
  137. $\Gamma^*$ is consistent (or !!{complete} or saturated, for that
  138. matter), but just on the fact that $\Struct{M(\Gamma^*)}$ is covered.}{}
  139. The proof of the Truth Lemma (\olref[mod]{lem:truth}) goes through if
  140. we replace references to \olref[ccs]{prop:ccs}\iftag{FOL}{ and
  141. \olref[hen]{prop:saturated-instances} by references to
  142. \olref{prop:fsat-ccs} and \olref{prop:fsat-instances}}.
  143. \end{proof}
  145. \tagprob{FOL}
  146. \begin{prob}
  147. Write out the complete proof of the Truth Lemma
  148. (\olref[fol][com][mod]{lem:truth}) in the version required for the
  149. proof of \olref[fol][com][cpd]{thm:compactness-direct}.
  150. \end{prob}
  151. \tagendprob
  153. \tagprob{notFOL}
  154. \begin{prob}
  155. Write out the complete proof of the Truth Lemma
  156. (\olref[pl][com][mod]{lem:truth}) in the version required for the
  157. proof of \olref[pl][com][cpd]{thm:compactness-direct}.
  158. \end{prob}
  159. \tagendprob
  161. \end{document}

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

63 lines; SHA-256 6f442281e52dd720acdd540039544c4e8b998906154aa5c4cf7f5da0d9500c48. Open preserved source.

  1. % Part: first-order-logic
  2. % Chapter: completeness
  3. % Section: downward-ls
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{com}{dls}
  10. \olsection{The L\"owenheim--Skolem Theorem}
  12. The L\"owenheim--Skolem Theorem says that if a theory has an infinite
  13. model, then it also has a model that is at most !!{denumerable}. An
  14. immediate consequence of this fact is that first-order logic cannot
  15. express that the size of !!a{structure} is !!{nonenumerable}: any
  16. !!{sentence} or set of !!{sentence}s satisfied in all
  17. !!{nonenumerable} !!{structure}s is also satisfied in some
  18. !!{enumerable} structure.
  20. \begin{thm}
  21. \ollabel{thm:downward-ls} If $\Gamma$ is consistent then it has
  22. !!a{enumerable} model, i.e., it is satisfiable in !!a{structure}
  23. whose domain is either finite or !!{denumerable}.
  24. \end{thm}
  26. \begin{proof}
  27. If $\Gamma$ is consistent, the !!{structure}~$\Struct M$ delivered by
  28. the proof of the completeness theorem has a domain $\Domain{M}$ that
  29. is no larger than the set of the terms of the language~$\Lang L$. So
  30. $\Struct M$ is at most !!{denumerable}.
  31. \end{proof}
  33. \begin{thm}
  34. \ollabel{noidentity-ls} If $\Gamma$ is a consistent set of !!{sentence}s
  35. in the language of first-order logic without identity, then it has
  36. !!a{denumerable} model, i.e., it is satisfiable in !!a{structure}
  37. whose domain is infinite and !!{enumerable}.
  38. \end{thm}
  40. \begin{proof}
  41. If $\Gamma$ is consistent and contains no sentences in which identity
  42. appears, then the !!{structure}~$\Struct M$ delivered by the proof of
  43. the completeness theorem has a domain $\Domain{M}$ identical to the set
  44. of terms of the language~$\Lang L'$. So $\Struct{M}$ is
  45. !!{denumerable}, since $\Trm[L']$ is.
  46. \end{proof}
  48. \begin{ex}[Skolem's Paradox]
  49. Zermelo--Fraenkel set theory~$\Log{ZFC}$ is a very powerful framework
  50. in which practically all mathematical statements can be expressed,
  51. including facts about the sizes of sets. So for instance, $\Log{ZFC}$
  52. can prove that the set~$\Real$ of real numbers is !!{nonenumerable},
  53. it can prove Cantor's Theorem that the power set of any set is larger
  54. than the set itself, etc. If $\Log{ZFC}$ is consistent, its models
  55. are all infinite, and moreover, they all contain !!{element}s about
  56. which the theory says that they are !!{nonenumerable}, such as the
  57. element that makes true the theorem of~$\Log{ZFC}$ that the power set
  58. of the natural numbers exists. By the L\"owenheim--Skolem Theorem,
  59. $\Log{ZFC}$ also has !!{enumerable} models---models that contain
  60. ``!!{nonenumerable}'' sets but which themselves are !!{enumerable}.
  61. \end{ex}
  63. \end{document}