The Open Logic Text — accessible offline edition

Tableaux — Source and provenance

Tableaux

Source and provenance

All fourteen authority files and all 2,208 lines are shown exactly and packaged byte-for-byte. Seven source defects remain unchanged and are disclosed with explicit reader corrections. Two additional internal source-semantic discrepancies remain unchanged and are disclosed at nineteen exact anchors. Open the exact accepted projected chapter transcript (SHA-256 b334a2859045228ae1f049ebc10f23ab1aa40a487b75fa519cd392adf6dd0bfe). Technical source commit: 9620cc73f9c8e0ad003c514a5d3748f29611c4c0. AI production model: OpenAI Codex gpt-5.6-sol, Ultra. Source authorship remains with the credited Open Logic Project contributors.

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

54 lines; SHA-256 eaf9e7719e1e71efb2b82fa80bae67063790e30ef901686a065a23536e253098. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: tableaux
  4. \documentclass[../../../include/open-logic-chapter]{subfiles}
  6. \begin{document}
  8. \iftag{FOL}
  9. {\olchapter{fol}{tab}{Tableaux}}
  10. {\olchapter{pl}{tab}{Tableaux}}
  12. \begin{editorial}
  13. This chapter presents a signed analytic tableaux system.
  15. To include or exclude material relevant to natural deduction as a
  16. proof system, use the ``prfTab'' tag.
  17. \end{editorial}
  19. \olimport{rules-and-proofs}
  21. \olimport{propositional-rules}
  23. \iftag{FOL}{%
  24. \olimport{quantifier-rules}
  25. }{}
  27. \olimport{derivations}
  29. \olimport{proving-things}
  31. \iftag{FOL}{%
  32. \olimport{proving-things-quant}
  33. }{}
  35. \olimport{proof-theoretic-notions}
  37. \olimport{provability-consistency}
  39. \olimport{provability-propositional}
  41. \iftag{FOL}{%
  42. \olimport{provability-quantifiers}
  43. }{}
  45. \olimport{soundness}
  47. \iftag{FOL}{%
  48. \olimport{identity}
  49. \olimport{soundness-identity}
  50. }{}
  52. \OLEndChapterHook
  54. \end{document}

content/first-order-logic/tableaux/rules-and-proofs.tex

59 lines; SHA-256 93cbe7b304b8ad0c3140c23d139dccdf37df9fe8756cb25d8ca47efe1ee6f84d. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: tableaux
  3. % Section: rules-and-proofs
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{tab}{rul}}
  11. {\olfileid{pl}{tab}{rul}}
  13. \olsection{Rules and \usetoken{P}{tableau}}
  15. !!^a{tableau} is a systematic survey of the possible ways
  16. !!a{sentence} can be true or false in !!a{structure}. The building
  17. blocks of a tableau are !!{signed formula}s: !!{sentence}s plus a
  18. truth value ``sign,'' either $\True$ or~$\False$. These signed
  19. !!{formula}s are arranged in a (downward growing) tree.
  21. \begin{defn}
  22. A \emph{!!{signed formula}} is a pair consisting of a truth value
  23. and !!a{sentence}, i.e., either:
  24. \[
  25. \sFmla{\True}{!A} \text{ or } \sFmla{\False}{!A}.
  26. \]
  27. \end{defn}
  29. Intuitively, we might read $\sFmla{\True}{!A}$ as ``$!A$ might be
  30. true'' and $\sFmla{\False}{!A}$ as ``$!A$ might be false'' (in some
  31. !!{structure}).
  33. Each !!{signed formula} in the tree is either an \emph{assumption}
  34. (which are listed at the very top of the tree), or it is obtained from
  35. !!a{signed formula} above it by one of a number of rules of
  36. inference. There are two rules for each possible !!{main operator} of
  37. the preceding !!{formula}, one for the case where the sign is~$\True$,
  38. and one for the case where the sign is~$\False$. Some rules allow the
  39. tree to branch, and some only add !!{signed formula}s to the branch.
  40. A rule may be (and often must be) applied not to the immediately
  41. preceding !!{signed formula}, but to any !!{signed formula} in the
  42. branch from the root to the place the rule is applied.
  44. A branch is \emph{closed} when it contains both $\sFmla{\True}{!A}$
  45. and $\sFmla{\False}{!A}$. A closed !!{tableau} is one where every branch
  46. is closed. Under the intuitive interpretation, any branch describes a
  47. joint possibility, but $\sFmla{\True}{!A}$ and $\sFmla{\False}{!A}$
  48. are not jointly possible. In other words, if a branch is closed, the
  49. possibility it describes has been ruled out. In particular, that means
  50. that a closed !!{tableau} rules out all possibilities of simultaneously
  51. making every assumption of the form $\sFmla{\True}{!A}$ true and every
  52. assumption of the form~$\sFmla{\False}{!A}$ false.
  54. A closed !!{tableau} \emph{for $!A$} is a closed !!{tableau} with
  55. root~$\sFmla{\False}{!A}$. If such a closed !!{tableau} exists, all
  56. possibilities for~$!A$ being false have been ruled out; i.e., $!A$
  57. must be true in every !!{structure}.
  59. \end{document}

content/first-order-logic/tableaux/propositional-rules.tex

93 lines; SHA-256 0e0a8d69ddabb157d54f03e7ff21416fb0c818e481343f4ac00ee4ba1d5bf151. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: tableaux
  3. % Section: propositional-rules
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{tab}{prl}}
  11. {\olfileid{pl}{tab}{prl}}
  13. \olsection{Propositional Rules}
  15. \subsection{Rules for $\lnot$}
  17. \begin{defish}
  18. \AxiomC{\sFmla{\True}{\lnot !A}}
  19. \RightLabel{\TRule{\True}{\lnot}}
  20. \UnaryInfC{\sFmla{\False}{!A}}
  21. \DisplayProof
  22. \hfill
  23. \AxiomC{\sFmla{\False}{\lnot !A}}
  24. \RightLabel{\TRule{\False}{\lnot}}
  25. \UnaryInfC{\sFmla{\True}{!A}}
  26. \DisplayProof
  27. \end{defish}
  29. \subsection{Rules for $\land$}
  31. \begin{defish}\noindent
  32. \AxiomC{\sFmla{\True}{!A \land !B}}
  33. \RightLabel{\TRule{\True}{\land}}
  34. \UnaryInfC{\sFmla{\True}{!A}}
  35. \noLine
  36. \UnaryInfC{\sFmla{\True}{!B}}
  37. \DisplayProof
  38. \hfill
  39. \AxiomC{\sFmla{\False}{!A \land !B}}
  40. \RightLabel{\TRule{\False}{\land}}
  41. \UnaryInfC{$\sFmla{\False}{!A} \quad \mid \quad \sFmla{\False}{!B}$}
  42. \DisplayProof
  43. \end{defish}
  45. \subsection{Rules for $\lor$}
  47. \begin{defish}
  48. \AxiomC{\sFmla{\True}{!A \lor !B}}
  49. \RightLabel{\TRule{\True}{\lor}}
  50. \UnaryInfC{$\sFmla{\True}{!A} \quad \mid \quad \sFmla{\True}{!B}$}
  51. \DisplayProof
  52. \hfill
  53. \AxiomC{\sFmla{\False}{!A \lor !B}}
  54. \RightLabel{\TRule{\False}{\lor}}
  55. \UnaryInfC{\sFmla{\False}{!A}}
  56. \noLine
  57. \UnaryInfC{\sFmla{\False}{!B}}
  58. \DisplayProof
  59. \end{defish}
  61. \subsection{Rules for $\lif$}
  63. \begin{defish}
  64. \AxiomC{\sFmla{\True}{!A \lif !B}}
  65. \RightLabel{\TRule{\True}{\lif}}
  66. \UnaryInfC{$\sFmla{\False}{!A} \quad \mid \quad \sFmla{\True}{!B}$}
  67. \DisplayProof
  68. \hfill
  69. \AxiomC{\sFmla{\False}{!A \lif !B}}
  70. \RightLabel{\TRule{\False}{\lif}}
  71. \UnaryInfC{\sFmla{\True}{!A}}
  72. \noLine
  73. \UnaryInfC{\sFmla{\False}{!B}}
  74. \DisplayProof
  75. \end{defish}
  77. \subsection{The Cut Rule}
  79. \begin{defish}
  80. \AxiomC{}
  81. \RightLabel{\Cut}
  82. \UnaryInfC{$\sFmla{\True}{!A} \quad \mid \quad \sFmla{\False}{!A}$}
  83. \DisplayProof
  84. \end{defish}
  86. The \Cut{} rule is not applied ``to'' a previous !!{signed formula}; rather,
  87. it allows every branch in !!a{tableau} to be split in two, one branch
  88. containing $\sFmla{\True}{!A}$, the other~$\sFmla{\False}{!A}$. It is
  89. not necessary---any set of !!{signed formula}s with a closed
  90. !!{tableau} has one not using \Cut---but it allows us to combine
  91. !!{tableau}s in a convenient way.
  93. \end{document}

content/first-order-logic/tableaux/quantifier-rules.tex

109 lines; SHA-256 800bfbb72d36d3e2c8f6d652146a797235f1cc785ad66457e2500919e2cc7a80. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: tableaux
  3. % Section: quantifier-rules
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{tab}{qrl}
  11. \olsection{Quantifier Rules}
  13. \subsection{Rules for $\lforall$}
  15. \begin{defish}
  16. \AxiomC{\sFmla{\True}{\lforall[x][!A(x)]}}
  17. \RightLabel{\TRule{\True}{\forall}}
  18. \UnaryInfC{\sFmla{\True}{!A(t)}}
  19. \DisplayProof
  20. \hfill
  21. \AxiomC{\sFmla{\False}{\lforall[x][!A(x)]}}
  22. \RightLabel{\TRule{\False}{\lforall}}
  23. \UnaryInfC{\sFmla{\False}{!A(a)}}
  24. \DisplayProof
  25. \end{defish}
  27. In \TRule{\True}{\lforall}, $t$ is a closed term (i.e., one without
  28. variables). In \TRule{\False}{\lforall}, $a$~is !!a{constant} which
  29. must not occur anywhere in the branch above \TRule{\False}{\lforall}
  30. rule. We call $a$ the \emph{eigenvariable} of the
  31. \TRule{\False}{\forall} inference.\footnote{We use the term
  32. ``eigenvariable'' even though $a$ in the above rule is !!a{constant}.
  33. This has historical reasons.}
  35. \subsection{Rules for $\lexists$}
  37. \begin{defish}
  38. \AxiomC{\sFmla{\True}{\lexists[x][!A(x)]}}
  39. \RightLabel{\TRule{\True}{\lexists}}
  40. \UnaryInfC{\sFmla{\True}{!A(a)}}
  41. \DisplayProof
  42. \hfill
  43. \AxiomC{\sFmla{\False}{\lexists[x][!A(x)]}}
  44. \RightLabel{\TRule{\False}{\lexists}}
  45. \UnaryInfC{\sFmla{\False}{!A(t)}}
  46. \DisplayProof
  47. \end{defish}
  49. Again, $t$~is a closed term, and $a$~is !!a{constant} which does not
  50. occur in the branch above the~\TRule{\True}{\lexists} rule. We call
  51. $a$ the \emph{eigenvariable} of the \TRule{\True}{\lexists} inference.
  53. The condition that an eigenvariable not occur in the branch above the
  54. \TRule{\False}{\lforall} or \TRule{\True}{\lexists} inference is
  55. called the \emph{eigenvariable condition}.
  57. \begin{explain}
  58. Recall the convention that when $!A$ is !!a{formula} with the
  59. !!{variable}~$x$ free, we indicate this by writing~$!A(x)$. In the
  60. same context, $!A(t)$ then is short for~$\Subst{!A}{t}{x}$. So we
  61. could also write the \TRule{\False}{\lexists} rule as:
  62. \begin{prooftree}
  63. \AxiomC{\sFmla{\False}{\lexists[x][!A]}}
  64. \RightLabel{\TRule{\False}{\lexists}}
  65. \UnaryInfC{\sFmla{\False}{\Subst{!A}{t}{x}}}
  66. \end{prooftree}
  67. Note that $t$ may already occur in~$!A$, e.g., $!A$~might
  68. be~$\Atom{\Obj P}{t,x}$. Thus, inferring $\sFmla{\False}{\Atom{\Obj
  69. P}{t,t}}$ from~$ \sFmla{\False}{\lexists[x][\Atom{\Obj P}{t,x}]}$ is
  70. a correct application of~\TRule{\False}{\lexists}. However, the
  71. eigenvariable conditions in \TRule{\False}{\lforall}
  72. and~\TRule{\True}{\lexists} require that the !!{constant}~$a$ does
  73. not occur in~$!A$. So, you cannot correctly infer
  74. $\sFmla{\False}{\Atom{\Obj P}{a,a}}$ from
  75. $\sFmla{\False}{\lforall[x][\Atom{\Obj P}{a,x}]}$
  76. using~$\TRule{\False}{\lforall}$.
  77. \end{explain}
  79. \begin{explain}
  80. In \TRule{\True}{\lforall} and \TRule{\False}{\lexists} there are no
  81. restrictions on the term~$t$. On the other hand, in the
  82. \TRule{\True}{\lexists} and \TRule{\False}{\lforall} rules, the
  83. eigenvariable condition requires that the !!{constant}~$a$ does not
  84. occur anywhere in the branches above the respective inference. It is
  85. necessary to ensure that the system is sound. Without this condition,
  86. the following would be a closed !!{tableau} for
  87. $\lexists[x][\formula{A}(x)] \lif \lforall[x][\formula{A}(x)]$:
  88. \begin{center}
  89. \begin{tableau}{}
  90. [\sFmla{\False}{\lexists[x][\formula{A}(x)] \lif \lforall[x][\formula{A}(x)]}, just=\TAss
  91. [\sFmla{\True}{\lexists[x][\formula{A}(x)]},
  92. just={\TRule{\False}{\lif}[1]}
  93. [\sFmla{\False}{\lforall[x][\formula{A}(x)]},
  94. just={\TRule{\False}{\lif}[1]}
  95. [\sFmla{\True}{\formula{A}(a)},
  96. just={\TRule{\True}{\lexists}[2]}
  97. [\sFmla{\False}{\formula{A}(a)},
  98. just={\TRule{\False}{\lforall}[3]}, close]
  99. ]
  100. ]
  101. ]
  102. ]
  103. \end{tableau}
  104. \end{center}
  105. However, $\lexists[x][\formula{A}(x)] \lif
  106. \lforall[x][\formula{A}(x)]$ is not valid.
  107. \end{explain}
  109. \end{document}

