Propositional and First-Order Logic

⚡ Key Takeaways

Propositional and first-order logic are the two foundational formal systems for representing and reasoning about truth. Propositional logic combines atomic statements with connectives (¬, ∧, ∨, →, ↔); first-order logic adds quantifiers (∀, ∃), variables, predicates, and functions. Key result: both are sound and complete (Gödel, 1929–30) — provability and semantic truth coincide. Applied across mathematics, computer science, philosophy, and AI. Originated with Frege (1879), formalized by Russell, Hilbert, and Gödel.

💡 The Core Insight

Logic separates syntax (formal symbol manipulation: which strings are formulas, which derivations are proofs) from semantics (meaning: when is a formula true under an interpretation). The central achievement is showing these two perspectives agree. A formula is provable from a set of premises if and only if it is true in every model of those premises. This bridge — soundness one way, completeness the other — turns reasoning into computation and meaning into mechanism.

Formal Statement

DefinitionPropositional Language

The language of propositional logic is built from:

  • A countable set of propositional variables p,q,r,…p, q, r, \dots
  • Connectives: ¬\neg (not), ∧\wedge (and), ∨\vee (or), →\to (implies), ↔\leftrightarrow (iff)
  • Parentheses for grouping.

Well-formed formulas (wffs) are defined recursively: every variable is a wff; if φ,ψ\varphi, \psi are wffs, so are ¬φ\neg\varphi, (φ∧ψ)(\varphi \wedge \psi), (φ∨ψ)(\varphi \vee \psi), (φ→ψ)(\varphi \to \psi), (φ↔ψ)(\varphi \leftrightarrow \psi).

The semantics is given by truth-value assignments v:Vars→{T,F}v : \text{Vars} \to \{T, F\}, extended to all formulas:

1
v(¬φ)=T  ⟺  v(φ)=F\quad v(\neg\varphi) = T \iff v(\varphi) = F

Derivation hint: negation flips the truth value; this is the defining truth-table row for ¬.

2
v(φ∧ψ)=T  ⟺  v(φ)=T and v(ψ)=T\quad v(\varphi \wedge \psi) = T \iff v(\varphi) = T \text{ and } v(\psi) = T

Derivation hint: conjunction is true only when both conjuncts hold — the AND truth table.

3
v(φ→ψ)=T  ⟺  v(φ)=F or v(ψ)=T\quad v(\varphi \to \psi) = T \iff v(\varphi) = F \text{ or } v(\psi) = T

Derivation hint: material implication is false only in the one case T→F; equivalently φ→ψ≡¬φ∨ψ\varphi \to \psi \equiv \neg\varphi \vee \psi.

DefinitionTautology, Satisfiability, Entailment
  • A formula φ\varphi is a tautology (⊨φ\models \varphi) if v(φ)=Tv(\varphi) = T for every assignment vv.
  • φ\varphi is satisfiable if some vv makes it true.
  • A set Γ\Gamma entails φ\varphi (Γ⊨φ\Gamma \models \varphi) if every vv satisfying all of Γ\Gamma also satisfies φ\varphi.
DefinitionFirst-Order Language

A first-order language L\mathcal{L} consists of:

  • Variables x,y,z,…x, y, z, \dots
  • Logical symbols: connectives, quantifiers ∀,∃\forall, \exists, equality == (optional)
  • Non-logical symbols (the signature): constant symbols cc, function symbols ff (with arities), predicate/relation symbols PP (with arities).

Terms: every variable and constant is a term; if t1,…,tnt_1,\dots,t_n are terms and ff is nn-ary, f(t1,…,tn)f(t_1,\dots,t_n) is a term. Atomic formulas: P(t1,…,tn)P(t_1,\dots,t_n) and t1=t2t_1 = t_2. Formulas: built from atomics with connectives and quantifiers ∀x φ\forall x\,\varphi, ∃x φ\exists x\,\varphi.

The semantics uses a structure (model) M=(D,I)\mathcal{M} = (D, I) with nonempty domain DD and interpretation II assigning meanings to symbols, plus a variable assignment s:Vars→Ds : \text{Vars} \to D.

4
M,s⊨∀x φ  ⟺  for all d∈D, M,s[x↦d]⊨φ\quad \mathcal{M}, s \models \forall x\, \varphi \iff \text{for all } d \in D,\ \mathcal{M}, s[x \mapsto d] \models \varphi

Derivation hint: the universal quantifier ranges over every element of the domain; s[x↦d]s[x\mapsto d] reassigns xx to dd.

5
M,s⊨∃x φ  ⟺  there exists d∈D with M,s[x↦d]⊨φ\quad \mathcal{M}, s \models \exists x\, \varphi \iff \text{there exists } d \in D \text{ with } \mathcal{M}, s[x \mapsto d] \models \varphi

Derivation hint: ∃x φ\exists x\,\varphi is equivalent to ¬∀x ¬φ\neg \forall x\, \neg\varphi — duality of quantifiers.

