The Open Logic Text — accessible offline edition

Derivation Systems — Source and provenance

Derivation Systems

Source and provenance

All six authority files and all 461 lines are shown exactly and packaged byte-for-byte. These files are shared with the earlier propositional profile; this route binds the canonical First-order tag state and FOL semantic meanings. The spelling correction and source-label disclosure affect reader presentation only; source bytes and the projected transcript remain unchanged. Open the exact accepted projected chapter transcript (SHA-256 ba553e37375752c5db946151d8873c36f0cf65118f5beec33a1925c013288d7e). AI production model: OpenAI Codex gpt-5.6-sol, Ultra. Source authorship remains with the credited Open Logic Project contributors.

content/first-order-logic/proof-systems/proof-systems.tex

31 lines; SHA-256 85b8a0fca16c329ad16b3c17975735c159e0cf9d38e8dfc7501acba84171fb6c. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: proof-systems
  4. \documentclass[../../../include/open-logic-chapter]{subfiles}
  6. \begin{document}
  8. \iftag{FOL}
  9. {\olchapter{fol}{prf}{\usetoken{S}{derivation} Systems}}
  10. {\olchapter{pl}{prf}{\usetoken{S}{derivation} Systems}}
  12. \begin{editorial}
  13. This chapter collects general material on !!{derivation} systems. A
  14. textbook using a specific system can insert the introduction section
  15. plus the relevant survey section at the beginning of the chapter
  16. introducing that system.
  17. \end{editorial}
  19. \olimport{introduction}
  21. \olimport{sequent-calculus}
  23. \olimport{natural-deduction}
  25. \olimport{tableaux}
  27. \olimport{axiomatic-deduction}
  29. \OLEndChapterHook
  31. \end{document}

content/first-order-logic/proof-systems/introduction.tex

