Suppes–Lemmon notation is a natural deductive logic notation system developed by E.J. Lemmon. Derived from Suppes' method, it represents natural deduction proofs as sequences of justified steps. Both methods use inference rules 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.

Description of the deductive system

Suppes–Lemmon notation is a notation for predicate calculus with equality, so its description can be separated into two parts: the general proof syntax and the context specific rules.

General Proof Syntax

A proof is a table with 4 columns and unlimited ordered rows. From left to right the columns hold: The following is an example: The second column holds line numbers. The third holds a wff, which is justified by the rule held in the fourth along with auxiliary information about other wffs, possibly in other proofs. The first column represents the line numbers of the assumptions the wff rests on, determined by the application of the cited rule in context. Any line of any valid proof can be converted into a sequent by listing the wffs at the cited lines as the premises and the wff at the line as the conclusion. Analogously, they can be converted into conditionals where the antecedent is a conjunction. These sequents are often listed above the proof, as Modus Tollens is above.

Rules of Predicate Calculus with Equality

The above proof is a valid one, but proofs don't need to be to conform to the general syntax of the proof system. To guarantee a sequent's validity, however, we must conform to carefully specified rules. The rules can be divided into four groups: the propositional rules (1-10), the predicate rules (11-14), the rules of equality (15-16), and the rule of substitution (17). Adding these groups in order allows one to build a propositional calculus, then a predicate calculus, then a predicate calculus with equality, then a predicate calculus with equality allowing for the derivation of new rules. Some of the propositional calculus rules, like MTT, are superfluous and can be derived as rules from other rules. P → Q and P respectively, "a,b MPP" justifies Q. The assumptions are the collective pool of lines a and b.

Examples

An example of the proof of a sequent (a theorem in this case): A proof of the principle of explosion using monotonicity of entailment. Some have called the following technique, demonstrated in lines 3-6, the Rule of (Finite) Augmentation of Premises: An example of substitution and ∨E:

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.