Propositional Logic

Propositional logic is the simplest formal system for representing facts and inferences.

Syntax

• Atomic propositions $P, Q, R, \dots$: each is either true or false.
• Connectives: $\neg$ (not), $\wedge$ (and), $\vee$ (or), $\to$ (implies), $\leftrightarrow$ (iff).
• Sentences: built recursively from atoms and connectives.

Semantics

An interpretation (or model) assigns true/false to every atom. The truth value of a compound sentence follows from the standard truth tables.

A sentence is:

• Valid (or a tautology): true in every interpretation. $P \vee \neg P$.
• Satisfiable: true in at least one. $P \wedge Q$.
• Unsatisfiable: false in every interpretation. $P \wedge \neg P$.

Entailment

$\alpha$ entails $\beta$, written $\alpha \models \beta$, if every model that makes $\alpha$ true also makes $\beta$ true. Inference is the process of computing whether $\alpha \models \beta$.

Key fact: $\alpha \models \beta$ iff $\alpha \wedge \neg \beta$ is unsatisfiable. Reduces entailment to satisfiability — the SAT problem.

SAT and CNF

A formula in Conjunctive Normal Form (CNF) is an AND of ORs of literals (atoms or their negations). Every propositional formula can be converted to CNF (with potential blowup, but linear in size if you allow auxiliary variables — the Tseitin transformation).

SAT solvers operate on CNF. They decide whether a formula has any satisfying interpretation. The classic NP-complete problem; modern CDCL SAT solvers (Glucose, MiniSat, Kissat) handle instances with millions of variables for many real-world problems.

What propositional logic can't do

• Quantify over objects ("every employee has a manager" — needs first-order logic).
• Express relations between objects directly.
• Reason about functions and identities.

For most realistic knowledge representation, you need at least first-order logic.

Where propositional logic still rules

• Hardware verification: every circuit state is a propositional model.
• Software model checking: bounded model checking unrolls program traces into CNF.
• Configuration and dependency: package managers solve SAT problems on dependency constraints.
• Scheduling and planning as SAT: when problems can be flattened to propositional form, SAT solvers beat custom code.