101 lines; SHA-256 5172343625a0d66971257858a1a6e359805ffeec979bd5afdc0377864799a756. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: proof-systems
  3. % Section: introduction
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{prf}{int}}
  11. {\olfileid{pl}{prf}{int}}
  13. \olsection{Introduction}
  15. Logics commonly have both a semantics and !!a{derivation}
  16. system. The semantics concerns concepts such as truth, satisfiability,
  17. validity, and entailment. The purpose of !!{derivation} systems is to
  18. provide a purely syntactic method of establishing entailment and
  19. validity. They are purely syntactic in the sense that a
  20. !!{derivation} in such a system is a finite syntactic object, usually
  21. a sequence (or other finite arrangement) of !!{sentence}s or
  22. !!{formula}s. Good !!{derivation} systems have the property that any
  23. given sequence or arrangement of !!{sentence}s or !!{formula}s can be
  24. verified mechanically to be ``correct.''
  26. The simplest (and historically first) !!{derivation} systems for
  27. first-order logic were \emph{axiomatic}. A sequence of !!{formula}s
  28. counts as !!a{derivation} in such a system if each individual
  29. !!{formula} in it is either among a fixed set of ``axioms'' or follows
  30. from !!{formula}s coming before it in the sequence by one of a fixed
  31. number of ``inference rules''---and it can be mechanically verified if
  32. !!a{formula} is an axiom and whether it follows correctly from other
  33. !!{formula}s by one of the inference rules. Axiomatic !!{derivation}
  34. systems are easy to describe---and also easy to handle
  35. meta-theoretically---but !!{derivation}s in them are hard to read and
  36. understand, and are also hard to produce.
  38. Other !!{derivation} systems have been developed with the aim of
  39. making it easier to construct !!{derivation}s or easier to understand
  40. !!{derivation}s once they are complete. Examples are natural
  41. deduction, truth trees, also known as tableaux proofs, and the sequent
  42. calculus. Some !!{derivation} systems are designed especially with
  43. mechanization in mind, e.g., the resolution method is easy to
  44. implement in software (but its !!{derivation}s are essentially
  45. impossible to understand). Most of these other !!{derivation} systems
  46. represent !!{derivation}s as trees of !!{formula}s rather than
  47. sequences. This makes it easier to see which parts of !!a{derivation}
  48. depend on which other parts.
  50. So for a given logic, such as first-order logic, the different
  51. !!{derivation} systems will give different explications of what it is
  52. for !!a{sentence} to be a \emph{theorem} and what it means for
  53. !!a{sentence} to be !!{derivable} from some others. However that is
  54. done (via axiomatic !!{derivation}s, natural deductions, sequent
  55. !!{derivation}s, truth trees, resolution refutations), we want these
  56. relations to match the semantic notions of validity and
  57. entailment. Let's write $\Proves !A$ for ``$!A$~is a theorem'' and
  58. ``$\Gamma \Proves !A$'' for ``$!A$~is !!{derivable} from~$\Gamma$.''
  59. However $\Proves$~is defined, we want it to match up with $\Entails$,
  60. that is:
  61. \begin{enumerate}
  62. \item $\Proves !A$ if and only if $\Entails !A$
  63. \item $\Gamma \Proves !A$ if and only if $\Gamma \Entails !A$
  64. \end{enumerate}
  65. The ``only if'' direction of the above is called
  66. \emph{soundness}. !!^a{derivation} system is sound if !!{derivability}
  67. guarantees entailment (or validity). Every decent !!{derivation}
  68. system has to be sound; unsound !!{derivation} systems are not useful
  69. at all. After all, the entire purpose of !!a{derivation} is to provide
  70. a syntactic guarantee of validity or entailment. We'll prove soundness
  71. for the !!{derivation} systems we present.
  73. The converse ``if'' direction is also important: it is called
  74. \emph{completeness}. A complete !!{derivation} system is strong enough
  75. to show that $!A$~is a theorem whenever $!A$~is valid, and that
  76. $\Gamma \Proves !A$ whenever $\Gamma \Entails !A$.
  77. Completeness is harder to establish, and some logics have no complete
  78. !!{derivation} systems. First-order logic does. Kurt G\"odel was the
  79. first one to prove completeness for !!a{derivation} system of
  80. first-order logic in his 1929 dissertation.
  82. Another concept that is connected to !!{derivation} systems is that of
  83. \emph{consistency}. A set of !!{sentence}s is called inconsistent if
  84. anything whatsoever can be !!{derive}d from it, and consistent
  85. otherwise. Inconsistency is the syntactic counterpart to
  86. unsatisfiablity: like unsatisfiable sets, inconsistent sets of
  87. !!{sentence}s do not make good theories, they are defective in a
  88. fundamental way. Consistent sets of !!{sentence}s may not be true or
  89. useful, but at least they pass that minimal threshold of logical
  90. usefulness. For different !!{derivation} systems the specific
  91. definition of consistency of sets of !!{sentence}s might differ, but
  92. like~$\Proves$, we want consistency to coincide with its semantic
  93. counterpart, satisfiability. We want it to always be the case that
  94. $\Gamma$ is consistent if and only if it is satisfiable. Here, the
  95. ``only if'' direction amounts to completeness (consistency guarantees
  96. satisfiability), and the ``if'' direction amounts to soundness
  97. (satisfiability guarantees consistency). In fact, for classical
  98. first-order logic, the two versions of soundness and completeness are
  99. equivalent.
  101. \end{document}

content/first-order-logic/proof-systems/sequent-calculus.tex

