Predicate Logic

What It Adds Over Propositional Logic

Propositional logic treats whole sentences as atoms. It cannot say "every natural number has a successor"; it can only treat that English sentence as a single propositional letter. Predicate logic, also called first-order logic, breaks the atom open and gives us:

1. Terms: variables ($x, y, z$), constants ($a, b, 0$), and function symbols ($f(x, y)$, $S(x)$, $x + y$). Terms denote objects in the domain of discussion.
2. Predicates: relation symbols ($P(x)$, $R(x, y)$, $=$). Predicates denote properties and relations.
3. Quantifiers: the universal $\forall$ and the existential $\exists$. Quantifiers say for all or there exists.

The combination is enough to express most of mathematics. Statements like "every prime greater than 2 is odd" or "there exists an irrational number whose square is rational" go directly into first-order logic over arithmetic. Whether everything in mathematics is expressible in first-order logic is a separate, more subtle question, taken up below.

This page assumes What Is Logic?, Validity vs Soundness, Syntax vs Semantics in Formal Systems, and Propositional Logic. The construction of predicate logic uses every concept introduced in those pages. If anything below is unfamiliar, read them first.

Notation: Terms, Atomic Formulas, Quantified Formulas

The alphabet of first-order logic over a signature $\Sigma$:

• A countable set of variables: $x, y, z, x_1, x_2, \ldots$.
• The signature's constant symbols: $c, a, 0, 1, \ldots$.
• The signature's function symbols, each with an arity: $f, g, +, \times, S, \ldots$.
• The signature's predicate symbols, each with an arity: $P, Q, R, =, <, \ldots$.
• Logical connectives from propositional logic: $\neg, \land, \lor, \to, \leftrightarrow$.
• Quantifiers: $\forall$ (universal) and $\exists$ (existential).
• Auxiliary punctuation: parentheses, comma.

The signature is what fixes which "language" we are working in. Arithmetic uses $\Sigma_{\text{arith}} = \{0, S, +, \times\}$ plus equality. Set theory uses just $\{\in\}$ plus equality. Group theory uses $\{e, \cdot, ^{-1}\}$. Different signatures, same logical machinery on top.

The formation rules are recursive.

Terms:

1. Every variable is a term.
2. Every constant symbol is a term.
3. If $f$ is an $n$-ary function symbol and $t_1, \ldots, t_n$ are terms, then $f(t_1, \ldots, t_n)$ is a term.

Atomic formulas:

4. If $P$ is an $n$-ary predicate symbol and $t_1, \ldots, t_n$ are terms, then $P(t_1, \ldots, t_n)$ is an atomic formula.
5. If $t_1$ and $t_2$ are terms, then $t_1 = t_2$ is an atomic formula (if equality is included in the signature).

Formulas:

6. Every atomic formula is a formula.
7. If $\varphi$ is a formula, so is $\neg \varphi$.
8. If $\varphi$ and $\psi$ are formulas, so are $(\varphi \land \psi)$, $(\varphi \lor \psi)$, $(\varphi \to \psi)$, $(\varphi \leftrightarrow \psi)$.
9. If $\varphi$ is a formula and $x$ is a variable, then $\forall x\, \varphi$ and $\exists x\, \varphi$ are formulas.
10. Nothing else is a formula.

A sentence is a formula with no free variables (every variable is bound by a quantifier in whose scope it appears).

By these rules:

• $\forall x\, P(x)$ is a sentence: every $x$ in the domain has property $P$.
• $\exists x\, (P(x) \land Q(x))$ is a sentence: some $x$ has both $P$ and $Q$.
• $P(x)$ alone is a formula but not a sentence: $x$ is free.
• $\forall x\, \exists y\, R(x, y)$ is a sentence: for every $x$, there is some $y$ standing in relation $R$ to it.

Tarski-Style Semantics: Satisfaction in a Structure

A first-order formula does not have a truth value on its own. It has a truth value relative to a structure. This is the central conceptual move.

A structure $\mathcal{M}$ for signature $\Sigma$ consists of:

• A non-empty domain $D$ (the universe of discourse).
• For each constant symbol $c$, an element $c^{\mathcal{M}} \in D$.
• For each $n$-ary function symbol $f$, a function $f^{\mathcal{M}}: D^n \to D$.
• For each $n$-ary predicate symbol $P$, a relation $P^{\mathcal{M}} \subseteq D^n$.
• (When equality is in the signature) the relation $=^{\mathcal{M}}$ is identity on $D$.

