The Open Logic Text — accessible offline edition

Natural Deduction — Source and provenance

Natural Deduction

Source and provenance

All fourteen authority files and all 1,984 lines are shown exactly and packaged byte-for-byte. Two source prose defects remain unchanged and are disclosed with explicit reader corrections. Open the exact accepted projected chapter transcript (SHA-256 aeb0985c36e99f18eccc0e957d3c039e8d590f9c9f390c9d061b34b014dbb75f). 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/natural-deduction/natural-deduction.tex

55 lines; SHA-256 8fa1e5a3e1211ce9c55e0ff66acbb8d5a6a9af360529d7775587a626fbe49b8e. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: natural-deduction
  4. \documentclass[../../../include/open-logic-chapter]{subfiles}
  6. \begin{document}
  8. \iftag{FOL}
  9. {\olchapter{fol}{ntd}{Natural Deduction}}
  10. {\olchapter{pl}{ntd}{Natural Deduction}}
  12. \begin{editorial}
  13. This chapter presents a natural deduction system in the style of
  14. Gentzen/Prawitz.
  16. To include or exclude material relevant to natural deduction as a
  17. proof system, use the ``prfND'' tag.
  18. \end{editorial}
  20. \olimport{rules-and-proofs}
  22. \olimport{propositional-rules}
  24. \iftag{FOL}{%
  25. \olimport{quantifier-rules}
  26. }{}
  28. \olimport{derivations}
  30. \olimport{proving-things}
  32. \iftag{FOL}{%
  33. \olimport{proving-things-quant}
  34. }{}
  36. \olimport{proof-theoretic-notions}
  38. \olimport{provability-consistency}
  40. \olimport{provability-propositional}
  42. \iftag{FOL}{%
  43. \olimport{provability-quantifiers}
  44. }{}
  46. \olimport{soundness}
  48. \iftag{FOL}{%
  49. \olimport{identity}
  50. \olimport{soundness-identity}
  51. }{}
  53. \OLEndChapterHook
  55. \end{document}

content/first-order-logic/natural-deduction/rules-and-proofs.tex

52 lines; SHA-256 0556326eefd6fbb957243d9f94969fd23adefb4af69f80419d4a2818d53088f0. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: natural-deduction
  3. % Section: rules-and-proofs
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{ntd}{rul}}
  11. {\olfileid{pl}{ntd}{rul}}
  13. \olsection{Rules and \usetoken{P}{derivation}}
  15. \begin{explain}
  16. Natural deduction systems are meant to closely parallel the informal
  17. reasoning used in mathematical proof (hence it is somewhat
  18. ``natural''). Natural deduction proofs begin with assumptions.
  19. Inference rules are then applied. Assumptions are ``!!{discharged}''
  20. by the \Intro{\lnot}, \Intro{\lif}, \iftag{FOL}{\Elim{\lor} and
  21. \Elim{\lexists}}{ and \Elim{\lor}} inference rules, and the label of
  22. the !!{discharged} assumption is placed beside the inference for
  23. clarity.
  24. \end{explain}
  26. \begin{defn}[Assumption]
  27. An \emph{assumption} is any !!{sentence}
  28. in the topmost position of any branch.
  29. \end{defn}
  31. !!^{derivation}s in natural deduction are certain trees of
  32. !!{sentence}s, where the topmost !!{sentence}s are assumptions, and if
  33. !!a{sentence} stands below one, two, or three other sequents, it must
  34. follow correctly by a rule of inference. The !!{sentence}s at the top
  35. of the inference are called the \emph{premises} and the !!{sentence}
  36. below the \emph{conclusion} of the inference. The rules come in
  37. pairs, an introduction and an elimination rule for each
  38. !!{operator}. They introduce !!a{operator} in the conclusion or
  39. remove !!a{operator} from a premise of the rule. Some of the rules
  40. allow an assumption of a certain type to be \emph{!!{discharged}}. To
  41. indicate which assumption is !!{discharged} by which inference, we
  42. also assign labels to both the assumption and the inference. This is
  43. indicated by writing the assumption as ``$\Discharge{!A}{n}$.''
  45. % Only include this sentence is on of \land, lor, lif or lnot is defined.
  47. \iftag{notprvNot,notprvAnd,notprvOr,notprvIf}{}%
  48. {It is customary to consider rules for all the !!{operator}s $\land$, $\lor$, $\lif$, $\lnot$, and $\lfalse$, even if some of those are defined.}
  52. \end{document}

content/first-order-logic/natural-deduction/propositional-rules.tex

120 lines; SHA-256 c22d2603cc9c4a79d630a4bc00b817c57c07b000e5d4bc443815e13b4f4cb515. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: natural-deduction
  3. % Section: propositional-rules
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{ntd}{prl}}
  11. {\olfileid{pl}{ntd}{prl}}
  13. \olsection{Propositional Rules}
  16. \subsection{Rules for $\land$}
  18. \begin{defish}
  19. \AxiomC{$!A$}
  20. \AxiomC{$!B$}
  21. \RightLabel{\Intro{\land}}
  22. \BinaryInfC{$!A \land !B$}
  23. \DisplayProof
  24. \hfill
  25. \begin{tabular}{r}
  26. \AxiomC{$!A \land !B$}
  27. \RightLabel{\Elim{\land}}
  28. \UnaryInfC{$!A$}
  29. \DisplayProof
  30. \\[3ex]
  31. \AxiomC{$!A \land !B$}
  32. \RightLabel{\Elim{\land}}
  33. \UnaryInfC{$!B$}
  34. \DisplayProof
  35. \end{tabular}
  36. \end{defish}
  38. \subsection{Rules for $\lor$}
  40. \begin{defish}
  41. \begin{tabular}{r}
  42. \AxiomC{$!A$}
  43. \RightLabel{\Intro{\lor}}
  44. \UnaryInfC{$!A \lor !B$}
  45. \DisplayProof
  46. \\[3ex]
  47. \AxiomC{$!B$}
  48. \RightLabel{\Intro{\lor}}
  49. \UnaryInfC{$!A \lor !B$}
  50. \DisplayProof
  51. \end{tabular}
  52. \hfill
  53. \AxiomC{$!A \lor !B$}
  54. \AxiomC{$\Discharge{!A}{n}$}
  55. \DeduceC{$!C$}
  56. \AxiomC{$\Discharge{!B}{n}$}
  57. \DeduceC{$!C$}
  58. \DischargeRule{\Elim{\lor}}{n}
  59. \TrinaryInfC{$!C$}
  60. \DisplayProof
  61. \end{defish}
  63. \subsection{Rules for $\lif$}
  65. \begin{defish}
  66. \AxiomC{$\Discharge{!A}{n}$}
  67. \DeduceC{$!B$}
  68. \DischargeRule{\Intro{\lif}}{n}
  69. \UnaryInfC{$!A \lif !B$}
  70. \DisplayProof
  71. \hfill
  72. \AxiomC{$!A \lif !B$}
  73. \AxiomC{$!A$}
  74. \RightLabel{\Elim{\lif}}
  75. \BinaryInfC{$!B$}
  76. \DisplayProof
  77. \end{defish}
  79. \subsection{Rules for $\lnot$}
  81. \begin{defish}
  82. \AxiomC{$\Discharge{!A}{n}$}
  83. \noLine
  84. \DeduceC{$\lfalse$}
  85. \DischargeRule{\Intro{\lnot}}{n}
  86. \UnaryInfC{$\lnot !A$}
  87. \DisplayProof
  88. \hfill
  89. \AxiomC{$\lnot !A$}
  90. \AxiomC{$!A$}
  91. \RightLabel{\Elim{\lnot}}
  92. \BinaryInfC{$\lfalse$}
  93. \DisplayProof
  94. \end{defish}
  96. \subsection{Rules for $\lfalse$}
  98. \begin{defish}
  99. \AxiomC{$\lfalse$}
  100. \RightLabel{\FalseInt}
  101. \UnaryInfC{$!A$}
  102. \DisplayProof
  103. \hfill
  104. \AxiomC{$\Discharge{\lnot !A}{n}$}
  105. \DeduceC{$\lfalse$}
  106. \DischargeRule{\FalseCl}{n}
  107. \UnaryInfC{$!A$}
  108. \DisplayProof
  109. \end{defish}
  111. Note that $\Intro{\lnot}$ and $\FalseCl$ are very similar: The
  112. difference is that $\Intro{\lnot}$ derives a negated
  113. !!{sentence}~$\lnot !A$ but $\FalseCl$ a positive !!{sentence}~$!A$.
  115. Whenever a rule indicates that some assumption may be discharged, we
  116. take this to be a permission, but not a requirement. E.g., in the
  117. $\Intro{\lif}$ rule, we may discharge any number of assumptions of the
  118. form~$!A$ in the !!{derivation} of the premise~$!B$, including zero.
  120. \end{document}

content/first-order-logic/natural-deduction/quantifier-rules.tex

111 lines; SHA-256 5d9c3a507fe1b79e4d376963b5e3efca4a3352cc7cef7d18255c61e60592f71b. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: natural-deduction
  3. % Section: quantifier-rules
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{ntd}{qrl}
  11. \olsection{Quantifier Rules}
  13. \subsection{Rules for $\lforall$}
  15. \begin{defish}
  16. \AxiomC{$!A(a)$}
  17. \RightLabel{\Intro{\lforall}}
  18. \UnaryInfC{$\lforall[x][\Atom{!A}{x}]$}
  19. \DisplayProof
  20. \hfill
  21. \AxiomC{$\lforall[x][\Atom{!A}{x}]$}
  22. \RightLabel{\Elim{\lforall}}
  23. \UnaryInfC{$!A(t)$}
  24. \DisplayProof
  25. \end{defish}
  27. In the rules for~$\lforall$, $t$ is a closed term (a term that does
  28. not contain any variables), and $a$~is !!a{constant} which does not
  29. occur in the conclusion~$\lforall[x][!A(x)]$, or in any assumption
  30. which is !!{undischarged} in the !!{derivation} ending with the
  31. premise~$!A(a)$. We call $a$ the \emph{eigenvariable} of the
  32. \Intro{\lforall} inference.\footnote{We use the term ``eigenvariable''
  33. even though $a$ in the above rule is a constant. This has historical
  34. reasons.}
  36. \subsection{Rules for $\lexists$}
  38. \begin{defish}
  39. \AxiomC{$\Atom{!A}{t}$}
  40. \RightLabel{\Intro{\lexists}}
  41. \UnaryInfC{$\lexists[x][\Atom{!A}{x}]$}
  42. \DisplayProof
  43. \hfill
  44. \AxiomC{$\lexists[x][\Atom{!A}{x}]$}
  45. \AxiomC{[$\Atom{!A}{a}$]$^n$}
  46. \DeduceC{$!C$}
  47. \DischargeRule{\Elim{\lexists}}{n}
  48. \BinaryInfC{$!C$}
  49. \DisplayProof
  50. \end{defish}
  52. Again, $t$ is a closed term, and $a$ is !!a{constant} which does not
  53. occur in the premise $\lexists[x][!A(x)]$, in the conclusion~$!C$, or
  54. any assumption which is !!{undischarged} in the !!{derivation}s ending
  55. with the two premises (other than the assumptions $!A(a)$). We call
  56. $a$ the \emph{eigenvariable} of the \Elim{\lexists} inference.
  58. The condition that an eigenvariable neither occur in the premises nor
  59. in any assumption that is !!{undischarged} in the !!{derivation}s
  60. leading to the premises for the \Intro{\lforall} or \Elim{\lexists}
  61. inference is called the \emph{eigenvariable condition}.
  63. \begin{explain}
  64. Recall the convention that when $!A$ is !!a{formula} with the
  65. !!{variable}~$x$ free, we indicate this by writing~$!A(x)$. In the
  66. same context, $!A(t)$ then is short for~$\Subst{!A}{t}{x}$. So we
  67. could also write the $\Intro\lexists$ rule as:
  68. \begin{prooftree}
  69. \AxiomC{$\Subst{!A}{t}{x}$}
  70. \RightLabel{\Intro{\lexists}}
  71. \UnaryInfC{$\lexists[x][!A]$}
  72. \end{prooftree}
  73. Note that $t$ may already occur in~$!A$, e.g., $!A$~might
  74. be~$\Atom{\Obj P}{t,x}$. Thus, inferring $\lexists[x][\Atom{\Obj
  75. P}{t,x}]$ from~$\Atom{\Obj P}{t,t}$ is a correct application
  76. of~$\Intro\lexists$---you may ``replace'' one or more, and not
  77. necessarily all, occurrences of~$t$ in the premise by the bound
  78. !!{variable}~$x$. However, the eigenvariable conditions in
  79. $\Intro\lforall$ and~$\Elim\lexists$ require that the !!{constant}~$a$
  80. does not occur in~$!A$. So, you cannot correctly infer
  81. $\lforall[x][\Atom{\Obj P}{a,x}]$ from $\Atom{\Obj P}{a,a}$
  82. using~$\Intro\lforall$.
  83. \end{explain}
  85. \begin{explain}
  86. In \Intro{\lexists} and \Elim{\lforall} there are no restrictions, and
  87. the term~$t$ can be anything, so we do not have to worry about any
  88. conditions. On the other hand, in the \Elim{\lexists} and
  89. \Intro{\lforall} rules, the eigenvariable condition requires that the
  90. !!{constant}~$a$ does not occur anywhere in the conclusion or in an
  91. !!{undischarged} assumption. The condition is necessary to ensure that
  92. the system is sound, i.e., only !!{derive}s !!{sentence}s from
  93. !!{undischarged} assumptions from which they follow. Without this
  94. condition, the following would be allowed:
  95. \begin{prooftree}
  96. \AxiomC{$\lexists[x][!A(x)]$}
  97. \AxiomC{$\Discharge{!A(a)}{1}$}
  98. \RightLabel{*\Intro{\lforall}}
  99. \UnaryInfC{$\lforall[x][!A(x)]$}
  100. \RightLabel{\Elim{\lexists}}
  101. \BinaryInfC{$\lforall[x][!A(x)]$}
  102. \end{prooftree}
  103. However, $\lexists[x][!A(x)] \Entails/ \lforall[x][!A(x)]$.
  105. As the elimination rules for quantifiers only allow substituting
  106. closed terms for !!{variable}s, it follows that any !!{formula} that
  107. can be derived from a set of !!{sentence}s is itself !!a{sentence}.
  108. \end{explain}
  111. \end{document}