67 lines; SHA-256 9a847c7bd45afe0d177230807fb2ba9dda820b4c0551a9274002db8776182003. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: proof-systems
  3. % Section: seqeunt-calculus
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{prf}{seq}}
  11. {\olfileid{pl}{prf}{seq}}
  13. \olsection{The Sequent Calculus}
  15. While many !!{derivation} systems operate with arrangements of
  16. !!{sentence}s, the sequent calculus operates with \emph{sequents}. A
  17. sequent is an expression of the form
  18. \[
  19. !A_1, \dots, !A_m \Sequent !B_1, \dots, !B_m,
  20. \]
  21. that is a pair of sequences of !!{sentence}s, separated by the sequent
  22. symbol~$\Sequent$. Either sequence may be empty. !!^a{derivation} in
  23. the sequent calculus is a tree of sequents, where the topmost sequents
  24. are of a special form (they are called ``initial sequents'' or
  25. ``axioms'') and every other sequent follows from the sequents
  26. immediately above it by one of the rules of inference. The rules of
  27. inference either manipulate the !!{sentence}s in the sequents (adding,
  28. removing, or rearranging them on either the left or the right), or
  29. they introduce a complex !!{formula} in the conclusion of the rule.
  30. For instance, the $\LeftR{\land}$ rule allows the inference from $!A,
  31. \Gamma \Sequent \Delta$ to $!A \land !B, \Gamma \Sequent \Delta$, and
  32. the $\RightR{\lif}$ allows the inference from $!A, \Gamma \Sequent
  33. \Delta, !B$ to $\Gamma \Sequent \Delta, !A \lif !B$, for any $\Gamma$,
  34. $\Delta$, $!A$, and~$!B$. (In particular, $\Gamma$ and~$\Delta$ may be
  35. empty.)
  37. The $\Proves$ relation based on the sequent calculus is defined as
  38. follows: $\Gamma \Proves !A$ iff there is some sequence $\Gamma_0$
  39. such that every $!A$ in $\Gamma_0$ is in~$\Gamma$ and there is a
  40. !!{derivation} with the sequent~$\Gamma_0 \Sequent !A$ at its root.
  41. $!A$ is a theorem in the sequent calculus if the sequent~$\Sequent !A$
  42. has !!a{derivation}. For instance, here is !!a{derivation} that shows
  43. that $\Proves (!A \land !B) \lif !A$:
  44. \begin{prooftree}
  45. \Axiom$!A \fCenter !A$
  46. \RightLabel{\LeftR{\land}}
  47. \UnaryInf$!A \land !B \fCenter !A$
  48. \RightLabel{\RightR{\lif}}
  49. \UnaryInf$\fCenter (!A \land !B) \lif !A$
  50. \end{prooftree}
  52. A set $\Gamma$ is inconsistent in the sequent calculus if there is
  53. !!a{derivation} of $\Gamma_0 \Sequent$ (where every $!A \in \Gamma_0$
  54. is in~$\Gamma$ and the right side of the sequent is empty). Using the
  55. rule \RightR{\Weakening}, any !!{sentence} can be !!{derive}d from an
  56. inconsistent set.
  58. The sequent calculus was invented in the 1930s by Gerhard Gentzen.
  59. Because of its systematic and symmetric design, it is a very useful
  60. formalism for developing a theory of !!{derivation}s. It is relatively
  61. easy to find !!{derivation}s in the sequent calculus, but these
  62. !!{derivation}s are often hard to read and their connection to proofs
  63. are sometimes not easy to see. It has proved to be a very elegant
  64. approach to !!{derivation} systems, however, and many logics have
  65. sequent calculus systems.
  67. \end{document}

content/first-order-logic/proof-systems/natural-deduction.tex

