Propositional Logic¶
Job: Define classical propositional syntax and truth-functional semantics; state completeness, compactness, and normal-form tools.
Core¶
Syntax. Propositional variables \(\mathrm{Var}\); formulas generated by $$ \varphi::= p\mid \bot\mid \varphi\to\varphi\mid \ldots $$ (standard complete connectives \(\{\neg,\vee,\wedge,\to\}\)). Unique readability.
Semantics. Valuation \(v:\mathrm{Var}\to\{0,1\}\) extends to \(\llbracket\varphi\rrbracket_v\in\{0,1\}\) by truth tables. \(\varphi\) valid (tautology) if true under all \(v\); satisfiable if true under some \(v\). Semantic entailment \(\Gamma\models\varphi\): every \(v\) satisfying \(\Gamma\) satisfies \(\varphi\).
Proof systems. Hilbert calculus (axioms + MP); natural deduction; sequent calculus (Gentzen). Soundness: \(\Gamma\vdash\varphi\Rightarrow\Gamma\models\varphi\). Completeness (propositional): \(\Gamma\models\varphi\Rightarrow\Gamma\vdash\varphi\). Corollary: tautologies are exactly the theorems of pure propositional calculus.
Compactness. \(\Gamma\) satisfiable iff every finite \(\Gamma_0\subseteq\Gamma\) is. Proof via completeness + finiteness of proofs, or topological Tychonoff on \(\{0,1\}^{\mathrm{Var}}\).
Normal forms. Every formula equivalent to CNF and DNF. Tseitin transformation: equisatisfiable CNF with linear size overhead (fresh variables).
Resolution. Refutation complete for CNF: \(\Gamma\models\bot\) iff empty clause derivable by resolution (with suitable lifting). Complexity: SAT NP-complete; 2-SAT in P; Horn-SAT in P.
Interpolation / Beth (pointer): Craig interpolation for classical propositional and FOL fragments.
Boolean algebra link: Lindenbaum–Tarski algebra of formulas mod \(\leftrightarrow\) is the free Boolean algebra on \(\mathrm{Var}\).
See it¶
Compactness application: if every finite subgraph of an infinite graph \(G\) is \(k\)-colorable, then \(G\) is \(k\)-colorable. Encode colors by propositional variables \(p_{v,i}\) with clauses enforcing proper coloring; finite satisfiability \(\Rightarrow\) global by compactness.
Check¶
Show \(\{\neg p\vee q,\ p\}\vdash q\) is valid semantically and give a proof sketch.
Any \(v\) with both premises true forces \(v(q)=1\) (truth table / cases on \(v(p)\)). Proof: from \(p\) and \(\neg p\vee q\) (i.e. \(p\to q\)) apply MP.
Does propositional compactness need the axiom of choice?
For countable \(\mathrm{Var}\), sequential arguments / König's lemma-style constructions can avoid full AC. For arbitrary \(\mathrm{Var}\), the topological proof uses Tychonoff on \(2^{\mathrm{Var}}\), which is choice-flavored (equivalent to Boolean prime ideal theorem / weaker than full AC).
Pitfalls¶
- Semantic entailment is about all valuations; syntactic \(\vdash\) depends on the calculus — completeness bridges them.
- Equivalence \(\neq\) equisatisfiability (Tseitin).
- Classical \(\varphi\vee\neg\varphi\) fails in intuitionistic propositional logic.
Refs¶
Enderton; van Dalen; Mendelson; Troelstra–Schwichtenberg (proof theory); Buss handbook chapters.