content/first-order-logic/natural-deduction/derivations.tex

110 lines; SHA-256 04cdbaa301a71243b78d880551ce2f8edbf6f059764eceacd5b8910f0459cb26. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: natural-deduction
  3. % Section: derivations
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{ntd}{der}}
  11. {\olfileid{pl}{ntd}{der}}
  13. \olsection{\usetoken{P}{derivation}}
  15. \begin{explain}
  16. We've said what an assumption is, and we've given the rules of
  17. inference. !!^{derivation}s in natural deduction are inductively
  18. generated from these: each !!{derivation} either is an assumption
  19. on its own, or consists of one, two, or three !!{derivation}s followed
  20. by a correct inference.
  21. \end{explain}
  23. \begin{defn}[!!^{derivation}]
  24. \Article{derivation} \emph{!!{derivation}} of !!a{sentence}~$!A$ from
  25. assumptions~$\Gamma$ is a finite tree of !!{sentence}s satisfying the
  26. following conditions:
  27. \begin{enumerate}
  28. \item The topmost !!{sentence}s of the tree are either in $\Gamma$ or
  29. are !!{discharged} by an inference in the tree.
  30. \item The bottommost !!{sentence} of the tree is~$!A$.
  31. \item Every !!{sentence} in the tree except the sentence~$!A$ at
  32. the bottom is a premise of a correct application of an inference
  33. rule whose conclusion stands directly below that !!{sentence} in the
  34. tree.
  35. \end{enumerate}
  36. We then say that $!A$ is the \emph{conclusion} of the !!{derivation}
  37. and $\Gamma$ its !!{undischarged} assumptions.
  39. If !!a{derivation} of $!A$ from~$\Gamma$ exists, we say that $!A$ is
  40. \emph{!!{derivable}} from~$\Gamma$, or in symbols: $\Gamma \Proves
  41. !A$. If there is !!a{derivation} of~$!A$ in which every assumption is
  42. !!{discharged}, we write~$\Proves !A$.
  43. \end{defn}
  45. \begin{ex}
  46. Every assumption on its own is !!a{derivation}. So, e.g., $!A$ by
  47. itself is !!a{derivation}, and so is $!B$ by itself. We can obtain a
  48. new !!{derivation} from these by applying, say, the $\Intro{\land}$
  49. rule,
  50. \begin{prooftree}
  51. \AxiomC{$!A$}
  52. \AxiomC{$!B$}
  53. \RightLabel{\Intro{\land}}
  54. \BinaryInfC{$!A \land !B$}
  55. \end{prooftree}
  56. These rules are meant to be general: we can replace the $!A$ and~$!B$
  57. in it with any !!{sentence}s, e.g., by $!C$ and~$!D$. Then the
  58. conclusion would be $!C \land !D$, and so
  59. \begin{prooftree}
  60. \AxiomC{$!C$}
  61. \AxiomC{$!D$}
  62. \RightLabel{\Intro{\land}}
  63. \BinaryInfC{$!C \land !D$}
  64. \end{prooftree}
  65. is a correct !!{derivation}. Of course, we can also switch the
  66. assumptions, so that $!D$ plays the role of~$!A$ and $!C$ that
  67. of~$!B$. Thus,
  68. \begin{prooftree}
  69. \AxiomC{$!D$}
  70. \AxiomC{$!C$}
  71. \RightLabel{\Intro{\land}}
  72. \BinaryInfC{$!D \land !C$}
  73. \end{prooftree}
  74. is also a correct !!{derivation}.
  76. We can now apply another rule, say, $\Intro{\lif}$, which allows us to
  77. conclude a conditional and allows us to !!{discharge} any assumption
  78. that is identical to the antecedent of that conditional. So both of
  79. the following would be correct !!{derivation}s:
  80. \begin{prooftree}
  81. \AxiomC{$\Discharge{!C}{1}$}
  82. \AxiomC{$!D$}
  83. \RightLabel{\Intro{\land}}
  84. \BinaryInfC{$!C \land !D$}
  85. \DischargeRule{\Intro{\lif}}{1}
  86. \UnaryInfC{$!C \lif (!C \land !D)$}
  87. \DisplayProof\bottomAlignProof
  88. \AxiomC{$!C$}
  89. \AxiomC{$\Discharge{!D}{1}$}
  90. \RightLabel{\Intro{\land}}
  91. \BinaryInfC{$!C \land !D$}
  92. \DischargeRule{\Intro{\lif}}{1}
  93. \UnaryInfC{$!D \lif (!C \land !D)$}
  94. \end{prooftree}
  95. They show, respectively, that $!D \Proves !C \lif (!C \land !D)$ and
  96. $!C \Proves !D \lif (!C \land !D)$.
  98. Remember that discharging of assumptions is a permission, not a
  99. requirement: we don't have to discharge the assumptions. In
  100. particular, we can apply a rule even if the assumptions are not
  101. present in the !!{derivation}. For instance, the following is legal, even
  102. though there is no assumption~$!A$ to be !!{discharged}:
  103. \begin{prooftree}
  104. \AxiomC{$!B$}
  105. \DischargeRule{\Intro{\lif}}{1}
  106. \UnaryInfC{$!A \lif !B$}
  107. \end{prooftree}
  108. \end{ex}
  110. \end{document}

content/first-order-logic/natural-deduction/proving-things.tex