content/first-order-logic/tableaux/derivations.tex

96 lines; SHA-256 3f3e041127342c4f2565632d33c855fcb7a87964d63beb38bd8313c8a71ad294. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: tableaux
  3. % Section: derivations
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{tab}{der}}
  11. {\olfileid{pl}{tab}{der}}
  13. \olsection{\usetoken{P}{tableau}}
  15. \begin{explain}
  16. We've said what an assumption is, and we've given the rules of
  17. inference. !!^{tableau}s are inductively generated from these: each
  18. !!{tableau} either is a single branch consisting of one or more
  19. assumptions, or it results from !!a{tableau} by applying one of the
  20. rules of inference on a branch.
  21. \end{explain}
  23. \begin{defn}[!!^{tableau}]
  24. !!^a{tableau} for assumptions $\sFmla{S_1}{!A_1}$, \dots,
  25. $\sFmla{S_n}{!A_n}$ (where each $S_i$ is either $\True$ or~$\False$) is
  26. a finite tree of !!{signed formula}s satisfying the following conditions:
  27. \begin{enumerate}
  28. \item The $n$ topmost !!{signed formula}s of the tree are
  29. $\sFmla{S_i}{!A_i}$, one below the other.
  30. \item Every !!{signed formula} in the tree that is not one of the
  31. assumptions results from a correct application of an inference rule
  32. to !!a{signed formula} in the branch above it.
  33. \end{enumerate}
  34. A branch of !!a{tableau} is \emph{closed} iff it contains both
  35. $\sFmla{\True}{!A}$ and~$\sFmla{\False}{!A}$, and \emph{open}
  36. otherwise. !!^a{tableau} in which every branch is closed is a
  37. \emph{closed !!{tableau}} (for its set of assumptions). If !!a{tableau} is
  38. not closed, i.e., if it contains at least one open branch, it is
  39. \emph{open}.
  40. \end{defn}
  42. \begin{ex}
  43. Every set of assumptions on its own is !!a{tableau}, but it will
  44. generally not be closed. (Obviously, it is closed only if the
  45. assumptions already contain a pair of !!{signed formula}s
  46. $\sFmla{\True}{!A}$ and~$\sFmla{\False}{!A}$.)
  48. From !!a{tableau} (open or closed) we can obtain a new, larger one by
  49. applying one of the rules of inference to !!a{signed formula}~$!A$
  50. in it. The rule will append one or more !!{signed formula}s to the end of
  51. any branch containing the occurrence of~$!A$ to which we apply the
  52. rule.
  54. For instance, consider the assumption $\sFmla{\True}{!A \land \lnot
  55. !A}$. Here is the (open) !!{tableau} consisting of just that
  56. assumption:
  57. \begin{center}
  58. \begin{tableau}{}
  59. [\sFmla{\True}{\formula{A} \land \lnot \formula{A}}, just=\TAss]
  60. \end{tableau}{}
  61. \end{center}
  62. We obtain a new !!{tableau} from it by applying the $\TRule{\True}{\land}$
  63. rule to the assumption. That rule allows us to add two new lines to
  64. the !!{tableau}, $\sFmla{\True}{!A}$ and $\sFmla{\True}{\lnot !A}$:
  65. \begin{center}
  66. \begin{tableau}{}
  67. [\sFmla{\True}{\formula{A} \land \lnot \formula{A}}, just=\TAss
  68. [\sFmla{\True}{\formula{A}}, just={\TRule{\True}{\land}[1]},
  69. [\sFmla{\True}{\lnot \formula{A}}, just={\TRule{\True}{\land}[1]}
  70. ]
  71. ]
  72. ]
  73. \end{tableau}{}
  74. \end{center}
  75. When we write down !!{tableau}s, we record the rules we've applied
  76. on the right (e.g., $\TRule{\True}{\land} 1$ means that the
  77. !!{signed formula} on that line is the result of applying the
  78. $\TRule{\True}{\land}$ rule to the !!{signed formula} on line~$1$).
  79. This new !!{tableau} now contains additional !!{signed formula}s,
  80. but to only one ($\sFmla{\True}{\lnot !A}$) can we apply a rule (in
  81. this case, the $\TRule{\True}{\lnot}$ rule). This results in the closed
  82. !!{tableau}
  83. \begin{center}
  84. \begin{tableau}{}
  85. [\sFmla{\True}{\formula{A} \land \lnot \formula{A}}, just=\TAss
  86. [\sFmla{\True}{\formula{A}}, just={\TRule{\True}{\land}[1]}
  87. [\sFmla{\True}{\lnot \formula{A}}, just={\TRule{\True}{\land}[1]}
  88. [\sFmla{\False}{\formula{A}}, just={\TRule{\True}{\lnot}[3]}, close]
  89. ]
  90. ]
  91. ]
  92. \end{tableau}{}
  93. \end{center}
  94. \end{ex}
  96. \end{document}

content/first-order-logic/tableaux/proving-things.tex