TheoremGödel Completeness Theorem (1929)

For first-order logic, semantic entailment and syntactic provability coincide:

6
Γ⊨φ  ⟺  Γ⊢φ\quad \Gamma \models \varphi \iff \Gamma \vdash \varphi

Derivation hint: ⇐ is soundness (proof rules preserve truth); ⇒ is completeness, proved via Henkin's maximal consistent set construction.

TheoremSoundness and Compactness

Soundness: if Γ⊢φ\Gamma \vdash \varphi then Γ⊨φ\Gamma \models \varphi. Compactness: Γ\Gamma has a model iff every finite subset of Γ\Gamma has a model. Compactness follows directly from completeness, since proofs are finite.

Why It Holds / Derivation

ProofSketch of Completeness (Henkin Method)

We prove the contrapositive: if Γ⊬φ\Gamma \not\vdash \varphi, then Γ\Gamma has a model in which φ\varphi is false. 1. Consistency: If Γ⊬φ\Gamma \not\vdash \varphi, then Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} is consistent (no contradiction derivable). 2. Lindenbaum extension: Extend Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} to a maximal consistent set Γ∗\Gamma^* — adding formulas one at a time, keeping consistency, until every formula or its negation is included. 3. Henkin witnesses: Augment the language with new constants and add "witness" axioms: for each ∃x ψ\exists x\,\psi, ensure a constant cc with ψ(c)\psi(c). This guarantees Γ∗\Gamma^* "talks about" enough individuals. 4. Term model construction: Build a model whose domain is the set of closed terms, modulo the equivalence t1∼t2  ⟺  (t1=t2)∈Γ∗t_1 \sim t_2 \iff (t_1 = t_2) \in \Gamma^*. Interpret symbols so that membership in Γ∗\Gamma^* matches truth. 5. Truth Lemma: By induction on formula structure, M⊨ψ  ⟺  ψ∈Γ∗\mathcal{M} \models \psi \iff \psi \in \Gamma^* for all sentences ψ\psi. 6. Conclusion: Since ¬φ∈Γ∗\neg\varphi \in \Gamma^*, the model satisfies Γ\Gamma but not φ\varphi. Hence Γ⊭φ\Gamma \not\models \varphi. ∎

∎
mathematician · Kurt Gödel | 1906–1978

Austrian-American logician whose 1929 doctoral dissertation proved the completeness theorem for first-order logic, establishing that the predicate calculus captures all valid inferences. Just two years later (1931), he delivered his incompleteness theorems, showing that any consistent, recursively axiomatized theory strong enough for arithmetic cannot prove its own consistency and must leave true statements unprovable. These two results — completeness of logic and incompleteness of arithmetical theories — are not contradictory: completeness concerns logical consequence, incompleteness concerns the limits of axiom systems. Gödel later worked on set theory (the constructible universe LL, proving the consistency of the Continuum Hypothesis) and emigrated to Princeton, where he became a close friend of Einstein.

Building Intuition

🧠 Intuition

Think of propositional logic as circuit wiring: variables are switches (on/off), connectives are logic gates, and a tautology is a circuit that outputs "on" no matter how you flip the switches. There are only finitely many switch configurations (2n2^n for nn variables), so truth tables decide everything — this is why propositional logic is decidable. First-order logic is more like describing the rules of a board game without fixing the board. "For every piece there is a square it occupies" is a sentence; a model is a particular board configuration that obeys your rules. The same set of axioms can have wildly different models (e.g., the axioms of group theory hold in Z\mathbb{Z}, in symmetry groups, in Z/2Z\mathbb{Z}/2\mathbb{Z}). Quantifiers let you "scan" an entire domain, but because domains can be infinite, you can no longer just enumerate cases — which is precisely why FOL is undecidable yet still complete.

Figure
The syntax–semantics bridge: provability and truth meet via soundness and completeness
Syntax ⟷ Semantics SYNTAX Axioms + Rules Formal proofs Γ ⊢ φ "φ is provable" SEMANTICS Models / structures Truth assignments Γ ⊨ φ "φ is true in all models" Soundness Completeness Together: Γ ⊢ φ ⟺ Γ ⊨ φ

Worked Examples

ExamplePropositional: Verifying a Tautology by Truth Table

Given: Show that ((p→q)∧p)→q((p \to q) \wedge p) \to q (modus ponens) is a tautology.

Steps: There are 22=42^2 = 4 assignments. Evaluate column by column.

ppqqp→qp\to q(p→q)∧p(p\to q)\wedge pwhole formula
TTTTT
TFFFT
FTTFT
FFTFT

The final column is T in all 4 rows. The antecedent (p→q)∧p(p\to q)\wedge p is only true in row 1, where qq is also true, so the implication never fails.

Answer: ⊨((p→q)∧p)→q(tautology)\boxed{\models ((p \to q) \wedge p) \to q \quad\text{(tautology)}}