An assignment is a function $s$ from variables to elements of $D$. The assignment is needed to evaluate formulas with free variables; for sentences it is irrelevant.

Tarski's recursive definition of satisfaction. We write $\mathcal{M}, s \models \varphi$ to mean the structure $\mathcal{M}$ under assignment $s$ satisfies $\varphi$.¹

For atomic formulas:

• $\mathcal{M}, s \models P(t_1, \ldots, t_n)$ iff $(t_1^{\mathcal{M}, s}, \ldots, t_n^{\mathcal{M}, s}) \in P^{\mathcal{M}}$.
• $\mathcal{M}, s \models t_1 = t_2$ iff $t_1^{\mathcal{M}, s}$ and $t_2^{\mathcal{M}, s}$ are the same element of $D$.

For propositional connectives:

• $\mathcal{M}, s \models \neg \varphi$ iff not $\mathcal{M}, s \models \varphi$.
• $\mathcal{M}, s \models \varphi \land \psi$ iff $\mathcal{M}, s \models \varphi$ and $\mathcal{M}, s \models \psi$.
• (etc., as in propositional logic)

For quantifiers:

• $\mathcal{M}, s \models \forall x\, \varphi$ iff for every $d \in D$, $\mathcal{M}, s[x \mapsto d] \models \varphi$.
• $\mathcal{M}, s \models \exists x\, \varphi$ iff for some $d \in D$, $\mathcal{M}, s[x \mapsto d] \models \varphi$.

Here $s[x \mapsto d]$ denotes the assignment that agrees with $s$ everywhere except at $x$, where it sends $x$ to $d$.

A sentence $\varphi$ is true in $\mathcal{M}$ (write $\mathcal{M} \models \varphi$) iff $\mathcal{M}, s \models \varphi$ for any (equivalently, every) assignment $s$. The choice of $s$ does not matter for sentences because none of their variables are free.

A set of sentences $\Gamma$ semantically entails $\varphi$, written $\Gamma \models \varphi$, iff every structure that satisfies all of $\Gamma$ also satisfies $\varphi$.

A Worked Example

Take a tiny structure $\mathcal{M}$ with domain $D = \{0, 1, 2\}$, no constants, and one binary predicate $<$ interpreted as the standard ordering on $\{0, 1, 2\}$:

$<^{\mathcal{M}} = \{(0, 1), (0, 2), (1, 2)\}$.

Evaluate the sentence $\forall x\, \exists y\, x < y$ in $\mathcal{M}$.

Reading: "for every $x$, there is some $y$ such that $x < y$."

Check:

• $x = 0$: is there $y$ with $0 < y$? Yes: $y = 1$ works (also $y = 2$).
• $x = 1$: is there $y$ with $1 < y$? Yes: $y = 2$.
• $x = 2$: is there $y$ with $2 < y$? No: no element of $D$ is greater than 2.

So $\mathcal{M} \not\models \forall x\, \exists y\, x < y$. The sentence is false in this structure. It would be true in $(\mathbb{N}, <)$ because the natural numbers have no maximum, but it is false in the bounded $\{0, 1, 2\}$.

Now evaluate $\exists y\, \forall x\, x < y$ in the same $\mathcal{M}$.

Reading: "there is some $y$ such that for every $x$, $x < y$."

Check whether any $y \in D$ is greater than every element. None: 0 is not greater than 1 or 2; 1 is not greater than 2; 2 is not greater than itself (since the ordering is strict). So $\mathcal{M} \not\models \exists y\, \forall x\, x < y$.

The two sentences differ only in the order of the quantifiers. Both are false in this structure, but they are not the same sentence. In general, $\forall x\, \exists y\, R(x, y)$ does not entail $\exists y\, \forall x\, R(x, y)$, and vice versa. The former says everyone has a partner; the latter says someone is everyone's partner. The order matters.

The Natural-Deduction Quantifier Rules

Predicate logic extends propositional natural deduction with introduction and elimination rules for the quantifiers.

Universal quantifier:

• $\forall$-introduction: if you can derive $\varphi(c)$ for an arbitrary fresh constant $c$ that does not appear elsewhere in your assumptions, then you may infer $\forall x\, \varphi(x)$.
• $\forall$-elimination (universal instantiation): from $\forall x\, \varphi(x)$, infer $\varphi(t)$ for any term $t$.

Existential quantifier:

• $\exists$-introduction (existential generalization): from $\varphi(t)$, infer $\exists x\, \varphi(x)$.
• $\exists$-elimination: from $\exists x\, \varphi(x)$, assume $\varphi(c)$ for a fresh constant $c$; if you can derive some conclusion $\psi$ (not mentioning $c$), discharge the assumption and infer $\psi$.

The "fresh constant" condition in $\forall$-introduction and $\exists$-elimination is the classic technical hurdle for students. It captures the informal idea: to prove "for all," show it for an arbitrary individual; to use "there exists," reason about some individual whose specific identity does not enter the conclusion.

A worked derivation. To show $\forall x\, (P(x) \to Q(x)),\, \forall x\, P(x) \vdash \forall x\, Q(x)$:

1.  ∀x (P(x) → Q(x))           premise
2.  ∀x P(x)                    premise
3.  P(c) → Q(c)                ∀-elim from 1, with c fresh
4.  P(c)                       ∀-elim from 2
5.  Q(c)                       modus ponens on 3, 4
6.  ∀x Q(x)                    ∀-intro on 5 (c fresh, not in 1 or 2)

The derivation is a syntactic proof. Combined with the soundness theorem below, it shows the conclusion is true in every structure satisfying both premises.

Soundness, Completeness, Undecidability

Three results that together characterize first-order logic. The first two are good news; the third is bad news.

Soundness theorem. If $\Gamma \vdash \varphi$, then $\Gamma \models \varphi$. Anything provable in the natural-deduction system is true in every model of the premises. The proof is by induction on the structure of derivations: each rule is shown to preserve truth in every structure.

Completeness theorem (Gödel 1929/30).² If $\Gamma \models \varphi$, then $\Gamma \vdash \varphi$. Anything semantically valid has a syntactic proof. This is far harder than soundness; the standard proof uses Henkin's method (1949), constructing a witnessing model from a maximally consistent extension of $\neg \varphi$.

Undecidability theorem (Church 1936; Turing 1936). There is no algorithm that, given an arbitrary first-order sentence $\varphi$, decides whether $\models \varphi$. The set of valid first-order sentences is recursively enumerable (we can list them by enumerating proofs) but not recursive (we cannot decide membership in finite time for arbitrary inputs).

The contrast with propositional logic is sharp:

Predicate logic is the gold standard of formal mathematical reasoning, but the cost of the expressive jump from propositional logic is decidability.

What First-Order Logic Cannot Express

First-order logic is expressive enough for most working mathematics, but several intuitive concepts escape it.

Finiteness. "There are only finitely many $x$ such that $P(x)$" cannot be expressed in first-order logic. By the compactness theorem (a consequence of completeness), if a first-order theory has arbitrarily large finite models, it has an infinite model. A first-order theory cannot pin down "finite" exactly.

Continuity (in the standard formulation). The standard analytic definition of a continuous function uses second-order quantification over neighborhoods. First-order analysis can express continuity in a single signature with carefully chosen primitives, but the natural mathematical statement requires second-order machinery.

Identity-of-indiscernibles in the strong sense. "For any property, $a$ has it iff $b$ has it" requires quantifying over properties, which is second-order. First-order identity is a primitive relation between objects, not a quantification over their predicates.

The natural numbers up to isomorphism. First-order Peano arithmetic has non-standard models containing infinite-but-finite-looking elements. Pinning down $\mathbb{N}$ uniquely requires second-order induction.

The standard escape is higher-order logic, which adds quantification over predicates and functions. Higher-order logic is more expressive but loses Gödel completeness: there are higher-order semantic validities that are not provable in any sound, recursively-axiomatizable system. Choosing first-order versus higher-order is therefore a genuine trade-off, not a question of one being uniformly better.

Common Confusions

Confusion 1: $\forall \exists$ vs $\exists \forall$. The most common quantifier mistake. $\forall x\, \exists y\, R(x, y)$ says "for each $x$, some $y$ depends on it." $\exists y\, \forall x\, R(x, y)$ says "there is one fixed $y$ that works for every $x$." The second implies the first; the first does not imply the second. Everyone has a mother (universal-existential) does not entail someone is everyone's mother (existential-universal).