460 lines; SHA-256 ba6a2d3c2f7c7504daa17942290c75084bbfab92663a492557ca6530a175d914. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: tableaux
  3. % Section: proving-things
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{tab}{pro}}
  11. {\olfileid{pl}{tab}{pro}}
  13. \olsection{Examples of \usetoken{P}{tableau}}
  15. \begin{ex}
  16. Let's find a closed !!{tableau} for the !!{sentence} $(!A \land !B) \lif !A$.
  18. We begin by writing the corresponding assumption at the top of the
  19. !!{tableau}.
  20. \begin{oltableau}
  21. [\sFmla{\False}{(\formula{A} \land \formula{B}) \lif \formula{A}},
  22. just = \TAss]
  23. \end{oltableau}
  25. There is only one assumption, so only one !!{signed formula} to which
  26. we can apply a rule. (For every !!{signed formula}, there is always at
  27. most one rule that can be applied: it's the rule for the corresponding
  28. sign and !!{main operator} of the !!{sentence}.) In this case, this
  29. means, we must apply $\TRule{\False}{\lif}$.
  30. \begin{oltableau}
  31. [\sFmla{\False}{(\formula{A} \land \formula{B}) \lif \formula{A}},
  32. checked, just = \TAss
  33. [\sFmla{\True}{\formula{A} \land \formula{B}},
  34. just={\TRule{\False}{\lif}[1]}
  35. [\sFmla{\False}{\formula{A}}, just={\TRule{\False}{\lif}[1]}]
  36. ]
  37. ]
  38. \end{oltableau}
  39. To keep track of which !!{signed formula}s we have applied their
  40. corresponding rules to, we write a checkmark next to the
  41. sentence. However, \emph{only} write a checkmark if the rule has been
  42. applied to all open branches. Once !!a{signed formula} has had the
  43. corresponding rule applied in every open branch, we will not have to
  44. return to it and apply the rule again. In this case, there is only one
  45. branch, so the rule only has to be applied once. (Note that checkmarks
  46. are only a convenience for constructing tableaux and are not
  47. officially part of the syntax of tableaux.)
  49. There is one new !!{signed formula} to which we can apply a rule: the
  50. $\sFmla{\True}{!A \land !B}$ on line~$2$. Applying the
  51. $\TRule{\True}{\land}$ rule results in:
  52. \begin{oltableau}
  53. [\sFmla{\False}{(\formula{A} \land \formula{B}) \lif \formula{A}},
  54. checked, just = \TAss
  55. [\sFmla{\True}{\formula{A} \land \formula{B}},
  56. just={\TRule{\False}{\lif}[1]}, checked
  57. [\sFmla{\False}{\formula{A}}, just={\TRule{\False}{\lif}[1]}
  58. [\sFmla{\True}{\formula{A}}, just={\TRule{\True}{\land}[2]}
  59. [\sFmla{\True}{\formula{B}}, just={\TRule{\True}{\land}[2]}, close
  60. ]
  61. ]
  62. ]
  63. ]
  64. ]
  65. \end{oltableau}
  66. Since the branch now contains both $\sFmla{\True}{!A}$ (on line~$4$)
  67. and $\sFmla{\False}{!A}$ (on line~$3$), the branch is closed. Since it
  68. is the only branch, the !!{tableau} is closed. We have found
  69. a closed !!{tableau} for~$(!A \land !B) \lif !A$.
  70. \end{ex}
  72. \begin{ex}
  73. Now let's find a closed !!{tableau} for $(\lnot !A \lor !B) \lif (!A
  74. \lif !B)$.
  76. We begin with the corresponding assumption:
  77. \begin{oltableau}
  78. [\sFmla{\False}{(\lnot \formula{A} \lor \formula{B}) \lif
  79. (\formula{A} \lif \formula{B})}, just=\TAss]
  80. \end{oltableau}
  81. The one !!{signed formula} in this !!{tableau} has !!{main operator}~$\lif$
  82. and sign~$\False$, so we apply the $\TRule{\False}{\lif}$ rule to it
  83. to obtain:
  84. \begin{oltableau}
  85. [\sFmla{\False}{(\lnot \formula{A} \lor \formula{B})
  86. \lif (\formula{A} \lif \formula{B})}, just=\TAss, checked
  87. [\sFmla{\True}{\lnot \formula{A} \lor \formula{B}},
  88. just={\TRule{\False}{\lif}[1]}
  89. [\sFmla{\False}{(\formula{A} \lif \formula{B})},
  90. just={\TRule{\False}{\lif}[1]}
  91. ]
  92. ]
  93. ]
  94. \end{oltableau}
  95. We now have a choice as to whether to apply~$\TRule{\True}{\lor}$ to
  96. line~$2$ or $\TRule{\False}{\lif}$ to line~$3$. It actually doesn't
  97. matter which order we pick, as long as each !!{signed formula} has its
  98. corresponding rule applied in every branch. So let's pick the first
  99. one. The $\TRule{\True}{\lor}$ rule allows the !!{tableau} to branch,
  100. and the two conclusions of the rule will be the new !!{signed formula}s
  101. added to the two new branches. This results in:
  102. \begin{oltableau}
  103. [\sFmla{\False}{(\lnot \formula{A} \lor \formula{B}) \lif
  104. (\formula{A} \lif \formula{B})}, just=\TAss, checked
  105. [\sFmla{\True}{\lnot \formula{A} \lor \formula{B}},
  106. just={\TRule{\False}{\lif}[1]}, checked
  107. [\sFmla{\False}{(\formula{A} \lif \formula{B})},
  108. just={\TRule{\False}{\lif}[1]}
  109. [\sFmla{\True}{\lnot \formula{A}}, just={\TRule{\True}{\lor}[2]}]
  110. [\sFmla{\True}{\formula{B}}, just={\TRule{\True}{\lor}[2]}]
  111. ]
  112. ]
  113. ]
  114. \end{oltableau}
  115. We have not applied the $\TRule{\False}{\lif}$ rule to line~$3$ yet:
  116. let's do that now. To save time, we apply it to both branches.
  117. Recall that we write a checkmark next to !!a{signed formula} only if
  118. we have applied the corresponding rule in every open branch. So it's a
  119. good idea to apply a rule at the end of every branch that contains the
  120. !!{signed formula} the rule applies to. That way we won't have to
  121. return to that !!{signed formula} lower down in the various branches.
  122. \begin{oltableau}
  123. [\sFmla{\False}{(\lnot \formula{A} \lor \formula{B}) \lif
  124. (\formula{A} \lif \formula{B})}, just=\TAss, checked
  125. [\sFmla{\True}{\lnot \formula{A} \lor \formula{B}},
  126. just={\TRule{\False}{\lif}[1]}, checked
  127. [\sFmla{\False}{(\formula{A} \lif \formula{B})},
  128. just={\TRule{\False}{\lif}[1]}, checked
  129. [\sFmla{\True}{\lnot \formula{A}}, just={\TRule{\True}{\lor}[2]}
  130. [\sFmla{\True}{\formula{A}}, just={\TRule{\False}{\lif}[3]}
  131. [\sFmla{\False}{\formula{B}}, just={\TRule{\False}{\lif}[3]}]
  132. ]
  133. ]
  134. [\sFmla{\True}{\formula{B}}, just={\TRule{\True}{\lor}[2]}
  135. [\sFmla{\True}{\formula{A}}, just={\TRule{\False}{\lif}[3]}
  136. [\sFmla{\False}{\formula{B}}, just={\TRule{\False}{\lif}[3]}, close]
  137. ]
  138. ]
  139. ]
  140. ]
  141. ]
  142. \end{oltableau}
  143. The right branch is now closed. On the left branch, we can still apply
  144. the $\TRule{\True}{\lnot}$ rule to line~$4$. This results
  145. in~$\sFmla{\False}{!A}$ and closes the left branch:
  146. \begin{oltableau}
  147. [\sFmla{\False}{(\lnot \formula{A} \lor \formula{B}) \lif
  148. (\formula{A} \lif \formula{B})}, just=\TAss, checked
  149. [\sFmla{\True}{\lnot \formula{A} \lor \formula{B}},
  150. just={\TRule{\False}{\lif}[1]}, checked
  151. [\sFmla{\False}{(\formula{A} \lif \formula{B})},
  152. just={\TRule{\False}{\lif}[1]}, checked
  153. [\sFmla{\True}{\lnot \formula{A}}, just={\TRule{\True}{\lor}[2]}
  154. [\sFmla{\True}{\formula{A}}, just={\TRule{\False}{\lif}[3]}
  155. [\sFmla{\False}{\formula{B}}, just={\TRule{\False}{\lif}[3]}
  156. [\sFmla{\False}{\formula{A}},
  157. just={\TRule{\True}{\lnot}[4]}, close]
  158. ]
  159. ]
  160. ]
  161. [\sFmla{\True}{\formula{B}}, just={\TRule{\True}{\lor}[2]}
  162. [\sFmla{\True}{\formula{A}}, just={\TRule{\False}{\lif}[3]}
  163. [\sFmla{\False}{\formula{B}},
  164. just={\TRule{\False}{\lif}[3]}, close]
  165. ]
  166. ]
  167. ]
  168. ]
  169. ]
  170. \end{oltableau}
  171. \end{ex}
  173. \begin{ex}
  174. We can give !!{tableau}s for any number of !!{signed formula}s as
  175. assumptions. Often it is also necessary to apply more than one rule
  176. that allows branching; and in general !!a{tableau} can have any number
  177. of branches. For instance, consider !!a{tableau} for
  178. $\{\sFmla{\True}{!A \lor (!B \land !C)}, \sFmla{\False}{(!A \lor !B) \land (!A
  179. \lor !C)}\}$. We start by applying the $\TRule{\True}{\lor}$ to the
  180. first assumption:
  181. \begin{oltableau}
  182. [\sFmla{\True}{\formula{A} \lor (\formula{B} \land \formula{C})},
  183. just=\TAss, checked
  184. [\sFmla{\False}{(\formula{A} \lor \formula{B}) \land
  185. (\formula{A} \lor \formula{C})}, just=\TAss
  186. [\sFmla{\True}{\formula{A}}, just={\TRule{\True}{\lor}[1]}]
  187. [\sFmla{\True}{\formula{B} \land \formula{C}},
  188. just={\TRule{\True}{\lor}[1]}]
  189. ]
  190. ]
  191. \end{oltableau}
  192. Now we can apply the $\TRule{\False}{\land}$ rule to line~$2$. We do
  193. this on both branches simultaneously, and can therefore check off
  194. line~$2$:
  195. \begin{oltableau}
  196. [\sFmla{\True}{\formula{A} \lor (\formula{B} \land \formula{C})},
  197. just=\TAss, checked
  198. [\sFmla{\False}{(\formula{A} \lor \formula{B}) \land
  199. (\formula{A} \lor \formula{C})}, just=\TAss, checked
  200. [\sFmla{\True}{\formula{A}}, just={\TRule{\True}{\lor}[1]}
  201. [\sFmla{\False}{\formula{A} \lor \formula{B}},
  202. just={\TRule{\False}{\land}[2]}]
  203. [\sFmla{\False}{\formula{A} \lor \formula{C}},
  204. just={\TRule{\False}{\land}[2]}]
  205. ]
  206. [\sFmla{\True}{\formula{B} \land \formula{C}},
  207. just={\TRule{\True}{\lor}[1]}
  208. [\sFmla{\False}{\formula{A} \lor \formula{B}},
  209. just={\TRule{\False}{\land}[2]}]
  210. [\sFmla{\False}{\formula{A} \lor \formula{C}},
  211. just={\TRule{\False}{\land}[2]}]
  212. ]
  213. ]
  214. ]
  215. \end{oltableau}
  216. Now we can apply $\TRule{\False}{\lor}$ to all the branches containing
  217. $!A \lor !B$:
  218. \begin{oltableau}
  219. [\sFmla{\True}{\formula{A} \lor (\formula{B} \land \formula{C})},
  220. just=\TAss, checked
  221. [\sFmla{\False}{(\formula{A} \lor \formula{B}) \land
  222. (\formula{A} \lor \formula{C})}, just=\TAss, checked
  223. [\sFmla{\True}{\formula{A}}, just={\TRule{\True}{\lor}[1]}
  224. [\sFmla{\False}{\formula{A} \lor \formula{B}},
  225. just={\TRule{\False}{\land}[2]}, checked
  226. [\sFmla{\False}{\formula{A}}, just={\TRule{\False}{\lor}[4]}
  227. [\sFmla{\False}{\formula{B}},
  228. just={\TRule{\False}{\lor}[4]}, close]
  229. ]
  230. ]
  231. [\sFmla{\False}{\formula{A} \lor \formula{C}},
  232. just={\TRule{\False}{\land}[2]}]
  233. ]
  234. [\sFmla{\True}{\formula{B} \land \formula{C}},
  235. just={\TRule{\True}{\lor}[1]}
  236. [\sFmla{\False}{\formula{A} \lor \formula{B}},
  237. just={\TRule{\False}{\land}[2]}, checked
  238. [\sFmla{\False}{\formula{A}}, just={\TRule{\False}{\lor}[4]}
  239. [\sFmla{\False}{\formula{B}},
  240. just={\TRule{\False}{\lor}[4]}]
  241. ]
  242. ]
  243. [\sFmla{\False}{\formula{A} \lor \formula{C}},
  244. just={\TRule{\False}{\land}[2]}]
  245. ]
  246. ]
  247. ]
  248. \end{oltableau}
  249. The leftmost branch is now closed. Let's now apply
  250. $\TRule{\False}{\lor}$ to $!A \lor !C$:
  251. \begin{oltableau}
  252. [\sFmla{\True}{\formula{A} \lor (\formula{B} \land \formula{C})},
  253. just=\TAss, checked
  254. [\sFmla{\False}{(\formula{A} \lor \formula{B}) \land
  255. (\formula{A} \lor \formula{C})}, just=\TAss, checked
  256. [\sFmla{\True}{\formula{A}}, just={\TRule{\True}{\lor}[1]}
  257. [\sFmla{\False}{\formula{A} \lor \formula{B}},
  258. just={\TRule{\False}{\land}[2]}, checked
  259. [\sFmla{\False}{\formula{A}},
  260. just={\TRule{\False}{\lor}[4]}
  261. [\sFmla{\False}{\formula{B}},
  262. just={\TRule{\False}{\lor}[4]}, close]
  263. ]
  264. ]
  265. [\sFmla{\False}{\formula{A} \lor \formula{C}},
  266. just={\TRule{\False}{\land}[2]}, checked
  267. [\sFmla{\False}{\formula{A}},
  268. just={\TRule{\False}{\lor}[4]}, move by=2
  269. [\sFmla{\False}{\formula{C}},
  270. just={\TRule{\False}{\lor}[4]}, close]
  271. ]
  272. ]
  273. ]
  274. [\sFmla{\True}{\formula{B} \land \formula{C}},
  275. just={\TRule{\True}{\lor}[1]}
  276. [\sFmla{\False}{\formula{A} \lor \formula{B}},
  277. just={\TRule{\False}{\land}[2]}, checked
  278. [\sFmla{\False}{\formula{A}},
  279. just={\TRule{\False}{\lor}[4]}
  280. [\sFmla{\False}{\formula{B}},
  281. just={\TRule{\False}{\lor}[4]}
  282. ]
  283. ]
  284. ]
  285. [\sFmla{\False}{\formula{A} \lor \formula{C}},
  286. just={\TRule{\False}{\land}[2]}, checked
  287. [\sFmla{\False}{\formula{A}},
  288. just={\TRule{\False}{\lor}[4]}, move by=2
  289. [\sFmla{\False}{\formula{C}},
  290. just={\TRule{\False}{\lor}[4]}]
  291. ]
  292. ]
  293. ]
  294. ]
  295. ]
  296. \end{oltableau}
  297. Note that we moved the result of applying $\TRule{\False}{\lor}$ a
  298. second time below for clarity. In this instance it would not have been
  299. needed, since the justifications would have been the same.
  301. Two branches remain open, and $\sFmla{\True}{!B \land !C}$ on line~$3$
  302. remains unchecked. We apply $\TRule{\True}{\land}$ to it to obtain a
  303. closed !!{tableau}:
  304. \begin{oltableau}
  305. [\sFmla{\True}{\formula{A} \lor (\formula{B} \land \formula{C})},
  306. just=\TAss, checked
  307. [\sFmla{\False}{(\formula{A} \lor \formula{B}) \land
  308. (\formula{A} \lor \formula{C})}, just=\TAss, checked
  309. [\sFmla{\True}{\formula{A}}, just={\TRule{\True}{\lor}[1]}
  310. [\sFmla{\False}{\formula{A} \lor \formula{B}},
  311. just={\TRule{\False}{\land}[2]}, checked
  312. [\sFmla{\False}{\formula{A}},
  313. just={\TRule{\False}{\lor}[4]}
  314. [\sFmla{\False}{\formula{B}},
  315. just={\TRule{\False}{\lor}[4]}, close]
  316. ]
  317. ]
  318. [\sFmla{\False}{\formula{A} \lor \formula{C}},
  319. just={\TRule{\False}{\land}[2]}, checked
  320. [\sFmla{\False}{\formula{A}},
  321. just={\TRule{\False}{\lor}[4]}
  322. [\sFmla{\False}{\formula{C}},
  323. just={\TRule{\False}{\lor}[4]}, close]
  324. ]
  325. ]
  326. ]
  327. [\sFmla{\True}{\formula{B} \land \formula{C}},
  328. just={\TRule{\True}{\lor}[1]}, checked
  329. [\sFmla{\False}{\formula{A} \lor \formula{B}},
  330. just={\TRule{\False}{\land}[2]}, checked
  331. [\sFmla{\False}{\formula{A}},
  332. just={\TRule{\False}{\lor}[4]}
  333. [\sFmla{\False}{\formula{B}},
  334. just={\TRule{\False}{\lor}[4]}
  335. [\sFmla{\True}{\formula{B}},
  336. just={\TRule{\True}{\land}[3]}
  337. [\sFmla{\True}{\formula{C}},
  338. just={\TRule{\True}{\land}[3]},close
  339. ]
  340. ]
  341. ]
  342. ]
  343. ]
  344. [\sFmla{\False}{\formula{A} \lor \formula{C}},
  345. just={\TRule{\False}{\land}[2]}, checked
  346. [\sFmla{\False}{\formula{A}},
  347. just={\TRule{\False}{\lor}[4]}
  348. [\sFmla{\False}{\formula{C}},
  349. just={\TRule{\False}{\lor}[4]}
  350. [\sFmla{\True}{\formula{B}},
  351. just={\TRule{\True}{\land}[3]}
  352. [\sFmla{\True}{\formula{C}},
  353. just={\TRule{\True}{\land}[3]},close
  354. ]
  355. ]
  356. ]
  357. ]
  358. ]
  359. ]
  360. ]
  361. ]
  362. \end{oltableau}
  364. For comparison, here's a closed !!{tableau} for the same set of
  365. assumptions in which the rules are applied in a different order:
  366. \begin{oltableau}
  367. [\sFmla{\True}{\formula{A} \lor (\formula{B} \land \formula{C})},
  368. just=\TAss, checked
  369. [\sFmla{\False}{(\formula{A} \lor \formula{B}) \land
  370. (\formula{A} \lor \formula{C})}, just=\TAss, checked
  371. [\sFmla{\False}{\formula{A} \lor \formula{B}},
  372. just={\TRule{\False}{\land}[2]}, checked
  373. [\sFmla{\False}{\formula{A}},
  374. just={\TRule{\False}{\lor}[3]}
  375. [\sFmla{\False}{\formula{B}},
  376. just={\TRule{\False}{\lor}[3]}
  377. [\sFmla{\True}{\formula{A}},
  378. just={\TRule{\True}{\lor}[1]},close
  379. ]
  380. [\sFmla{\True}{\formula{B} \land \formula{C}},
  381. just={\TRule{\True}{\lor}[1]}, checked
  382. [\sFmla{\True}{\formula{B}},
  383. just={\TRule{\True}{\land}[6]}
  384. [\sFmla{\True}{\formula{C}},
  385. just={\TRule{\True}{\land}[6]},close
  386. ]
  387. ]
  388. ]
  389. ]
  390. ]
  391. ]
  392. [\sFmla{\False}{\formula{A} \lor \formula{C}},
  393. just={\TRule{\False}{\land}[2]}, checked
  394. [\sFmla{\False}{\formula{A}},
  395. just={\TRule{\False}{\lor}[3]}
  396. [\sFmla{\False}{\formula{C}},
  397. just={\TRule{\False}{\lor}[3]}
  398. [\sFmla{\True}{\formula{A}},
  399. just={\TRule{\True}{\lor}[1]},close
  400. ]
  401. [\sFmla{\True}{\formula{B} \land \formula{C}},
  402. just={\TRule{\True}{\lor}[1]}, checked
  403. [\sFmla{\True}{\formula{B}},
  404. just={\TRule{\True}{\land}[6]}
  405. [\sFmla{\True}{\formula{C}},
  406. just={\TRule{\True}{\land}[6]},close
  407. ]
  408. ]
  409. ]
  410. ]
  411. ]
  412. ]
  413. ]
  414. ]
  415. \end{oltableau}
  416. \end{ex}
  418. \begin{prob}
  419. Give closed !!{tableau}s of the following:
  420. \begin{enumerate}
  421. \item $\sFmla{\True}{!A \land (!B \land !C)}, \sFmla{\False}{(!A \land !B) \land !C}$.
  422. \item $\sFmla{\True}{!A \lor (!B \lor !C)}, \sFmla{\False}{(!A \lor !B) \lor !C}$.
  423. \item $\sFmla{\True}{!A \lif (!B \lif !C)}, \sFmla{\False}{!B \lif (!A \lif !C)}$.
  424. \item $\sFmla{\True}{!A}, \sFmla{\False}{\lnot\lnot !A}$.
  425. \end{enumerate}
  426. \end{prob}
  428. \begin{prob}
  429. Give closed !!{tableau}s of the following:
  430. \begin{enumerate}
  431. \item $\sFmla{\True}{(!A \lor !B) \lif !C}, \sFmla{\False}{!A \lif !C}$.
  432. \item $\sFmla{\True}{(!A \lif !C) \land (!B \lif !C)}, \sFmla{\False}{(!A \lor !B) \lif !C}$.
  433. \item $\sFmla{\False}{\lnot(!A \land \lnot !A)}$.
  434. \item $\sFmla{\True}{!B \lif !A}, \sFmla{\False}{\lnot !A \lif \lnot !B}$.
  435. \item $\sFmla{\False}{(!A \lif \lnot !A) \lif \lnot !A}$.
  436. \item $\sFmla{\False}{\lnot(!A \lif !B) \lif \lnot !B}$.
  437. \item $\sFmla{\True}{!A \lif !C}, \sFmla{\False}{\lnot (!A \land \lnot !C)}$.
  438. \item $\sFmla{\True}{!A \land \lnot !C}, \sFmla{\False}{\lnot (!A \lif !C)}$.
  439. \item $\sFmla{\True}{!A \lor !B, \lnot !B}, \sFmla{\False}{!A}$.
  440. \item $\sFmla{\True}{\lnot !A \lor \lnot !B}, \sFmla{\False}{\lnot(!A \land !B)}$.
  441. \item $\sFmla{\False}{(\lnot !A \land \lnot !B) \lif\lnot(!A \lor !B)}$.
  442. \item $\sFmla{\False}{\lnot(!A \lor !B) \lif (\lnot !A \land \lnot !B)}$.
  443. \end{enumerate}
  444. \end{prob}
  446. \begin{prob}
  447. Give closed !!{tableau}s of the following:
  448. \begin{enumerate}
  449. \item $\sFmla{\True}{\lnot(!A \lif !B)}, \sFmla{\False}{!A}$.
  450. \item $\sFmla{\True}{\lnot(!A \land !B)}, \sFmla{\False}{\lnot !A \lor \lnot !B}$.
  451. \item $\sFmla{\True}{!A \lif !B}, \sFmla{\False}{\lnot !A \lor !B}$.
  452. \item $\sFmla{\False}{\lnot \lnot !A \lif !A}$.
  453. \item $\sFmla{\True}{!A \lif !B}, \sFmla{\True}{\lnot !A \lif !B}, \sFmla{\False}{!B}$.
  454. \item $\sFmla{\True}{(!A \land !B) \lif !C}, \sFmla{\False}{(!A \lif !C) \lor (!B \lif !C)}$.
  455. \item $\sFmla{\True}{(!A \lif !B) \lif !A}, \sFmla{\False}{!A}$.
  456. \item $\sFmla{\False}{(!A \lif !B) \lor (!B \lif !C)}$.
  457. \end{enumerate}
  458. \end{prob}
  460. \end{document}