310 lines; SHA-256 ff58b86389a21dbc6f240f49e62d5fca0bdb4d3ba54e0d364792cdcddd34724f. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: natural-deduction
  3. % Section: proving-things
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{ntd}{pro}}
  11. {\olfileid{pl}{ntd}{pro}}
  13. \olsection{Examples of \usetoken{P}{derivation}}
  15. \begin{ex}
  16. Let's give !!a{derivation} of the !!{sentence} $(!A \land !B) \lif !A$.
  18. We begin by writing the desired conclusion at the bottom of the
  19. !!{derivation}.
  20. \begin{prooftree}
  21. \AxiomC{}
  22. \UnaryInfC{$(!A\land !B) \lif !A$}
  23. \end{prooftree}
  25. Next, we need to figure out what kind of inference could result in
  26. !!a{sentence} of this form. The !!{main operator} of the
  27. conclusion is $\lif$, so we'll try to arrive at the
  28. conclusion using the \Intro{\lif} rule. It is best to write down
  29. the assumptions involved and label the inference rules as you
  30. progress, so it is easy to see whether all assumptions have been
  31. !!{discharged} at the end of the proof.
  32. \begin{prooftree}
  33. \AxiomC{$\Discharge{!A \land !B}{1}$}
  34. \DeduceC{$!A$}
  35. \DischargeRule{\Intro{\lif}}{1}
  36. \UnaryInfC{$(!A\land !B) \lif !A$}
  37. \end{prooftree}
  39. We now need to fill in the steps from the assumption $!A \land !B$ to $!A$.
  40. Since we only have one connective to deal with, $\land$, we must
  41. use the $\land$ elim rule. This gives us the following proof:
  42. \begin{prooftree}
  43. \AxiomC{$\Discharge{!A \land !B}{1}$}
  44. \RightLabel{\Elim{\land}}
  45. \UnaryInfC{$!A$}
  46. \DischargeRule{\Intro{\lif}}{1}
  47. \UnaryInfC{$(!A\land !B) \lif !A$}
  48. \end{prooftree}
  49. We now have a correct !!{derivation} of $(!A \land
  50. !B) \lif !A$.
  51. \end{ex}
  53. \begin{ex}
  54. Now let's give !!a{derivation} of $(\lnot !A \lor !B)
  55. \lif (!A \lif !B)$.
  57. We begin by writing the desired conclusion at the bottom of the
  58. !!{derivation}.
  59. \begin{prooftree}
  60. \AxiomC{}
  61. \UnaryInfC{$(\lnot !A \lor !B) \lif (!A \lif !B)$}
  62. \end{prooftree}
  63. To find a logical rule that could give us this conclusion, we
  64. look at the logical connectives in the conclusion: $\lnot$,
  65. $\lor$, and $\lif$. We only care at the moment about the first
  66. occurrence of $\lif$ because it is the !!{main operator} of the
  67. !!{sentence} in the end-sequent, while $\lnot$, $\lor$ and the second
  68. occurrence of $\lif$ are inside the scope of another connective, so we
  69. will take care of those later. We therefore start with the
  70. \Intro{\lif} rule. A correct application must look like this:
  71. \begin{prooftree}
  72. \AxiomC{$\Discharge{\lnot !A \lor !B}{1}$}
  73. \DeduceC{$!A \lif !B$}
  74. \DischargeRule{\Intro{\lif}}{1}
  75. \UnaryInfC{$(\lnot !A \lor !B) \lif (!A \lif !B)$}
  76. \end{prooftree}
  77. This leaves us with two possibilities to continue. Either we can
  78. keep working from the bottom up and look for another application
  79. of the \Intro{\lif} rule, or we can work from the top down and apply a
  80. \Elim{\lor} rule. Let us apply the latter. We will use the assumption
  81. $\lnot !A \lor !B$ as the leftmost premise of \Elim{\lor}. For a valid
  82. application of \Elim{\lor}, the other two premises must be identical
  83. to the conclusion $!A \lif !B$, but each may be derived in turn from
  84. another assumption, namely one of the two disjuncts of $\lnot !A \lor !B$.
  85. So our !!{derivation} will look like this:
  86. \begin{prooftree}
  87. \AxiomC{$\Discharge{\lnot !A \lor !B}{1}$}
  88. \AxiomC{$\Discharge{\lnot !A}{2}$}
  89. \DeduceC{$!A \lif !B$}
  90. \AxiomC{$\Discharge{!B}{2}$}
  91. \DeduceC{$!A \lif !B$}
  92. \DischargeRule{\Elim{\lor}}{2}
  93. \TrinaryInfC{$!A \lif !B$}
  94. \DischargeRule{\Intro{\lif}}{1}
  95. \UnaryInfC{$(\lnot !A \lor !B) \lif (!A \lif !B)$}
  96. \end{prooftree}
  98. In each of the two branches on the right, we want to !!{derive} $!A
  99. \lif !B$, which is best done using \Intro{\lif}.
  100. \begin{prooftree}
  101. \AxiomC{$\Discharge{\lnot !A \lor !B}{1}$}
  102. \AxiomC{$\Discharge{\lnot !A}{2}, \Discharge{!A}{3}$}
  103. \DeduceC{$!B$}
  104. \DischargeRule{\Intro{\lif}}{3}
  105. \UnaryInfC{$!A \lif !B$}
  106. \AxiomC{$\Discharge{!B}{2}, \Discharge{!A}{4}$}
  107. \DeduceC{$!B$}
  108. \DischargeRule{\Intro{\lif}}{4}
  109. \UnaryInfC{$!A \lif !B$}
  110. \DischargeRule{\Elim{\lor}}{2}
  111. \TrinaryInfC{$!A \lif !B$}
  112. \DischargeRule{\Intro{\lif}}{1}
  113. \UnaryInfC{$(\lnot !A \lor !B) \lif (!A \lif !B)$}
  114. \end{prooftree}
  116. For the two missing parts of the !!{derivation}, we need
  117. !!{derivation}s of $!B$ from $\lnot !A$ and $!A$ in the middle, and
  118. from $!A$ and $!B$ on the left. Let's take the former first. $\lnot
  119. !A$ and $!A$ are the two premises of \Elim{\lnot}:
  120. \begin{prooftree}
  121. \AxiomC{$\Discharge{\lnot !A}{2}$}
  122. \AxiomC{$\Discharge{!A}{3}$}
  123. \RightLabel{\Elim{\lnot}}
  124. \BinaryInfC{$\lfalse$}
  125. \DeduceC{$!B$}
  126. \end{prooftree}
  127. By using \FalseInt, we can obtain $!B$ as a conclusion and
  128. complete the branch.
  129. \begin{prooftree}
  130. \AxiomC{$\Discharge{\lnot !A \lor !B}{1}$}
  131. \AxiomC{$\Discharge{\lnot !A}{2}$}
  132. \AxiomC{$\Discharge{!A}{3}$}
  133. \RightLabel{\Intro{\lfalse}}
  134. \BinaryInfC{$\lfalse$}
  135. \RightLabel{\FalseInt}
  136. \UnaryInfC{$!B$}
  137. \DischargeRule{\Intro{\lif}}{3}
  138. \UnaryInfC{$!A \lif !B$}
  139. \AxiomC{$\Discharge{!B}{2}, \Discharge{!A}{4}$}
  140. \DeduceC{$!B$}
  141. \DischargeRule{\Intro{\lif}}{4}
  142. \UnaryInfC{$!A \lif !B$}
  143. \DischargeRule{\Elim{\lor}}{2}
  144. \TrinaryInfC{$!A \lif !B$}
  145. \DischargeRule{\Intro{\lif}}{1}
  146. \UnaryInfC{$(\lnot !A \lor !B) \lif (!A \lif !B)$}
  147. \end{prooftree}
  149. Let's now look at the rightmost branch. Here it's important to
  150. realize that the definition of !!{derivation} \emph{allows assumptions
  151. to be discharged} but \emph{does not require} them to be. In other
  152. words, if we can derive $!B$ from one of the assumptions $!A$ and $!B$
  153. without using the other, that's ok. And to !!{derive} $!B$ from~$!B$
  154. is trivial: $!B$ by itself is such !!a{derivation}, and no inferences
  155. are needed. So we can simply delete the assumption~$!A$.
  156. \begin{prooftree}
  157. \AxiomC{$\Discharge{\lnot !A \lor !B}{1}$}
  158. \AxiomC{$\Discharge{\lnot !A}{2}$}
  159. \AxiomC{$\Discharge{!A}{3}$}
  160. \RightLabel{\Elim{\lnot}}
  161. \BinaryInfC{$\lfalse$}
  162. \RightLabel{\FalseInt}
  163. \UnaryInfC{$!B$}
  164. \DischargeRule{\Intro{\lif}}{3}
  165. \UnaryInfC{$!A \lif !B$}
  166. \AxiomC{$\Discharge{!B}{2}$}
  167. \RightLabel{\Intro{\lif}}
  168. \UnaryInfC{$!A \lif !B$}
  169. \DischargeRule{\Elim{\lor}}{2}
  170. \TrinaryInfC{$!A \lif !B$}
  171. \DischargeRule{\Intro{\lif}}{1}
  172. \UnaryInfC{$(\lnot !A \lor !B) \lif (!A \lif !B)$}
  173. \end{prooftree}
  174. Note that in the finished !!{derivation}, the rightmost \Intro{\lif}
  175. inference does not actually discharge any assumptions.
  176. \end{ex}
  178. \begin{ex}
  179. So far we have not needed the \FalseCl{} rule. It is special in that
  180. it allows us to discharge an assumption that isn't a sub-!!{formula} of
  181. the conclusion of the rule. It is closely related to the \FalseInt{}
  182. rule. In fact, the \FalseInt{} rule is a special case of the
  183. \FalseCl{} rule---there is a logic called ``intuitionistic logic'' in
  184. which only \FalseInt{} is allowed. The \FalseCl{} rule is a last
  185. resort when nothing else works. For instance, suppose we want to
  186. !!{derive} $!A \lor \lnot !A$. Our usual strategy would be to attempt
  187. to !!{derive} $!A \lor \lnot !A$ using $\Intro{\lor}$. But this would
  188. require us to !!{derive} either $!A$ or $\lnot !A$ from no
  189. assumptions, and this can't be done. \FalseCl{} to the rescue!
  190. \begin{prooftree}
  191. \AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}$}
  192. \DeduceC{$\lfalse$}
  193. \DischargeRule{\FalseCl}{1}
  194. \UnaryInfC{$!A \lor \lnot !A$}
  195. \end{prooftree}
  196. Now we're looking for !!a{derivation} of $\lfalse$ from $\lnot(!A \lor
  197. \lnot !A)$. Since $\lfalse$ is the conclusion of $\Elim{\lnot}$ we
  198. might try that:
  199. \begin{prooftree}
  200. \AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}$}
  201. \DeduceC{$\lnot !A$}
  202. \AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}$}
  203. \DeduceC{$!A$}
  204. \RightLabel{\Elim{\lnot}}
  205. \BinaryInfC{$\lfalse$}
  206. \DischargeRule{\FalseCl}{1}
  207. \UnaryInfC{$!A \lor \lnot !A$}
  208. \end{prooftree}
  209. Our strategy for finding !!a{derivation} of~$\lnot !A$ calls for an
  210. application of~$\Intro{\lnot}$:
  211. \begin{prooftree}
  212. \AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}, \Discharge{!A}{2}$}
  213. \DeduceC{$\lfalse$}
  214. \DischargeRule{\Intro{\lnot}}{2}
  215. \UnaryInfC{$\lnot !A$}
  216. \AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}$}
  217. \DeduceC{$!A$}
  218. \RightLabel{\Elim{\lnot}}
  219. \BinaryInfC{$\lfalse$}
  220. \DischargeRule{\FalseCl}{1}
  221. \UnaryInfC{$!A \lor \lnot !A$}
  222. \end{prooftree}
  223. Here, we can get $\lfalse$ easily by applying $\Elim{\lnot}$ to the
  224. assumption $\lnot(!A \lor \lnot !A)$ and $!A \lor \lnot !A$ which
  225. follows from our new assumption $!A$ by~$\Intro{\lor}$:
  226. \begin{prooftree}
  227. \AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}$}
  228. \AxiomC{$\Discharge{!A}{2}$}
  229. \RightLabel{\Intro{\lor}}
  230. \UnaryInfC{$!A \lor \lnot !A$}
  231. \RightLabel{\Elim{\lnot}}
  232. \BinaryInfC{$\lfalse$}
  233. \DischargeRule{\Intro{\lnot}}{2}
  234. \UnaryInfC{$\lnot !A$}
  235. \AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}$}
  236. \DeduceC{$!A$}
  237. \RightLabel{\Elim{\lnot}}
  238. \BinaryInfC{$\lfalse$}
  239. \DischargeRule{\FalseCl}{1}
  240. \UnaryInfC{$!A \lor \lnot !A$}
  241. \end{prooftree}
  242. On the right side we use the same strategy, except we get $!A$ by~\FalseCl:
  243. \begin{prooftree}
  244. \AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}$}
  245. \AxiomC{$\Discharge{!A}{2}$}
  246. \RightLabel{\Intro{\lor}}
  247. \UnaryInfC{$!A \lor \lnot !A$}
  248. \RightLabel{\Elim{\lnot}}
  249. \BinaryInfC{$\lfalse$}
  250. \DischargeRule{\Intro{\lnot}}{2}
  251. \UnaryInfC{$\lnot !A$}
  252. \AxiomC{$\Discharge{\lnot(!A \lor \lnot !A)}{1}$}
  253. \AxiomC{$\Discharge{\lnot !A}{3}$}
  254. \RightLabel{\Intro{\lor}}
  255. \UnaryInfC{$!A \lor \lnot !A$}
  256. \RightLabel{\Elim{\lnot}}
  257. \BinaryInfC{$\lfalse$}
  258. \DischargeRule{\FalseCl}{3}
  259. \UnaryInfC{$!A$}
  260. \RightLabel{\Elim{\lnot}}
  261. \BinaryInfC{$\lfalse$}
  262. \DischargeRule{\FalseCl}{1}
  263. \UnaryInfC{$!A \lor \lnot !A$}
  264. \end{prooftree}
  265. \end{ex}
  267. \begin{prob}
  268. Give !!{derivation}s that show the following:
  269. \begin{enumerate}
  270. \item $!A \land (!B \land !C) \Proves (!A \land !B) \land !C$.
  271. \item $!A \lor (!B \lor !C) \Proves (!A \lor !B) \lor !C$.
  272. \item $!A \lif (!B \lif !C) \Proves !B \lif (!A \lif !C)$.
  273. \item $!A \Proves \lnot\lnot !A$.
  274. \end{enumerate}
  275. \end{prob}
  277. \begin{prob}
  278. Give !!{derivation}s that show the following:
  279. \begin{enumerate}
  280. \item $(!A \lor !B) \lif !C \Proves !A \lif !C$.
  281. \item $(!A \lif !C) \land (!B \lif !C) \Proves (!A \lor !B) \lif !C$.
  282. \item $\Proves \lnot(!A \land \lnot !A)$.
  283. \item $!B \lif !A \Proves \lnot !A \lif \lnot !B$.
  284. \item $\Proves (!A \lif \lnot !A) \lif \lnot !A$.
  285. \item $\Proves \lnot(!A \lif !B) \lif \lnot !B$.
  286. \item $!A \lif !C \Proves \lnot (!A \land \lnot !C)$.
  287. \item $!A \land \lnot !C \Proves \lnot (!A \lif !C)$.
  288. \item $!A \lor !B, \lnot !B \Proves !A$.
  289. \item $\lnot !A \lor \lnot !B \Proves \lnot(!A \land !B)$.
  290. \item $\Proves (\lnot !A \land \lnot !B) \lif\lnot(!A \lor !B)$.
  291. \item $\Proves \lnot(!A \lor !B) \lif (\lnot !A \land \lnot !B)$.
  292. \end{enumerate}
  293. \end{prob}
  295. \begin{prob}
  296. Give !!{derivation}s that show the following:
  297. \begin{enumerate}
  298. \item $\lnot(!A \lif !B) \Proves !A$.
  299. \item $\lnot(!A \land !B) \Proves \lnot !A \lor \lnot !B$.
  300. \item $!A \lif !B \Proves \lnot !A \lor !B$.
  301. \item $\Proves \lnot \lnot !A \lif !A$.
  302. \item $!A \lif !B, \lnot !A \lif !B \Proves !B$.
  303. \item $(!A \land !B) \lif !C \Proves (!A \lif !C) \lor (!B \lif !C)$.
  304. \item $(!A \lif !B) \lif !A \Proves !A$.
  305. \item $\Proves (!A \lif !B) \lor (!B \lif !C)$.
  306. \end{enumerate}
  307. (These all require the $\FalseCl$~rule.)
  308. \end{prob}
  310. \end{document}

