Module I·Article I·~5 min read
Syntax and Semantics of Propositional Logic
Propositional Logic
Turn this article into a podcast
Pick voices, format, length — AI generates the audio
Motivation: Why Formalize Reasoning?
Mathematical proofs consist of steps in which some statements are derived from others. But what is a “correct” step? Propositional logic provides a precise language: syntax (how to write formulas) and semantics (what they mean). This is the foundation underlying automated provers, compilers, and program verification systems.
Syntax
Alphabet:
- Propositional variables: p, q, r, p₁, p₂, ...
- Logical connectives: ¬ (negation), ∧ (conjunction—“and”), ∨ (disjunction—“or”), → (implication—“if... then”), ↔ (equivalence—“if and only if”).
- Parentheses: (, ).
Inductive definition of formulas:
- Every variable p is a formula.
- If φ is a formula, then ¬φ is a formula.
- If φ and ψ are formulas, then (φ ∧ ψ), (φ ∨ ψ), (φ → ψ), (φ ↔ ψ) are formulas.
- Nothing else is a formula.
Semantics: Truth Tables
Interpretation (valuation): function I: {variables} → {0, 1}. Extends to all formulas:
- I(¬φ) = 1 − I(φ)
- I(φ ∧ ψ) = min(I(φ), I(ψ)) — true if both are true
- I(φ ∨ ψ) = max(I(φ), I(ψ)) — true if at least one is true
- I(φ → ψ) = max(1−I(φ), I(ψ)) — false only when φ=1, ψ=0
- I(φ ↔ ψ) = 1 if and only if I(φ) = I(ψ)
Key notions:
- Tautology: I(φ) = 1 for all interpretations. Denotation: ⊨ φ.
- Contradiction (antitautology): I(φ) = 0 for all interpretations.
- Satisfiability: I(φ) = 1 for some I.
Logical Consequence and Equivalence
Consequence: Γ ⊨ φ if every I that makes all ψ ∈ Γ true makes φ true.
Logical equivalence: φ ≡ ψ if I(φ) = I(ψ) for all I. Examples:
- ¬¬p ≡ p (double negation)
- (p → q) ≡ (¬p ∨ q) (implication via disjunction)
- ¬(p ∧ q) ≡ (¬p ∨ ¬q) (De Morgan’s law)
- ¬(p ∨ q) ≡ (¬p ∧ ¬q) (De Morgan’s law)
Laws of distributivity:
- p ∧ (q ∨ r) ≡ (p ∧ q) ∨ (p ∧ r)
- p ∨ (q ∧ r) ≡ (p ∨ q) ∧ (p ∨ r)
Numerical Example
Problem: Prove the tautology called the “law of syllogism”: (p → q) → ((q → r) → (p → r)).
Step 1. Suppose the whole expression is false. Then (p → q) = 1 and ((q → r) → (p → r)) = 0.
Step 2. (q → r) → (p → r) = 0 → (q → r) = 1 and (p → r) = 0.
Step 3. (p → r) = 0 → p = 1 and r = 0.
Step 4. (q → r) = 1 with r = 0 → q = 0.
Step 5. (p → q) = 1 with p = 1 → q = 1. But from step 4: q = 0. Contradiction!
Conclusion: Assuming falsity leads to a contradiction → the formula is identically true ⊨ (p→q)→((q→r)→(p→r)).
Truth table (abbreviated): For p=1, q=0, r=0: (p→q) = (1→0) = 0. Whole expression: 0 → ... = 1 ✓. For p=1, q=1, r=0: (p→q)=1, (q→r)=(1→0)=0, (q→r)→(p→r)=0→0=1, result: 1→1=1 ✓.
Real-world Application
Hardware verification: logical circuits (AND/OR/NOT/NAND) implement propositional formulas. Tools like CBMC (Bounded Model Checker) automatically check that a circuit meets specification—essentially, they verify a tautology.
Additional Aspects
Propositional logic is not only a theoretical foundation, but also a practical tool: SAT solvers (Z3, MiniSAT, CryptoMiniSAT) solve millions of propositional formulas daily in circuit verification, action planning, cryptanalysis, and automated theorem proving. The theoretical boundary—NP-completeness of the SAT problem (Cook–Levin theorem, 1971)—means that in the worst case any algorithm requires exponential time, but modern heuristics (CDCL—conflict-driven clause learning, restarts, watched literals) make tasks with millions of variables practically solvable. At the interface of logic and mathematics, propositional logic underlies Boolean networks and models of biological gene regulation.
Connection with Other Branches of Mathematics
Propositional logic is naturally interpreted as a special case of Boolean algebras, described by G. Boole in the mid-19th century and axiomatized by M. Stone. Stone’s representation theorem for Boolean algebras connects the syntax of logic with topological spaces: every Boolean algebra corresponds to a compact totally disconnected space (ultrafilter space), and logical operations are realized via operations on closed sets. This construction is used in the theory of dynamical systems with discrete states, where logical formulas encode invariants and sets of trajectories.
The connection with algebra also appears via lattices: the laws of distributivity and De Morgan are special cases of general facts about distributive lattices studied in universal algebra. In probability theory, logical connectives model events and their combinations: Kolmogorov’s classical formalization relies on σ-algebras, which are “σ-versions” of Boolean algebras. Tautologies of propositional logic turn into identity-like probabilistic equalities for any model, e.g., the rules of summing and conditional probability.
In numerical methods, especially for solving differential equations with switching conditions, logical formulas define regions in the phase space where one or another system of equations applies. Hybrid systems are described as a combination of continuous dynamics and discrete logic, and here logic-algebraic verification methods are used: logical invariants, computed via abstract interpretation, guarantee correctness of numerical schemes. In combinatorial optimization, propositional constraints are translated into SAT problems; then linear and integer programming (the works of J. Gomory, R. Karp) combine with logical solvers, forming so-called SMT methods used in modern analysis of algorithms and models.
Historical Background and Development of the Idea
The first rigorous system of propositional calculus was essentially formulated by Frege in “Begriffsschrift” (1879), where he introduced a formal language to represent mathematical reasoning. However, the idea of a clear separation of syntax and semantics was systematized already in the early 20th century by Hilbert and his school; their course “Grundlagen der Mathematik” (1934–1939) provided axiomatic systems for propositional and predicate logic. Alfred Tarski in the 1930s offered a model-theoretic interpretation of truth, where the semantics of propositional logic are formulated through valuations and structures.
§ Act · what next