content/first-order-logic/tableaux/proving-things-quant.tex

344 lines; SHA-256 72370c12bee0766fb0e674ebae09ec7940f611ff7f9592284dadfe21516b4032. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: tableaux
  3. % Section: proving-things-quant
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{tab}{prq}
  11. \olsection{\usetoken{P}{tableau} with Quantifiers}
  13. \begin{ex}
  14. When dealing with quantifiers, we have to make sure not to violate the
  15. eigenvariable condition, and sometimes this requires us to play around
  16. with the order of carrying out certain inferences. In general, it
  17. helps to try and take care of rules subject to the eigenvariable
  18. condition first (they will be higher up in the finished !!{tableau}).
  20. Let's see how we'd give !!a{tableau} for the !!{sentence}
  21. $\lexists[x][\lnot !A(x)] \lif \lnot \lforall[x][!A(x)]$.
  22. Starting as usual, we start by recording the assumption,
  23. \begin{oltableau}
  24. [\sFmla{\False}{\lexists[x][\lnot \formula{A}(x)]\lif \lnot
  25. \lforall[x][\formula{A}(x)]}, just=\TAss]
  26. \end{oltableau}
  27. Since the !!{main operator} is $\lif$, we apply the
  28. $\TRule{\False}{\lif}$:
  29. \begin{oltableau}
  30. [\sFmla{\False}{\lexists[x][\lnot \formula{A}(x)]\lif \lnot
  31. \lforall[x][\formula{A}(x)]}, just=\TAss, checked
  32. [\sFmla{\True}{\lexists[x][\lnot \formula{A}(x)]},
  33. just={\TRule{\False}{\lif}[1]}
  34. [\sFmla{\False}{\lnot\lforall[x][\formula{A}(x)]},
  35. just={\TRule{\False}{\lif}[1]}]
  36. ]
  37. ]
  38. \end{oltableau}
  39. The next line to deal with is~$2$. We use
  40. $\TRule{\True}{\lexists}$. This requires a new !!{constant}; since no
  41. !!{constant}s yet occur, we can pick any one, say,~$a$.
  42. \begin{oltableau}
  43. [\sFmla{\False}{\lexists[x][\lnot \formula{A}(x)]\lif \lnot
  44. \lforall[x][\formula{A}(x)]}, just=\TAss, checked
  45. [\sFmla{\True}{\lexists[x][\lnot \formula{A}(x)]},
  46. just={\TRule{\False}{\lif}[1]}, checked
  47. [\sFmla{\False}{\lnot\lforall[x][\formula{A}(x)]},
  48. just={\TRule{\False}{\lif}[1]}
  49. [\sFmla{\True}{\lnot\formula{A}(a)}, just={\TRule{\True}{\lexists}[2]}]
  50. ]
  51. ]
  52. ]
  53. \end{oltableau}
  54. Now we apply $\TRule{\False}{\lnot}$ to line~$3$:
  55. \begin{oltableau}
  56. [\sFmla{\False}{\lexists[x][\lnot \formula{A}(x)]\lif \lnot
  57. \lforall[x][\formula{A}(x)]}, just=\TAss, checked
  58. [\sFmla{\True}{\lexists[x][\lnot \formula{A}(x)]},
  59. just={\TRule{\False}{\lif}[1]}, checked
  60. [\sFmla{\False}{\lnot\lforall[x][\formula{A}(x)]},
  61. just={\TRule{\False}{\lif}[1]}, checked
  62. [\sFmla{\True}{\lnot\formula{A}(a)}, just={\TRule{\True}{\lexists}[2]}
  63. [\sFmla{\True}{\lforall[x][\formula{A}(x)]},
  64. just = {\TRule{\False}{\lnot}[3]}
  65. ]
  66. ]
  67. ]
  68. ]
  69. ]
  70. \end{oltableau}
  71. We obtain a closed !!{tableau} by applying $\TRule{\True}{\lnot}$ to
  72. line~$4$, followed by $\TRule{\True}{\lforall}$ to line~$5$.
  73. \begin{oltableau}
  74. [\sFmla{\False}{\lexists[x][\lnot \formula{A}(x)]\lif \lnot
  75. \lforall[x][\formula{A}(x)]}, just=\TAss, checked
  76. [\sFmla{\True}{\lexists[x][\lnot \formula{A}(x)]},
  77. just={\TRule{\False}{\lif}[1]}, checked
  78. [\sFmla{\False}{\lnot\lforall[x][\formula{A}(x)]},
  79. just={\TRule{\False}{\lif}[1]}, checked
  80. [\sFmla{\True}{\lnot\formula{A}(a)}, just={\TRule{\True}{\lexists}[2]}
  81. [\sFmla{\True}{\lforall[x][\formula{A}(x)]},
  82. just = {\TRule{\False}{\lnot}[3]}
  83. [\sFmla{\False}{\formula{A}(a)}, just={\TRule{\True}{\lnot}[4]}
  84. [\sFmla{\True}{\formula{A}(a)},
  85. just={\TRule{\True}{\lforall}[5]}, close
  86. ]
  87. ]
  88. ]
  89. ]
  90. ]
  91. ]
  92. ]
  93. \end{oltableau}
  94. \end{ex}
  96. \begin{ex}
  97. Let's see how we'd give !!a{tableau} for the set
  98. \[
  99. \sFmla{\False}{\lexists[x][!C(x,b)]},
  100. \sFmla{\True}{\lexists[x][(!A(x) \land !B(x))]},
  101. \sFmla{\True}{\lforall[x][(!B(x) \lif !C(x,b))]}.
  102. \]
  103. Starting as usual, we start with the assumptions:
  104. \begin{oltableau}
  105. [\sFmla{\False}{\lexists[x][\formula{C}(x,b)]}, just=\TAss
  106. [\sFmla{\True}{\lexists[x][(\formula{A}(x) \land \formula{B}(x))]},
  107. just=\TAss
  108. [\sFmla{\True}{\lforall[x][(\formula{B}(x) \lif \formula{C}(x,b))]},
  109. just=\TAss]
  110. ]
  111. ]
  112. \end{oltableau}
  113. We should always apply a rule with the eigenvariable condition first;
  114. in this case that would be $\TRule{\True}{\lexists}$ to
  115. line~$2$. Since the assumptions contain the !!{constant}~$b$, we have
  116. to use a different one; let's pick~$a$ again.
  117. \begin{oltableau}
  118. [\sFmla{\False}{\lexists[x][\formula{C}(x,b)]}, just=\TAss
  119. [\sFmla{\True}{\lexists[x][(\formula{A}(x) \land \formula{B}(x))]},
  120. just=\TAss, checked
  121. [\sFmla{\True}{\lforall[x][(\formula{B}(x) \lif \formula{C}(x,b))]},
  122. just=\TAss
  123. [\sFmla{\True}{\formula{A}(a) \land \formula{B}(a)},
  124. just={\TRule{\True}{\lexists}[2]}]
  125. ]
  126. ]
  127. ]
  128. \end{oltableau}
  129. If we now apply $\TRule{\False}{\lexists}$ to line~$1$ or
  130. $\TRule{\True}{\lforall}$ to line~$3$, we have to decide which term~$t$
  131. to substitute for~$x$. Since there is no eigenvariable condition for
  132. these rules, we can pick any term we like. In some cases we may even
  133. have to apply the rule several times with different~$t$s. But as a
  134. general rule, it pays to pick one of the terms already occurring in the
  135. !!{tableau}---in this case, $a$ and~$b$---and in this case we can
  136. guess that $a$ will be more likely to result in a closed branch.
  137. \begin{oltableau}
  138. [\sFmla{\False}{\lexists[x][\formula{C}(x,b)]}, just=\TAss
  139. [\sFmla{\True}{\lexists[x][(\formula{A}(x) \land \formula{B}(x))]},
  140. just=\TAss, checked
  141. [\sFmla{\True}{\lforall[x][(\formula{B}(x) \lif \formula{C}(x,b))]}, just=\TAss
  142. [\sFmla{\True}{\formula{A}(a) \land \formula{B}(a)}, just={\TRule{\True}{\lexists}[2]}
  143. [\sFmla{\False}{\formula{C}(a,b)}, just={\TRule{\False}{\lexists}[1]}
  144. [\sFmla{\True}{\formula{B}(a) \lif \formula{C}(a,b)},
  145. just={\TRule{\True}{\lforall}[3]}
  146. ]
  147. ]
  148. ]
  149. ]
  150. ]
  151. ]
  152. \end{oltableau}
  153. We don't check the !!{signed formula}s in lines $1$ and $3$, since we may
  154. have to use them again. Now apply $\TRule{\True}{\land}$ to line~$4$:
  155. \begin{oltableau}
  156. [\sFmla{\False}{\lexists[x][\formula{C}(x,b)]}, just=\TAss
  157. [\sFmla{\True}{\lexists[x][(\formula{A}(x) \land \formula{B}(x))]},
  158. just=\TAss, checked
  159. [\sFmla{\True}{\lforall[x][(\formula{B}(x) \lif \formula{C}(x,b))]}, just=\TAss
  160. [\sFmla{\True}{\formula{A}(a) \land \formula{B}(a)},
  161. just={\TRule{\True}{\lexists}[2]}, checked
  162. [\sFmla{\False}{\formula{C}(a,b)}, just={\TRule{\False}{\lexists}[1]}
  163. [\sFmla{\True}{\formula{B}(a) \lif \formula{C}(a,b)},
  164. just={\TRule{\True}{\lforall}[3]}
  165. [\sFmla{\True}{\formula{A}(a)}, just={\TRule{\True}{\land}[4]}
  166. [\sFmla{\True}{\formula{B}(a)}, just={\TRule{\True}{\land}[4]}
  167. ]
  168. ]
  169. ]
  170. ]
  171. ]
  172. ]
  173. ]
  174. ]
  175. \end{oltableau}
  176. If we now apply $\TRule{\True}{\lif}$ to line~$6$, the !!{tableau} closes:
  177. \begin{oltableau}
  178. [\sFmla{\False}{\lexists[x][\formula{C}(x,b)]}, just=\TAss
  179. [\sFmla{\True}{\lexists[x][(\formula{A}(x) \land \formula{B}(x))]},
  180. just=\TAss, checked
  181. [\sFmla{\True}{\lforall[x][(\formula{B}(x) \lif \formula{C}(x,b))]},
  182. just=\TAss
  183. [\sFmla{\True}{\formula{A}(a) \land \formula{B}(a)},
  184. just={\TRule{\True}{\lexists}[2]}, checked
  185. [\sFmla{\False}{\formula{C}(a,b)},
  186. just={\TRule{\False}{\lexists}[1]}
  187. [\sFmla{\True}{\formula{B}(a) \lif \formula{C}(a,b)},
  188. just={\TRule{\True}{\lforall}[3]}, checked
  189. [\sFmla{\True}{\formula{A}(a)},
  190. just={\TRule{\True}{\land}[4]}
  191. [\sFmla{\True}{\formula{B}(a)},
  192. just={\TRule{\True}{\land}[4]}
  193. [\sFmla{\False}{\formula{B}(a)},
  194. just={\TRule{\True}{\lif}[6]},close
  195. ]
  196. [\sFmla{\True}{\formula{C}(a,b)},
  197. just={\TRule{\True}{\lif}[6]},close
  198. ]
  199. ]
  200. ]
  201. ]
  202. ]
  203. ]
  204. ]
  205. ]
  206. ]
  207. \end{oltableau}
  210. \end{ex}
  212. \begin{ex}
  213. We construct !!a{tableau} for the set
  214. \[
  215. \sFmla{\True}{\lforall[x][!A(x)]}, \sFmla{\True}{\lforall[x][!A(x)]
  216. \lif \lexists[y][!B(y)]}, \sFmla{\True}{\lnot\lexists[y][!B(y)]}.
  217. \]
  218. Starting as usual, we write down the assumptions:
  219. \begin{oltableau}
  220. [\sFmla{\True}{\lforall[x][\formula{A}(x)]}, just=\TAss
  221. [\sFmla{\True}{\lforall[x][\formula{A}(x)] \lif
  222. \lexists[y][\formula{B}(y)]}, just=\TAss
  223. [\sFmla{\True}{\lnot\lexists[y][\formula{B}(y)]}, just=\TAss
  224. ]
  225. ]
  226. ]
  227. \end{oltableau}
  228. We begin by applying the $\TRule{\True}{\lnot}$ rule to line~$3$. A
  229. corollary to the rule ``always apply rules with eigenvariable
  230. conditions first'' is ``defer applying quantifier rules without
  231. eigenvariable conditions until needed.'' Also, defer rules that result
  232. in a split.
  233. \begin{oltableau}
  234. [\sFmla{\True}{\lforall[x][\formula{A}(x)]}, just=\TAss
  235. [\sFmla{\True}{\lforall[x][\formula{A}(x)] \lif
  236. \lexists[y][\formula{B}(y)]}, just=\TAss
  237. [\sFmla{\True}{\lnot\lexists[y][\formula{B}(y)]}, just=\TAss, checked
  238. [\sFmla{\False}{\lexists[y][\formula{B}(y)]}, just={\TRule{\True}{\lnot}[3]}]
  239. ]
  240. ]
  241. ]
  242. \end{oltableau}
  243. The new line~$4$ requires $\TRule{\False}{\lexists}$, a quantifier
  244. rule without the eigenvariable condition. So we defer this in favor of
  245. using $\TRule{\True}{\lif}$ on line~$2$.
  246. \begin{oltableau}
  247. [\sFmla{\True}{\lforall[x][\formula{A}(x)]}, just=\TAss
  248. [\sFmla{\True}{\lforall[x][\formula{A}(x)] \lif
  249. \lexists[y][\formula{B}(y)]}, just=\TAss, checked
  250. [\sFmla{\True}{\lnot\lexists[y][\formula{B}(y)]}, just=\TAss, checked
  251. [\sFmla{\False}{\lexists[y][\formula{B}(y)]},
  252. just={\TRule{\True}{\lnot}[3]},
  253. [\sFmla{\False}{\lforall[x][\formula{A}(x)]}, just={\TRule{\True}{\lif}[2]}]
  254. [\sFmla{\True}{\lexists[y][\formula{B}(y)]}, just={\TRule{\True}{\lif}[2]}]
  255. ]
  256. ]
  257. ]
  258. ]
  259. \end{oltableau}
  260. Both new !!{signed formula}s require rules with eigenvariable conditions, so
  261. these should be next:
  262. \begin{oltableau}
  263. [\sFmla{\True}{\lforall[x][\formula{A}(x)]}, just=\TAss
  264. [\sFmla{\True}{\lforall[x][\formula{A}(x)] \lif
  265. \lexists[y][\formula{B}(y)]}, just=\TAss, checked
  266. [\sFmla{\True}{\lnot\lexists[y][\formula{B}(y)]}, just=\TAss, checked
  267. [\sFmla{\False}{\lexists[y][\formula{B}(y)]},
  268. just={\TRule{\True}{\lnot}[3]}
  269. [\sFmla{\False}{\lforall[x][\formula{A}(x)]}, just={\TRule{\True}{\lif}[2]},checked
  270. [\sFmla{\False}{\formula{A}(b)}, just={\TRule{\False}{\lforall}[5]}]
  271. ]
  272. [\sFmla{\True}{\lexists[y][\formula{B}(y)]}, just={\TRule{\True}{\lif}[2]},checked
  273. [\sFmla{\True}{\formula{B}(c)}, just={\TRule{\True}{\lexists}[5]}]
  274. ]
  275. ]
  276. ]
  277. ]
  278. ]
  279. \end{oltableau}
  280. To close the branches, we have to use the !!{signed formula}s on lines $1$
  281. and~$3$. The corresponding rules (\TRule{\True}{\lforall} and
  282. \TRule{\False}{\lexists}) don't have eigenvariable conditions, so we
  283. are free to pick whichever terms are suitable. In this case, that's
  284. $b$ and~$c$, respectively.
  285. \begin{oltableau}
  286. [\sFmla{\True}{\lforall[x][\formula{A}(x)]}, just=\TAss
  287. [\sFmla{\True}{\lforall[x][\formula{A}(x)] \lif
  288. \lexists[y][\formula{B}(y)]}, just=\TAss, checked
  289. [\sFmla{\True}{\lnot\lexists[y][\formula{B}(y)]}, just=\TAss, checked
  290. [\sFmla{\False}{\lexists[y][\formula{B}(y)]},
  291. just={\TRule{\True}{\lnot}[3]}
  292. [\sFmla{\False}{\lforall[x][\formula{A}(x)]},
  293. just={\TRule{\True}{\lif}[2]},checked
  294. [\sFmla{\False}{\formula{A}(b)},
  295. just={\TRule{\False}{\lforall}[5]}
  296. [\sFmla{\True}{\formula{A}(b)},
  297. just={\TRule{\True}{\lforall}[1]},close
  298. ]
  299. ]
  300. ]
  301. [\sFmla{\True}{\lexists[y][\formula{B}(y)]},
  302. just={\TRule{\True}{\lif}[2]},checked
  303. [\sFmla{\True}{\formula{B}(c)},
  304. just={\TRule{\True}{\lexists}[5]}
  305. [\sFmla{\False}{\formula{B}(c)},
  306. just={\TRule{\False}{\lexists}[4]},close
  307. ]
  308. ]
  309. ]
  310. ]
  311. ]
  312. ]
  313. ]
  314. \end{oltableau}
  315. \end{ex}
  317. \begin{prob}
  318. Give closed !!{tableau}s of the following:
  319. \begin{enumerate}
  320. \item $\sFmla{\False}{(\lforall[x][!A(x)] \land \lforall[y][!B(y)])
  321. \lif \lforall[z][(!A(z) \land !B(z))]}$.
  322. \item $\sFmla{\False}{(\lexists[x][!A(x)] \lor \lexists[y][!B(y)])
  323. \lif \lexists[z][(!A(z) \lor !B(z))]}$.
  324. \item $\sFmla{\True}{\lforall[x][(!A(x) \lif !B)]},
  325. \sFmla{\False}{\lexists[y][!A(y)] \lif !B}$.
  326. \item $\sFmla{\True}{\lforall[x][\lnot !A(x)]},
  327. \sFmla{\False}{\lnot\lexists[x][!A(x)]}$.
  328. \item $\sFmla{\False}{\lnot\lexists[x][!A(x)] \lif \lforall[x][\lnot
  329. !A(x)]}$.
  330. \item $\sFmla{\False}{\lnot\lexists[x][\lforall[y][((!A(x,y) \lif
  331. \lnot !A(y,y)) \land (\lnot !A(y,y) \lif !A(x,y)))]]}$.
  332. \end{enumerate}
  333. \end{prob}
  335. \begin{prob}
  336. Give closed !!{tableau}s of the following:
  337. \begin{enumerate}
  338. \item $\sFmla{\False}{\lnot\lforall[x][!A(x)] \lif \lexists[x][\lnot!A(x)]}$.
  339. \item $\sFmla{\True}{(\lforall[x][!A(x)] \lif !B)}, \sFmla{\False}{\lexists[y][(!A(y) \lif !B)]}$.
  340. \item $\sFmla{\False}{\lexists[x][(!A(x) \lif \lforall[y][!A(y)])]}$.
  341. \end{enumerate}
  342. \end{prob}
  344. \end{document}

