First-Order Logic and Predicate Calculus

First-Order Logic (FOL), also called predicate calculus, is a formal system that extends propositional logic with quantifiers (∀, ∃), variables, predicates, and functions, allowing precise statements about objects and their relationships. Key result: FOL is sound and complete (Gödel, 1929) — every logically valid formula is provable, and every provable formula is valid. Where it applies: mathematics foundations, automated theorem proving, formal verification, database query languages, and the semantics of natural language. Who/when: Frege (1879), Peirce, Skolem, Hilbert & Ackermann, and Gödel (1929–1930).

First-order logic is the standard formal language for expressing mathematical statements with quantification over individuals. It augments propositional logic — which can only combine atomic truth-bearers with connectives — by introducing a domain of objects, variables ranging over that domain, predicate symbols denoting properties and relations, function symbols, and the two quantifiers "for all" (∀) and "there exists" (∃). Its central importance lies in being expressive enough to formalize essentially all of classical mathematics (via set theory) while remaining tame enough to enjoy a complete proof system. A surprising fact: although FOL is complete, it is also undecidable (Church–Turing, 1936) — there is no algorithm that decides validity in general — and it cannot pin down the natural numbers up to isomorphism (the Löwenheim–Skolem theorems guarantee unintended models of every size).

The Core Insight

Propositional logic treats "Socrates is mortal" as a single opaque atom. First-order logic decomposes it into a predicate applied to a term: $Mortal (socrates)$ . By introducing variables and quantifiers, we can then say things like "every human is mortal," $\forall x (Human (x) \to Mortal (x))$ , and combine such statements to derive new ones. The genius is the clean separation between syntax (what strings count as formulas and proofs) and semantics (what those strings mean over a structure), bridged by the soundness and completeness theorems.

Formal Statement

The Language (Signature) of First-Order Logic

A first-order signature (or vocabulary) $σ$ consists of:

A set of constant symbols $c, d, \dots$ (names for fixed objects).
A set of function symbols $f, g, \dots$ , each with an arity $n \geq 1$ .
A set of predicate (relation) symbols $P, Q, R, \dots$ , each with an arity $n \geq 0$ .

Together with a fixed countable supply of variables $x, y, z, \dots$ , the logical symbols $\neg, \land, \lor, \to, \leftrightarrow$ , the quantifiers $\forall, \exists$ , the equality symbol $=$ (in FOL with equality), and parentheses.

Terms are defined recursively:

t ::= x ∣ c ∣ f (t_{1}, \dots, t_{n})

⟳A term is either a variable, a constant, or a function symbol applied to the right number of previously-built terms; this recursion bottoms out at variables and constants.

Formulas are defined recursively:

φ ::= P (t_{1}, \dots, t_{n}) ∣ t_{1} = t_{2} ∣ \neg φ ∣ (φ \land ψ) ∣ (φ \lor ψ) ∣ (φ \to ψ) ∣ \forall x φ ∣ \exists x φ

⟳Atomic formulas come from applying a predicate to terms or asserting equality; complex formulas are built by connectives and quantifiers. The first two cases (atomic) anchor the recursion.

Free and Bound Variables; Sentences

An occurrence of a variable $x$ is bound if it lies within the scope of a quantifier $\forall x$ or $\exists x$ ; otherwise it is free. A formula with no free variables is a sentence (closed formula). Only sentences have a definite truth value in a structure. The set of free variables of $φ$ is written $FV (φ)$ .

The substitution $φ [t / x]$ replaces every free occurrence of $x$ by the term $t$ , provided $t$ is free for $x$ in $φ$ (no variable of $t$ becomes accidentally captured by a quantifier).

Structures and Satisfaction (Tarskian Semantics)

A structure (model) $M$ for signature $σ$ consists of a nonempty domain $M$ and an interpretation assigning:

to each constant $c$ an element $c^{M} \in M$ ;
to each $n$ -ary function symbol $f$ a function $f^{M} : M^{n} \to M$ ;
to each $n$ -ary predicate $P$ a relation $P^{M} \subseteq M^{n}$ .

A variable assignment $s$ maps variables to elements of $M$ . The value of a term $t^{M} [s]$ and the satisfaction relation $M ⊨ φ [s]$ are defined recursively. The two crucial clauses are:

M ⊨ \forall x φ [s] ⟺ for all a \in M, M ⊨ φ [s (x \mapsto a)]

⟳The universal quantifier is satisfied exactly when the body holds under every possible reassignment of

x

to an element of the domain — the assignment

