Editing Natural deduction (section)

== Suppes–Lemmon-style propositional logic ==

=== Suppes–Lemmon-style inference rules ===
Natural deduction inference rules, due ultimately to [[Gerhard Gentzen|Gentzen]], are given below.{{sfn|Lemmon|1978|pages=passim, especially 39-40}}{{sfn|Lemmon|1978|pages=passim, especially 39-40}} There are ten primitive rules of proof, which are the rule ''assumption'', plus four pairs of introduction and elimination rules for the binary connectives, and the rule ''reductio ad adbsurdum''.{{sfn|Allen|Hand|2022}} Disjunctive Syllogism can be used as an easier alternative to the proper ∨-elimination,{{sfn|Allen|Hand|2022}} and MTT and DN are commonly given rules,{{sfn|Lemmon|1978|pages=passim, especially 39-40}} although they are not primitive.{{sfn|Allen|Hand|2022}}

{| class="wikitable" style="margin:auto;"

|+ List of Inference Rules
|-
! Rule Name
! Alternative names
! Annotation
!Assumption set
! Statement
|-
| Rule of Assumptions{{sfn|Lemmon|1978|pages=passim, especially 39-40}}|| Assumption{{sfn|Allen|Hand|2022}}|| '''A{{sfn|Lemmon|1978|pages=passim, especially 39-40}}{{sfn|Allen|Hand|2022}}'''
|The current line number.{{sfn|Allen|Hand|2022}}|| At any stage of the argument, introduce a proposition as an assumption of the argument.{{sfn|Lemmon|1978|pages=passim, especially 39-40}}{{sfn|Allen|Hand|2022}}
|-
| Conjunction introduction|| Ampersand introduction,{{sfn|Lemmon|1978|pages=passim, especially 39-40}}{{sfn|Allen|Hand|2022}} conjunction (CONJ){{sfn|Allen|Hand|2022}}{{sfn|Arthur|2017}}|| '''m, n &I{{sfn|Allen|Hand|2022}}{{sfn|Lemmon|1978|pages=passim, especially 39-40}}'''
|The union of the assumption sets at lines '''m''' and '''n'''.{{sfn|Allen|Hand|2022}}|| From <math>\varphi</math> and <math>\psi</math> at lines '''m''' and '''n''', infer <math>\varphi ~ \& ~ \psi</math>.{{sfn|Lemmon|1978|pages=passim, especially 39-40}}{{sfn|Allen|Hand|2022}}
|-
| Conjunction elimination|| Simplification (S),{{sfn|Allen|Hand|2022}} ampersand elimination{{sfn|Lemmon|1978|pages=passim, especially 39-40}}{{sfn|Allen|Hand|2022}}|| '''m &E{{sfn|Allen|Hand|2022}}{{sfn|Lemmon|1978|pages=passim, especially 39-40}}'''
|The same as at line '''m'''.{{sfn|Allen|Hand|2022}}|| From <math>\varphi ~ \& ~ \psi</math> at line '''m''', infer <math>\varphi</math> and <math>\psi</math>.{{sfn|Allen|Hand|2022}}{{sfn|Lemmon|1978|pages=passim, especially 39-40}}
|-
| Disjunction introduction{{sfn|Lemmon|1978|pages=passim, especially 39-40}}|| Addition (ADD){{sfn|Allen|Hand|2022}}|| '''m ∨I{{sfn|Allen|Hand|2022}}{{sfn|Lemmon|1978|pages=passim, especially 39-40}}'''
|The same as at line '''m'''.{{sfn|Allen|Hand|2022}}|| From <math>\varphi</math> at line '''m''', infer <math>\varphi \lor \psi</math>, whatever <math>\psi</math> may be.{{sfn|Allen|Hand|2022}}{{sfn|Lemmon|1978|pages=passim, especially 39-40}}
|-
| Disjunction elimination|| Wedge elimination,{{sfn|Lemmon|1978|pages=passim, especially 39-40}} dilemma (DL){{sfn|Arthur|2017}}|| '''j,k,l,m,n ∨E{{sfn|Lemmon|1978|pages=passim, especially 39-40}}'''
|The lines '''j,k,l,m,n'''.{{sfn|Lemmon|1978|pages=passim, especially 39-40}}|| From <math>\varphi \lor \psi</math> at line '''j''', and an assumption of <math>\varphi</math> at line '''k''', and a derivation of <math>\chi</math> from <math>\varphi</math> at line '''l''', and an assumption of <math>\psi</math> at line '''m''', and a derivation of <math>\chi</math> from <math>\psi</math> at line '''n''', infer <math>\chi</math>.{{sfn|Lemmon|1978|pages=passim, especially 39-40}}
|-
|Disjunctive Syllogism
|Wedge elimination (∨E),{{sfn|Allen|Hand|2022}} modus tollendo ponens (MTP){{sfn|Allen|Hand|2022}}
|'''m,n DS{{sfn|Allen|Hand|2022}}'''
|The union of the assumption sets at lines '''m''' and '''n'''.{{sfn|Allen|Hand|2022}}
|From <math>\varphi \lor \psi</math> at line '''m''' and <math>- \varphi</math> at line '''n''', infer <math>\psi</math>; from <math>\varphi \lor \psi</math> at line '''m''' and <math>- \psi</math> at line '''n''', infer <math>\varphi</math>.{{sfn|Allen|Hand|2022}}
|-
| Arrow elimination{{sfn|Allen|Hand|2022}}|| Modus ponendo ponens (MPP),{{sfn|Lemmon|1978|pages=passim, especially 39-40}}{{sfn|Allen|Hand|2022}} modus ponens (MP),{{sfn|Arthur|2017}}{{sfn|Allen|Hand|2022}} conditional elimination || '''m, n →E{{sfn|Allen|Hand|2022}}{{sfn|Lemmon|1978|pages=passim, especially 39-40}}'''
|The union of the assumption sets at lines '''m''' and '''n'''.{{sfn|Allen|Hand|2022}}|| From <math>\varphi \to \psi</math> at line '''m''', and <math>\varphi</math> at line '''n''', infer <math>\psi</math>.{{sfn|Allen|Hand|2022}}
|-
| Arrow introduction{{sfn|Allen|Hand|2022}}|| Conditional proof (CP),{{sfn|Arthur|2017}}{{sfn|Lemmon|1978|pages=passim, especially 39-40}}{{sfn|Allen|Hand|2022}} conditional introduction || '''n, →I (m){{sfn|Allen|Hand|2022}}{{sfn|Lemmon|1978|pages=passim, especially 39-40}}'''
|Everything in the assumption set at line '''n''', excepting '''m''', the line where the antecedent was assumed.{{sfn|Allen|Hand|2022}}|| From <math>\psi</math> at line '''n''', following from the assumption of <math>\varphi</math> at line '''m''', infer <math>\varphi \to \psi</math>.{{sfn|Allen|Hand|2022}}
|-
| Reductio ad absurdum{{sfn|Lemmon|1978|pages=passim, especially 39-40}}|| Indirect Proof (IP),{{sfn|Allen|Hand|2022}} negation introduction (−I),{{sfn|Allen|Hand|2022}} negation elimination (−E){{sfn|Allen|Hand|2022}}|| '''m,'''&nbsp;'''n'''&nbsp;'''RAA'''&nbsp;'''(k){{sfn|Allen|Hand|2022}}'''
|The union of the assumption sets at lines '''m''' and '''n''', excluding '''k''' (the denied assumption).{{sfn|Allen|Hand|2022}}|| From a sentence and its denial{{refn|To simplify the statement of the rule, the word "denial" here is used in this way: the ''denial'' of a formula <math>\varphi</math> that is not a ''negation'' is <math>- \varphi</math>, whereas a ''negation'', <math>- \varphi</math>, has two ''denials'', viz., <math>\varphi</math> and <math>- - \varphi</math>.{{sfn|Allen|Hand|2022}}}} at lines '''m''' and '''n''', infer the denial of any assumption appearing in the proof (at line '''k''').{{sfn|Allen|Hand|2022}}
|-
| Double arrow introduction{{sfn|Allen|Hand|2022}}|| Biconditional definition (''Df'' ↔),{{sfn|Lemmon|1978|pages=passim, especially 39-40}} biconditional introduction|| '''m, n ↔ I{{sfn|Allen|Hand|2022}}'''
|The union of the assumption sets at lines '''m''' and '''n'''.{{sfn|Allen|Hand|2022}}|| From <math>\varphi \to \psi</math> and <math>\psi \to \varphi</math> at lines '''m''' and '''n''', infer <math>\varphi \leftrightarrow \psi</math>.{{sfn|Allen|Hand|2022}}
|-
| Double arrow elimination{{sfn|Allen|Hand|2022}}|| Biconditional definition (''Df'' ↔),{{sfn|Lemmon|1978|pages=passim, especially 39-40}} biconditional elimination|| '''m ↔ E{{sfn|Allen|Hand|2022}}'''
|The same as at line '''m'''.{{sfn|Allen|Hand|2022}}|| From <math>\varphi \leftrightarrow \psi</math> at line '''m''', infer either <math>\varphi \to \psi</math> or <math>\psi \to \varphi</math>.{{sfn|Allen|Hand|2022}}
|-
| Double negation{{sfn|Lemmon|1978|pages=passim, especially 39-40}}{{sfn|Arthur|2017}}|| Double negation elimination|| '''m DN{{sfn|Lemmon|1978|pages=passim, especially 39-40}}'''
|The same as at line '''m'''.{{sfn|Lemmon|1978|pages=passim, especially 39-40}}|| From <math>- - \varphi</math> at line '''m''', infer <math>\varphi</math>.{{sfn|Lemmon|1978|pages=passim, especially 39-40}}
|-
| Modus tollendo tollens{{sfn|Lemmon|1978|pages=passim, especially 39-40}}|| Modus tollens (MT){{sfn|Arthur|2017}}|| '''m, n MTT{{sfn|Lemmon|1978|pages=passim, especially 39-40}}'''
|The union of the assumption sets at lines '''m''' and '''n'''.{{sfn|Lemmon|1978|pages=passim, especially 39-40}}|| From <math>\varphi \to \psi</math> at line '''m''', and <math>- \psi</math> at line '''n''', infer <math>- \varphi</math>.{{sfn|Lemmon|1978|pages=passim, especially 39-40}}
|}