90 lines; SHA-256 c203daa5161eed34188e9fb9022b83be4f0201904f31cef386c5b838fb9e7d49. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: proof-systems
  3. % Section: natural-deduction
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{prf}{ntd}}
  11. {\olfileid{pl}{prf}{ntd}}
  13. \olsection{Natural Deduction}
  15. Natural deduction is !!a{derivation} system intended to mirror actual
  16. reasoning (especially the kind of regimented reasoning employed by
  17. mathematicians). Actual reasoning proceeds by a number of ``natural''
  18. patterns. For instance, proof by cases allows us to establish a
  19. conclusion on the basis of a disjunctive premise, by establishing that
  20. the conclusion follows from either of the disjuncts. Indirect proof
  21. allows us to establish a conclusion by showing that its negation leads
  22. to a contradiction. Conditional proof establishes a conditional claim
  23. ``if \dots then \dots'' by showing that the consequent follows from
  24. the antecedent. Natural deduction is a formalization of some of these
  25. natural inferences. Each of the logical connectives and quantifiers
  26. comes with two rules, an introduction and an elimination rule, and
  27. they each correspond to one such natural inference pattern. For
  28. instance, $\Intro{\lif}$ corresponds to conditional proof, and
  29. $\Elim{\lor}$ to proof by cases. A particularly simple rule is
  30. $\Elim{\land}$ which allows the inference from $!A \land !B$ to~$!A$
  31. (or $!B$).
  33. One feature that distinguishes natural deduction from other
  34. !!{derivation} systems is its use of assumptions. !!^a{derivation} in
  35. natural deduction is a tree of !!{formula}s. A single !!{formula}
  36. stands at the root of the tree of !!{formula}s, and the ``leaves'' of
  37. the tree are !!{formula}s from which the conclusion is derived. In
  38. natural deduction, some leaf !!{formula}s play a role inside the
  39. !!{derivation} but are ``used up'' by the time the !!{derivation}
  40. reaches the conclusion. This corresponds to the practice, in actual
  41. reasoning, of introducing hypotheses which only remain in effect for a
  42. short while. For instance, in a proof by cases, we assume the truth
  43. of each of the disjuncts; in conditional proof, we assume the truth of
  44. the antecedent; in indirect proof, we assume the truth of the negation
  45. of the conclusion. This way of introducing hypothetical assumptions
  46. and then doing away with them in the service of establishing an
  47. intermediate step is a hallmark of natural deduction. The formulas at
  48. the leaves of a natural deduction !!{derivation} are called
  49. assumptions, and some of the rules of inference may ``!!{discharge}''
  50. them. For instance, if we have !!a{derivation} of~$!B$ from some
  51. assumptions which include~$!A$, then the $\Intro{\lif}$ rule allows us
  52. to infer~$!A \lif !B$ and discharge any assumption of the form~$!A$.
  53. (To keep track of which assumptions are discharged at which
  54. inferences, we label the inference and the assumptions it discharges
  55. with a number.) The assumptions that remain !!{undischarged} at the
  56. end of the !!{derivation} are together sufficient for the truth of the
  57. conclusion, and so !!a{derivation} establishes that its
  58. !!{undischarged} assumptions entail its conclusion.
  60. The relation $\Gamma \Proves !A$ based on natural deduction holds iff
  61. there is !!a{derivation} in which $!A$~is the last !!{sentence} in the
  62. tree, and every leaf which is !!{undischarged} is in~$\Gamma$. $!A$~is
  63. a theorem in natural deduction iff there is !!a{derivation} in which
  64. $!A$~is the last !!{sentence} and all assumptions are !!{discharged}.
  65. For instance, here is !!a{derivation} that shows that $\Proves (!A
  66. \land !B) \lif !A$:
  67. \begin{prooftree}
  68. \AxiomC{$\Discharge{!A \land !B}{1}$}
  69. \RightLabel{\Elim{\land}}
  70. \UnaryInfC{$!A$}
  71. \DischargeRule{\Intro{\lif}}{1}
  72. \UnaryInfC{$(!A \land !B) \lif !A$}
  73. \end{prooftree}
  74. The label~$1$ indicates that the assumption $!A \land !B$ is
  75. !!{discharged} at the \Intro{\lif} inference.
  77. A set~$\Gamma$ is inconsistent iff $\Gamma \Proves \lfalse$ in natural
  78. deduction. The rule \FalseInt{} makes it so that from an inconsistent
  79. set, any !!{sentence} can be !!{derive}d.
  81. Natural deduction systems were developed by Gerhard Gentzen and
  82. Stanis\l{}aw Ja\'skowski in the 1930s, and later developed by Dag
  83. Prawitz and Frederic Fitch. Because its inferences mirror natural
  84. methods of proof, it is favored by philosophers. The versions
  85. developed by Fitch are often used in introductory logic textbooks. In
  86. the philosophy of logic, the rules of natural deduction have sometimes
  87. been taken to give the meanings of the logical operators
  88. (``proof-theoretic semantics'').
  90. \end{document}

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