s (x \mapsto a)

agrees with

s

except it sends

x

a

M ⊨ \exists x φ [s] ⟺ there exists a \in M with M ⊨ φ [s (x \mapsto a)]

⟳The existential is the dual; satisfaction needs only one witness

a

. Note

\exists x φ \equiv \neg\forall x \neg φ

, so [4] follows from [3] and the clause for

\neg

Validity, Satisfiability, Entailment

$φ$ is valid ( $⊨ φ$ ) if $M ⊨ φ$ for every structure and assignment.
$φ$ is satisfiable if some structure satisfies it.
A set of sentences $Γ$ entails $φ$ ( $Γ ⊨ φ$ ) if every model of all of $Γ$ is also a model of $φ$ .

Γ ⊨ φ ⟺ Γ \cup {\neg φ} is unsatisfiable

⟳If every model of

Γ

satisfies

φ

, no model can satisfy both

Γ

and

\neg φ

, and conversely; this is the semantic refutation principle underlying resolution.

Gödel's Completeness Theorem (1929)

For a first-order theory with a sound and complete deductive system $⊢$ (e.g., a Hilbert system or natural deduction):

Γ ⊢ φ ⟺ Γ ⊨ φ

⟳Soundness (

\Rightarrow

) is proved by induction on proof length, checking each inference rule preserves truth. Completeness (

\Leftarrow

) is proved by contraposition: if

Γ ⊬ φ

then

Γ \cup {\neg φ}

is consistent, hence (Henkin construction) has a model, so

Γ ⊭ φ

Compactness and Löwenheim–Skolem

Compactness:

Γ

has a model iff every finite subset of

Γ

has a model. Downward Löwenheim–Skolem: If a countable signature theory has an infinite model, it has a countably infinite model. Upward Löwenheim–Skolem: If it has an infinite model, it has models of every infinite cardinality

κ \geq ∣ σ ∣ + ℵ_{0}

Why It Holds / Derivation

Soundness of First-Order Deduction

We show $Γ ⊢ φ \Rightarrow Γ ⊨ φ$ by induction on the length of the derivation, using a natural-deduction-style system.

Step 1 (Base — assumptions/axioms). If

φ \in Γ

, then trivially every model of

Γ

satisfies

φ

. Logical axioms (e.g.,

φ \to (ψ \to φ)

) are tautologies, valid in every structure. Step 2 (Modus ponens). Suppose by induction

Γ ⊨ ψ

and

Γ ⊨ (ψ \to φ)

. Take any model

M ⊨ Γ

. Then

M ⊨ ψ

and

M ⊨ ψ \to φ

, so by the semantic clause for

\to

M ⊨ φ

. Hence

Γ ⊨ φ

. Step 3 (Universal generalization). Suppose

Γ ⊨ φ

and

x \in / FV (Γ)

; we must show

Γ ⊨ \forall x φ

. Let

M ⊨ Γ

under assignment

s

. For any

a \in M

, since

x

is not free in

Γ

M ⊨ Γ

also under

s (x \mapsto a)

, so

M ⊨ φ [s (x \mapsto a)]

. By [3],

M ⊨ \forall x φ [s]

. Step 4 (Universal instantiation). From

\forall x φ

infer

φ [t / x]

for

t

free for

x

. If

M ⊨ \forall x φ

, then

φ

holds for every domain element, in particular for

t^{M} [s]

, which (by the substitution lemma) is what

φ [t / x]

asserts.

Each rule preserves validity over models of $Γ$ ; by induction the full derivation does. $■$

Sketch of Completeness via Henkin Construction

Goal: a consistent $Γ$ has a model.

Step 1. Expand the language with a countable set of fresh witness constants. For each formula

\exists x φ

, add a Henkin axiom

\exists x φ \to φ [c / x]

with a new constant

c

. The resulting theory remains consistent. Step 2. Extend

Γ

to a maximal consistent set

Γ^{*}

