Axioms for propositional calculational logic

 
Teaching OO using Java
Calculational
logic
festive occasions
ABC book
CS Faculty over the years
CS@Cornell
The Triple-I Administration
How Bush Operated

 

 

The axioms of equational propositional logic C are listed in the order in which they are usually presented and taught. Note that equivalence comes first. Note also that, after the first axiom, we take advantage of associativity of equivalence and write sequences of equivalences without parentheses. We use == for equivalence, | for disjunction, & for conjunction, ~ for negation (not), => for implication, and <= for consequence.

  • Associativity of ==: ((p == q) == r) == (p == (q == r))
  • Symmetry of ==: p == q == q == p
  • Identity of ==: true == q == q

  • Definition of false: false == ~true
  • Distributivity of not: ~(p == q) == ~p == q
  • Definition of =/=: (p =/= q) == ~(p == q)

  • Associativity of |: (p | q) & r == p | (q | r)
  • Symmetry of |: p | q == q | p
  • Idempotency of |: p | p == p
  • Distributivity of |: p |(q == r) == p | q == p | r
  • Excluded Middle: p | ~p

  • Golden rule: p & q == p == q == p | q

  • Implication: p => q == p | q == q
  • Consequence: p <= q == q => p