89 lines; SHA-256 6abf691f97c618dd41bc0c30a21dcf74fa7025228aa378cfd9f0369a898c2966. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: proof-systems
  3. % Section: tableaux
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{prf}{tab}}
  11. {\olfileid{pl}{prf}{tab}}
  13. \olsection{\usetoken{P}{tableau}}
  15. While many !!{derivation} systems operate with arrangements of
  16. !!{sentence}s, !!{tableau}s operate with !!{signed formula}s.
  17. !!^a{signed formula} is a pair consisting of a truth value sign
  18. ($\True$ or $\False$) and !!a{sentence}
  19. \[
  20. \sFmla{\True}{!A} \text{ or } \sFmla{\False}{!A}.
  21. \]
  22. !!^a{tableau} consists of !!{signed formula}s arranged in a
  23. downward-branching tree. It begins with a number of \emph{assumptions}
  24. and continues with !!{signed formula}s which result from one of the
  25. !!{signed formula}s above it by applying one of the rules of
  26. inference. Each rule allows us to add one or more !!{signed formula}s
  27. to the end of a branch, or two !!{signed formula}s side by side---in
  28. this case a branch splits into two, with the two added !!{signed
  29. formula}s forming the ends of the two branches.
  31. A rule applied to a complex !!{signed formula} results in the addition
  32. of !!{signed formula}s which are immediate sub-!!{formula}s. They come
  33. in pairs, one rule for each of the two signs. For instance, the
  34. $\TRule{\True}{\land}$ rule applies to $\sFmla{\True}{!A \land !B}$,
  35. and allows the addition of both the two !!{signed formula}s
  36. $\sFmla{\True}{!A}$ and~$\sFmla{\True}{!B}$ to the end of any branch
  37. containing $\sFmla{\True}{!A \land !B}$, and the rule
  38. $\TRule{\False}{!A \land !B}$ allows a branch to be split by adding
  39. $\sFmla{\False}{!A}$ and $\sFmla{\False}{!B}$ side-by-side.
  40. !!^a{tableau} is closed if every one of its branches contains a
  41. matching pair of !!{signed formula}s $\sFmla{\True}{!A}$ and
  42. $\sFmla{\False}{!A}$.
  44. The $\Proves$ relation based on !!{tableau}s is defined as follows:
  45. $\Gamma \Proves !A$ iff there is some finite set~$\Gamma_0 = \{!B_1,
  46. \dots, !B_n\} \subseteq \Gamma$ such that there is a closed !!{tableau}
  47. for the assumptions
  48. \[
  49. \{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}
  50. \]
  51. For instance, here is a closed !!{tableau} that shows that $\Proves
  52. (!A \land !B) \lif !A$:
  53. \begin{oltableau}
  54. [\sFmla{\False}{(\formula{A} \land \formula{B}) \lif \formula{A}}, just = \TAss
  55. [\sFmla{\True}{\formula{A} \land \formula{B}}, just = {\TRule{\False}{\lif}[1]}
  56. [\sFmla{\False}{\formula{A}}, just = {\TRule{\False}{\lif}[1]}
  57. [\sFmla{\True}{\formula{A}}, just = {\TRule{\True}{\lif}[2]}
  58. [\sFmla{\True}{\formula{B}}, just = {\TRule{\True}{\lif}[2]}, close]
  59. ]
  60. ]
  61. ]
  62. ]
  63. \end{oltableau}
  65. A set $\Gamma$ is inconsistent in the !!{tableau} calculus if there is
  66. a closed !!{tableau} for assumptions
  67. \[
  68. \{\sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}
  69. \]
  70. for some $!B_i \in \Gamma$.
  72. !!^{tableau}s were invented in the 1950s independently by Evert
  73. Beth and Jaakko Hintikka, and simplified and popularized by Raymond
  74. Smullyan. They are very easy to use, since constructing !!a{tableau} is a
  75. very systematic procedure. Because of the systematic nature of
  76. !!{tableau}s, they also lend themselves to implementation by
  77. computer. However, !!a{tableau} is often hard to read and their
  78. connection to proofs are sometimes not easy to see. The approach is
  79. also quite general, and many different logics have !!{tableau}
  80. systems. !!^{tableau}s also help us to find !!{structure}s that
  81. satisfy given (sets of) !!{sentence}s: if the set is satisfiable, it
  82. won't have a closed !!{tableau}, i.e., any !!{tableau} will have an
  83. open branch. The satisfying !!{structure} can be ``read off'' an open
  84. branch, provided every rule it is possible to apply has been applied
  85. on that branch. There is also a very close connection to the sequent
  86. calculus: essentially, a closed !!{tableau} is a condensed
  87. !!{derivation} in the sequent calculus, written upside-down.
  89. \end{document}

content/first-order-logic/proof-systems/axiomatic-deduction.tex