(Lindenbaum's lemma): every sentence or its negation is in

Γ^{*}

, and

Γ^{*}

is deductively closed. Step 3. Build the term model: the domain is the set of closed terms, quotiented by the equivalence

t \sim u ⟺ (t = u) \in Γ^{*}

. Interpret symbols by their syntactic action on terms. Step 4 (Truth lemma). Prove by induction on formula structure that

M ⊨ φ ⟺ φ \in Γ^{*}

. The Henkin axioms make the existential case work: a witness constant supplies the required domain element. Step 5. Since

Γ \subseteq Γ^{*}

M ⊨ Γ

. Thus consistency implies satisfiability; contrapositively,

Γ ⊨ φ \Rightarrow Γ ⊢ φ

■

Kurt Gödel | 1906–1978

Born in Brünn (now Brno), Gödel proved the completeness theorem for first-order logic in his 1929 doctoral dissertation at the University of Vienna, settling a problem Hilbert and Ackermann had posed. Just two years later he overturned the foundationalist program with his incompleteness theorems, showing that any consistent, sufficiently strong, recursively axiomatized theory cannot prove its own consistency and leaves true arithmetical sentences unprovable. The contrast is essential: completeness is about the logic (FOL captures all valid consequences), while incompleteness is about particular theories (no axiom set fully captures arithmetic). Gödel later emigrated to Princeton, became a close friend of Einstein, and made deep contributions to set theory (the constructible universe $L$ and the consistency of CH and AC) and even general relativity.

Building Intuition

Think of FOL as a precise grammar for "objects and their relationships." A structure is a world: a bag of objects together with facts about which properties they have and which relations hold among them. A formula with free variables is like a sentence with blanks — "___ loves ___" — that becomes true or false only once you fill the blanks with specific objects (the assignment $s$ ). The quantifiers automate the filling: $\forall x$ says "try every object in the blank and it always works," while $\exists x$ says "some object makes it work."

The key conceptual leap from propositional logic is quantifier scope and variable binding. The same letter $x$ can mean different things in different scopes, exactly like local variables in a programming function. Capture-avoiding substitution is the logical analogue of safe variable renaming. And the order of quantifiers matters profoundly: " $\forall x \exists y (x < y)$ " (every number has a bigger one — true for integers) is wholly different from " $\exists y \forall x (x < y)$ " (one number bigger than all — false).

Quantifier order: ∀x∃y vs ∃y∀x over a domain

Worked Examples

Translating and Evaluating a Sentence over the Integers

Given: Domain

M = Z

, with the usual interpretation of

<

and

+

. Consider the sentence

φ : \forall x \exists y (x + y = 0) .

Step 1 — Read the structure. The quantifiers range over all integers;

+

is integer addition;

=

is equality. Step 2 — Verify the body for arbitrary $x$ . Fix any integer

a

(the value assigned to

x

). We need a

b

with

a + b = 0

. Step 3 — Supply a witness. Take

b = - a

, which exists in

Z

. Then

a + (- a) = 0

holds. By clause [4],

\exists y (x + y = 0)

is satisfied under

x \mapsto a

. Step 4 — Generalize. Since

a

was arbitrary, by clause [3] the universal statement holds. Boxed answer:

Z ⊨ \forall x \exists y (x + y = 0) (TRUE)

Contrast: over $N$ this is false (no witness for $x = 1$ , since $- 1 \in / N$ ) — demonstrating that truth depends on the structure.

A Formal Natural-Deduction Proof

Given: Prove

\forall x (P (x) \to Q (x)), \exists x P (x) ⊢ \exists x Q (x) .

Step 1 — Existential elimination. From

\exists x P (x)

, introduce a fresh constant

a

(not occurring elsewhere) with the assumption

P (a)

. Step 2 — Universal instantiation. From

\forall x (P (x) \to Q (x))

infer

P (a) \to Q (a)

by substituting

a

for

x

(rule from proof Step 4 above). Step 3 — Modus ponens. From

P (a)

and

P (a) \to Q (a)

derive

Q (a)

. Step 4 — Existential introduction. From

Q (a)

derive

\exists x Q (x)

. Step 5 — Discharge. Since

\exists x Q (x)

contains no occurrence of the fresh constant

a

, the

\exists

-elimination box closes legitimately, yielding

\exists x Q (x)

from the original premises. Boxed answer:

\forall x (P (x) \to Q (x)), \exists x P (x) ⊢ \exists x Q (x)

The eigenvariable condition (fresh $a$ not in conclusion or premises) is what makes Step 5 valid; violating it leads to fallacies.

Common Misconceptions

Quantifier scope and the eigenvariable condition

A very common error is treating $\forall x \exists y$ and $\exists y \forall x$ as interchangeable — they are not (see the diagram above). Another frequent mistake is illegitimate substitution that captures variables: substituting $y$ for $x$ in $\exists y (x \neq = y)$ would wrongly yield $\exists y (y \neq = y)$ , a falsehood, because $t$ was not free for $x$ . Always rename bound variables first. Finally, in natural deduction, the eigenvariable / fresh-constant condition on $\forall$ -introduction and $\exists$ -elimination is not optional bookkeeping — dropping it lets you "prove" $\exists x P (x) ⊢ \forall x P (x)$ , which is invalid.

FOL cannot express "finitely many" or define the standard naturals

One might hope FOL can characterize the natural numbers. It cannot. By compactness, add to the Peano axioms a new constant $c$ together with the infinitely many sentences $c \neq = 0, c \neq = S 0, c \neq = S S 0, \dots$ . Every finite subset is satisfiable (interpret $c$ as a large enough standard number), so by compactness the whole set has a model — a nonstandard model of arithmetic containing an "infinite" element $c$ unreachable from $0$ by finitely many successors. Likewise, "there are finitely many objects" is not expressible by any single first-order sentence, nor is the notion of a well-ordering or connectedness of a graph. These limitations motivate second-order logic and infinitary logics.

Connections

First-order logic sits between weaker and stronger systems. It strictly extends Propositional Logic by adding quantifiers and internal structure to atomic statements; conversely, the propositional fragment is recovered by treating $0$ -ary predicates as proposition letters. Above it lies Second-Order Logic, which quantifies over predicates and sets, gaining expressive power (it can characterize $N$ categorically) but losing completeness and compactness. FOL is the working language of Zermelo–Fraenkel Set Theory, in which virtually all mathematics is formalized, and its metatheory connects to Model Theory (study of structures and definability) and Computability Theory (via the undecidability of validity). The deductive side links to Natural Deduction and Resolution, the backbone of automated provers.

Real-World Applications

Automated theorem proving: Systems like Vampire, E, and Prover9 use first-order resolution and superposition to prove mathematical and verification goals automatically.
Formal verification of hardware/software: SMT solvers (Z3, CVC5) decide fragments of FOL with theories (arithmetic, arrays) to verify circuits, compilers, and concurrent protocols.
Relational databases: SQL's core is essentially the FOL fragment relational calculus; Codd's theorem equates it with relational algebra, so every safe FOL query corresponds to an executable query plan.
Knowledge representation / the Semantic Web: Description logics underpinning OWL are decidable fragments of FOL used in ontologies (e.g., medical SNOMED CT, Google's Knowledge Graph).
Logic programming: Prolog computes with Horn-clause subsets of FOL via SLD-resolution, used in expert systems and natural-language parsing.
Compiler and program analysis: Hoare-logic verification conditions and separation-logic proofs are discharged as FOL entailments.
Formal mathematics libraries: Proof assistants (Mizar, Metamath, parts of Isabelle) encode theorems as first-order or higher-order derivations checkable by machine.

Historical Development

1879 — Gottlob Frege publishes Begriffsschrift, introducing quantifiers and bound variables — the birth of modern predicate logic (in a two-dimensional notation).
1885 — Charles Sanders Peirce and his student O. H. Mitchell independently develop quantifier notation; Peirce coins much of the relational vocabulary.
1910–1913 — Whitehead and Russell's Principia Mathematica systematizes logic and attempts to derive mathematics from it.
1915–1920 — Leopold Löwenheim (1915) and Thoralf Skolem (1920) prove the Löwenheim–Skolem theorems, exposing the existence of unintended models.
1928 — Hilbert and Ackermann's Grundzüge der theoretischen Logik cleanly isolates first-order logic and poses the completeness question.
1929–1930 — Kurt Gödel proves the completeness theorem in his dissertation; published 1930.
1931 — Gödel's incompleteness theorems show no recursive consistent theory of arithmetic is complete.
1936 — Alonzo Church and Alan Turing independently prove the undecidability of first-order validity (the Entscheidungsproblem has no solution).
1949–1965 — Henkin's elegant completeness proof (1949), Robinson's resolution (1965) launching automated deduction.

Subtleties & Limits

First-order logic is undecidable in general (no algorithm decides validity), yet many fragments are decidable, and the precise boundary is a rich research area: the two-variable fragment $FO^{2}$ is decidable, as is the guarded fragment, while $FO^{3}$ is undecidable. Determining the exact complexity of important fragments (e.g., extensions with counting quantifiers, transitive closure, or modal/temporal operators) remains active. Open and hard practical questions include: scalable decision procedures for combined theories (SMT), the precise expressive trade-offs of description logics for the Semantic Web, and the long-standing program of finite model theory — where compactness and completeness fail and whose central question, the existence of a logic capturing exactly the polynomial-time queries (Chandra–Harel / Gurevich conjecture), is intimately tied to P versus NP.