Using PL to Describe Properties of Systems

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