content/first-order-logic/natural-deduction/proving-things-quant.tex

255 lines; SHA-256 6f49b930a86f60a1cca318d70259378f7bc6b5ebb76f307665c4eb4363e8235f. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: natural-deduction
  3. % Section: proving-things-quant
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{ntd}{prq}
  11. \olsection{\usetoken{P}{derivation} 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 lower down in the finished proof).
  20. Let's see how we'd give !!a{derivation} of the !!{formula}
  21. $\lexists[x][\lnot !A(x)] \lif \lnot \lforall[x][!A(x)]$.
  22. Starting as usual, we write
  23. \begin{prooftree}
  24. \AxiomC{}
  25. \UnaryInfC{$\lexists[x][\lnot !A(x)]\lif \lnot \lforall[x][!A(x)]$}
  26. \end{prooftree}
  27. We start by writing down what it would take to justify that last step
  28. using the \Intro{\lif} rule.
  29. \begin{prooftree}
  30. \AxiomC{$\Discharge{\lexists[x][\lnot !A(x)]}{1}$}
  31. \DeduceC{$\lnot \lforall[x][!A(x)]$}
  32. \DischargeRule{\Intro{\lif}}{1}
  33. \UnaryInfC{$\lexists[x][\lnot !A(x)]\lif \lnot \lforall[x][!A(x)]$}
  34. \end{prooftree}
  35. Since there is no obvious rule to apply to $\lnot \lforall[x][!A(x)]$,
  36. we will proceed by setting up the !!{derivation} so we can use the
  37. \Elim{\lexists} rule. Here we must pay attention to the eigenvariable
  38. condition, and choose a constant that does not appear in
  39. $\lexists[x][!A(x)]$ or any assumptions that it depends on.
  40. (Since no !!{constant}s appear, however, any choice will do fine.)
  41. \begin{prooftree}
  42. \AxiomC{$\Discharge{\lexists[x][\lnot !A(x)]}{1}$}
  43. \AxiomC{$\Discharge{\lnot !A(a)}{2}$}
  44. \DeduceC{$\lnot \lforall[x][!A(x)]$}
  45. \DischargeRule{\Elim{\lexists}}{2}
  46. \BinaryInfC{$\lnot \lforall[x][!A(x)]$}
  47. \DischargeRule{\Intro{\lif}}{1}
  48. \UnaryInfC{$\lexists[x][\lnot !A(x)] \lif \lnot \lforall[x][!A(x)]$}
  49. \end{prooftree}
  50. In order to derive $\lnot \lforall[x][!A(x)]$, we will attempt to use
  51. the \Intro{\lnot} rule: this requires that we derive a contradiction,
  52. possibly using $\lforall[x][!A(x)]$ as an additional assumption. Of
  53. course, this contradiction may involve the assumption $\lnot !A(a)$
  54. which will be discharged by the \Elim{\lexists} inference. We can set it
  55. up as follows:
  56. \begin{prooftree}
  57. \AxiomC{$\Discharge{\lexists[x][\lnot !A(x)]}{1}$}
  58. \AxiomC{$\Discharge{\lnot !A(a)}{2}, \Discharge{\lforall[x][!A(x)]}{3}$}
  59. \DeduceC{$\lfalse$}
  60. \DischargeRule{\Intro{\lnot}}{3}
  61. \UnaryInfC{$\lnot \lforall[x][!A(x)]$}
  62. \DischargeRule{\Elim{\lexists}}{2}
  63. \BinaryInfC{$\lnot \lforall[x][!A(x)]$}
  64. \DischargeRule{\Intro{\lif}}{1}
  65. \UnaryInfC{$\lexists[x][\lnot !A(x)]\lif \lnot \lforall[x][!A(x)]$}
  66. \end{prooftree}
  67. It looks like we are close to getting a contradiction. The easiest
  68. rule to apply is the \Elim{\lforall}, which has no eigenvariable
  69. conditions. Since we can use any term we want to replace the
  70. universally quantified~$x$, it makes the most sense to continue
  71. using~$a$ so we can reach a contradiction.
  72. \begin{prooftree}
  73. \AxiomC{$\Discharge{\lexists[x][\lnot !A(x)]}{1}$}
  74. \AxiomC{$\Discharge{\lnot !A(a)}{2}$}
  75. \AxiomC{$\Discharge{\lforall[x][!A(x)]}{3}$}
  76. \RightLabel{\Elim{\lforall}}
  77. \UnaryInfC{$!A(a)$}
  78. \RightLabel{\Elim{\lnot}}
  79. \BinaryInfC{$\lfalse$}
  80. \DischargeRule{\Intro{\lnot}}{3}
  81. \UnaryInfC{$\lnot \lforall[x][!A(x)]$}
  82. \DischargeRule{\Elim{\lexists}}{2}
  83. \BinaryInfC{$\lnot \lforall[x][!A(x)]$}
  84. \DischargeRule{\Intro{\lif}}{1}
  85. \UnaryInfC{$\lexists[x][\lnot !A(x)]\lif \lnot \lforall[x][!A(x)]$}
  86. \end{prooftree}
  88. It is important, especially when dealing with quantifiers, to double
  89. check at this point that the eigenvariable condition has not been
  90. violated. Since the only rule we applied that is subject to the
  91. eigenvariable condition was \Elim{\exists}, and the eigenvariable~$a$
  92. does not occur in any assumptions it depends on, this is a
  93. correct !!{derivation}.
  94. \end{ex}
  96. \begin{ex}
  97. Sometimes we may derive !!a{formula} from other !!{formula}s.
  98. In these cases, we may have undischarged assumptions. It is
  99. important to keep track of our assumptions as well
  100. as the end goal.
  102. Let's see how we'd give !!a{derivation} of the !!{formula}
  103. $\lexists[x][!C(x,b)]$ from the assumptions $\lexists[x][(!A(x)
  104. \land !B(x))]$ and $\lforall[x][(!B(x) \lif !C(x,b))]$.
  105. Starting as usual, we write the conclusion at the
  106. bottom.
  107. \begin{prooftree}
  108. \AxiomC{}
  109. \UnaryInfC{$\lexists[x][!C(x,b)]$}
  110. \end{prooftree}
  112. We have two premises to work with. To use the first, i.e., try to find
  113. !!a{derivation} of $\lexists[x][!C(x, b)]$ from $\lexists[x][(!A(x)
  114. \land !B(x))]$ we would use the \Elim{\lexists} rule. Since it has
  115. an eigenvariable condition, we will apply that rule first. We get the
  116. following:
  117. \begin{prooftree}
  118. \AxiomC{$\lexists[x][(!A(x) \land !B(x))]$}
  119. \AxiomC{$\Discharge{!A(a) \land !B(a)}{1}$}
  120. \DeduceC{$\lexists[x][!C(x,b)]$}
  121. \DischargeRule{\Elim{\lexists}}{1}
  122. \BinaryInfC{$\lexists[x][!C(x,b)]$}
  123. \end{prooftree}
  124. The two assumptions we are working with share~$!B$. It may be useful
  125. at this point to apply \Elim{\land} to separate out~$!B(a)$.
  126. \begin{prooftree}
  127. \AxiomC{$\lexists[x][(!A(x) \land !B(x)])$}
  128. \AxiomC{$\Discharge{!A(a)
  129. \land !B(a)}{1}$}
  130. \RightLabel{\Elim{\land}}
  131. \UnaryInfC{$!B(a)$}
  132. \DeduceC{$\lexists[x][!C(x,b)]$}
  133. \DischargeRule{\Elim{\lexists}}{1}
  134. \BinaryInfC{$\lexists[x][!C(x,b)]$}
  135. \end{prooftree}
  137. The second assumption we have to work with is~$\lforall[x][(!B(x) \lif
  138. !C(x,b))]$. Since there is no eigenvariable condition we can
  139. instantiate $x$ with the !!{constant}~$a$ using \Elim{\lforall} to get
  140. $!B(a) \lif !C(a, b)$. We now have both $!B(a) \lif !C(a,b)$ and
  141. $!B(a)$. Our next move should be a straightforward application of the
  142. \Elim{\lif} rule.
  143. \begin{prooftree}
  144. \AxiomC{$\lexists[x][(!A(x) \land !B(x))]$}
  145. \AxiomC{$\lforall[x][(!B(x) \lif !C(x,b))]$}
  146. \RightLabel{\Elim{\lforall}}
  147. \UnaryInfC{$!B(a) \lif !C(a,b)$}
  148. \AxiomC{$\Discharge{!A(a)
  149. \land !B(a)}{1}$}
  150. \RightLabel{\Elim{\land}}
  151. \UnaryInfC{$!B(a)$}
  152. \RightLabel{\Elim{\lif}}
  153. \BinaryInfC{$!C(a,b)$}
  154. \DeduceC{$\lexists[x][!C(x,b)]$}
  155. \DischargeRule{\Elim{\lexists}}{1}
  156. \insertBetweenHyps{\hspace{-5em}}
  157. \BinaryInfC{$\lexists[x][!C(x,b)]$}
  158. \end{prooftree}
  159. We are so close!{} One application of \Intro{\lexists} and we
  160. have reached our goal.
  161. \begin{prooftree}
  162. \AxiomC{$\lexists[x][(!A(x) \land !B(x))]$}
  163. \AxiomC{$\lforall[x][(!B(x) \lif !C(x,b))]$}
  164. \RightLabel{\Elim{\lforall}}
  165. \UnaryInfC{$!B(a) \lif !C(a,b)$}
  166. \AxiomC{$\Discharge{!A(a)
  167. \land !B(a)}{1}$}
  168. \RightLabel{\Elim{\land}}
  169. \UnaryInfC{$!B(a)$}
  170. \RightLabel{\Elim{\lif}}
  171. \BinaryInfC{$!C(a,b)$}
  172. \RightLabel{\Intro{\lexists}}
  173. \UnaryInfC{$\lexists[x][!C(x,b)]$}
  174. \DischargeRule{\Elim{\lexists}}{1}
  175. \insertBetweenHyps{\hspace{-5em}}
  176. \BinaryInfC{$\lexists[x][!C(x,b)]$}
  177. \end{prooftree}
  178. Since we ensured at each step that the eigenvariable
  179. conditions were not violated, we can be confident that this
  180. is a correct !!{derivation}.
  181. \end{ex}
  183. \begin{ex}
  184. Give !!a{derivation} of the !!{formula}
  185. $\lnot\lforall[x][!A(x)]$ from the assumptions $\lforall[x][!A(x)]
  186. \lif \lexists[y][!B(y)]$ and $\lnot\lexists[y][!B(y)]$.
  187. Starting as usual, we write the target !!{formula} at the bottom.
  188. \begin{prooftree}
  189. \AxiomC{}
  190. \UnaryInfC{$\lnot\lforall[x][!A(x)]$}
  191. \end{prooftree}
  192. The last line of the !!{derivation} is a negation, so let's try using
  193. \Intro{\lnot}. This will require that we figure out how to !!{derive}
  194. a contradiction.
  195. \begin{prooftree}
  196. \AxiomC{$\Discharge{\lforall[x][!A(x)]}{1}$}
  197. \DeduceC{$\lfalse$}
  198. \DischargeRule{\Intro{\lnot}}{1}
  199. \UnaryInfC{$\lnot\lforall[x][!A(x)]$}
  200. \end{prooftree}
  201. So far so good. We can use \Elim{\lforall} but it's not obvious
  202. if that will help us get to our goal. Instead, let's use one of our
  203. assumptions. $\lforall[x][!A(x)] \lif \lexists[y][!B(y)]$ together
  204. with $\lforall[x][!A(x)]$ will allow us to use the \Elim{\lif} rule.
  205. \begin{prooftree}
  206. \AxiomC{$\lforall[x][!A(x)] \lif \lexists[y][!B(y)]$}
  207. \AxiomC{$\Discharge{\lforall[x][!A(x)]}{1}$}
  208. \RightLabel{\Elim{\lif}}
  209. \BinaryInfC{$\lexists[y][!B(y)]$}
  210. \DeduceC{$\lfalse$}
  211. \DischargeRule{\Intro{\lnot}}{1}
  212. \UnaryInfC{$\lnot\lforall[x][!A(x)]$}
  213. \end{prooftree}
  214. We now have one final assumption to work with,
  215. and it looks like this will help us reach a contradiction
  216. by using \Elim{\lnot}.
  217. \begin{prooftree}
  218. \AxiomC{$\lnot\lexists[y][!B(y)]$}
  219. \AxiomC{$\lforall[x][!A(x)] \lif \lexists[y][!B(y)]$}
  220. \AxiomC{$\Discharge{\lforall[x][!A(x)]}{1}$}
  221. \RightLabel{\Elim{\lif}}
  222. \BinaryInfC{$\lexists[y][!B(y)]$}
  223. \RightLabel{\Elim{\lnot}}
  224. \BinaryInfC{$\lfalse$}
  225. \DischargeRule{\Intro{\lnot}}{1}
  226. \UnaryInfC{$\lnot\lforall[x][!A(x)]$}
  227. \end{prooftree}
  228. \end{ex}
  230. \begin{prob}
  231. Give !!{derivation}s that show the following:
  232. \begin{enumerate}
  233. \item $\Proves (\lforall[x][!A(x)] \land \lforall[y][!B(y)]) \lif
  234. \lforall[z][(!A(z) \land !B(z))]$.
  235. \item $\Proves (\lexists[x][!A(x)] \lor \lexists[y][!B(y)]) \lif
  236. \lexists[z][(!A(z) \lor !B(z))]$.
  237. \item $\lforall[x][(!A(x) \lif !B)] \Proves \lexists[y][!A(y)] \lif !B$.
  238. \item $\lforall[x][\lnot !A(x)] \Proves \lnot\lexists[x][!A(x)]$.
  239. \item $\Proves \lnot\lexists[x][!A(x)] \lif \lforall[x][\lnot !A(x)]$.
  240. \item $\Proves \lnot\lexists[x][\lforall[y][((!A(x,y) \lif \lnot
  241. !A(y,y)) \land (\lnot !A(y,y) \lif !A(x,y)))]]$.
  242. \end{enumerate}
  243. \end{prob}
  245. \begin{prob}
  246. Give !!{derivation}s that show the following:
  247. \begin{enumerate}
  248. \item $\Proves \lnot\lforall[x][!A(x)] \lif \lexists[x][\lnot!A(x)]$.
  249. \item $(\lforall[x][!A(x)] \lif !B) \Proves \lexists[y][(!A(y) \lif !B)]$.
  250. \item $\Proves \lexists[x][(!A(x) \lif \lforall[y][!A(y)])]$.
  251. \end{enumerate}
  252. (These all require the $\FalseCl$~rule.)
  253. \end{prob}
  255. \end{document}