content/first-order-logic/tableaux/proof-theoretic-notions.tex

190 lines; SHA-256 bad25c1ba9db9de17f7c2ff5fffa2c4f9f00aa13d23c197e5337fe759d6fdd39. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: tableaux
  3. % Section: proof-theoretic-notions
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{tab}{ptn}}
  11. {\olfileid{pl}{tab}{ptn}}
  13. \olsection{Proof-Theoretic Notions}
  15. \begin{editorial}
  16. This section collects the definitions of the provability relation
  17. and consistency for tableaux.
  18. \end{editorial}
  20. \begin{explain}
  21. Just as we've defined a number of important semantic notions
  22. (validity, entailment, satisfiability), we now define corresponding
  23. \emph{proof-theoretic notions}. These are not defined by appeal to
  24. satisfaction of !!{sentence}s in !!{structure}s, but by appeal to the
  25. existence of certain closed !!{tableau}x. It was an important
  26. discovery that these notions coincide. That they do is the content of
  27. the \emph{soundness} and \emph{completeness theorems}.
  28. \end{explain}
  31. \begin{defn}[Theorems]
  32. A !!{sentence}~$!A$ is a \emph{theorem} if there is a closed
  33. !!{tableau} for~$\sFmla{\False}{!A}$. We write $\Proves !A$ if $!A$
  34. is a theorem and $\Proves/ !A$ if it is not.
  35. \end{defn}
  37. \begin{defn}[!!^{derivability}]
  38. !!^a{sentence} $!A$ is \emph{!!{derivable} from} a set of
  39. !!{sentence}s~$\Gamma$, $\Gamma \Proves !A$ iff there is a
  40. finite set $\{!B_1, \dots, !B_n\} \subseteq \Gamma$
  41. and a closed !!{tableau} for the set
  42. \[
  43. \{
  44. \sFmla{\False}{!A},
  45. \sFmla{\True}{!B_1}, \dots,
  46. \sFmla{\True}{!B_n}
  47. \}.
  48. \]
  49. If $!A$ is not !!{derivable} from $\Gamma$ we write $\Gamma \Proves/
  50. !A$.
  51. \end{defn}
  53. \begin{defn}[Consistency]
  54. A set of !!{sentence}s~$\Gamma$ is \emph{inconsistent} iff there is a
  55. finite set $\{!B_1, \dots, !B_n\} \subseteq \Gamma$ and a closed
  56. !!{tableau} for the set
  57. \[
  58. \{
  59. \sFmla{\True}{!B_1}, \dots,
  60. \sFmla{\True}{!B_n}
  61. \}.
  62. \]
  63. If $\Gamma$ is not inconsistent, we say it is \emph{consistent}.
  64. \end{defn}
  66. \begin{prop}[Reflexivity]
  67. \ollabel{prop:reflexivity}
  68. If $!A \in \Gamma$, then $\Gamma \Proves !A$.
  69. \end{prop}
  71. \begin{proof}
  72. If $!A \in \Gamma$, $\{!A\}$ is a finite subset of~$\Gamma$ and the !!{tableau}
  73. \begin{oltableau}
  74. [\sFmla{\False}{\formula{A}}, just = \TAss
  75. [\sFmla{\True}{\formula{A}}, just = \TAss,close]
  76. ]
  77. \end{oltableau}
  78. is closed.
  79. \end{proof}
  82. \begin{prop}[Monotonicity]
  83. \ollabel{prop:monotonicity}
  84. If $\Gamma \subseteq \Delta$ and $\Gamma \Proves !A$, then $\Delta
  85. \Proves !A$.
  86. \end{prop}
  88. \begin{proof}
  89. Any finite subset of~$\Gamma$ is also a finite subset of~$\Delta$.
  90. \end{proof}
  92. \begin{prop}[Transitivity]
  93. \ollabel{prop:transitivity}
  94. If $\Gamma \Proves !A$ and $\{!A\} \cup
  95. \Delta \Proves !B$, then $\Gamma \cup \Delta \Proves !B$.
  96. \end{prop}
  98. \begin{proof}
  99. If $\{!A\} \cup \Delta \Proves !B$, then there is a finite subset $\Delta_0 =
  100. \{!C_1, \dots, !C_n\} \subseteq \Delta$ such that
  101. \begin{align*}
  102. \{\sFmla{\False}{!B}, & \sFmla{\True}{!A}, \sFmla{\True}{!C_1},
  103. \dots, \sFmla{\True}{!C_n}\}
  104. \intertext{has a closed !!{tableau}. If $\Gamma \Proves !A$ then there
  105. are $!D_1$, \dots, $!D_m \subseteq \Gamma$ such that}
  106. \{\sFmla{\False}{!A}, & \sFmla{\True}{!D_1},
  107. \dots, \sFmla{\True}{!D_m}\}
  108. \end{align*}
  109. has a closed !!{tableau}.
  111. Now consider the !!{tableau} with assumptions
  112. \[
  113. \sFmla{\False}{!B},
  114. \sFmla{\True}{!C_1}, \dots, \sFmla{\True}{!C_n},
  115. \sFmla{\True}{!D_1}, \dots, \sFmla{\True}{!D_m}.
  116. \]
  117. Apply the \Cut{} rule on~$!A$. This generates two branches, one has
  118. $\sFmla{\True}{!A}$ in it, the other $\sFmla{\False}{!A}$. Thus,
  119. on the one branch, all of
  120. \[
  121. \{\sFmla{\False}{!B}, \sFmla{\True}{!A},
  122. \sFmla{\True}{!C_1}, \dots, \sFmla{\True}{!C_n}\}
  123. \]
  124. are available. Since there is a closed !!{tableau} for these
  125. assumptions, we can attach it to that branch; every branch through
  126. $\sFmla{\True}{!A}$ closes. On the other branch, all of
  127. \[
  128. \{\sFmla{\False}{!A}, \sFmla{\True}{!D_1}, \dots,
  129. \sFmla{\True}{!D_m}\}
  130. \]
  131. are available, so we can also complete the other side to obtain a
  132. closed !!{tableau}. This shows $\Gamma \cup \Delta \Proves !B$.
  133. \end{proof}
  135. Note that this means that in particular if $\Gamma \Proves !A$ and $!A
  136. \Proves !B$, then $\Gamma \Proves !B$. It follows also that if $!A_1,
  137. \dots, !A_n \Proves !B$ and $\Gamma \Proves !A_i$ for each~$i$, then
  138. $\Gamma \Proves !B$.
  140. \begin{prop}
  141. \ollabel{prop:incons}
  142. $\Gamma$ is inconsistent iff $\Gamma \Proves !A$ for every
  143. !!{sentence}~$!A$.
  144. \end{prop}
  146. \begin{proof}
  147. Exercise.
  148. \end{proof}
  150. \tagprob{FOL}
  151. \begin{prob}
  152. Prove \olref[fol][tab][ptn]{prop:incons}
  153. \end{prob}
  154. \tagendprob
  156. \tagprob{notFOL}
  157. \begin{prob}
  158. Prove \olref[pl][tab][ptn]{prop:incons}
  159. \end{prob}
  160. \tagendprob
  162. \begin{prop}[Compactness]
  163. \ollabel{prop:proves-compact}
  164. \begin{enumerate}
  165. \item If $\Gamma \Proves !A$ then there is a finite subset $\Gamma_0
  166. \subseteq \Gamma$ such that $\Gamma_0 \Proves !A$.
  167. \item If every finite subset of~$\Gamma$ is
  168. consistent, then $\Gamma$ is consistent.
  169. \end{enumerate}
  170. \end{prop}
  172. \begin{proof}
  173. \begin{enumerate}
  174. \item If $\Gamma \Proves !A$, then there is a finite subset
  175. $\Gamma_0 = \{!B_1, \dots, !B_n\}$ and a closed !!{tableau} for
  176. \[
  177. \{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}
  178. \]
  179. This !!{tableau} also shows $\Gamma_0 \Proves !A$.
  180. \item If $\Gamma$ is inconsistent, then for some finite subset
  181. $\Gamma_0 = \{!B_1, \dots, !B_n\}$ there is a closed !!{tableau}
  182. for
  183. \[
  184. \{\sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}
  185. \]
  186. This closed !!{tableau} shows that $\Gamma_0$ is inconsistent.
  187. \end{enumerate}
  188. \end{proof}
  190. \end{document}