=== Suppes–Lemmon-style example proof ===
Recall that an example proof was already given when introducing {{section link||Suppes–Lemmon notation}}. This is a second example.
{| class="wikitable" style="margin:auto;"
|+Suppes–Lemmon style proof (second example)
!Assumption set
!Line number
!Sentence of proof
!Annotation
|-
|{{EquationRef|1}}
|{{EquationRef|1}}
|<math>P \lor Q</math>
|'''A'''
|-
|{{EquationRef|2}}
|{{EquationRef|2}}
|<math>\neg P</math>
|'''A'''
|-
|{{EquationRef|3}}
|{{EquationRef|3}}
|<math>\neg P \to \neg Q</math>
|'''A'''
|-
|{{EquationRef|2}}, {{EquationRef|3}}
|{{EquationRef|4}}
|<math>\neg Q</math>
|{{EquationRef|2}}, {{EquationRef|3}} '''→E'''
|-
|{{EquationRef|1}}, {{EquationRef|2}}, {{EquationRef|3}}
|{{EquationRef|5}}
|<math>P</math>
|{{EquationRef|1}}, {{EquationRef|4}} '''&E'''
|-
|{{EquationRef|1}}, {{EquationRef|3}}
|{{EquationRef|6}}
|<math>P</math>
|{{EquationRef|2}}, {{EquationRef|5}} '''RAA(2)'''
|-
|{{EquationRef|2}}, {{EquationRef|3}}
|{{EquationRef|7}}
|<math>\neg P</math>
|{{EquationRef|2}}, {{EquationRef|3}} '''RAA(1)'''
|}