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