content/first-order-logic/tableaux/provability-consistency.tex

150 lines; SHA-256 6d159d1c93f6b4bb24cf3d16e7f18096e15881679ef5f64db5b25cee57cccdef. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: tableaux
  3. % Section: provability-consistency
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{tab}{prv}}
  11. {\olfileid{pl}{tab}{prv}}
  13. \olsection{\usetoken{S}{derivability} and Consistency}
  15. We will now establish a number of properties of the !!{derivability}
  16. relation. They are independently interesting, but each will play a
  17. role in the proof of the completeness theorem.
  19. \begin{prop}\ollabel{prop:provability-contr}
  20. If $\Gamma \Proves !A$ and $\Gamma \cup \{!A\}$ is
  21. inconsistent, then $\Gamma$ is inconsistent.
  22. \end{prop}
  24. \begin{proof}
  25. There are finite $\Gamma_0 = \{!B_1, \dots, !B_n\}$ and $\Gamma_1
  26. =\{!C_1, \dots, !C_n\} \subseteq \Gamma$ such that
  27. \begin{align*}
  28. \{\sFmla{\False}{!A}, &
  29. \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\} \\
  30. \{\sFmla{\True}{!A}, &
  31. \sFmla{\True}{!C_1}, \dots, \sFmla{\True}{!C_m}\}
  32. \end{align*}
  33. have closed !!{tableau}s. Using the \Cut{} rule on $!A$ we can
  34. combine these into a single closed !!{tableau} that shows $\Gamma_0
  35. \cup \Gamma_1$ is inconsistent. Since $\Gamma_0
  36. \subseteq \Gamma$ and $\Gamma_1 \subseteq \Gamma$, $\Gamma_0 \cup
  37. \Gamma_1 \subseteq \Gamma$, hence $\Gamma$~is inconsistent.
  38. \end{proof}
  40. \begin{prop}
  41. \ollabel{prop:prov-incons}
  42. $\Gamma \Proves !A$ iff $\Gamma \cup \{\lnot !A\}$ is inconsistent.
  43. \end{prop}
  45. \begin{proof}
  46. First suppose $\Gamma \Proves !A$, i.e., there is
  47. a closed !!{tableau} for
  48. \[
  49. \{\sFmla{\False}{!A},
  50. \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}
  51. \]
  52. Using the $\TRule{\True}{\lnot}$ rule, this can be turned into a
  53. closed !!{tableau} for
  54. \[
  55. \{\sFmla{\True}{\lnot !A},
  56. \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}.
  57. \]
  59. On the other hand, if there is a closed !!{tableau} for the latter, we
  60. can turn it into a closed !!{tableau} of the former by removing every
  61. formula that results from \TRule{\True}{\lnot} applied to the first
  62. assumption~$\sFmla{\True}{\lnot !A}$ as well as that assumption, and
  63. adding the assumption $\sFmla{\False}{!A}$. For if a branch was closed
  64. before because it contained the conclusion of \TRule{\True}{\lnot}
  65. applied to $\sFmla{\True}{\lnot !A}$, i.e., $\sFmla{\False}{!A}$, the
  66. corresponding branch in the new !!{tableau} is also closed. If a
  67. branch in the old tableau was closed because it contained the
  68. assumption $\sFmla{\True}{\lnot !A}$ as well as $\sFmla{\False}{\lnot
  69. !A}$ we can turn it into a closed branch by applying
  70. $\TRule{\False}{\lnot}$ to $\sFmla{\False}{\lnot !A}$ to obtain
  71. $\sFmla{\True}{!A}$. This closes the branch since we added
  72. $\sFmla{\False}{!A}$ as an assumption.
  73. \end{proof}
  75. \begin{prob}
  76. Prove that $\Gamma \Proves \lnot !A$ iff $\Gamma \cup \{!A\}$ is inconsistent.
  77. \end{prob}
  79. \begin{prop}\ollabel{prop:explicit-inc}
  80. If $\Gamma \Proves !A$ and $\lnot !A \in \Gamma$, then $\Gamma$ is
  81. inconsistent.
  82. \end{prop}
  84. \begin{proof}
  85. Suppose $\Gamma \Proves !A$ and $\lnot !A \in \Gamma$. Then there
  86. are $!B_1$, \dots, $!B_n \in \Gamma$ such that \
  87. \[
  88. \{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}
  89. \]
  90. has a closed tableau. Replace the assumption \sFmla{\False}{!A} by
  91. \sFmla{\True}{\lnot !A}, and insert the conclusion of
  92. \TRule{\True}{\lnot} applied to \sFmla{\False}{!A} after the
  93. assumptions. Any !!{sentence} in the !!{tableau} justified by appeal
  94. to line~$1$ in the old !!{tableau} is now justified by appeal to
  95. line~$n+1$. So if the old !!{tableau} was closed, the new one is.
  96. It shows that $\Gamma$ is inconsistent, since all assumptions are
  97. in~$\Gamma$.
  98. \end{proof}
  100. \begin{prop}\ollabel{prop:provability-exhaustive}
  101. If $\Gamma \cup \{!A\}$ and $\Gamma \cup \{\lnot !A\}$ are both
  102. inconsistent, then $\Gamma$ is inconsistent.
  103. \end{prop}
  105. \begin{proof}
  106. If there are $!B_1$, \dots, $!B_n \in \Gamma$ and $!C_1$, \dots,
  107. $!C_m \in \Gamma$ such that
  108. \begin{align*}
  109. \{\sFmla{\True}{!A}, &
  110. \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\} \text{ and}\\
  111. \{\sFmla{\True}{\lnot !A}, &
  112. \sFmla{\True}{!C_1}, \dots, \sFmla{\True}{!C_m}\}
  113. \end{align*}
  114. both have closed !!{tableau}s, we can construct a single, combined
  115. !!{tableau} that shows that $\Gamma$ is inconsistent by using as
  116. assumptions $\sFmla{\True}{!B_1}$, \dots, $\sFmla{\True}{!B_n}$
  117. together with $\sFmla{\True}{!C_1}$, \dots, $\sFmla{\True}{!C_m}$,
  118. followed by an application of the \Cut{} rule. This yields two
  119. branches, one starting with $\sFmla{\True}{!A}$, the other with
  120. $\sFmla{\False}{!A}$.
  122. On the left left side, add the part of the first
  123. !!{tableau} below its assumptions. Here, every rule application is still
  124. correct, since each of the assumptions of the first !!{tableau},
  125. including $\sFmla{\True}{!A}$, is available. Thus, every branch
  126. below $\sFmla{\True}{!A}$ closes.
  128. On the right side, add the part of the second !!{tableau} below its
  129. assumption, with the results of any applications
  130. of~$\TRule{\True}{\lnot}$ to $\sFmla{\True}{\lnot !A}$ removed. The
  131. conclusion of $\TRule{\True}{\lnot}$ to $\sFmla{\True}{\lnot !A}$ is
  132. $\sFmla{\False}{!A}$, which is nevertheless available, as it is the
  133. conclusion of the \Cut{} rule on the right side of the combined !!{tableau}.
  135. If a branch in the second tableau was closed because it contained
  136. the assumption $\sFmla{\True}{\lnot !A}$ (which no longer appears as
  137. an assumption in the combined !!{tableau}) as well as
  138. $\sFmla{\False}{\lnot !A}$, we can applying $\TRule{\False}{\lnot}$
  139. to $\sFmla{\False}{\lnot !A}$ to obtain $\sFmla{\True}{!A}$. Now the
  140. corresponding branch in the combined !!{tableau} also closes,
  141. because it contains the right-hand conclusion of the \Cut{} rule,
  142. $\sFmla{\False}{!A}$. If a branch in the second !!{tableau} closed
  143. for any other reason, the corresponding branch in the combined
  144. !!{tableau} also closes, since any !!{signed formula}s other than
  145. $\sFmla{\True}{\lnot !A}$ occurring on the branch in the old, second
  146. !!{tableau} also occur on the corresponding branch in the combined
  147. !!{tableau}.
  148. \end{proof}
  150. \end{document}

content/first-order-logic/tableaux/provability-propositional.tex

175 lines; SHA-256 5df9f0cf1b10689babb2051daad6426e2abee00e55001f14a896d1a37ae30446. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: tableaux
  3. % Section: provability-propositional
  5. % verification of properties of provability needed for maximally
  6. % consistent sets in the completeness chapter.
  8. \documentclass[../../../include/open-logic-section]{subfiles}
  10. \begin{document}
  12. \iftag{FOL}
  13. {\olfileid{fol}{tab}{ppr}}
  14. {\olfileid{pl}{tab}{ppr}}
  16. \olsection{\usetoken{S}{derivability} and the Propositional Connectives}
  18. \begin{explain}
  19. We establish that the !!{derivability} relation~$\Proves$ of
  20. tableaux is strong enough to establish some basic facts involving
  21. the propositional connectives, such as that $!A \land !B \Proves !A$
  22. and $!A, !A \lif !B \Proves !B$ (modus ponens). These facts are
  23. needed for the proof of the completeness theorem.
  24. \end{explain}
  26. \begin{prop}\ollabel{prop:provability-land}
  27. \begin{enumerate}
  28. \item \ollabel{prop:provability-land-left} Both $!A \land !B \Proves
  29. !A$ and $!A \land !B \Proves !B$.
  30. \item \ollabel{prop:provability-land-right} $!A, !B \Proves !A \land
  31. !B$.
  32. \end{enumerate}
  33. \end{prop}
  35. \begin{proof}
  36. \begin{enumerate}
  37. \item Both $\{\sFmla{\False}{!A}, \sFmla{\True}{!A \land !B}\}$ and
  38. $\{\sFmla{\False}{!B}, \sFmla{\True}{!A \land !B}\}$ have closed
  39. !!{tableau}s
  40. \begin{oltableau}{}
  41. [\sFmla{\False}{\formula{A}}, just=\TAss
  42. [\sFmla{\True}{\formula{A} \land \formula{B}}, just=\TAss
  43. [\sFmla{\True{\formula{A}}},just={\TRule{\True}{\land}[2]}
  44. [\sFmla{\True{\formula{B}}},just={\TRule{\True}{\land}[2]}, close
  45. ]
  46. ]
  47. ]
  48. ]
  49. \end{oltableau}
  50. \begin{oltableau}{}
  51. [\sFmla{\False}{\formula{B}}, just=\TAss
  52. [\sFmla{\True}{\formula{A} \land \formula{B}}, just=\TAss
  53. [\sFmla{\True{\formula{A}}},just={\TRule{\True}{\land}[2]}
  54. [\sFmla{\True{\formula{B}}},just={\TRule{\True}{\land}[2]}, close
  55. ]
  56. ]
  57. ]
  58. ]
  59. \end{oltableau}
  60. \item Here is a closed !!{tableau} for $\{\sFmla{\True}{!A},
  61. \sFmla{\True}{!B}, \sFmla{\False}{!A \land !B}\}$:
  62. \begin{oltableau}
  63. [\sFmla{\False}{\formula{A} \land \formula{B}}, just = \TAss
  64. [\sFmla{\True}{\formula{A}}, just = \TAss
  65. [\sFmla{\True}{\formula{B}}, just=\TAss
  66. [\sFmla{\False}{\formula{A}}, just = {\TRule{\False}{\land}[1]}, close]
  67. [\sFmla{\False}{\formula{B}}, just = {\TRule{\False}{\land}[1]}, close]
  68. ]
  69. ]
  70. ]
  71. \end{oltableau}
  72. \end{enumerate}
  73. \end{proof}
  75. \begin{prop}\ollabel{prop:provability-lor}
  76. \begin{enumerate}
  77. \item $\{!A \lor !B, \lnot !A, \lnot !B\}$ is inconsistent.
  78. \item Both $!A \Proves !A \lor !B$ and $!B \Proves !A \lor !B$.
  79. \end{enumerate}
  80. \end{prop}
  82. \begin{proof}
  83. \begin{enumerate}
  84. \item We give a closed !!{tableau} of $\{\sFmla{\True}{!A \lor !B},
  85. \sFmla{\True}{\lnot !A}, \sFmla{\True}{\lnot !B}\}$:
  86. \begin{oltableau}
  87. [\sFmla{\True}{\formula{A} \lor \formula{B}}, just = \TAss
  88. [\sFmla{\True}{\lnot \formula{A}}, just = \TAss
  89. [\sFmla{\True}{\lnot \formula{B}}, just = \TAss
  90. [\sFmla{\False}{\formula{A}}, just = {\TRule{\True}{\lnot}[2]}
  91. [\sFmla{\False}{\formula{B}}, just = {\TRule{\True}{\lnot}[3]}
  92. [\sFmla{\True}{\formula{A}}, just = {\TRule{\True}{\lor}[1]}, close]
  93. [\sFmla{\True}{\formula{B}}, just = {\TRule{\True}{\lor}[1]}, close]
  94. ]
  95. ]
  96. ]
  97. ]
  98. ]
  99. \end{oltableau}
  100. \item Both $\{\sFmla{\False}{!A \lor !B}, \sFmla{\True}{!A}\}$ and
  101. $\{\sFmla{\False}{!A \lor !B}, \sFmla{\True}{!B}\}$ have closed
  102. !!{tableau}s:
  103. \begin{oltableau}{}
  104. [\sFmla{\False}{\formula{A} \lor \formula{B}}, just=\TAss
  105. [\sFmla{\True}{\formula{A}}, just=\TAss
  106. [\sFmla{\False{\formula{A}}},just={\TRule{\False}{\lor}[1]}
  107. [\sFmla{\False{\formula{B}}},just={\TRule{\False}{\lor}[1]}, close
  108. ]
  109. ]
  110. ]
  111. ]
  112. \end{oltableau}
  113. \begin{oltableau}{}
  114. [\sFmla{\False}{\formula{A} \lor \formula{B}}, just=\TAss
  115. [\sFmla{\True}{\formula{B}}, just=\TAss
  116. [\sFmla{\False{\formula{A}}},just={\TRule{\False}{\lor}[1]}
  117. [\sFmla{\False{\formula{B}}},just={\TRule{\False}{\lor}[1]}, close
  118. ]
  119. ]
  120. ]
  121. ]
  122. \end{oltableau}
  123. \end{enumerate}
  124. \end{proof}
  126. \begin{prop}\ollabel{prop:provability-lif}
  127. \begin{enumerate}
  128. \item \ollabel{prop:provability-lif-left} $!A, !A \lif !B \Proves !B$.
  129. \item \ollabel{prop:provability-lif-right}
  130. Both $\lnot !A \Proves !A \lif !B$ and $!B \Proves !A \lif !B$.
  131. \end{enumerate}
  132. \end{prop}
  134. \begin{proof}
  135. \begin{enumerate}
  136. \item $\{\sFmla{\False}{!B}, \sFmla{\True}{!A \lif !B},
  137. \sFmla{\True}{!A}\}$ has a closed !!{tableau}:
  138. \begin{oltableau}
  139. [\sFmla{\False}{\formula{B}}, just=\TAss
  140. [\sFmla{\True}{\formula{A} \lif \formula{B}}, just=\TAss
  141. [\sFmla{\True}{\formula{A}}, just=\TAss
  142. [\sFmla{\False}{\formula{A}}, just = {\TRule{\True}{\lif}[2]}, close]
  143. [\sFmla{\True}{\formula{B}}, just = {\TRule{\True}{\lif}[2]}, close]
  144. ]
  145. ]
  146. ]
  147. \end{oltableau}
  148. \item Both $\{\sFmla{\False}{!A \lif !B},
  149. \sFmla{\True}{\lnot !A}\}$ and $\{\sFmla{\False}{!A \lif !B},
  150. \sFmla{\True}{!B}\}$ have closed !!{tableau}s:
  151. \begin{oltableau}
  152. [\sFmla{\False}{\formula{A} \lif \formula{B}}, just = \TAss
  153. [\sFmla{\True}{\lnot \formula{A}}, just = \TAss
  154. [\sFmla{\True}{\formula{A}}, just = {\TRule{\False}{\lif}[1]}
  155. [\sFmla{\False}{\formula{B}}, just = {\TRule{\False}{\lif}[1]}
  156. [\sFmla{\False}{\formula{A}}, just = {\TRule{\True}{\lnot}[2]}, close]
  157. ]
  158. ]
  159. ]
  160. ]
  161. \end{oltableau}
  162. \begin{oltableau}
  163. [\sFmla{\False}{\formula{A} \lif \formula{B}}, just = \TAss
  164. [\sFmla{\True}{\formula{B}}, just = \TAss
  165. [\sFmla{\True}{\formula{A}}, just = {\TRule{\False}{\lif}[1]}
  166. [\sFmla{\False}{\formula{B}}, just = {\TRule{\False}{\lif}[1]},close
  167. ]
  168. ]
  169. ]
  170. ]
  171. \end{oltableau}
  172. \end{enumerate}
  173. \end{proof}
  175. \end{document}