83 lines; SHA-256 0269390efeb94a0522020ce00d45f1d1e752e4a32db564b7519d7a939fa13034. Open the byte-exact preserved source file.

  1. % Part: first-order-logic
  2. % Chapter: proof-systems
  3. % Section: axiomatic-deduction
  5. \documentclass[../../../include/open-logic-section]{subfiles}
  7. \begin{document}
  9. \iftag{FOL}
  10. {\olfileid{fol}{prf}{axd}}
  11. {\olfileid{pl}{prf}{axd}}
  13. \olsection{Axiomatic \usetoken{P}{derivation}}
  15. Axiomatic !!{derivation}s are the oldest and simplest logical
  16. !!{derivation} systems. Its !!{derivation}s are simply sequences of
  17. !!{sentence}s. A sequence of !!{sentence}s counts as a correct
  18. !!{derivation} if every !!{sentence}~$!A$ in it satisfies one of the
  19. following conditions:
  20. \begin{enumerate}
  21. \item $!A$ is an axiom, or
  22. \item $!A$ is !!a{element} of a given set~$\Gamma$ of !!{sentence}s, or
  23. \item $!A$ is justified by a rule of inference.
  24. \end{enumerate}
  25. To be an axiom, $!A$ has to have the form of one of a number of fixed
  26. !!{sentence} schemas. There are many sets of axiom schemas that
  27. provide a satisfactory (sound and complete) !!{derivation} system for
  28. first-order logic. Some are organized according to the connectives
  29. they govern, e.g., the schemas
  30. \[
  31. !A \lif (!B \lif !A) \qquad !B \lif (!B \lor !C) \qquad (!B \land !C) \lif !B
  32. \]
  33. are common axioms that govern $\lif$, $\lor$ and~$\land$. Some axiom systems
  34. aim at a minimal number of axioms. Depending on the connectives that
  35. are taken as primitives, it is even possible to find axiom systems
  36. that consist of a single axiom.
  38. A rule of inference is a conditional statement that gives a sufficient
  39. condition for !!a{sentence} in !!a{derivation} to be justified. Modus
  40. ponens is one very common such rule: it says that if $!A$ and $!A \lif
  41. !B$ are already justified, then $!B$ is justified. This means that a
  42. line in !!a{derivation} containing the !!{sentence}~$!B$ is justified,
  43. provided that both $!A$ and $!A \lif !B$ (for some !!{sentence}~$!A$)
  44. appear in the !!{derivation} before~$!B$.
  46. The $\Proves$ relation based on axiomatic !!{derivation}s is defined
  47. as follows: $\Gamma \Proves !A$ iff there is !!a{derivation} with the
  48. !!{sentence}~$!A$ as its last formula (and $\Gamma$ is taken as the
  49. set of !!{sentence}s in that !!{derivation} which are justified by~(2) above). $!A$
  50. is a theorem if~$!A$ has !!a{derivation} where~$\Gamma$ is empty,
  51. i.e., every !!{sentence} in the !!{derivation} is justified either by (1)
  52. or~(3). For instance, here is !!a{derivation} that shows that $\Proves
  53. !A \lif (!B \lif (!B \lor !A))$:
  54. \begin{derivation}
  55. 1. & $!B \lif (!B \lor !A)$ \\
  56. 2. & $(!B \lif (!B \lor !A)) \lif (!A \lif (!B \lif (!B \lor !A)))$\\
  57. 3. & $!A \lif (!B \lif (!B \lor !A))$
  58. \end{derivation}
  59. The !!{sentence} on line~1 is of the form of the axiom $!A \lif (!A
  60. \lor !B)$ (with the roles of $!A$ and $!B$ reversed). The sentence on
  61. line~2 is of the form of the axiom $!A \lif (!B \lif !A)$. Thus, both
  62. lines are justified. Line~3 is justified by modus ponens: if we
  63. abbreviate it as $!D$, then line~2 has the form $!C \lif !D$, where
  64. $!C$ is $!B \lif (!B \lor !A)$, i.e., line~1.
  66. A set $\Gamma$ is inconsistent if $\Gamma \Proves \lfalse$. A complete
  67. axiom system will also prove that $\lfalse \lif !A$ for any~$!A$, and
  68. so if $\Gamma$ is inconsistent, then $\Gamma \Proves !A$ for any~$!A$.
  70. Systems of axiomatic !!{derivation}s for logic were first given by
  71. Gottlob Frege in his 1879 \emph{Begriffsschrift}, which for this
  72. reason is often considered the first work of modern logic. They were
  73. perfected in Alfred North Whitehead and Bertrand Russell's
  74. \emph{Principia Mathematica} and by David Hilbert and his students in
  75. the 1920s. They are thus often called ``Frege systems'' or ``Hilbert
  76. systems.'' They are very versatile in that it is often easy to find
  77. an axiomatic system for a logic. Because !!{derivation}s have a very
  78. simple structure and only one or two inference rules, it is also
  79. relatively easy to prove things \emph{about} them. However, they are
  80. very hard to use in practice, i.e., it is difficult to find and write
  81. proofs.
  83. \end{document}