content/first-order-logic/natural-deduction/proof-theoretic-notions.tex

159 lines; SHA-256 7e05743251dd0c5071685193a98c28baea1c77b06836f11e3f3e3aa6a6bd9198. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: natural-deduction
  3. % Section: proof-theoretic-notions
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{ntd}{ptn}}
  11. {\olfileid{pl}{ntd}{ptn}}
  13. \olsection{Proof-Theoretic Notions}
  15. \begin{editorial}
  16. This section collects the definitions the provability relation
  17. and consistency for natural deduction.
  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. !!{derivability} or !!{nonderivability} of certain !!{sentence}s from
  26. others. It was an important discovery that these notions coincide.
  27. That they do is the content of the \emph{soundness} and
  28. \emph{completeness theorems}.
  29. \end{explain}
  32. \begin{defn}[Theorems]
  33. A !!{sentence}~$!A$ is a \emph{theorem} if there is !!a{derivation}
  34. of~$!A$ in natural deduction in which all assumptions are
  35. !!{discharged}. We write $\Proves !A$ if $!A$ is a theorem and
  36. $\Proves/ !A$ if it is not.
  37. \end{defn}
  39. \begin{defn}[!!^{derivability}]
  40. !!^a{sentence} $!A$ is \emph{!!{derivable} from} a set of
  41. !!{sentence}s~$\Gamma$, $\Gamma \Proves !A$, if there is a
  42. !!{derivation} with conclusion~$!A$ and in which every assumption
  43. is either !!{discharged} or is in~$\Gamma$. If $!A$ is not
  44. !!{derivable} from $\Gamma$ we write $\Gamma \Proves/ !A$.
  45. \end{defn}
  47. \begin{defn}[Consistency]
  48. A set of !!{sentence}s~$\Gamma$ is \emph{inconsistent} iff $\Gamma
  49. \Proves \lfalse$. If $\Gamma$ is not inconsistent, i.e., if
  50. $\Gamma \Proves/ \lfalse$, we say it is \emph{consistent}.
  51. \end{defn}
  53. \begin{prop}[Reflexivity]
  54. \ollabel{prop:reflexivity}
  55. If $!A \in \Gamma$, then $\Gamma \Proves !A$.
  56. \end{prop}
  58. \begin{proof}
  59. The assumption $!A$ by itself is !!a{derivation} of~$!A$ where every
  60. !!{undischarged} assumption (i.e., $!A$) is in~$\Gamma$.
  61. \end{proof}
  64. \begin{prop}[Monotonicity]
  65. \ollabel{prop:monotonicity}
  66. If $\Gamma \subseteq \Delta$ and $\Gamma \Proves !A$, then $\Delta
  67. \Proves !A$.
  68. \end{prop}
  70. \begin{proof}
  71. Any !!{derivation} of $!A$ from $\Gamma$ is also !!a{derivation} of
  72. $!A$ from~$\Delta$.
  73. \end{proof}
  75. \begin{prop}[Transitivity]
  76. \ollabel{prop:transitivity}
  77. If $\Gamma \Proves !A$ and $\{!A\} \cup \Delta \Proves
  78. !B$, then $\Gamma \cup \Delta \Proves !B$.
  79. \end{prop}
  81. \begin{proof}
  82. If $\Gamma \Proves !A$, there is !!a{derivation}~$\delta_0$ of~$!A$
  83. with all !!{undischarged} assumptions in~$\Gamma$. If $\{!A\} \cup
  84. \Delta \Proves !B$, then there is !!a{derivation}~$\delta_1$ of~$!B$
  85. with all !!{undischarged} assumptions in~$\{!A\} \cup \Delta$.
  86. Now consider:
  87. \begin{prooftree}
  88. \AxiomC{$\Delta, \Discharge{!A}{1}$}
  89. \RightLabel{$\delta_1$}
  90. \DeduceC{$!B$}
  91. \DischargeRule{\Intro{\lif}}{1}
  92. \UnaryInfC{$!A \lif !B$}
  93. \AxiomC{$\Gamma$}
  94. \RightLabel{$\delta_0$}
  95. \DeduceC{$!A$}
  96. \RightLabel{\Elim{\lif}}
  97. \BinaryInfC{$!B$}
  98. \end{prooftree}
  99. The !!{undischarged} assumptions are now all among $\Gamma \cup
  100. \Delta$, so this shows $\Gamma \cup \Delta \Proves !B$.
  101. \end{proof}
  103. When $\Gamma = \{!A_1, !A_2, \ldots, !A_k\}$ is a finite set we may use the simplified notation $!A_1,!A_2,\ldots,!A_k \Proves !B$ for $\Gamma \Proves !B$, in particular $!A \Proves !B$ means that $\{!A\} \Proves !B$.
  105. Note that if $\Gamma \Proves !A$ and $!A
  106. \Proves !B$, then $\Gamma \Proves !B$. It follows also that if $!A_1,
  107. \dots, !A_n \Proves !B$ and $\Gamma \Proves !A_i$ for each~$i$, then
  108. $\Gamma \Proves !B$.
  110. \begin{prop}
  111. \ollabel{prop:incons}
  112. The following are equivalent.
  113. \begin{enumerate}
  114. \item \( \Gamma \) is inconsistent.
  115. \item \( \Gamma \Proves {!A} \) for every !!{sentence}~\( {!A} \).
  116. \item \( \Gamma \Proves {!A} \) and \( \Gamma \Proves \lnot {!A} \) for some !!{sentence}~\( {!A} \).
  117. \end{enumerate}
  118. \end{prop}
  120. \begin{proof}
  121. Exercise.
  122. \end{proof}
  124. \tagprob{FOL}
  125. \begin{prob}
  126. Prove \olref[fol][ntd][ptn]{prop:incons}
  127. \end{prob}
  128. \tagendprob
  130. \tagprob{notFOL}
  131. \begin{prob}
  132. Prove \olref[pl][ntd][ptn]{prop:incons}
  133. \end{prob}
  134. \tagendprob
  136. \begin{prop}[Compactness]
  137. \ollabel{prop:proves-compact}
  138. \begin{enumerate}
  139. \item If $\Gamma \Proves !A$ then there is a finite subset $\Gamma_0
  140. \subseteq \Gamma$ such that $\Gamma_0 \Proves !A$.
  141. \item If every finite subset of~$\Gamma$ is
  142. consistent, then $\Gamma$ is consistent.
  143. \end{enumerate}
  144. \end{prop}
  146. \begin{proof}
  147. \begin{enumerate}
  148. \item If $\Gamma \Proves !A$, then there is
  149. !!a{derivation}~$\delta$ of~$!A$ from~$\Gamma$. Let $\Gamma_0$
  150. be the set of !!{undischarged} assumptions of~$\delta$. Since
  151. any !!{derivation} is finite, $\Gamma_0$ can only contain
  152. finitely many !!{sentence}s. So, $\delta$ is !!a{derivation}
  153. of~$!A$ from a finite~$\Gamma_0 \subseteq \Gamma$.
  154. \item This is the contrapositive of (1) for the special case $!A
  155. \ident \lfalse$.
  156. \end{enumerate}
  157. \end{proof}
  159. \end{document}

content/first-order-logic/natural-deduction/provability-consistency.tex

