Basic and derived argument forms

Name Sequent Description
Modus Ponens \(( ( p → q ) ∧ p ) ⊢ q \)
 If p then q; p; therefore q
Modus Tollens \(( ( p → q ) ∧ ¬ q ) ⊢ ¬ p \)
 If p then q; not q; therefore not p
Hypothetical Syllogism \(( ( p → q ) ∧ ( q → r ) ) ⊢ ( p → r ) \)
 If p then q; if q then r; therefore, if p then r
Disjunctive Syllogism \(( ( p ∨ q ) ∧ ¬ p ) ⊢ q \)
 Either p or q, or both; not p; therefore, q
Constructive Dilemma \(( ( p → q ) ∧ ( r → s ) ∧ ( p ∨ r ) ) ⊢ ( q ∨ s )\)
If p then q; and if r then s; but p or r; therefore q or s
Destructive Dilemma \(( ( p → q ) ∧ ( r → s ) ∧ ( ¬ q ∨ ¬ s ) ) ⊢ ( ¬ p ∨ ¬ r ) \)
 If p then q; and if r then s; but not q or not s; therefore not p or not r
Bidirectional Dilemma \(( ( p → q ) ∧ ( r → s ) ∧ ( p ∨ ¬ s ) ) ⊢ ( q ∨ ¬ r ) \)
 If p then q; and if r then s; but p or not s; therefore q or not r
Simplification \(( p ∧ q ) ⊢ p \)
 p and q are true; therefore p is true
Conjunction \(p , q ⊢ ( p ∧ q ) \)
 p and q are true separately; therefore they are true conjointly
Addition \(p ⊢ ( p ∨ q ) \)
 p is true; therefore the disjunction (p or q) is true
Composition \(( ( p → q ) ∧ ( p → r ) ) ⊢ ( p → ( q ∧ r ) ) \)
 If p then q; and if p then r; therefore if p is true then q and r are true
De Morgan's Theorem (1) \(¬ ( p ∧ q ) ⊣⊢ ( ¬ p ∨ ¬ q ) \)
 The negation of (p and q) is equiv. to (not p or not q)
De Morgan's Theorem (2) \(¬ ( p ∨ q ) ⊣⊢ ( ¬ p ∧ ¬ q ) \)
 The negation of (p or q) is equiv. to (not p and not q)
Commutation (1) \(( p ∨ q ) ⊣⊢ ( q ∨ p ) \)
 (p or q) is equiv. to (q or p)
Commutation (2) \(( p ∧ q ) ⊣⊢ ( q ∧ p ) \)
 (p and q) is equiv. to (q and p)
Commutation (3) \(( p ↔ q ) ⊣⊢ ( q ↔ p ) \)
 (p iff q) is equiv. to (q iff p)
Association (1) \(( p ∨ ( q ∨ r ) ) ⊣⊢ ( ( p ∨ q ) ∨ r ) \)
 p or (q or r) is equiv. to (p or q) or r
Association (2) \(( p ∧ ( q ∧ r ) ) ⊣⊢ ( ( p ∧ q ) ∧ r ) \)
 p and (q and r) is equiv. to (p and q) and r
Distribution (1) \(( p ∧ ( q ∨ r ) ) ⊣⊢ ( ( p ∧ q ) ∨ ( p ∧ r ) ) \)
 p and (q or r) is equiv. to (p and q) or (p and r)
Distribution (2) \(( p ∨ ( q ∧ r ) ) ⊣⊢ ( ( p ∨ q ) ∧ ( p ∨ r ) ) \)
 p or (q and r) is equiv. to (p or q) and (p or r)
Double Negation \(p ⊣⊢ ¬ ¬ p \)
 p is equivalent to the negation of not p
Transposition \(( p → q ) ⊣⊢ ( ¬ q → ¬ p ) \)
 If p then q is equiv. to if not q then not p
Material Implication \(( p → q ) ⊣⊢ ( ¬ p ∨ q ) \)
 If p then q is equiv. to not p or q
Material Equivalence (1) \(( p ↔ q ) ⊣⊢ ( ( p → q ) ∧ ( q → p ) ) \)
 (p iff q) is equiv. to (if p is true then q is true) and (if q is true then p is true)
Material Equivalence (2) \(( p ↔ q ) ⊣⊢ ( ( p ∧ q ) ∨ ( ¬ p ∧ ¬ q ) ) \)
 (p iff q) is equiv. to either (p and q are true) or (both p and q are false)
Material Equivalence (3) \(( p ↔ q ) ⊣⊢ ( ( p ∨ ¬ q ) ∧ ( ¬ p ∨ q ) ) \)
 (p iff q) is equiv to., both (p or not q is true) and (not p or q is true)
Exportation \(( ( p ∧ q ) → r ) ⊢ ( p → ( q → r ) ) \)
 from (if p and q are true then r is true) we can prove (if q is true then r is true, if p is true)
Importation \(( p → ( q → r ) ) ⊣⊢ ( ( p ∧ q ) → r ) \)
 If p then (if q then r) is equivalent to if p and q then r
Tautology (1) \(p ⊣⊢ ( p ∨ p ) \)
 p is true is equiv. to p is true or p is true
Tautology (2) \(p ⊣⊢ ( p ∧ p ) \)
 p is true is equiv. to p is true and p is true
Tertium non datur (Law of Excluded Middle) \(⊢ ( p ∨ ¬ p ) \)
 p or not p is true
Law of Non-Contradiction \(⊢ ¬ ( p ∧ ¬ p ) \)
 p and not p is false, is a true statement