Confusion 2: scope. $\forall x\, P(x) \to Q(x)$ is ambiguous in informal notation. Strictly, by precedence, $\forall x$ scopes only over $P(x)$, so the formula reads $(\forall x\, P(x)) \to Q(x)$ with $x$ free in the consequent. The intended reading is usually $\forall x\, (P(x) \to Q(x))$, with parentheses making the scope explicit. When in doubt, parenthesize.

Confusion 3: completeness vs incompleteness. Gödel proved both a completeness theorem (1929/30, for first-order logic) and incompleteness theorems (1931, for formal arithmetic). They are not contradictory. First-order logic itself is complete: every semantic validity has a syntactic proof. Theories in first-order logic, like first-order Peano arithmetic, can be incomplete: there are sentences in their language that are neither provable nor refutable from the theory's axioms. The distinction is between the logic and a particular theory expressed in it.

Confusion 4: recursive vs recursively enumerable. First-order validity is recursively enumerable but not recursive. We can list valid sentences by enumerating proofs, but given an arbitrary sentence, there is no general algorithm to decide whether it is valid in finite time. If the sentence is valid, search will eventually find a proof; if it is invalid, search may run forever without ever discovering that fact.

Three Exercises

Exercise 1. Translate the following English statements into first-order logic, using a signature with constant $0$, function symbol $S$ (successor), and binary predicate $<$:

(a) Zero is the smallest natural number. (b) Every natural number has a successor. (c) For every natural number, there is a larger natural number. (d) No natural number is its own successor.

Exercise 2. Decide whether the inference is valid. If valid, give a natural-deduction derivation. If invalid, give a structure showing the premises true and the conclusion false.

Premise 1: $\forall x\, (P(x) \to Q(x))$. Premise 2: $\exists x\, P(x)$. Conclusion: $\exists x\, Q(x)$.

Exercise 3. Consider the structure $\mathcal{M}$ with domain $D = \{a, b\}$, unary predicate $P$ with $P^{\mathcal{M}} = \{a\}$, and binary predicate $R$ with $R^{\mathcal{M}} = \{(a, b), (b, a)\}$. Evaluate each sentence in $\mathcal{M}$:

(a) $\forall x\, P(x)$. (b) $\exists x\, \forall y\, R(x, y)$. (c) $\forall x\, \exists y\, R(x, y)$. (d) $\forall x\, (P(x) \lor \exists y\, R(x, y))$.

Answers

Answer 1:

(a) $\forall x\, (x = 0 \lor 0 < x)$. This says every $x$ is either zero or greater than zero. (Equivalently: $\forall x\, \neg (x < 0)$, depending on whether $<$ is strict.)

(b) $\forall x\, \exists y\, y = S(x)$. Every $x$ has some $y$ that is its successor. If we treat $S$ as a total function symbol, this is automatic from the syntax: $S(x)$ is always a term, denoting an element of the domain. The interesting first-order statement is more often: $\forall x\, x < S(x)$, expressing the relation between successor and ordering.

(c) $\forall x\, \exists y\, x < y$. The unboundedness statement.

(d) $\forall x\, \neg (S(x) = x)$, equivalently $\forall x\, S(x) \neq x$.

Answer 2: valid. Derivation:

1.  ∀x (P(x) → Q(x))           premise
2.  ∃x P(x)                    premise
3.  | P(c)                     assumption (for ∃-elim)
4.  | P(c) → Q(c)              ∀-elim from 1
5.  | Q(c)                     modus ponens on 3, 4
6.  | ∃x Q(x)                  ∃-intro on 5
7.  ∃x Q(x)                    ∃-elim on 2, discharging 3

The fresh-constant convention is satisfied: $c$ does not appear in 1 or 2.

Answer 3.

(a) $\forall x\, P(x)$: false. $b \in D$ but $b \notin P^{\mathcal{M}}$. The sentence requires every domain element to be in $P$.

(b) $\exists x\, \forall y\, R(x, y)$: false. For $x = a$: we need $R(a, a)$ and $R(a, b)$. But $(a, a) \notin R^{\mathcal{M}}$, only $(a, b) \in R^{\mathcal{M}}$. For $x = b$: we need $R(b, a)$ and $R(b, b)$. $(b, a) \in R^{\mathcal{M}}$ but $(b, b) \notin R^{\mathcal{M}}$. Neither $x$ works.

