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.

Metatheory. Post (1921) proved soundness and completeness for the two-element Boolean algebra — the standard Hilbert, natural deduction, sequent and resolution systems derive exactly the tautologies — and in the same paper established functional completeness, so {¬, ∧}, {¬, ∨}, {¬, →} and each of NAND and NOR alone express every truth function; his later classification of the clones of Boolean functions (1941) settles which sets do, a set being complete exactly when it escapes all five maximal clones — 0-preserving, 1-preserving, monotone, self-dual, affine. Validity is decidable by truth tables in O(2ⁿ) for n atoms, and the exact complexity is the reference point for the whole field: SAT is NP-complete by Cook (1971) and Levin (1973), so TAUT and the entailment relation are coNP-complete and a polynomial-time decision procedure for either would prove P = NP. Compactness follows from the finiteness of derivations for countable languages and is equivalent to the Boolean prime ideal theorem in general. Craig interpolation holds (Craig 1957), and the Lindenbaum–Tarski algebra of the calculus on n atoms is the free Boolean algebra on n generators, with 2^(2ⁿ) elements. Proof length is a separate matter from decidability: Haken (1985) proved that resolution refutations of the pigeonhole formulas are of exponential size.

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

Limitations. Atoms have no internal structure, so "Socrates is mortal" is the letter p with no access to Socrates or to mortality, and the syllogism from "all men are mortal" is invalid in the calculus — the inferences that motivated logic in the first place need quantifiers the language does not have. Truth functionality is the binding constraint: a connective's value depends on the values of its arguments and on nothing else, which makes → material, so ¬φ ⊨ φ → ψ and ψ ⊨ φ → ψ hold, and it puts necessity, time, knowledge, obligation, relevance and counterfactual dependence outside the language entirely, since none of these is a function of truth values. Decidability holds at a complexity the results make exact: TAUT is coNP-complete, so no proof system for the calculus is polynomially bounded unless NP = coNP, and Haken's lower bound shows resolution in particular is not. Compactness fails to give any finitary handle on infinite premise sets in the presence of infinitely many atoms without the Boolean prime ideal theorem, which is unprovable in ZF. And the calculus is two-valued by construction, so partiality, vagueness and inconsistent information have no representation short of changing the algebra.

© 2026 Lingenic LLC