content/first-order-logic/tableaux/provability-quantifiers.tex

88 lines; SHA-256 e12b4c0aff44de0e26d0a5c1e9b7ec2a781be5677035cb2c79cad3a7487c32e3. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: tableaux
  3. % Section: provability-quantifiers
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{tab}{qpr}
  10. \olsection{\usetoken{S}{derivability} and the Quantifiers}
  12. \begin{explain}
  13. The completeness theorem also requires that the tableaux rules yield
  14. the facts about~$\Proves$ established in this section.
  15. \end{explain}
  17. \begin{thm}
  18. \ollabel{thm:strong-generalization} If $c$ is a constant not occurring
  19. in $\Gamma$ or~$!A(x)$ and $\Gamma \Proves !A(c)$, then $\Gamma
  20. \Proves \lforall[x][!A(x)]$.
  21. \end{thm}
  23. \begin{proof}
  24. Suppose $\Gamma \Proves !A(c)$, i.e., there are $!B_1$, \dots, $!B_n
  25. \in \Gamma$ and a closed !!{tableau} for
  26. \begin{align*}
  27. \{ \sFmla{\False}{!A(c)}, &
  28. \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n} \}.
  29. \intertext{We have to show that there is also a closed !!{tableau} for}
  30. \{ \sFmla{\False}{\lforall[x][!A(x)]}, &
  31. \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n} \}.
  32. \end{align*}
  33. Take the closed !!{tableau} and replace the first assumption with
  34. $\sFmla{\False}{\lforall[x][!A(x)]}$, and insert
  35. $\sFmla{\False}{!A(c)}$ after the assumptions.
  36. \begin{center}
  37. \begin{tableau}{not line numbering}
  38. [\sFmla{\False}{\formula{A}(c)}
  39. [\sFmla{\True}{\formula{B}_1}
  40. [\vdots
  41. [\sFmla{\True}{\formula{B}_n},
  42. [][][]]]]]
  43. \end{tableau}\qquad
  44. \begin{tableau}{not line numbering}
  45. [\sFmla{\False}{\lforall[x][\formula{A}(x)]}
  46. [\sFmla{\True}{\formula{B}_1}
  47. [\vdots
  48. [\sFmla{\True}{\formula{B}_n},
  49. [\sFmla{\False}{\formula{A}(c)}
  50. [][][]]]]]]
  51. \end{tableau}
  52. \end{center}
  53. The tableau is still closed, since all !!{sentence}s available as
  54. assumptions before are still available at the top of the
  55. !!{tableau}. The inserted line is the result of a correct application
  56. of $\TRule{\False}{\lforall}$, since the !!{constant}~$c$ does not
  57. occur in $!B_1$, \dots, $!B_n$ or $\lforall[x][!A(x)]$, i.e., it does
  58. not occur above the inserted line in the new !!{tableau}.
  59. \end{proof}
  61. \begin{prop}
  62. \ollabel{prop:provability-quantifiers}
  63. \begin{tagenumerate}{prvEx,prvAll}
  64. \tagitem{prvEx}{$!A(t) \Proves \lexists[x][!A(x)]$.}{}
  65. \tagitem{prvAll}{$\lforall[x][!A(x)] \Proves !A(t)$.}{}
  66. \end{tagenumerate}
  67. \end{prop}
  69. \begin{proof}
  70. \begin{tagenumerate}{prvEx,prvAll}
  71. \tagitem{prvEx}{A closed !!{tableau} for
  72. $\sFmla{\False}{\lexists[x][!A(x)]}, \sFmla{\True}{!A(t)}$ is:
  73. \begin{oltableau}
  74. [\sFmla{\False}{\lexists[x][\formula{A}(x)]}, just = \TAss
  75. [\sFmla{\True}{\formula{A}(t)}, just = \TAss
  76. [\sFmla{\False}{\formula{A}(t)}, just = {\TRule{\False}{\lexists}[1]}, close]]]
  77. \end{oltableau}}{}
  78. \tagitem{prvAll}{A closed !!{tableau} for
  79. $\sFmla{\False}{\formula{A}(t)}, \sFmla{\True}{\lforall[x][!A(x)]}, $ is:
  80. \begin{oltableau}
  81. [\sFmla{\False}{\formula{A}(t)}, just = \TAss
  82. [\sFmla{\True}{\lforall[x][\formula{A}(x)]}, just = \TAss
  83. [\sFmla{\True}{\formula{A}(t)}, just = {\TRule{\True}{\lforall}[2]}, close]]]
  84. \end{oltableau}}{}
  85. \end{tagenumerate}
  86. \end{proof}
  88. \end{document}

content/first-order-logic/tableaux/soundness.tex

