System L

System L is a natural deductive logic developed by E.J. Lemmon.[1] Derived from Suppes' method,[2] it represents natural deduction proofs as sequences of justified steps. Both methods are derived from Gentzen's 1934/1935 natural deduction system,[3] in which proofs were presented in tree-diagram form rather than in the tabular form of Suppes and Lemmon. Although the tree-diagram layout has advantages for philosophical and educational purposes, the tabular layout is much more convenient for practical applications.

A similar tabular layout is presented by Kleene.[4] The main difference is that Kleene does not abbreviate the left-hand sides of assertions to line numbers, preferring instead to either give full lists of precedent propositions or alternatively indicate the left-hand sides by bars running down the left of the table to indicate dependencies. However, Kleene's version has the advantage that it is presented, although only very sketchily, within a rigorous framework of metamathematical theory, whereas the books by Suppes[2] and Lemmon[1] are applications of the tabular layout for teaching introductory logic.

Description of the deductive system

The syntax of proof is governed by nine primitive rules:

  1. The Rule of Assumption (A)
  2. Modus Ponendo Ponens (MPP)
  3. The Rule of Double Negation (DN)
  4. The Rule of Conditional Proof (CP)
  5. The Rule of ∧-introduction (∧I)
  6. The Rule of ∧-elimination (∧E)
  7. The Rule of ∨-introduction (∨I)
  8. The Rule of ∨-elimination (∨E)
  9. Reductio Ad Absurdum (RAA)

In system L, a proof has a definition with the following conditions:

  1. has a finite sequence of well-formed formulas (or wffs)
  2. each line of it is justified by a rule of the system L
  3. the last line of the proof is what is intended, and this last line of the proof uses only the premises that were given, if any.

If no premise is given, the sequent is called a theorem. Therefore, the definition of a theorem in system L is:

  • a theorem is a sequent that can be proved in system L, using an empty set of assumptions.

Examples

An example of the proof of a sequent (Modus Tollendo Tollens in this case):

p → q, ¬q ⊢ ¬p [Modus Tollendo Tollens (MTT)]
Assumption number Line number Formula (wff) Lines in-use and Justification
1 (1) (p → q) A
2 (2) ¬q A
3 (3) p A (for RAA)
1, 3 (4) q 1, 3, MPP
1, 2, 3 (5) q ∧ ¬q 2, 4, ∧I
1, 2 (6) ¬p 3, 5, RAA
Q.E.D

An example of the proof of a sequent (a theorem in this case):

⊢p ∨ ¬p
Assumption number Line number Formula (wff) Lines in-use and Justification
1 (1) ¬(p ∨ ¬p) A (for RAA)
2 (2) p A (for RAA)
2 (3) (p ∨ ¬p) 2, ∨I
1, 2 (4) (p ∨ ¬p) ∧ ¬(p ∨ ¬p) 3, 1, ∧I
1 (5) ¬p 2, 4, RAA
1 (6) (p ∨ ¬p) 5, ∨I
1 (7) (p ∨ ¬p) ∧ ¬(p ∨ ¬p) 1, 6, ∧I
(8) ¬¬(p ∨ ¬p) 1, 7, RAA
(9) (p ∨ ¬p) 8, DN
Q.E.D

Each rule of system L has its own requirements for the type of input(s) or entry(es) that it can accept and has its own way of treating and calculating the assumptions used by its inputs.

History of tabular natural deduction systems

