Propositional logic

  • Formulas composed of propositional variables (p, q, r, …), negation (¬) and connectives (∧, ∨, →, ↔):
    • (¬(p ∨ q) ∧ r) ∨ p
    • ((p → q) → p) → p
  • Classical logic: an assignment of true/false to the variables fixes whether a formula is true or false.
    For (¬(p ∨ q) ∧ r) ∨ p:
    • p = true, q = false, r = false makes it true: a satisfying assignment
    • p = false, q = false, r = false makes it false: a counterexample
  • Satisfiable formulas have satisfying assignments, valid formulas have no counterexamples:
    • (¬(p ∨ q) ∧ r) ∨ p is satisfiable
    • ((p → q) → p) → p is valid