131 lines; SHA-256 9d967013e14c7f911bf612ddab65b22a2e5f8d90f182926741c0bf7cab5076bc. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: natural-deduction
  3. % Section: provability-consistency
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{ntd}{prv}}
  11. {\olfileid{pl}{ntd}{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 inconsistent,
  21. then $\Gamma$ is inconsistent.
  22. \end{prop}
  24. \begin{proof}
  25. Let the !!{derivation} of~$!A$ from~$\Gamma$ be~$\delta_1$ and the
  26. !!{derivation} of~$\lfalse$ from $\Gamma \cup \{!A\}$
  27. be~$\delta_2$. We can then !!{derive}:
  28. \begin{prooftree}
  29. \AxiomC{$\Gamma, \Discharge{!A}{1}$}
  30. \RightLabel{$\delta_2$}
  31. \DeduceC{$\lfalse$}
  32. \DischargeRule{\Intro{\lnot}}{1}
  33. \UnaryInfC{$\lnot !A$}
  34. \AxiomC{$\Gamma$}
  35. \RightLabel{$\delta_1$}
  36. \DeduceC{$!A$}
  37. \RightLabel{\Elim{\lnot}}
  38. \BinaryInfC{$\lfalse$}
  39. \end{prooftree}
  40. In the new !!{derivation}, the assumption~$!A$ is !!{discharged}, so it is
  41. !!a{derivation} from~$\Gamma$.
  42. \end{proof}
  44. \begin{prop}
  45. \ollabel{prop:prov-incons}
  46. $\Gamma \Proves !A$ iff $\Gamma \cup \{\lnot !A\}$ is inconsistent.
  47. \end{prop}
  49. \begin{proof}
  50. First suppose $\Gamma \Proves !A$, i.e., there is
  51. !!a{derivation}~$\delta_0$ of~$!A$ from !!{undischarged}
  52. assumptions~$\Gamma$. We obtain !!a{derivation} of $\lfalse$ from
  53. $\Gamma \cup \{\lnot !A\}$ as follows:
  54. \begin{prooftree}
  55. \AxiomC{$\lnot !A$}
  56. \AxiomC{$\Gamma$}
  57. \RightLabel{$\delta_0$}
  58. \DeduceC{$!A$}
  59. \RightLabel{\Elim{\lnot}}
  60. \BinaryInfC{$\lfalse$}
  61. \end{prooftree}
  63. Now assume $\Gamma \cup \{\lnot !A\}$ is inconsistent, and let
  64. $\delta_1$ be the corresponding !!{derivation} of~$\lfalse$ from
  65. !!{undischarged} assumptions in~$\Gamma \cup \{\lnot !A\}$. We obtain
  66. !!a{derivation} of~$!A$ from~$\Gamma$ alone by using~$\FalseCl$:
  67. \begin{prooftree}
  68. \AxiomC{$\Gamma, \Discharge{\lnot !A}{1}$}
  69. \RightLabel{$\delta_1$}
  70. \DeduceC{$\lfalse$}
  71. \RightLabel{\FalseCl}
  72. \DischargeRule{\FalseCl}{1}
  73. \UnaryInfC{$!A$}
  74. \end{prooftree}
  75. \end{proof}
  77. \begin{prob}
  78. Prove that $\Gamma \Proves \lnot !A$ iff $\Gamma \cup \{!A\}$ is
  79. inconsistent.
  80. \end{prob}
  82. \begin{prop}\ollabel{prop:explicit-inc}
  83. If $\Gamma \Proves !A$ and $\lnot !A \in \Gamma$, then $\Gamma$ is
  84. inconsistent.
  85. \end{prop}
  87. \begin{proof}
  88. Suppose $\Gamma \Proves !A$ and $\lnot !A \in \Gamma$. Then there
  89. is !!a{derivation}~$\delta$ of~$!A$ from~$\Gamma$. Consider this
  90. simple application of the $\Elim{\lnot}$ rule:
  91. \begin{prooftree}
  92. \AxiomC{$\lnot !A$}
  93. \AxiomC{$\Gamma$}
  94. \RightLabel{$\delta$}
  95. \DeduceC{$!A$}
  96. \RightLabel{\Elim{\lnot}}
  97. \BinaryInfC{$\lfalse$}
  98. \end{prooftree}
  99. Since $\lnot !A \in \Gamma$, all !!{undischarged} assumptions are
  100. in~$\Gamma$, this shows that $\Gamma \Proves \lfalse$.
  101. \end{proof}
  103. \begin{prop}\ollabel{prop:provability-exhaustive}
  104. If $\Gamma \cup \{!A\}$ and $\Gamma \cup \{\lnot !A\}$ are both
  105. inconsistent, then $\Gamma$ is inconsistent.
  106. \end{prop}
  108. \begin{proof}
  109. There are !!{derivation}s $\delta_1$ and $\delta_2$ of~$\lfalse$ from
  110. $\Gamma \cup \{ !A \}$ and $\lfalse$ from $\Gamma \cup \{ \lnot !A
  111. \}$, respectively. We can then !!{derive}
  112. \begin{prooftree}
  113. \AxiomC{$\Gamma, \Discharge{\lnot !A}{2}$}
  114. \RightLabel{$\delta_2$}
  115. \DeduceC{$\lfalse$}
  116. \DischargeRule{\Intro{\lnot}}{2}
  117. \UnaryInfC{$\lnot \lnot !A$}
  118. \AxiomC{$\Gamma, \Discharge{!A}{1}$}
  119. \RightLabel{$\delta_1$}
  120. \DeduceC{$\lfalse$}
  121. \DischargeRule{\Intro{\lnot}}{1}
  122. \UnaryInfC{$\lnot !A$}
  123. \RightLabel{\Elim{\lnot}}
  124. \BinaryInfC{$\lfalse$}
  125. \end{prooftree}
  126. Since the assumptions $!A$ and $\lnot !A$ are !!{discharged}, this is
  127. !!a{derivation} of~$\lfalse$ from~$\Gamma$ alone. Hence $\Gamma$ is
  128. inconsistent.
  129. \end{proof}
  131. \end{document}

content/first-order-logic/natural-deduction/provability-propositional.tex

133 lines; SHA-256 7be41cbf7877f1b7163f3cc9ad98867b4cf793b69f4a98e5734f731e3e802016. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: natural-deduction
  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}{ntd}{ppr}}
  14. {\olfileid{pl}{ntd}{ppr}}
  16. \olsection{\usetoken{S}{derivability} and the Propositional Connectives}
  18. \begin{explain}
  19. We establish that the !!{derivability} relation~$\Proves$ of natural
  20. deduction is strong enough to establish some basic facts
  21. involving the propositional connectives, such as that $!A \land !B
  22. \Proves !A$ and $!A, !A \lif !B \Proves !B$ (modus ponens). These
  23. facts are 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 !B$.
  31. \end{enumerate}
  32. \end{prop}
  34. \begin{proof}
  35. \begin{enumerate}
  36. \item We can !!{derive} both
  37. \begin{prooftree}
  38. \AxiomC{$!A \land !B$}
  39. \RightLabel{\Elim{\land}}
  40. \UnaryInfC{$!A$}
  41. \DisplayProof\qquad\bottomAlignProof
  42. \AxiomC{$!A \land !B$}
  43. \RightLabel{\Elim{\land}}
  44. \UnaryInfC{$!B$}
  45. \end{prooftree}
  46. \item We can !!{derive}:
  47. \begin{prooftree}
  48. \AxiomC{$!A$}
  49. \AxiomC{$!B$}
  50. \RightLabel{\Intro{\land}}
  51. \BinaryInfC{$!A \land !B$}
  52. \end{prooftree}
  53. \end{enumerate}
  54. \end{proof}
  57. \begin{prop}\ollabel{prop:provability-lor}
  58. \begin{enumerate}
  59. \item $!A \lor !B, \lnot !A, \lnot !B$ is inconsistent.
  60. \item Both $!A \Proves !A \lor !B$ and $!B \Proves !A \lor !B$.
  61. \end{enumerate}
  62. \end{prop}
  64. \begin{proof}
  65. \begin{enumerate}
  66. \item Consider the following !!{derivation}:
  67. \begin{prooftree}
  68. \AxiomC{$!A \lor !B$}
  69. \AxiomC{$\lnot !A$}
  70. \AxiomC{$\Discharge{!A}{1}$}
  71. \RightLabel{\Elim{\lnot}}
  72. \BinaryInfC{$\lfalse$}
  73. \AxiomC{$\lnot !B$}
  74. \AxiomC{$\Discharge{!B}{1}$}
  75. \RightLabel{\Elim{\lnot}}
  76. \BinaryInfC{$\lfalse$}
  77. \DischargeRule{\Elim{\lor}}{1}
  78. \TrinaryInfC{$\lfalse$}
  79. \end{prooftree}
  80. This is !!a{derivation} of~$\lfalse$ from !!{undischarged}
  81. assumptions $!A \lor !B$, $\lnot !A$, and $\lnot !B$.
  82. \item We can !!{derive} both
  83. \begin{prooftree}
  84. \AxiomC{$!A$}
  85. \RightLabel{\Intro{\lor}}
  86. \UnaryInfC{$!A \lor !B$}
  87. \DisplayProof\qquad\bottomAlignProof
  88. \AxiomC{$!B$}
  89. \RightLabel{\Intro{\lor}}
  90. \UnaryInfC{$!A \lor !B$}
  91. \end{prooftree}
  92. \end{enumerate}
  93. \end{proof}
  95. \begin{prop}\ollabel{prop:provability-lif}
  96. \begin{enumerate}
  97. \item \ollabel{prop:provability-lif-left} $!A, !A \lif !B \Proves !B$.
  98. \item \ollabel{prop:provability-lif-right}
  99. Both $\lnot !A \Proves !A \lif !B$ and $!B \Proves !A \lif !B$.
  100. \end{enumerate}
  101. \end{prop}
  103. \begin{proof}
  104. \begin{enumerate}
  105. \item We can !!{derive}:
  106. \begin{prooftree}
  107. \AxiomC{$!A \lif !B$}
  108. \AxiomC{$!A$}
  109. \RightLabel{\Elim{\lif}}
  110. \BinaryInfC{$!B$}
  111. \end{prooftree}
  113. \item This is shown by the following two !!{derivation}s:
  114. \begin{prooftree}
  115. \AxiomC{$\lnot !A$}
  116. \AxiomC{$\Discharge{!A}{1}$}
  117. \RightLabel{\Elim{\lnot}}
  118. \BinaryInfC{$\lfalse$}
  119. \RightLabel{\FalseInt}
  120. \UnaryInfC{$!B$}
  121. \DischargeRule{\Intro{\lif}}{1}
  122. \UnaryInfC{$!A \lif !B$}
  123. \DisplayProof\qquad\bottomAlignProof
  124. \AxiomC{$!B$}
  125. \RightLabel{\Intro{\lif}}
  126. \UnaryInfC{$!A \lif !B$}
  127. \end{prooftree}
  128. Note that $\Intro{\lif}$ may, but does not have to, !!{discharge} the
  129. assumption~$!A$.
  130. \end{enumerate}
  131. \end{proof}
  133. \end{document}

content/first-order-logic/natural-deduction/provability-quantifiers.tex

63 lines; SHA-256 c4a24bb64b2d02c75fcf5dcebe13d48c4684afd8f210da029ceefcb450990bf1. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: natural-deduction
  3. % Section: provability-quantifiers
  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. \olfileid{fol}{ntd}{qpr}
  14. \olsection{\usetoken{S}{derivability} and the Quantifiers}
  16. \begin{explain}
  17. The completeness theorem also requires that the natural deduction
  18. rules yield the facts about~$\Proves$ established in this section.
  19. \end{explain}
  21. \begin{thm}
  22. \ollabel{thm:strong-generalization} If $c$ is a constant not occurring
  23. in $\Gamma$ or $!A(x)$ and $\Gamma \Proves !A(c)$, then $\Gamma
  24. \Proves \lforall[x][!A(x)]$.
  25. \end{thm}
  27. \begin{proof}
  28. Let $\delta$ be !!a{derivation} of $!A(c)$ from $\Gamma$. By adding a
  29. \Intro{\lforall} inference, we obtain !!a{derivation} of
  30. $\lforall[x][!A(x)]$. Since $c$ does not occur in $\Gamma$ or $!A(x)$,
  31. the eigenvariable condition is satisfied.
  32. \end{proof}
  34. \begin{prop}
  35. \ollabel{prop:provability-quantifiers}
  36. \begin{tagenumerate}{prvEx,prvAll}
  37. \tagitem{prvEx}{$!A(t) \Proves \lexists[x][!A(x)]$.}{}
  39. \tagitem{prvAll}{$\lforall[x][!A(x)] \Proves !A(t)$.}{}
  40. \end{tagenumerate}
  41. \end{prop}
  43. \begin{proof}
  44. \begin{tagenumerate}{prvEx,prvAll}
  45. \tagitem{prvEx}{The following is !!a{derivation}
  46. of~$\lexists[x][!A(x)]$ from~$!A(t)$:
  47. \begin{prooftree}
  48. \AxiomC{$!A(t)$}
  49. \RightLabel{\Intro{\lexists}}
  50. \UnaryInfC{$\lexists[x][!A(x)]$}
  51. \end{prooftree}}{}
  53. \tagitem{prvAll}{The following is !!a{derivation} of~$!A(t)$
  54. from~$\lforall[x][!A(x)]$:
  55. \begin{prooftree}
  56. \AxiomC{$\lforall[x][!A(x)]$}
  57. \RightLabel{\Elim{\lforall}}
  58. \UnaryInfC{$!A(t)$}
  59. \end{prooftree}}{}
  60. \end{tagenumerate}
  61. \end{proof}
  63. \end{document}

content/first-order-logic/natural-deduction/soundness.tex