The historical development of tabular-layout natural deduction systems, which are rule-based, and which indicate antecedent propositions by line numbers (and related methods such as vertical bars or asterisks) includes the following publications.

  • 1940: In a textbook, Quine[5] indicated antecedent dependencies by line numbers in square brackets, anticipating Suppes' 1957 line-number notation.
  • 1950: In a textbook, Quine (1982, pp. 241–255) demonstrated a method of using one or more asterisks to the left of each line of proof to indicate dependencies. This is equivalent to Kleene's vertical bars. (It is not totally clear if Quine's asterisk notation appeared in the original 1950 edition or was added in a later edition.)
  • 1957: An introduction to practical logic theorem proving in a textbook by Suppes (1999, pp. 25–150). This indicated dependencies (i.e. antecedent propositions) by line numbers at the left of each line.
  • 1963: Stoll (1979, pp. 183–190, 215–219) uses sets of line numbers to indicate antecedent dependencies of the lines of sequential logical arguments based on natural deduction inference rules.
  • 1965: The entire textbook by Lemmon (1965) is an introduction to logic proofs using a method based on that of Suppes.
  • 1967: In a textbook, Kleene (2002, pp. 50–58, 128–130) briefly demonstrated two kinds of practical logic proofs, one system using explicit quotations of antecedent propositions on the left of each line, the other system using vertical bar-lines on the left to indicate dependencies.[6]
gollark: CCCloud Autoscaling™ will, if one computer hits a "too long without yielding" issue, spawn a new computer with exactly the same filesystem and randomly connect you to one of them when you use it.
gollark: There would be another bit for managing your "VMs", doing entirely pointless autoscaling and whatnot.
gollark: That would save a lot of programming, mean I wouldn't have to work around the nonexistent support for that one feature my canvas code needs, *and* involve more cloud.
gollark: Great idea, my "cloud platform" can just use Cloud Catcher for the UI!
gollark: The idea is for this thing to stream TRoR to/from a headless CCEmuX (ideally CraftOS-PC eventually) instance to either a browser or ingame computers, possibly with extensions for local peripheral control and stuff.

See also

Notes
  1. See Lemmon 1965 for an introductory presentation of Lemmon's natural deduction system.
  2. See Suppes 1999, pp. 25–150, for an introductory presentation of Suppes' natural deduction system.
  3. Gentzen 1934, Gentzen 1935.
  4. Kleene 2002, pp. 50–56, 128–130.
  5. Quine (1981). See particularly pages 91–93 for Quine's line-number notation for antecedent dependencies.
  6. A particular advantage of Kleene's tabular natural deduction systems is that he proves the validity of the inference rules for both propositional calculus and predicate calculus. See Kleene 2002, pp. 44–45, 118–119.

References
  • Gentzen, Gerhard Karl Erich (1934). "Untersuchungen über das logische Schließen. I". Mathematische Zeitschrift. 39 (2): 176–210. doi:10.1007/BF01201353.CS1 maint: ref=harv (link) (English translation Investigations into Logical Deduction in Szabo.)
  • Gentzen, Gerhard Karl Erich (1935). "Untersuchungen über das logische Schließen. II". Mathematische Zeitschrift. 39 (3): 405–431. doi:10.1007/bf01201363.CS1 maint: ref=harv (link)
  • Kleene, Stephen Cole (2002) [1967]. Mathematical logic. Mineola, New York: Dover Publications. ISBN 978-0-486-42533-7.CS1 maint: ref=harv (link)
  • Lemmon, Edward John (1965). Beginning logic. Thomas Nelson. ISBN 0-17-712040-1.CS1 maint: ref=harv (link)
  • Quine, Willard Van Orman (1981) [1940]. Mathematical logic (Revised ed.). Cambridge, Massachusetts: Harvard University Press. ISBN 978-0-674-55451-1.CS1 maint: ref=harv (link)
  • Quine, Willard Van Orman (1982) [1950]. Methods of logic (Fourth ed.). Cambridge, Massachusetts: Harvard University Press. ISBN 978-0-674-57176-1.CS1 maint: ref=harv (link)
  • Stoll, Robert Roth (1979) [1963]. Set Theory and Logic. Mineola, New York: Dover Publications. ISBN 978-0-486-63829-4.CS1 maint: ref=harv (link)
  • Suppes, Patrick Colonel (1999) [1957]. Introduction to logic. Mineola, New York: Dover Publications. ISBN 978-0-486-40687-9.CS1 maint: ref=harv (link)
  • Szabo, M.E. (1969). The collected papers of Gerhard Gentzen. Amsterdam: North-Holland.CS1 maint: ref=harv (link)
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.