(c) $\forall x\, \exists y\, R(x, y)$: true. For $x = a$: $y = b$ works since $(a, b) \in R^{\mathcal{M}}$. For $x = b$: $y = a$ works since $(b, a) \in R^{\mathcal{M}}$.

(d) $\forall x\, (P(x) \lor \exists y\, R(x, y))$: true. For $x = a$: $P(a)$ holds. For $x = b$: $P(b)$ does not hold, but $\exists y\, R(b, y)$ holds (with $y = a$).

Note that (b) and (c) differ only in quantifier order, and they have different truth values in the same structure. This is the canonical $\forall \exists$ vs $\exists \forall$ distinction in action.

Where Predicate Logic Lives in Practice

Three concrete uses.

Mathematical practice. Modern mathematical proofs are, with rare exceptions, formalizable in first-order logic plus set-theoretic axioms (typically ZFC). First-order logic is the default substrate of working mathematicians whether or not they consciously think in those terms. The Mizar, Metamath, and Lean libraries are large-scale formal-mathematics projects that demonstrate this concretely.

Database theory and query languages. First-order logic is essentially equivalent in expressive power to relational algebra, the formal foundation of relational databases. SQL queries can be translated to first-order formulas over the database's relations. Codd's seminal database papers (1970-1972) made this connection explicit.

Knowledge representation in AI. Description logics, OWL, and many classical AI knowledge bases use restricted fragments of first-order logic for tractability. The full first-order language is too expressive (undecidable) for general inference; carefully chosen sublanguages preserve decidability while keeping enough expressiveness for the domain.

The general lesson: first-order logic is the expressive target for many practical systems, with restrictions added to recover decidability or efficiency.

Prerequisites and Next Pages

• Prerequisites: What Is Logic?, Validity vs Soundness, Syntax vs Semantics in Formal Systems, Propositional Logic, What Is a Symbolic System?.
• Next: Modal Logic, the natural extension that adds operators for necessity and possibility.
• Next: Russell's Paradox, which exposes the naive comprehension principle that motivated the development of modern axiomatic set theory.
• Forward link: Goedel's incompleteness theorems (treated in Syntax vs Semantics) build directly on first-order Peano arithmetic.

References

Primary texts:

• Frege, Gottlob. Begriffsschrift. 1879. Introduces the modern notation for quantifiers and binding. The most important single document in the history of logic since Aristotle.
• Tarski, Alfred. "The Concept of Truth in Formalized Languages." 1933. The recursive definition of satisfaction. The technical foundation of modern model theory.
• Gödel, Kurt. Über die Vollständigkeit des Logikkalküls (On the Completeness of the Logical Calculus). 1929/30 dissertation. The completeness theorem for first-order logic.
• Church, Alonzo. "An Unsolvable Problem of Elementary Number Theory." American Journal of Mathematics 58, no. 2 (1936): 345-363.
• Turing, Alan M. "On Computable Numbers, with an Application to the Entscheidungsproblem." Proceedings of the London Mathematical Society s2-42 (1936): 230-265. The Church-Turing theorem on the undecidability of first-order validity.
• Henkin, Leon. "The Completeness of the First-Order Functional Calculus." Journal of Symbolic Logic 14, no. 3 (1949): 159-166. The standard modern proof of Gödel's completeness theorem.

Modern reference:

• Mendelson, Elliott. Introduction to Mathematical Logic. CRC Press, 6th ed., 2015. Standard graduate-level textbook with full treatment of soundness, completeness, and undecidability.
• Enderton, Herbert. A Mathematical Introduction to Logic. Academic Press, 2nd ed., 2001. Cleaner notation than Mendelson; same depth.
• van Dalen, Dirk. Logic and Structure. Springer, 5th ed., 2013. Uses natural deduction throughout; especially good on the proof-theoretic side.
• Boolos, George, John Burgess, and Richard Jeffrey. Computability and Logic. Cambridge, 5th ed., 2007. The bridge between first-order logic and computability theory.

Stanford Encyclopedia entries (link, do not paraphrase):

• "Classical Logic."
• "First-Order Model Theory."
• "Tarski's Truth Definitions."
• "Goedel's Theorems" (covers both completeness and incompleteness).