314 lines; SHA-256 e470b5e3a94dd4445dcedc0bbb2d4bb9c5520a3f79ea754f37e4ae1501376e35. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: natural-deduction
  3. % Section: soundness
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{ntd}{sou}}
  11. {\olfileid{pl}{ntd}{sou}}
  13. \olsection{Soundness}
  15. \begin{explain}
  16. !!^a{derivation} system, such as natural deduction, is \emph{sound}
  17. if it cannot !!{derive} things that do not actually follow. 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} !!{sentence} 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
  28. them do not hold, the !!{derivation} system is deficient---it would
  29. !!{derive} too much. Consequently, establishing the soundness of a
  30. !!{derivation} system is of the utmost importance.
  31. \end{explain}
  33. \begin{thm}[Soundness]
  34. \ollabel{thm:soundness}
  35. If $!A$ is !!{derivable} from the !!{undischarged} assumptions
  36. $\Gamma$, then $\Gamma \Entails !A$.
  37. \end{thm}
  39. \begin{proof}
  40. Let $\delta$ be !!a{derivation} of $!A$. We proceed by
  41. induction on the number of inferences in~$\delta$.
  43. For the induction basis we show the claim if the number of inferences
  44. is~$0$. In this case, $\delta$ consists only of a single
  45. !!{sentence}~$!A$, i.e., an assumption. That assumption is
  46. !!{undischarged}, since assumptions can only be !!{discharged} by
  47. inferences, and there are no inferences. So, any
  48. \iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$}
  49. that satisfies all of the !!{undischarged} assumptions of the proof
  50. also satisfies~$!A$.
  52. Now for the inductive step. Suppose that $\delta$ contains~$n$
  53. inferences. The premise(s) of the lowermost inference are !!{derive}d
  54. using sub-!!{derivation}s, each of which contains fewer than~$n$
  55. inferences. We assume the induction hypothesis: The premises of the
  56. lowermost inference follow from the !!{undischarged} assumptions of
  57. the sub-!!{derivation}s ending in those premises. We have to show
  58. that the conclusion~$!A$ follows from the !!{undischarged} assumptions
  59. of the entire proof.
  61. We distinguish cases according to the type of the lowermost inference.
  62. First, we consider the possible inferences with only one premise.
  64. \begin{enumerate}
  65. \item Suppose that the last inference is \Intro{\lnot}: The
  66. !!{derivation} has the form
  67. \begin{prooftree}
  68. \AxiomC{$\Gamma, \Discharge{!A}{n}$}
  69. \RightLabel{$\delta_1$}
  70. \DeduceC{$\lfalse$}
  71. \DischargeRule{\Intro{\lnot}}{n}
  72. \UnaryInfC{$\lnot !A$}
  73. \end{prooftree}
  74. By inductive hypothesis, $\lfalse$ follows from the !!{undischarged}
  75. assumptions $\Gamma \cup \{!A\}$ of~$\delta_1$. Consider
  76. \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}. We
  77. need to show that, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, then
  78. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\lnot !A}$. Suppose for reductio
  79. that $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, but
  80. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{\lnot !A}$, i.e.,
  81. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$. This would mean that
  82. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma \cup \{!A\}}$. This is
  83. contrary to our inductive hypothesis. So,
  84. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\lnot !A}$.
  86. \item The last inference is \Elim{\land}: There are two variants: $!A$
  87. or $!B$ may be inferred from the premise $!A \land !B$. Consider the
  88. first case. The !!{derivation}~$\delta$ looks like this:
  89. \begin{prooftree}
  90. \AxiomC{$\Gamma$}
  91. \RightLabel{$\delta_1$}
  92. \DeduceC{$!A \land !B$}
  93. \RightLabel{\Elim{\land}}
  94. \UnaryInfC{$!A$}
  95. \end{prooftree}
  96. By inductive hypothesis, $!A \land !B$ follows from the
  97. !!{undischarged} assumptions~$\Gamma$ of~$\delta_1$. Consider
  98. !!a{structure}~\iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$}. We need to
  99. show that, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, then
  100. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$. Suppose
  101. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$. By our inductive
  102. hypothesis ($\Gamma \Entails !A \land !B$), we know that
  103. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \land !B}$. By definition,
  104. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \land !B}$ iff
  105. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ and
  106. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$. (The case where $!B$ is
  107. inferred from $!A \land !B$ is handled similarly.)
  109. \item The last inference is \Intro{\lor}: There are two variants: $!A
  110. \lor !B$ may be inferred from the premise~$!A$ or the
  111. premise~$!B$. Consider the first case. The !!{derivation} has the form
  112. \begin{prooftree}
  113. \AxiomC{$\Gamma$}
  114. \RightLabel{$\delta_1$}
  115. \DeduceC{$!A$}
  116. \RightLabel{\Intro{\lor}}
  117. \UnaryInfC{$!A \lor !B$}
  118. \end{prooftree}
  119. By inductive hypothesis, $!A$ follows from the !!{undischarged}
  120. assumptions~$\Gamma$ of~$\delta_1$. Consider
  121. \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}. We
  122. need to show that, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$, then
  123. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \lor !B}$. Suppose
  124. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$; then
  125. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ since $\Gamma \Entails !A$ (the
  126. inductive hypothesis). So it must also be the case that
  127. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \lor !B}$. (The case where $!A
  128. \lor !B$ is inferred from~$!B$ is handled similarly.)
  130. \item The last inference is \Intro{\lif}: $!A \lif !B$ is inferred
  131. from a subproof with assumption~$!A$ and conclusion~$!B$, i.e.,
  132. \begin{prooftree}
  133. \AxiomC{$\Gamma, \Discharge{!A}{n}$}
  134. \RightLabel{$\delta_1$}
  135. \DeduceC{$!B$}
  136. \DischargeRule{\Intro{\lif}}{n}
  137. \UnaryInfC{$!A \lif !B$}
  138. \end{prooftree}
  139. By inductive hypothesis, $!B$ follows from the !!{undischarged}
  140. assumptions of~$\delta_1$, i.e., $\Gamma \cup \{!A\} \Entails
  141. !B$. Consider
  142. \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}. The
  143. !!{undischarged} assumptions of~$\delta$ are just $\Gamma$, since
  144. $!A$ is discharged at the last inference. So we need to show that
  145. $\Gamma \Entails !A \lif !B$. For reductio, suppose that for some
  146. \iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$},
  147. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$ but
  148. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A \lif !B}$. So,
  149. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ and
  150. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B}$. But by hypothesis, $!B$ is a
  151. consequence of $\Gamma \cup \{!A\}$, i.e.,
  152. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$, which is a contradiction. So,
  153. $\Gamma \Entails !A \lif !B$.
  155. \item The last inference is \FalseInt: Here, $\delta$ ends in
  156. \begin{prooftree}
  157. \AxiomC{$\Gamma$}
  158. \RightLabel{$\delta_1$}
  159. \DeduceC{$\lfalse$}
  160. \RightLabel{\FalseInt}
  161. \UnaryInfC{$!A$}
  162. \end{prooftree}
  163. By induction hypothesis, $\Gamma \Entails \lfalse$. We have to show
  164. that $\Gamma \Entails !A$. Suppose not; then for
  165. some~$\iftag{FOL}{\Struct{M}}{\pAssign{v}}$ we have
  166. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma}$ and
  167. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A}$. But we always have
  168. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{\lfalse}$, so this would mean
  169. that $\Gamma \Entails/ \lfalse$, contrary to the induction
  170. hypothesis.
  172. \item The last inference is \FalseCl: Exercise.
  174. \iftag{FOL}{
  175. \item The last inference is \Intro{\lforall}: Then $\delta$ has the form
  176. \begin{prooftree}
  177. \AxiomC{$\Gamma$}
  178. \RightLabel{$\delta_1$}
  179. \DeduceC{$!A(a)$}
  180. \RightLabel{\Intro{\lforall}}
  181. \UnaryInfC{$\lforall[x][!A(x)]$}
  182. \end{prooftree}
  183. The premise $!A(a)$ is a consequence of the !!{undischarged}
  184. assumptions $\Gamma$ by induction hypothesis. Consider some
  185. structure, $\Struct{M}$, such that $\Sat{M}{\Gamma}$. We need to
  186. show that $\Sat{M}{\lforall[x][!A(x)]}$. Since $\lforall[x][!A(x)]$
  187. is !!a{sentence}, this means we have to show that for every variable
  188. assignment~$s$, $\Sat{M}{!A(x)}[s]$
  189. (\olref[syn][ass]{prop:sat-quant}). Since $\Gamma$ consists entirely
  190. of sentences, $\Sat{M}{!B}[s]$ for all $!B \in \Gamma$ by
  191. \olref[syn][sat]{defn:satisfaction}. Let $\Struct{M'}$ be like
  192. $\Struct{M}$ except that $\Assign{a}{M'} = s(x)$. Since $a$ does
  193. not occur in~$\Gamma$, $\Sat{M'}{\Gamma}$ by
  194. \olref[syn][ext]{cor:extensionality-sent}. Since $\Gamma \Entails
  195. !A(a)$, $\Sat{M'}{!A(a)}$. Since $!A(a)$ is !!a{sentence},
  196. $\Sat{M'}{!A(a)}[s]$ by
  197. \olref[syn][ass]{prop:sentence-sat-true}. $\Sat{M'}{!A(x)}[s]$ iff
  198. $\Sat{M'}{!A(a)}$ by \olref[syn][ext]{prop:ext-formulas} (recall
  199. that $!A(a)$ is just $\Subst{!A(x)}{a}{x}$). So,
  200. $\Sat{M'}{!A(x)}[s]$. Since $a$ does not occur in~$!A(x)$, by
  201. \olref[syn][ext]{prop:extensionality}, $\Sat{M}{!A(x)}[s]$. But $s$
  202. was an arbitrary variable assignment, so
  203. $\Sat{M}{\lforall[x][!A(x)]}$.
  205. \item The last inference is \Intro{\lexists}: Exercise.
  207. \item The last inference is \Elim{\forall}: Exercise.
  208. }{}
  209. \end{enumerate}
  211. Now let's consider the possible inferences with several premises:
  212. \Elim{\lor}, \Intro{\land}, \iftag{FOL}{\Elim{\lif}, and
  213. \Elim{\lexists}}{and \Elim{\lif}}.
  214. \begin{enumerate}
  216. \item The last inference is \Intro{\land}. $!A \land !B$ is inferred
  217. from the premises $!A$ and $!B$ and $\delta$ has the form
  218. \begin{prooftree}
  219. \AxiomC{$\Gamma_1$}
  220. \RightLabel{$\delta_1$}
  221. \DeduceC{$!A$}
  222. \AxiomC{$\Gamma_2$}
  223. \RightLabel{$\delta_2$}
  224. \DeduceC{$!B$}
  225. \RightLabel{\Intro{\land}}
  226. \BinaryInfC{$!A \land !B$}
  227. \end{prooftree}
  228. By induction hypothesis, $!A$ follows from the !!{undischarged}
  229. assumptions~$\Gamma_1$ of~$\delta_1$ and $!B$ follows from the
  230. !!{undischarged} assumptions~$\Gamma_2$ of~$\delta_2$. The
  231. !!{undischarged} assumptions of~$\delta$ are $\Gamma_1 \cup
  232. \Gamma_2$, so we have to show that $\Gamma_1 \cup \Gamma_2 \Entails
  233. !A \land !B$. Consider
  234. \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}
  235. with $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_1 \cup \Gamma_2}$. Since
  236. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_1}$, it must be the case that
  237. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$ as $\Gamma_1 \Entails !A$, and
  238. since $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_2}$,
  239. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$ since $\Gamma_2 \Entails
  240. !B$. Together, $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \land !B}$.
  242. \item The last inference is \Elim{\lor}: Exercise.
  244. \item The last inference is \Elim{\lif}. $!B$ is inferred from the
  245. premises $!A \lif !B$ and~$!A$. The !!{derivation}~$\delta$ looks like this:
  246. \begin{prooftree}
  247. \AxiomC{$\Gamma_1$}
  248. \RightLabel{$\delta_1$}
  249. \DeduceC{$!A \lif !B$}
  250. \AxiomC{$\Gamma_2$}
  251. \RightLabel{$\delta_2$}
  252. \DeduceC{$!A$}
  253. \RightLabel{\Elim{\lif}}
  254. \BinaryInfC{$!B$}
  255. \end{prooftree}
  256. By induction hypothesis, $!A \lif !B$ follows from the
  257. !!{undischarged} assumptions~$\Gamma_1$ of~$\delta_1$ and $!A$
  258. follows from the !!{undischarged} assumptions~$\Gamma_2$
  259. of~$\delta_2$. Consider
  260. \iftag{FOL}{!!a{structure}~$\Struct{M}$}{!!a{valuation}~$\pAssign{v}$}. We
  261. need to show that, if $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_1 \cup
  262. \Gamma_2}$, then $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$. Suppose
  263. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{\Gamma_1 \cup \Gamma_2}$. Since
  264. $\Gamma_1 \Entails !A \lif !B$, $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A
  265. \lif !B}$. Since $\Gamma_2 \Entails !A$, we have
  266. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$. This means that
  267. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!B}$ (For if
  268. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!B}$, since
  269. $\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A}$, we'd have
  270. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{!A \lif !B}$,
  271. contradicting~$\iftag{FOL}{\Sat{M}}{\pSat{v}}{!A \lif !B}$).
  273. \item The last inference is \Elim{\lnot}: Exercise.
  275. \tagitem{FOL}{The last inference is \Elim{\lexists}: Exercise.}{}
  276. \end{enumerate}
  277. \end{proof}
  279. \tagprob{FOL}
  280. \begin{prob}
  281. Complete the proof of \olref[fol][ntd][sou]{thm:soundness}.
  282. \end{prob}
  283. \tagendprob
  285. \tagprob{notFOL}
  286. \begin{prob}
  287. Complete the proof of \olref[pl][ntd][sou]{thm:soundness}.
  288. \end{prob}
  289. \tagendprob
  291. \begin{cor}
  292. \ollabel{cor:weak-soundness}
  293. If $\Proves !A$, then $!A$ is \iftag{FOL}{valid}{a tautology}.
  294. \end{cor}
  296. \begin{cor}
  297. \ollabel{cor:consistency-soundness}
  298. If $\Gamma$ is satisfiable, then it is consistent.
  299. \end{cor}
  301. \begin{proof}
  302. We prove the contrapositive. Suppose that $\Gamma$ is not consistent.
  303. Then $\Gamma \Proves \lfalse$, i.e., there is !!a{derivation} of
  304. $\lfalse$ from !!{undischarged} assumptions in~$\Gamma$. By
  305. \olref{thm:soundness}, any
  306. \iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$}
  307. that satisfies $\Gamma$ must satisfy $\lfalse$. Since
  308. $\iftag{FOL}{\Sat/{M}}{\pSat/{v}}{\lfalse}$ for every
  309. \iftag{FOL}{!!{structure}~$\Struct{M}$}{!!{valuation}~$\pAssign{v}$},
  310. no \iftag{FOL}{$\Struct{M}$}{$\pAssign{v}$} can satisfy $\Gamma$,
  311. i.e., $\Gamma$ is not satisfiable.
  312. \end{proof}
  314. \end{document}

