Propositional Logic

Origin. Gottlob Frege's Begriffsschrift (1879) provided the first fully formal propositional calculus. Bertrand Russell and Alfred North Whitehead systematized it in Principia Mathematica (1910-1913). George Boole's earlier algebraic logic (1847, 1854) established the connection between logic and algebra. Also called sentential logic, statement logic, or zeroth-order logic.

Models. Truth and falsity of compound statements built from atomic propositions. How the truth of a whole depends on the truth of its parts. The logic of "and," "or," "not," "if-then" — the connectives that combine statements.

Formalism.

Syntax: Atomic propositions (p, q, r, ...) combined with connectives to form well-formed formulas (wffs). If φ and ψ are wffs, so are: ¬φ, (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ).

Semantics: A valuation v assigns each atom to {0, 1} (false, true). Truth tables define connective meanings:

v(¬φ) = 1 iff v(φ) = 0
v(φ ∧ ψ) = 1 iff v(φ) = 1 and v(ψ) = 1
v(φ ∨ ψ) = 1 iff v(φ) = 1 or v(ψ) = 1
v(φ → ψ) = 1 iff v(φ) = 0 or v(ψ) = 1
v(φ ↔ ψ) = 1 iff v(φ) = v(ψ)

Validity: φ is valid (tautology) iff true under all valuations. φ entails ψ (φ ⊨ ψ) iff every valuation making φ true makes ψ true.

Proof systems: Natural deduction, sequent calculus, Hilbert systems, resolution. All equivalent in power.

Symbols.

Symbol	Unicode	Name	Meaning
¬	U+00AC	Negation	Not
∧	U+2227	Conjunction	And
∨	U+2228	Disjunction	Or
→	U+2192	Implication	If...then
↔	U+2194	Biconditional	If and only if
⊤	U+22A4	Top / Verum	True (tautology)
⊥	U+22A5	Bottom / Falsum	False (contradiction)
⊨	U+22A8	Entailment	Semantically entails
⊢	U+22A2	Turnstile	Syntactically derives
∴	U+2234	Therefore	Conclusion follows

Metatheory. Decidable: truth-table method decides validity in O(2ⁿ) time for n atoms. SAT (satisfiability) is NP-complete — the canonical NP-complete problem (Cook-Levin theorem). Sound and complete: the standard proof systems derive exactly the valid formulas. Compactness: if every finite subset of a set of formulas is satisfiable, the whole set is satisfiable. Functional completeness: {¬, ∧}, {¬, ∨}, {¬, →}, or the single connective NAND (↑) or NOR (↓) suffice to express all truth functions.

Applies to. Digital circuit design. SAT solvers for verification and planning. Foundation for all richer logics. Boolean search queries. Formal specification.

Limitations. No internal structure of propositions — "Socrates is mortal" is just an atom p, with no access to Socrates or mortality. No quantification over individuals. Material implication (→) has "paradoxes": false antecedent makes any implication true. Cannot express necessity, time, knowledge, or obligation without extension.