## Definition
**Propositional logic** is the simplest formal logic: a language of *atomic propositions* (true/false statements) combined via Boolean connectives. It is the foundation for both [[First-Order Logic]] and modern automated reasoning.
## Syntax
- **Atomic propositions:** $P, Q, R, \dots$ (representing facts like "it is raining").
- **Connectives:** $\neg$ (not), $\land$ (and), $\lor$ (or), $\to$ (implies), $\leftrightarrow$ (iff).
- **Well-formed formulas (WFFs)** built recursively from atoms and connectives.
Example: $(P \to Q) \land \neg Q \to \neg P$ (the contrapositive law).
## Semantics
An **interpretation** assigns true/false to each atom. A formula is:
- **Satisfiable** — true under at least one interpretation.
- **Valid (tautology)** — true under every interpretation.
- **Unsatisfiable (contradiction)** — false under every interpretation.
- **A model** of formula $\alpha$ — an interpretation that makes $\alpha$ true.
## Entailment
$\alpha \models \beta$ ("$\alpha$ entails $\beta
quot;) holds when every model of $\alpha$ is also a model of $\beta$. The central inference question.
## Normal Forms
- **Conjunctive Normal Form (CNF):** conjunction of disjunctions of literals — $(P \lor \neg Q) \land (R \lor S)$. Used by SAT solvers and [[Resolution Inference]].
- **Disjunctive Normal Form (DNF):** disjunction of conjunctions — symmetrical opposite.
Every WFF has equivalent CNF and DNF forms.
## SAT Problem
**SAT** asks: is a given CNF formula satisfiable? It is the canonical NP-complete problem (Cook 1971). Modern SAT solvers (MiniSat, CaDiCaL) routinely handle problems with millions of variables — the practical breakthrough that made many planning, verification, and combinatorial problems tractable.
## Limitations
Propositional logic cannot express *quantification* ("for all", "there exists") or *relations between objects*. For that, [[First-Order Logic]] is required.
## Related
- [[First-Order Logic]]
- [[Inference Rules]]
- [[Resolution Inference]]
- [[Forward and Backward Chaining]]