Suppes–Lemmon notation

Suppes–Lemmon notation^[1] is a natural deductive logic notation system developed by E.J. Lemmon.^[2] Derived from Suppes' method,^[3] it represents natural deduction proofs as sequences of justified steps. Both methods use inference rules derived from Gentzen's 1934/1935 natural deduction system,^[4] 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.^[5] 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^[3] and Lemmon^[2] 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:

1. A set of positive integers, possibly empty
2. A positive integer
3. A well-formed formula (or wff)
4. A set of numbers, possibly empty; a rule; and possibly a reference to another proof

The following is an example:

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

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-11), the predicate rules (12-15), the rules of equality (15-16) and the rule of substitution (18). 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. In the table below, the derived propositional rules (10-11) are highlighted. They follow from the primitive (non-highlighted) Gentzen rules. The rules 8 (Double Negation Elimination) and 9 (Reductio Ad Absurdum) are equivalent. One of them can be dropped (or be assimilated to the derived rules).

List of Inference Rules

	Rule Name	Annotation	Description	Assumption
1	Assumptions	A	"A" justifies any wff. The only assumption is its own line number.	The only assumption is its own line number.
2	∧-introduction	a,b ∧I	If propositions ${\displaystyle P}$ and ${\displaystyle Q}$ are at lines a and b, "a,b ∧I" justifies ${\displaystyle P\wedge Q}$.	The assumptions are the collective pool of the conjoined propositions.
3	∧-elimination	a ∧E	If line a is a conjunction ${\displaystyle P\wedge Q}$, one can conclude either ${\displaystyle P}$ or ${\displaystyle Q}$ using "a ∧E". ∧I and ∧E allow for monotonicity of entailment, as when a proposition ${\displaystyle P}$ is joined with ${\displaystyle Q}$ with ∧I and separated with ∧E, it retains ${\displaystyle Q}$'s assumptions.	The assumptions are line a’s.
4	∨-introduction	a ∨I	For a line a with proposition ${\displaystyle P}$ one can introduce ${\displaystyle P\vee Q}$ citing "a ∨I".	The assumptions are a’s.
5	∨-elimination	a,b,c,d,e ∨E	For a disjunction ${\displaystyle P\vee Q}$, if one assumes ${\displaystyle P}$ and ${\displaystyle Q}$ and separately comes to the conclusion ${\displaystyle R}$ from each, then one can conclude ${\displaystyle R}$. The rule is cited as "a,b,c,d,e ∨E", where line a has the initial disjunction ${\displaystyle P\vee Q}$, lines b and d assume ${\displaystyle P}$ and ${\displaystyle Q}$ respectively, and lines c and e conclude ${\displaystyle R}$ with ${\displaystyle P}$ and ${\displaystyle Q}$ in their respective assumption pools.	The assumptions are the collective pools of the two lines concluding ${\displaystyle R}$, c and e, minus the lines assuming ${\displaystyle P}$ and ${\displaystyle Q}$, b and d.
6	Conditional Proof (→I)	b,a CP	If a line a with proposition ${\displaystyle P}$ has an assumption line b with proposition ${\displaystyle Q}$, "b,a CP" justifies ${\displaystyle Q\to P}$.	All of a’s assumptions aside b are kept.
7	Modus Ponendo Ponens (→E)	a,b MPP	If there are lines a and b previously in the proof containing ${\displaystyle P\to Q}$ and ${\displaystyle P}$ respectively, "a,b MPP" justifies ${\displaystyle Q}$.	The assumptions are the collective pool of lines a and b.
8	Double Negation (¬¬E)	a DN	"a DN" justifies adding or subtracting two negation symbols from the wff at a line a previously in the proof, making this rule a biconditional.	The assumption pool is the one of the line cited.
9	Reductio Ad Absurdum	b,a RAA	For a proposition ${\displaystyle P\wedge \neg P}$ on line a citing an assumption ${\displaystyle Q}$ on line b, one can cite "b,a RAA" and derive ${\displaystyle \neg Q}$ from the assumptions of line a aside from b.	The assumptions of line a aside from b.
10	Disjunctive Syllogism	a,b DS	The union of the assumption sets at lines a and b	From ${\displaystyle \varphi \lor \psi }$ at line a and ${\displaystyle \neg \varphi }$ at line b, infer ${\displaystyle \psi }$ From ${\displaystyle \varphi \lor \psi }$ at line a and ${\displaystyle \neg \psi }$ at line b, infer ${\displaystyle \varphi }$.
11	Modus Tollens	a,b MTT	For propositions ${\displaystyle P\to Q}$ and ${\displaystyle \neg Q}$ on lines a and b one can cite "a,b MTT" to derive ${\displaystyle \neg P}$. This is proven from other rules above.	The assumptions are those of lines a and b.
12	Universal Introduction	a UI	For a predicate ${\displaystyle Ra}$ on line a, one can cite "a UI" to justify a universal quantification, ${\displaystyle (\forall x)Rx}$, provided none of the assumptions on line a have the term ${\displaystyle a}$ anywhere.	The assumptions are those of line a.
13	Universal Elimination	a UE	For a universally quantified predicate ${\displaystyle (\forall x)Rx}$ on line a, one can cite "a UE" to justify ${\displaystyle Ra}$. UE is a duality with UI in that one can switch between quantified and free variables using these rules.	The assumptions are those of line a.
14	Existential Introduction	a EI	For a predicate ${\displaystyle Ra}$ on line a one can cite "a EI" to justify an existential quantification, ${\displaystyle (\exists x)Rx}$.	The assumptions are those of line a.
15	Existential Elimination	a,b,c EE	For an existentially quantified predicate ${\displaystyle (\exists x)Rx}$ on line a, if we assume ${\displaystyle Ra}$ to be true on line b and derive ${\displaystyle P}$ with it on line c, we can cite "a,b,c EE" to justify ${\displaystyle P}$. The term ${\displaystyle a}$ cannot appear in the conclusion ${\displaystyle P}$, any of its assumptions aside from line b, or on line a. EE and EI are in duality, as one can assume ${\displaystyle Ra}$ and use EI to reach a conclusion from ${\displaystyle (\exists x)Rx}$.	The assumptions are the assumptions on line a and any on line c aside from b.
16	Equality Introduction	=I	At any point one can introduce ${\displaystyle a=a}$ citing "=I" with no assumptions.	No assumptions.
17	Equality Elimination	a,b =E	For propositions ${\displaystyle a=b}$ and ${\displaystyle P}$ on lines a and b, one can cite "a,b =E" to justify changing any terms ${\displaystyle a}$ in ${\displaystyle P}$ to ${\displaystyle b}$.	The assumptions are the pool of lines a and b.
18	Substitution Instance	a,b SI(S) X	For a sequent ${\displaystyle P,Q\vdash R}$ proved in proof X and substitution instances of ${\displaystyle P}$ and ${\displaystyle Q}$ on lines a and b, one can cite "a,b SI(S) X" to justify introducing a substitution instance of ${\displaystyle R}$.	Assumptions of lines a and b.

The assumptions are those of lines a and b. A derived rule with no assumptions is a theorem, and can be introduced at any time with no assumptions. Some cite that as "TI(S)", for "theorem" instead of "sequent". Additionally, some cite only "SI" or "TI" in either case when a substitution instance isn't needed, as their propositions match the ones of the referenced proof exactly.

Examples

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

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:^[6]

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

An example of substitution and ∨E:

(p ∧ ¬p) ∨ (q ∧ ¬q) ⊢ r
Assumption number	Line number	Formula (wff)	Lines in-use and Justification
1	(1)	(p ∧ ¬p) ∨ (q ∧ ¬q)	A
2	(2)	p ∧ ¬p	A (for ∨E)
2	(3)	p	2 ∧E
2	(4)	¬p	2 ∧E
2	(5)	r	3, 4 SI(S) see above proof
6	(6)	q ∧ ¬q	A (for ∨E)
6	(7)	q	6 ∧E
6	(8)	¬q	2 ∧E
6	(9)	r	7, 8 SI(S) see above proof
1	(10)	r	1, 2, 5, 6, 9, ∨E
Q.E.D

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^[7] 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.^[8]

See also

• Natural deduction
• Sequent calculus
• Deductive systems