240 lines; SHA-256 49f119364f19485fa74c0c18e849f20b746e8edec9fdccb9e98a8aff7250a744. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: tableaux
  3. % Section: soundness.tex
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{tab}{sou}}
  11. {\olfileid{pl}{tab}{sou}}
  13. \olsection{Soundness}
  15. \begin{explain}
  16. !!^a{derivation} system, such as tableaux, is \emph{sound}
  17. if it cannot !!{derive} things that do not actually hold. Soundness is
  18. thus a kind of guaranteed safety property for !!{derivation} systems.
  19. Depending on which proof theoretic property is in question, we would
  20. like to know for instance, that
  21. \begin{enumerate}
  22. \item every !!{derivable}~$!A$ is \iftag{FOL}{valid}{a tautology};
  23. \item if !!a{sentence} is !!{derivable} from some others, it is also a
  24. consequence of them;
  25. \item if a set of !!{sentence}s is inconsistent, it is unsatisfiable.
  26. \end{enumerate}
  27. These are important properties of !!a{derivation} system. If any of them do
  28. not hold, the !!{derivation} system is deficient---it would !!{derive} too much.
  29. Consequently, establishing the soundness of !!a{derivation} system is of the
  30. utmost importance.
  32. Because all these proof-theoretic properties are defined via closed
  33. !!{tableau}s of some kind or other, proving (1)--(3) above requires
  34. proving something about the semantic properties of closed
  35. !!{tableau}s. We will first define what it means for !!a{signed
  36. formula} to be satisfied in a structure, and then show that if a
  37. !!{tableau} is closed, no structure satisfies all its assumptions.
  38. (1)--(3) then follow as corollaries from this result.
  39. \end{explain}
  41. \begin{defn}
  42. \iftag{FOL}{!!^a{structure}}{!!^a{valuation}}~$\iftag{FOL}{\Struct{M}}{\pAssign{v}}$
  43. \emph{satisfies} !!a{signed formula} $\sFmla{\True}{!A}$ iff
  44. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$, and it satisfies
  45. $\sFmla{\False}{!A}$ iff
  46. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A}$. $\iftag{FOL}{\Struct{M}}{\pAssign{v}}$
  47. satisfies a set of !!{signed formula}s~$\Gamma$ iff it satisfies every
  48. $\sFmla{S}{!A} \in \Gamma$. $\Gamma$~is \emph{satisfiable} if there is
  49. \iftag{FOL}{!!a{structure}}{!!a{valuation}} that satisfies it, and
  50. \emph{unsatisfiable} otherwise.
  51. \end{defn}
  53. \begin{thm}[Soundness]
  54. \ollabel{thm:tableau-soundness}
  55. If $\Gamma$ has a closed !!{tableau}, $\Gamma$ is unsatisfiable.
  56. \end{thm}
  58. \begin{proof}
  59. Let's call a branch of !!a{tableau} satisfiable iff the set of
  60. !!{signed formula}s on it is satisfiable, and let's call !!a{tableau}
  61. satisfiable if it contains at least one satisfiable branch.
  63. We show the following: Extending a satisfiable !!{tableau} by one of
  64. the rules of inference always results in a satisfiable !!{tableau}.
  65. This will prove the theorem: any closed !!{tableau} results by
  66. applying rules of inference to the !!{tableau} consisting only of
  67. assumptions from~$\Gamma$. So if $\Gamma$ were satisfiable, any
  68. !!{tableau} for it would be satisfiable. A closed !!{tableau},
  69. however, is clearly not satisfiable: every branch contains both
  70. $\sFmla{\True}{!A}$ and $\sFmla{\False}{!A}$, and no structure can
  71. both satisfy and not satisfy~$!A$.
  73. Suppose we have a satisfiable !!{tableau}, i.e., !!a{tableau} with at
  74. least one satisfiable branch. Applying a rule of inference either adds
  75. !!{signed formula}s to a branch, or splits a branch in two. If the
  76. !!{tableau} has a satisfiable branch which is not extended by the rule
  77. application in question, it remains a satisfiable branch in the
  78. extended !!{tableau}, so the extended tableau is satisfiable. So we
  79. only have to consider the case where a rule is applied to a
  80. satisfiable branch.
  82. Let $\Gamma$ be the set of !!{signed formula}s on that branch, and
  83. let $\sFmla{S}{!A} \in \Gamma$ be the !!{signed formula} to which the
  84. rule is applied. If the rule does not result in a split branch, we
  85. have to show that the extended branch, i.e., $\Gamma$ together with
  86. the conclusions of the rule, is still satisfiable. If the rule results
  87. in a split branch, we have to show that at least one of the two
  88. resulting branches is satisfiable.
  90. First, we consider the possible inferences that do not result in a split branch.
  91. \begin{enumerate}
  92. \item The branch is expanded by applying $\TRule{\True}{\lnot}$ to
  93. $\sFmla{\True}{\lnot !B} \in \Gamma$. Then the extended branch
  94. contains the !!{signed formula}s $\Gamma \cup
  95. \{\sFmla{\False}{!B}\}$. Suppose
  96. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$. In particular,
  97. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\lnot !B}$. Thus,
  98. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B}$, i.e.,
  99. $\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ satisfies
  100. $\sFmla{\False}{!B}$.
  101. \item The branch is expanded by applying $\TRule{\False}{\lnot}$ to
  102. $\sFmla{\False}{\lnot !B} \in \Gamma$: Exercise.
  103. \item The branch is expanded by applying $\TRule{\True}{\land}$ to
  104. $\sFmla{\True}{!B \land !C} \in \Gamma$, which results in two new
  105. !!{signed formula}s on the branch: $\sFmla{\True}{!B}$ and
  106. $\sFmla{\True}{!C}$. Suppose
  107. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, in particular
  108. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B \land !C}$. Then
  109. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$ and
  110. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!C}$. This means that
  111. $\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ satisfies both
  112. $\sFmla{\True}{!B}$ and $\sFmla{\True}{!C}$.
  113. \item The branch is expanded by applying $\TRule{\False}{\lor}$ to
  114. $\sFmla{\False}{!B \lor !C} \in \Gamma$: Exercise.
  115. \item The branch is expanded by applying $\TRule{\False}{\lif}$ to
  116. $\sFmla{\False}{!B \lif !C} \in \Gamma$: This results in two new
  117. !!{signed formula}s on the branch: $\sFmla{\True}{!B}$ and
  118. $\sFmla{\False}{!C}$. Suppose
  119. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, in particular
  120. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B \lif !C}$. Then
  121. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$ and
  122. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$. This means that
  123. $\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ satisfies both
  124. $\sFmla{\True}{!B}$ and $\sFmla{\False}{!C}$.
  126. \iftag{FOL}{%
  127. \item The branch is expanded by applying $\TRule{\True}{\lforall}$ to
  128. $\sFmla{\True}{\lforall[x][!B(x)]} \in \Gamma$: This results in a
  129. new !!{signed formula}~$\sFmla{\True}{!A(t)}$ on the branch.
  130. Suppose $\Sat{M}{\Gamma}$, in particular,
  131. $\Sat{M}{\lforall[x][!A(x)]}$. By
  132. \olref[syn][sem]{prop:quant-terms}, $\Sat{M}{!A(t)}$. Consequently,
  133. $\Struct{M}$ satisfies $\sFmla{\True}{!A(t)}$.
  135. \item The branch is expanded by applying $\TRule{\False}{\lforall}$ to
  136. $\sFmla{\False}{\lforall[x][!B(x)]} \in \Gamma$: This results in a
  137. new !!{signed formula}~$\sFmla{\False}{!A(a)}$ where $a$ is
  138. !!a{constant} not occurring in~$\Gamma$. Since $\Gamma$ is
  139. satisfiable, there is a $\Struct{M}$ such that $\Sat{M}{\Gamma}$, in
  140. particular $\Sat/{M}{\lforall[x][!B(x)]}$. We have to show that
  141. $\Gamma \cup \{\sFmla{\False}{!A(a)}\}$ is satisfiable. To do this,
  142. we define a suitable~$\Struct{M'}$ as follows.
  144. By \olref[syn][ass]{prop:sat-quant}, $\Sat/{M}{\lforall[x][!B(x)]}$
  145. iff for some $s$, $\Sat/{M}{!B(x)}[s]$. Now let $\Struct{M'}$ be
  146. just like $\Struct{M}$, except $\Assign{a}{M'} = s(x)$. By
  147. \olref[syn][ext]{cor:extensionality-sent}, for any
  148. $\sFmla{\True}{!C} \in \Gamma$, $\Sat{M'}{!C}$, and for any
  149. $\sFmla{\False}{!C} \in \Gamma$, $\Sat/{M'}{!C}$, since $a$ does not
  150. occur in~$\Gamma$.
  152. By \olref[syn][ext]{prop:extensionality}, $\Sat/{M'}{!A(x)}[s]$. By
  153. \olref[syn][ext]{prop:ext-formulas}, $\Sat/{M'}{!A(a)}[s]$. Since
  154. $!A(a)$ is !!a{sentence}, by
  155. \olref[syn][ass]{prop:sentence-sat-true}, $\Sat/{M'}{!A(a)}$, i.e.,
  156. $\Struct{M'}$ satisfies $\sFmla{\False}{!A(a)}$.
  157. \item The branch is expanded by applying $\TRule{\True}{\lexists}$ to
  158. $\sFmla{\True}{\lexists[x][!B(x)]} \in \Gamma$: Exercise.
  159. \item The branch is expanded by applying $\TRule{\False}{\lexists}$ to
  160. $\sFmla{\False}{\lexists[x][!B(x)]} \in \Gamma$: Exercise.}{}
  161. \end{enumerate}
  162. Now let's consider the possible inferences that result in a split branch.
  163. \begin{enumerate}
  164. \item The branch is expanded by applying $\TRule{\False}{\land}$ to
  165. $\sFmla{\False}{!B \land !C} \in \Gamma$, which results in two
  166. branches, a left one continuing through $\sFmla{\False}{!B}$ and a
  167. right one through $\sFmla{\False}{!C}$. Suppose
  168. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, in particular
  169. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B \land !C}$. Then
  170. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B}$ or
  171. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!C}$. In the former case,
  172. $\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ satisfies
  173. $\sFmla{\False}{!B}$, i.e., $\iftag{FOL}{\Struct{M}}{\pAssign{v}}$
  174. satisfies the formulas on the left branch. In the latter,
  175. $\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ satisfies
  176. $\sFmla{\False}{!C}$, i.e., $\iftag{FOL}{\Struct{M}}{\pAssign{v}}$
  177. satisfies the formulas on the right branch.
  178. \item The branch is expanded by applying $\TRule{\True}{\lor}$ to
  179. $\sFmla{\True}{!B \lor !C} \in \Gamma$: Exercise.
  180. \item The branch is expanded by applying $\TRule{\True}{\lif}$ to
  181. $\sFmla{\True}{!B \lif !C} \in \Gamma$: Exercise.
  182. \item The branch is expanded by \Cut: This results in two branches,
  183. one containing $\sFmla{\True}{!B}$, the other containing
  184. $\sFmla{\False}{!B}$. Since $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$
  185. and either $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$ or
  186. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B}$,
  187. $\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ satisfies either the left or
  188. the right branch.
  189. \end{enumerate}
  190. \end{proof}
  192. \tagprob{FOL}
  193. \begin{prob}
  194. Complete the proof of \olref[fol][tab][sou]{thm:tableau-soundness}.
  195. \end{prob}
  196. \tagendprob
  198. \tagprob{notFOL}
  199. \begin{prob}
  200. Complete the proof of \olref[pl][tab][sou]{thm:tableau-soundness}.
  201. \end{prob}
  202. \tagendprob
  204. \begin{cor}
  205. \ollabel{cor:weak-soundness}
  206. If $\Proves !A$ then $!A$ is \iftag{FOL}{valid}{a tautology}.
  207. \end{cor}
  209. \begin{cor}
  210. \ollabel{cor:entailment-soundness}
  211. If $\Gamma \Proves !A$ then $\Gamma \Entails !A$.
  212. \end{cor}
  214. \begin{proof}
  215. If $\Gamma \Proves !A$ then for some $!B_1$, \dots, $!B_n \in
  216. \Gamma$, $\{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots,
  217. \sFmla{\True}{!B_n}\}$ has a closed !!{tableau}. By
  218. \olref{thm:tableau-soundness}, every
  219. \iftag{FOL}{!!{structure}}{!!{valuation}}~$\iftag{FOL}{\Struct{M}}{\pAssign{v}}$
  220. either makes some $!B_i$ false or makes $!A$ true. Hence, if
  221. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$ then also
  222. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$.
  223. \end{proof}
  225. \begin{cor}
  226. \ollabel{cor:consistency-soundness}
  227. If $\Gamma$ is satisfiable, then it is consistent.
  228. \end{cor}
  230. \begin{proof}
  231. We prove the contrapositive. Suppose that $\Gamma$ is not consistent.
  232. Then there are $!B_1$, \dots, $!B_n \in \Gamma$ and a closed
  233. !!{tableau} for $\{\sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}$. By
  234. \olref{thm:tableau-soundness}, there is no
  235. $\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ such that
  236. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B_i}$ for all $i=1$, \dots,~$n$. But
  237. then $\Gamma$ is not satisfiable.
  238. \end{proof}
  240. \end{document}

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

105 lines; SHA-256 b40df45226792d6995a13afbc4341601207236b40cdb11920e9d48d0c81b2088. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: tableaux
  3. % Section: identity
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{tab}{ide}
  11. \olsection{\usetoken{P}{tableau} with \usetoken{S}{identity}}
  13. !!^{tableau}s with !!{identity} require additional inference rules.
  14. The rules for $\eq$ are ($t$, $t_1$, and $t_2$ are closed terms):
  16. \begin{defish}
  17. \AxiomC{}
  18. \RightLabel{$\eq$}
  19. \UnaryInfC{\sFmla{\True}{\eq[t][t]}}
  20. \DisplayProof
  21. \hfill
  22. \AxiomC{\sFmla{\True}{\eq[t_1][t_2]}}
  23. \noLine
  24. \UnaryInfC{\sFmla{\True}{!A(t_1)}}
  25. \RightLabel{$\TRule{\True}{\eq}$}
  26. \UnaryInfC{\sFmla{\True}{!A(t_2)}}
  27. \DisplayProof
  28. \hfill
  29. \AxiomC{\sFmla{\True}{\eq[t_1][t_2]}}
  30. \noLine
  31. \UnaryInfC{\sFmla{\False}{!A(t_1)}}
  32. \RightLabel{$\TRule{\False}{\eq}$}
  33. \UnaryInfC{\sFmla{\False}{!A(t_2)}}
  34. \DisplayProof
  35. \end{defish}
  36. Note that in contrast to all the other rules, $\TRule{\True}{\eq}$ and
  37. $\TRule{\False}{\eq}$ require that \emph{two} signed !!{formula}s
  38. already appear on the branch, namely both $\sFmla{\True}{\eq[t_1][t_2]}$
  39. and $\sFmla{S}{!A(t_1)}$.
  41. \begin{ex}
  42. If $s$ and $t$ are closed terms, then $\eq[s][t], !A(s)
  43. \Proves !A(t)$:
  44. \begin{oltableau}
  45. [\sFmla{\False}{\formula{A}(t)}, just = \TAss
  46. [\sFmla{\True}{\eq[s][t]}, just = \TAss
  47. [\sFmla{\True}{\formula{A}(s)}, just = \TAss
  48. [\sFmla{\True}{\formula{A}(t)}, just={\TRule{\True}{\eq}[2, 3]}, close]
  49. ]
  50. ]
  51. ]
  52. \end{oltableau}
  53. This may be familiar as the principle of substitutability of
  54. identicals, or Leibniz' Law.
  56. !!^{tableau}s prove that $\eq$ is symmetric, i.e., that $\eq[s_1][s_2]
  57. \Proves \eq[s_2][s_1]$:
  58. \begin{oltableau}
  59. [\sFmla{\False}{\eq[s_2][s_1]}, just = \TAss
  60. [\sFmla{\True}{\eq[s_1][s_2]}, just = \TAss
  61. [\sFmla{\True}{\eq[s_1][s_1]}, just = {$\eq$}
  62. [\sFmla{\True}{\eq[s_2][s_1]}, just = {\TRule{\True}{\eq}[2, 3]}, close]
  63. ]
  64. ]
  65. ]
  66. \end{oltableau}
  67. Here, line $2$ is the first prerequisite
  68. !!{formula}~$\sFmla{\True}{\eq[s_1][s_2]}$ of $\TRule{\True}{\eq}$.
  69. Line~$3$ is the second one, of the form $\sFmla{\True}{!A(s_2)}$---think of
  70. $!A(x)$ as
  71. $\eq[x][s_1]$, then $!A(s_1)$ is $\eq[s_1][s_1]$ and $!A(s_2)$ is $\eq[s_2][s_1]$.
  73. They also prove that $\eq$ is transitive, i.e., that $\eq[s_1][s_2],
  74. \eq[s_2][s_3] \Proves \eq[s_1][s_3]$:
  75. \begin{oltableau}
  76. [\sFmla{\False}{\eq[s_1][s_3]}, just = \TAss
  77. [\sFmla{\True}{\eq[s_1][s_2]}, just = \TAss
  78. [\sFmla{\True}{\eq[s_2][s_3]}, just = \TAss
  79. [\sFmla{\True}{\eq[s_1][s_3]}, just = {\TRule{\True}{\eq}[3, 2]}, close]
  80. ]
  81. ]
  82. ]
  83. \end{oltableau}
  84. In this !!{tableau}, the first prerequisite !!{formula} of
  85. $\TRule{\True}{\eq}$ is line~$3$, $\sFmla{\True}{\eq[s_2][s_3]}$
  86. ($s_2$ plays the role of~$t_1$, and $s_3$ the role of~$t_2$). The
  87. second prerequisite, of the form~$\sFmla{\True}{!A(s_2)}$ is line~$2$.
  88. Here, think of $!A(x)$ as $\eq[s_1][x]$; that makes $!A(s_2)$ into
  89. $\eq[t_1][t_2]$ (i.e., line~$2$) and $!A(s_3)$ into the
  90. !!{formula}~$\eq[s_1][s_3]$ in the conclusion.
  91. \end{ex}
  93. \begin{prob}
  94. Give closed !!{tableau}s for the following:
  95. \begin{enumerate}
  96. \item $\sFmla{\False}{\lforall[x][\lforall[y][((x = y \land !A(x))
  97. \lif !A(y))]]}$
  98. \item $\sFmla{\False}{\lexists[x][(!A(x) \land
  99. \lforall[y][(!A(y) \lif y = x)])]}$,\\
  100. $\sFmla{\True}{\lexists[x][!A(x)] \land
  101. \lforall[y][\lforall[z][((!A(y) \land !A(z)) \lif y = z)]]}$
  102. \end{enumerate}
  103. \end{prob}
  105. \end{document}

content/first-order-logic/tableaux/soundness-identity.tex

45 lines; SHA-256 3e9430f5d59a07997815894a8a190147e796825fea24a326dd9f7af6767ad519. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: tableaux
  3. % Section: soundness-identity
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{tab}{sid}
  11. \olsection{Soundness with \usetoken{S}{identity}}
  13. \begin{prop}
  14. !!^{tableau}s with rules for identity are sound: no closed !!{tableau}
  15. is satisfiable.
  16. \end{prop}
  18. \begin{proof}
  19. We just have to show as before that if !!a{tableau} has a satisfiable
  20. branch, the branch resulting from applying one of the rules for~$\eq$
  21. to it is also satisfiable. Let $\Gamma$ be the set of signed
  22. !!{formula}s on the branch, and let $\Struct{M}$ be !!a{structure}
  23. satisfying~$\Gamma$.
  25. Suppose the branch is expanded using~$\eq$, i.e., by adding the signed
  26. !!{formula}~$\sFmla{\True}{\eq[t][t]}$. Trivially,
  27. $\Sat{M}{\eq[t][t]}$, so $\Struct{M}$ also satisfies $\Gamma \cup
  28. \{\sFmla{\True}{\eq[t][t]}\}$.
  30. If the branch is expanded using $\TRule{\True}{\eq}$, we add a signed
  31. !!{formula}~$\sFmla{S}{!A(t_2)}$, but $\Gamma$ contains
  32. both~$\sFmla{\True}{\eq[t_1][t_2]}$ and $\sFmla{\True}{!A(t_1)}$. Thus
  33. we have $\Sat{M}{\eq[t_1][t_2]}$ and $\Sat{M}{!A(t_1)}$. Let $s$ be a
  34. variable assignment with $s(x) = \Value{t_1}{M}$. By
  35. \olref[syn][ass]{prop:sentence-sat-true}, $\Sat{M}{!A(t_1)}[s]$. Since
  36. $\varAssign{s}{s}{x}$, by \olref[syn][ext]{prop:ext-formulas},
  37. $\Sat{M}{!A(x)}[s]$. since $\Sat{M}{\eq[t_1][t_2]}$, we have
  38. $\Value{t_1}{M} = \Value{t_2}{M}$, and hence $s(x) = \Value{t_2}{M}$.
  39. By applying \olref[syn][ext]{prop:ext-formulas} again, we also have
  40. $\Sat{M}{!A(t_2)}[s]$. By \olref[syn][ass]{prop:sentence-sat-true},
  41. $\Sat{M}{!A(t_2)}$. The case of $\TRule{\False}{\eq}$ is treated
  42. similarly.
  43. \end{proof}
  45. \end{document}