Modal propositional logic adds depth to classical logic by introducing necessity and possibility operators. These operators allow us to reason about what must be true and what could be true across different possible worlds or scenarios.

The system builds on familiar propositional connectives, adding modal operators to create more complex formulas. Rules of inference and axioms provide a framework for deriving valid arguments and exploring the relationships between necessity and possibility.

Modal Propositional Logic

Modal propositional logic formulas

• Modal operators add qualifiers of necessity ($\square$) and possibility ($\diamond$) to propositions
  • $\square p$ asserts p is necessarily true (true in all possible worlds)
  • $\diamond p$ asserts p is possibly true (true in at least one possible world)
• Propositional connectives combine propositions to form compound statements
  • Negation $\neg$ reverses truth value ($\neg p$ is true when p is false)
  • Conjunction $\wedge$ asserts both propositions are true ($p \wedge q$)
  • Disjunction $\vee$ asserts at least one proposition is true ($p \vee q$)
  • Implication $\rightarrow$ asserts if antecedent is true, consequent must be true ($p \rightarrow q$)
  • Biconditional $\leftrightarrow$ asserts propositions have the same truth value ($p \leftrightarrow q$)
• Well-formed formulas (wffs) are syntactically correct combinations of propositions and connectives
  • Atomic propositions (p, q) are the simplest wffs
  • Applying $\neg$, $\square$, or $\diamond$ to a wff produces a new wff ($\neg p$, $\square q$)
  • Combining two wffs with a binary connective produces a new wff ($(p \wedge q)$, $(p \rightarrow q)$)

Rules of modal propositional inference

• Axioms are foundational principles assumed to be true
  • K: Distributivity of $\square$ over $\rightarrow$ ($\square (p \rightarrow q) \rightarrow (\square p \rightarrow \square q)$)
  • T: Reflexivity of $\square$ ($\square p \rightarrow p$)
  • 4: Transitivity of $\square$ ($\square p \rightarrow \square \square p$)
  • 5: Symmetry of $\diamond$ ($\diamond p \rightarrow \square \diamond p$)
• Rules of inference derive new theorems from existing ones
  • Modus Ponens infers $\psi$ from $\phi$ and $\phi \rightarrow \psi$
  • Necessitation infers $\square \phi$ from $\phi$

Validity in modal propositional logic

• Semantic methods interpret formulas in terms of possible worlds
  • Kripke semantics defines truth conditions using accessibility relations between worlds
    • $\square p$ is true at w if p is true at all worlds accessible from w
    • $\diamond p$ is true at w if p is true at some world accessible from w
  • An argument is valid if the conclusion is true whenever the premises are true
• Syntactic methods use formal proof systems to derive theorems from axioms
  • Natural deduction and Hilbert-style systems are common proof methods
  • Soundness ensures provable formulas are semantically valid
  • Completeness ensures valid formulas are syntactically provable

Relationships between modal operators

• Necessity ($\square$) and possibility ($\diamond$) are interdefinable
  • $\square p \equiv \neg \diamond \neg p$ (p is necessary iff not-p is not possible)
  • $\diamond p \equiv \neg \square \neg p$ (p is possible iff not-p is not necessary)
• Modal operators exhibit duality
  • $\neg \square p \equiv \diamond \neg p$ (not necessarily p iff possibly not-p)
  • $\neg \diamond p \equiv \square \neg p$ (not possibly p iff necessarily not-p)