System L is a natural deductive logic developed by E.J. Lemmon. Derived from Suppes' method, it represents natural deduction proofs as sequences of justified steps. Both methods are derived from Gentzen's 1934/1935 natural deduction system, 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. 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 and Lemmon are applications of the tabular layout for teaching introductory logic.
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 : An example of the proof of a sequent : Each rule of system L has its own requirements for the type of input or entry 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 includes the following publications.
1940: In a textbook, Quine indicated antecedent dependencies by line numbers in square brackets, anticipating Suppes' 1957 line-number notation.
1950: In a textbook, 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.
1957: An introduction to practical logic theorem proving in a textbook by. This indicated dependencies by line numbers at the left of each line.
1965: The entire textbook by is an introduction to logic proofs using a method based on that of Suppes.
1967: In a textbook, 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.
