| 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
|