Propositional and First-Order Logic

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. Propositional logic is the study of how the truth value of compound statements depends on the truth values of their atomic components, joined by truth-functional connectives. First-order logic (FOL), also called predicate logic, extends this by quantifying over individuals in a domain, allowing statements like "every number has a successor." Together they form the backbone of mathematical reasoning, the semantics of programming and databases, and the logical foundations of formal proof. They matter because nearly all of modern mathematics can be expressed within first-order logic over set theory (ZFC). A surprising fact: first-order logic is complete (every valid formula is provable) yet undecidable (no algorithm can determine validity in general) — completeness and decidability are independent properties.

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

Propositional Language

The language of propositional logic is built from:

A countable set of propositional variables $p, q, r, \dots$
Connectives: $\neg$ (not), $\land$ (and), $\lor$ (or), $\to$ (implies), $\leftrightarrow$ (iff)
Parentheses for grouping.

Well-formed formulas (wffs) are defined recursively: every variable is a wff; if

φ, ψ

are wffs, so are

\neg φ

(φ \land ψ)

(φ \lor ψ)

(φ \to ψ)

(φ \leftrightarrow ψ)

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

v (\neg φ) = T ⟺ v (φ) = F

⟳negation flips the truth value; this is the defining truth-table row for ¬.

v (φ \land ψ) = T ⟺ v (φ) = T and v (ψ) = T

⟳conjunction is true only when both conjuncts hold — the AND truth table.

v (φ \to ψ) = T ⟺ v (φ) = F or v (ψ) = T

⟳material implication is false only in the one case T→F; equivalently

φ \to ψ \equiv \neg φ \lor ψ

Tautology, Satisfiability, Entailment

A formula $φ$ is a tautology ( $⊨ φ$ ) if $v (φ) = T$ for every assignment $v$ .
$φ$ is satisfiable if some $v$ makes it true.
A set $Γ$ entails $φ$ ( $Γ ⊨ φ$ ) if every $v$ satisfying all of $Γ$ also satisfies $φ$ .

First-Order Language

A first-order language $L$ consists of:

Variables $x, y, z, \dots$
Logical symbols: connectives, quantifiers $\forall, \exists$ , equality $=$ (optional)
Non-logical symbols (the signature): constant symbols $c$ , function symbols $f$ (with arities), predicate/relation symbols $P$ (with arities).

Terms: every variable and constant is a term; if

t_{1}, \dots, t_{n}

are terms and

f

n

-ary,

f (t_{1}, \dots, t_{n})

is a term. Atomic formulas:

P (t_{1}, \dots, t_{n})

and

t_{1} = t_{2}

. Formulas: built from atomics with connectives and quantifiers

\forall x φ

\exists x φ

The semantics uses a structure (model) $M = (D, I)$ with nonempty domain $D$ and interpretation $I$ assigning meanings to symbols, plus a variable assignment $s : Vars \to D$ .

M, s ⊨ \forall x φ ⟺ for all d \in D, M, s [x \mapsto d] ⊨ φ

⟳the universal quantifier ranges over every element of the domain;

s [x \mapsto d]

reassigns

x

d

M, s ⊨ \exists x φ ⟺ there exists d \in D with M, s [x \mapsto d] ⊨ φ

⟳

\exists x φ

is equivalent to

\neg\forall x \neg φ

— duality of quantifiers.

Gödel Completeness Theorem (1929)

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

Γ ⊨ φ ⟺ Γ ⊢ φ

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

Soundness and Compactness

Soundness: if

Γ ⊢ φ

then

Γ ⊨ φ

. Compactness:

Γ

has a model iff every finite subset of

Γ

has a model. Compactness follows directly from completeness, since proofs are finite.

Why It Holds / Derivation

Sketch of Completeness (Henkin Method)

We prove the contrapositive: if $Γ \neq ⊢ φ$ , then $Γ$ has a model in which $φ$ is false.

Consistency: If $Γ \neq ⊢ φ$ , then $Γ \cup {\neg φ}$ is consistent (no contradiction derivable).

Lindenbaum extension: Extend $Γ \cup {\neg φ}$ to a maximal consistent set $Γ^{*}$ — adding formulas one at a time, keeping consistency, until every formula or its negation is included.

Henkin witnesses: Augment the language with new constants and add "witness" axioms: for each $\exists x ψ$ , ensure a constant $c$ with $ψ (c)$ . This guarantees $Γ^{*}$ "talks about" enough individuals.

Term model construction: Build a model whose domain is the set of closed terms, modulo the equivalence $t_{1} \sim t_{2} ⟺ (t_{1} = t_{2}) \in Γ^{*}$ . Interpret symbols so that membership in $Γ^{*}$ matches truth.

Truth Lemma: By induction on formula structure, $M ⊨ ψ ⟺ ψ \in Γ^{*}$ for all sentences $ψ$ .

Conclusion: Since $\neg φ \in Γ^{*}$ , the model satisfies $Γ$ but not $φ$ . Hence $Γ \neq ⊨ φ$ . ∎

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 $L$ , proving the consistency of the Continuum Hypothesis) and emigrated to Princeton, where he became a close friend of Einstein.

Building 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 ( $2^{n}$ for $n$ 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$ , in symmetry groups, in $Z /2 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.

The syntax–semantics bridge: provability and truth meet via soundness and completeness

Worked Examples

Propositional: Verifying a Tautology by Truth Table

Given: Show that

((p \to q) \land p) \to q

(modus ponens) is a tautology. Steps: There are

2^{2} = 4

assignments. Evaluate column by column.

| $p$ | $q$ | $p \to q$ | $(p \to q) \land p$ | whole formula | |---|---|---|---|---| | T | T | T | T | T | | T | F | F | F | T | | F | T | T | F | T | | F | F | T | F | T |

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

Answer:

⊨ ((p \to q) \land p) \to q (tautology)

First-Order: Counting Models of a Sentence

Given: Consider the signature with one binary relation

R

and the sentence

σ = \forall x \neg R (x, x) \land \forall x \forall y (R (x, y) \to R (y, x)) .

This says

R

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}

. Steps:

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

Answer:

8 models

(the 8 labeled graphs on 3 vertices, from the empty graph to the triangle).

Common Misconceptions

Material implication is not causation. The formula

p \to q

is true whenever

p

is false, regardless of any connection between

p

and

q

. "If

2 + 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,

\neg\forall x φ

means "not all," which equals

\exists x \neg φ

("some don't") — not "none."

Completeness ≠ 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 $φ$ valid?" for all $φ$ . 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

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

Digital circuit design: Propositional logic models combinational logic; minimization via Karnaugh maps and Boolean algebra reduces gate counts in CPUs and ASICs.
SAT/SMT solvers (MiniSat, Z3): Industrial tools that decide propositional and quantifier-free first-order satisfiability, used in hardware verification at Intel and AMD.
Relational databases: SQL queries correspond to first-order formulas over the database schema; the relational calculus is first-order logic restricted to finite models.
Automated theorem proving: Systems like Vampire, E, and Prover9 search for first-order proofs; used to verify the Robbins conjecture (EQP, 1996).
Formal verification of software: Tools like Dafny, Coq, and Isabelle use logical specifications to prove programs correct (e.g., the seL4 verified microkernel).
Knowledge representation in AI: Description logics (decidable fragments of FOL) underpin the Web Ontology Language (OWL) and the Semantic Web.
Prolog and logic programming: Computation as proof search over Horn clauses, a fragment of first-order logic.

Historical Development

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

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$ 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.