content/first-order-logic/natural-deduction/identity.tex

124 lines; SHA-256 d5df1d1bb3818a275e2439a584a3851036870182afde592fa6e8f80b55c00add. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: natural-deduction
  3. % Section: identity
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{ntd}{ide}
  11. \olsection{\usetoken{P}{derivation} with \usetoken{S}{identity}}
  13. !!^{derivation}s with !!{identity} require additional inference rules.
  15. \begin{defish}
  16. \AxiomC{}
  17. \RightLabel{\Intro{\eq}}
  18. \UnaryInfC{$\eq[t][t]$}
  19. \DisplayProof
  20. \hfill
  21. \begin{tabular}{r}
  22. \AxiomC{$\eq[t_1][t_2]$}
  23. \AxiomC{$!A(t_1)$}
  24. \RightLabel{\Elim{\eq}}
  25. \BinaryInfC{$!A(t_2)$}
  26. \DisplayProof
  27. \\[3ex]
  28. \AxiomC{$\eq[t_1][t_2]$}
  29. \AxiomC{$!A(t_2)$}
  30. \RightLabel{\Elim{\eq}}
  31. \BinaryInfC{$!A(t_1)$}
  32. \DisplayProof
  33. \end{tabular}
  34. \end{defish}
  36. In the above rules, $t$, $t_1$, and $t_2$ are closed terms. The
  37. \Intro{\eq} rule allows us to !!{derive} any identity statement of the
  38. form $\eq[t][t]$ outright, from no assumptions.
  40. \begin{ex}
  41. If $s$ and $t$ are closed terms, then $!A(s), \eq[s][t] \Proves !A(t)$:
  42. \begin{prooftree}
  43. \AxiomC{$\eq[s][t]$}
  44. \AxiomC{$!A(s)$}
  45. \RightLabel{$\Elim{\eq}$}
  46. \BinaryInfC{$!A(t)$}
  47. \end{prooftree}
  48. This may be familiar as the ``principle of substitutability of
  49. identicals,'' or Leibniz' Law.
  50. \end{ex}
  52. \begin{prob}
  53. Prove that $=$ is both symmetric and transitive, i.e., give
  54. !!{derivation}s of $\lforall[x][\lforall[y][(\eq[x][y] \lif
  55. \eq[y][x])]]$ and $\lforall[x][\lforall[y][\lforall[z]((\eq[x][y]
  56. \land \eq[y][z]) \lif \eq[x][z])]]$
  57. \end{prob}
  59. \begin{ex}
  60. We !!{derive} the !!{sentence}
  61. \begin{align*}
  62. & \lforall[x][\lforall[y][((!A(x) \land !A(y)) \lif \eq[x][y])]]
  63. \intertext{from the !!{sentence}}
  64. & \lexists[x][\lforall[y][(!A(y) \lif \eq[y][x])]]
  65. \end{align*}
  66. We develop the !!{derivation} backwards:
  67. \begin{prooftree}
  68. \AxiomC{$\lexists[x][\lforall[y][(!A(y) \lif \eq[y][x])]]
  69. \quad \Discharge{!A(a) \land !A(b)}{1}$}
  70. \DeduceC{$\eq[a][b]$}
  71. \DischargeRule{\Intro{\lif}}{1}
  72. \UnaryInfC{$((!A(a) \land !A(b)) \lif \eq[a][b])$}
  73. \RightLabel{\Intro{\lforall}}
  74. \UnaryInfC{$\lforall[y][((!A(a) \land !A(y)) \lif \eq[a][y])]$}
  75. \RightLabel{\Intro{\lforall}}
  76. \UnaryInfC{$\lforall[x][\lforall[y][((!A(x) \land !A(y)) \lif \eq[x][y])]]$}
  77. \end{prooftree}
  78. We'll now have to use the main assumption: since it is an existential
  79. !!{formula}, we use \Elim{\lexists} to !!{derive} the intermediary
  80. conclusion $\eq[a][b]$.
  81. \begin{prooftree}
  82. \AxiomC{$\lexists[x][\lforall[y][(!A(y) \lif \eq[y][x])]]$}
  83. \AxiomC{$\Discharge{\lforall[y][(!A(y) \lif \eq[y][c]])}{2}$}
  84. \noLine
  85. \UnaryInfC{$\Discharge{!A(a) \land !A(b)}{1}$}
  86. \DeduceC{$\eq[a][b]$}
  87. \DischargeRule{\Elim{\lexists}}{2}
  88. \BinaryInfC{$\eq[a][b]$}
  89. \DischargeRule{\Intro{\lif}}{1}
  90. \UnaryInfC{$((!A(a) \land !A(b)) \lif \eq[a][b])$}
  91. \RightLabel{\Intro{\lforall}}
  92. \UnaryInfC{$\lforall[y][((!A(a) \land !A(y)) \lif \eq[a][y])]$}
  93. \RightLabel{\Intro{\lforall}}
  94. \UnaryInfC{$\lforall[x][\lforall[y][((!A(x) \land !A(y)) \lif \eq[x][y])]]$}
  95. \end{prooftree}
  96. The sub-!!{derivation} on the top right is completed by using its
  97. assumptions to show that $\eq[a][c]$ and $\eq[b][c]$. This requires two
  98. separate !!{derivation}s. The !!{derivation} for $\eq[a][c]$ is as
  99. follows:
  100. \begin{prooftree}
  101. \AxiomC{$\Discharge{\lforall[y][(!A(y) \lif \eq[y][c]])}{2}$}
  102. \RightLabel{\Elim{\lforall}}
  103. \UnaryInfC{$!A(a) \lif \eq[a][c]$}
  104. \AxiomC{$\Discharge{!A(a) \land !A(b)}{1}$}
  105. \RightLabel{\Elim{\land}}
  106. \UnaryInfC{$!A(a)$}
  107. \RightLabel{\Elim{\lif}}
  108. \BinaryInfC{$\eq[a][c]$}
  109. \end{prooftree}
  110. From $\eq[a][c]$ and $\eq[b][c]$ we !!{derive} $\eq[a][b]$ by
  111. \Elim{\eq}.
  112. \end{ex}
  114. \begin{prob}
  115. Give !!{derivation}s of the following !!{formula}s:
  116. \begin{enumerate}
  117. \item $\lforall[x][\lforall[y][((\eq[x][y] \land !A(x)) \lif !A(y))]]$
  118. \item $\lexists[x][!A(x)] \land \lforall[y][\lforall[z][((!A(y) \land
  119. !A(z)) \lif \eq[y][z])]] \lif \lexists[x][(!A(x) \land
  120. \lforall[y][(!A(y) \lif \eq[y][x])])]$
  121. \end{enumerate}
  122. \end{prob}
  124. \end{document}

content/first-order-logic/natural-deduction/soundness-identity.tex

47 lines; SHA-256 2544f37fa6d7a3d81b12c7e7309e1416680df9ee0d8d4e033084299370da0bc8. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: natural-deduction
  3. % Section: soundness-identity
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \olfileid{fol}{ntd}{sid}
  11. \olsection{Soundness with \usetoken{S}{identity}}
  13. \begin{prop}
  14. Natural deduction with rules for $\eq$ is sound.
  15. \end{prop}
  17. \begin{proof}
  18. Any !!{formula} of the form $\eq[t][t]$ is valid, since
  19. for every !!{structure}~$\Struct M$, $\Sat{M}{\eq[t][t]}$. (Note that
  20. we assume the term $t$ to be closed, i.e., it contains no variables,
  21. so variable assignments are irrelevant).
  23. Suppose the last inference in !!a{derivation} is \Elim{\eq}, i.e., the
  24. !!{derivation} has the following form:
  25. \begin{prooftree}
  26. \AxiomC{$\Gamma_1$}
  27. \RightLabel{$\delta_1$}
  28. \DeduceC{$\eq[t_1][t_2]$}
  29. \AxiomC{$\Gamma_2$}
  30. \RightLabel{$\delta_2$}
  31. \DeduceC{$!A(t_1)$}
  32. \RightLabel{\Elim{\eq}}
  33. \BinaryInfC{$!A(t_2)$}
  34. \end{prooftree}
  35. The premises $\eq[t_1][t_2]$ and $!A(t_1)$ are !!{derive}d from
  36. !!{undischarged} assumptions~$\Gamma_1$ and $\Gamma_2$, respectively.
  37. We want to show that $!A(t_2)$ follows from $\Gamma_1 \cup \Gamma_2$.
  38. Consider !!a{structure}~$\Struct{M}$ with $\Sat{M}{\Gamma_1 \cup
  39. \Gamma_2}$. By induction hypothesis, $\Sat{M}{!A(t_1)}$ and
  40. $\Sat{M}{\eq[t_1][t_2]}$. Therefore, $\Value{t_1}{M} = \Value{t_2}{M}$. Let
  41. $s$ be any variable assignment, and $m = \Value{t_1}{M} = \Value{t_2}{M}$. By
  42. \olref[fol][syn][ext]{prop:ext-formulas}, $\Sat{M}{!A(t_1)}[s]$ iff
  43. $\Sat{M}{!A(x)}[\Subst{s}{m}{x}]$ iff $\Sat{M}{!A(t_2)}[s]$. Since
  44. $\Sat{M}{!A(t_1)}$, we have $\Sat{M}{!A(t_2)}$.
  45. \end{proof}
  47. \end{document}