ExampleFirst-Order: Counting Models of a Sentence

Given: Consider the signature with one binary relation RR and the sentence

σ=∀x ¬R(x,x) ∧ ∀x∀y (R(x,y)→R(y,x)).\sigma = \forall x\,\neg R(x,x) \ \wedge\ \forall x\forall y\,(R(x,y) \to R(y,x)).

This says RR is irreflexive and symmetric — i.e., the edge relation of a simple undirected graph. Count the number of models on a fixed 3-element domain D={1,2,3}D = \{1,2,3\}.

Steps: 1. Irreflexive symmetric relations on a 3-set ↔ simple undirected graphs on 3 labeled vertices. 2. The number of possible edges is (32)=3\binom{3}{2} = 3. 3. Each edge is independently present or absent: 23=82^3 = 8.

Answer: 8 models\boxed{8 \text{ models}} (the 8 labeled graphs on 3 vertices, from the empty graph to the triangle).

Common Misconceptions

⚠️ Common mistake

Material implication is not causation. The formula p→qp \to q is true whenever pp is false, regardless of any connection between pp and qq. "If 2+2=52+2=5, then the moon is cheese" is true in classical logic because the antecedent is false. Students must resist reading →\to as "causes" or "leads naturally to." Similarly, ¬∀x φ\neg\forall x\,\varphi means "not all," which equals ∃x ¬φ\exists x\,\neg\varphi ("some don't") — not "none."

CounterexampleCompleteness ≠ Decidability

One might assume that because FOL is complete (every valid formula is provable), there must be an algorithm to decide validity. This is false. By the Church–Turing theorem (1936), first-order validity is undecidable: no algorithm can correctly answer "is φ\varphi valid?" for all φ\varphi. The reason completeness doesn't give decidability: a proof search can confirm validity (it will eventually find the proof if one exists) but can run forever on an invalid formula without halting. FOL validity is semi-decidable, not decidable. Propositional logic, by contrast, is decidable via truth tables — but the decision problem (SAT) is NP-complete.

Connections

connection

Propositional logic is the propositional fragment of First-Order Logic and underlies Boolean Algebra, where formulas modulo logical equivalence form a Boolean algebra. Its decision problem, Boolean Satisfiability (SAT), is the canonical NP-complete problem in Computational Complexity Theory. First-order logic is the foundation of Model Theory (the study of structures satisfying theories), Proof Theory (the structure of formal derivations), and Set Theory (ZFC is a first-order theory). Gödel's completeness here contrasts sharply with his Gödel's Incompleteness Theorems, which concern arithmetical theories. The semantics connects to Universal Algebra and the compactness theorem links to Topology via Stone duality.

Real-World Applications

🔬 Where this appears

Historical Development

⏳ History
- 1847 — George Boole publishes The Mathematical Analysis of Logic, algebraizing propositional reasoning.
- 1879 — Gottlob Frege's Begriffsschrift introduces the first complete formal system with quantifiers and bound variables — the birth of predicate logic.
- 1889 — Giuseppe Peano formalizes arithmetic; his notation (∃\exists, ⊃\supset) influences modern symbolism.
- 1910–13 — Whitehead and Russell's Principia Mathematica attempts to derive mathematics from logic, refining the formal apparatus.
- 1915–20 — Löwenheim and Skolem prove the Löwenheim–Skolem theorem on cardinalities of models, foundational to model theory.
- 1928 — Hilbert and Ackermann pose the completeness of predicate logic as an open problem in Grundzüge der theoretischen Logik.
- 1929–30 — Kurt Gödel proves the completeness theorem in his doctoral dissertation.
- 1931 — Gödel's incompleteness theorems reveal the limits of formal arithmetical systems.
- 1936 — Church and Turing independently prove the undecidability of first-order validity (the Entscheidungsproblem).

Subtleties & Limits

open-problem

First-order logic has profound expressive limits revealed by the Löwenheim–Skolem theorem: any first-order theory with an infinite model has models of every infinite cardinality. This yields Skolem's paradox — the countable models of (first-order) set theory contain "uncountable" sets that are externally countable. FOL also cannot express finiteness, connectivity of graphs, or "well-foundedness" as single sentences (provable via compactness). Attempts to strengthen FOL run into trade-offs captured by Lindström's theorem (1969): first-order logic is the maximal logic satisfying both compactness and the (downward) Löwenheim–Skolem property — any genuinely stronger logic must sacrifice one. Second-order logic gains expressiveness (it can characterize N\mathbb{N} up to isomorphism) but loses completeness, compactness, and a recursive proof system. The open frontier concerns which fragments balance expressiveness and decidability — the two-variable fragment, guarded fragments, and finite model theory remain active research areas.

See Also

Boolean Satisfiability (SAT) · Model Theory · Proof Theory · Gödel's Incompleteness Theorems · Computability Theory · Boolean Algebra · Set Theory · Natural Deduction · Sequent Calculus · Description Logic