Editing Propositional calculus (section)

=== Inference rules ===
Natural deduction inference rules, due ultimately to [[Gerhard Gentzen|Gentzen]], are given below.<ref name=":38" /> 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''.<ref name=":35" /> Disjunctive Syllogism can be used as an easier alternative to the proper ∨-elimination,<ref name=":35" /> and MTT and DN are commonly given rules,<ref name=":38" /> although they are not primitive.<ref name=":35" />

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

|+ List of Inference Rules
|-
! Rule Name
! Alternative names
! Annotation
!Assumption set
! Statement
|-
| Rule of Assumptions<ref name=":38" />|| Assumption<ref name=":35" />|| '''A<ref name=":38" /><ref name=":35" />'''
|The current line number.<ref name=":35" />|| At any stage of the argument, introduce a proposition as an assumption of the argument.<ref name=":38" /><ref name=":35" />
|-
| Conjunction introduction|| Ampersand introduction,<ref name=":38" /><ref name=":35" /> conjunction (CONJ)<ref name=":35" /><ref name=":39"/>|| '''m, n &I<ref name=":35" /><ref name=":38" />'''
|The union of the assumption sets at lines '''m''' and '''n'''.<ref name=":35" />|| From <math>\varphi</math> and <math>\psi</math> at lines '''m''' and '''n''', infer <math>\varphi ~ \& ~ \psi</math>.<ref name=":38" /><ref name=":35" />
|-
| Conjunction elimination|| Simplification (S),<ref name=":35" /> ampersand elimination<ref name=":38" /><ref name=":35" />|| '''m &E<ref name=":35" /><ref name=":38" />'''
|The same as at line '''m'''.<ref name=":35" />|| From <math>\varphi ~ \& ~ \psi</math> at line '''m''', infer <math>\varphi</math> and <math>\psi</math>.<ref name=":35" /><ref name=":38" />
|-
| Disjunction introduction<ref name=":38" />|| Addition (ADD)<ref name=":35" />|| '''m ∨I<ref name=":35" /><ref name=":38" />'''
|The same as at line '''m'''.<ref name=":35" />|| From <math>\varphi</math> at line '''m''', infer <math>\varphi \lor \psi</math>, whatever <math>\psi</math> may be.<ref name=":35" /><ref name=":38" />
|-
| Disjunction elimination|| Wedge elimination,<ref name=":38" /> dilemma (DL)<ref name=":39" />|| '''j,k,l,m,n ∨E<ref name=":38" />'''
|The lines '''j,k,l,m,n'''.<ref name=":38" />|| 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>.<ref name=":38" />
|-
|Disjunctive Syllogism
|Wedge elimination (∨E),<ref name=":35" /> modus tollendo ponens (MTP)<ref name=":35" />
|'''m,n DS<ref name=":35" />'''
|The union of the assumption sets at lines '''m''' and '''n'''.<ref name=":35" />
|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>.<ref name=":35" />
|-
| Arrow elimination<ref name=":35" />|| Modus ponendo ponens (MPP),<ref name=":38" /><ref name=":35" /> modus ponens (MP),<ref name=":39" /><ref name=":35" /> conditional elimination || '''m, n →E<ref name=":35" /><ref name=":38" />'''
|The union of the assumption sets at lines '''m''' and '''n'''.<ref name=":35" />|| From <math>\varphi \to \psi</math> at line '''m''', and <math>\varphi</math> at line '''n''', infer <math>\psi</math>.<ref name=":35" />
|-
| Arrow introduction<ref name=":35" />|| Conditional proof (CP),<ref name=":39" /><ref name=":38" /><ref name=":35" /> conditional introduction || '''n, →I (m)<ref name=":35" /><ref name=":38" />'''
|Everything in the assumption set at line '''n''', excepting '''m''', the line where the antecedent was assumed.<ref name=":35" />|| From <math>\psi</math> at line '''n''', following from the assumption of <math>\varphi</math> at line '''m''', infer <math>\varphi \to \psi</math>.<ref name=":35" />
|-
| Reductio ad absurdum<ref name=":38" />|| Indirect Proof (IP),<ref name=":35" /> negation introduction (−I),<ref name=":35" /> negation elimination (−E)<ref name=":35" />|| '''m,'''&nbsp;'''n'''&nbsp;'''RAA'''&nbsp;'''(k)<ref name=":35" />'''
|The union of the assumption sets at lines '''m''' and '''n''', excluding '''k''' (the denied assumption).<ref name=":35" />|| From a sentence and its denial{{refn|group=lower-alpha|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>.<ref name=":35" />}} at lines '''m''' and '''n''', infer the denial of any assumption appearing in the proof (at line '''k''').<ref name=":35" />
|-
| Double arrow introduction<ref name=":35" />|| Biconditional definition (''Df'' ↔),<ref name=":38" /> biconditional introduction|| '''m, n ↔ I<ref name=":35" />'''
|The union of the assumption sets at lines '''m''' and '''n'''.<ref name=":35" />|| From <math>\varphi \to \psi</math> and <math>\psi \to \varphi</math> at lines '''m''' and '''n''', infer <math>\varphi \leftrightarrow \psi</math>.<ref name=":35" />
|-
| Double arrow elimination<ref name=":35" />|| Biconditional definition (''Df'' ↔),<ref name=":38" /> biconditional elimination|| '''m ↔ E<ref name=":35" />'''
|The same as at line '''m'''.<ref name=":35" />|| From <math>\varphi \leftrightarrow \psi</math> at line '''m''', infer either <math>\varphi \to \psi</math> or <math>\psi \to \varphi</math>.<ref name=":35" />
|-
| Double negation<ref name=":38" /><ref name=":39" />|| Double negation elimination|| '''m DN<ref name=":38" />'''
|The same as at line '''m'''.<ref name=":38" />|| From <math>- - \varphi</math> at line '''m''', infer <math>\varphi</math>.<ref name=":38" />
|-
| Modus tollendo tollens<ref name=":38" />|| Modus tollens (MT)<ref name=":39" />|| '''m, n MTT<ref name=":38" />'''
|The union of the assumption sets at lines '''m''' and '''n'''.<ref name=":38" />|| From <math>\varphi \to \psi</math> at line '''m''', and <math>- \psi</math> at line '''n''', infer <math>- \varphi</math>.<ref name=":38" />
|}