First-Order (Predicate) Logic

First-order logic (also called predicate logic) refines sentential logic by looking inside atomic statements — at objects, properties, relations, and quantifiers. It is the standard language in which modern mathematics is formalized. Where sentential logic cannot express that "every prime greater than $2$ is odd" follows from facts about individual numbers, first-order logic adds terms denoting objects, predicates denoting properties and relations, and quantifiers ranging over a domain.

As with sentential logic, the development separates syntax, semantics, and proof theory, and the central metatheorems — soundness, completeness, and compactness — tie them together.

Signatures and syntax

A first-order language (signature) $\mathcal{L}$ specifies:

• 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\ge 1$;
• a set of relation (predicate) symbols $R,P,\dots$, each with an arity $n\ge 0$;
• the distinguished binary relation equality $=$ (in first-order logic with equality).

Alongside $\mathcal{L}$ there is a countable supply of variables $x,y,z,\dots$.

Terms are built recursively: every variable and every constant is a term, and if $t_1,\dots ,t_n$ are terms and $f$ is an $n$-ary function symbol, then $f(t_1,\dots ,t_n)$ is a term. Terms are the noun phrases of the language — they denote objects.

Atomic formulas are $R(t_1,\dots ,t_n)$ for an $n$-ary relation symbol $R$, together with equalities $t_1=t_2$. General formulas are built from atomic ones using the sentential connectives $\neg ,\wedge ,\vee ,\to ,\leftrightarrow$ together with the quantifiers:

• the universal quantifier $\forall x\phi$ ("for all $x$, $\phi$");
• the existential quantifier $\exists x\phi$ ("there exists $x$ such that $\phi$").

The two quantifiers are interdefinable: $\forall x\phi \equiv \neg \exists x\neg \phi$.

An occurrence of a variable is bound if it lies within the scope of a quantifier over that variable, and free otherwise. A sentence is a formula with no free variables — only sentences have a determinate truth value in a structure. Substitution $\phi [t/x]$ replaces free occurrences of $x$ by the term $t$, subject to the side condition that $t$ is free for $x$ in $\phi$ (no variable of $t$ is accidentally captured by a quantifier).

Structures and semantics (Tarski)

An $\mathcal{L}$-structure (model) $\mathcal{M}$ consists of:

• a nonempty domain (universe) $M$;
• an element $c^{\mathcal{M}}\in M$ for each constant symbol $c$;
• a function $f^{\mathcal{M}}:M^n\to M$ for each $n$-ary function symbol $f$;
• a relation $R^{\mathcal{M}}\subseteq M^n$ for each $n$-ary relation symbol $R$.

To interpret formulas with free variables we also fix a variable assignment $s$ mapping variables to elements of $M$. Terms denote via the obvious recursion, $t^{\mathcal{M},s}\in M$. Satisfaction $\mathcal{M}\models \phi [s]$ is then defined by recursion on $\phi$ — Tarski's definition of truth:

• $\mathcal{M}\models R(t_1,\dots ,t_n)[s]$ iff $(t_1^{\mathcal{M},s},\dots ,t_n^{\mathcal{M},s})\in R^{\mathcal{M}}$;
• $\mathcal{M}\models (t_1=t_2)[s]$ iff $t_1^{\mathcal{M},s}=t_2^{\mathcal{M},s}$;
• the connectives are handled by the sentential truth tables;
• $\mathcal{M}\models \forall x\phi [s]$ iff $\mathcal{M}\models \phi [s(x\mapsto a)]$ for every $a\in M$;
• $\mathcal{M}\models \exists x\phi [s]$ iff $\mathcal{M}\models \phi [s(x\mapsto a)]$ for some $a\in M$.

For a sentence $\sigma$ the assignment is irrelevant, and we write $\mathcal{M}\models \sigma$ ("$\mathcal{M}$ is a model of $\sigma$"). A set of sentences $T$ is a theory; $\mathcal{M}\models T$ means $\mathcal{M}$ models every sentence of $T$. The semantic notions lift directly:

• $\sigma$ is valid ($\models \sigma$) if it holds in every structure;
• $T$ entails $\sigma$ ($T\models \sigma$) if every model of $T$ is a model of $\sigma$;
• $T$ is satisfiable if it has at least one model.

Deductive systems

First-order proof systems extend the sentential ones with rules and axioms governing the quantifiers and equality. In a Hilbert-style presentation one typically adds:

• Universal instantiation: $\forall x\phi \to \phi [t/x]$, provided $t$ is free for $x$ in $\phi$;
• Existential generalization: $\phi [t/x]\to \exists x\phi$, with the same proviso;
• a generalization rule: from $\phi$ infer $\forall x\phi$ (when $x$ is not free in the assumptions);
• the equality axioms: reflexivity $t=t$ together with substitution/congruence schemas allowing equals to replace equals.

Natural-deduction and sequent formulations add matching $\forall$/$\exists$ introduction and elimination rules with the customary eigenvariable side conditions. As before, $T⊢\sigma$ denotes derivability.

The fundamental metatheorems

First-order logic sits at a remarkable sweet spot: it is expressive enough to formalize ordinary mathematics, yet well-behaved enough to satisfy strong metatheorems.

• Soundness: if $T⊢\sigma$ then $T\models \sigma$.
• Gödel's Completeness Theorem: if $T\models \sigma$ then $T⊢\sigma$. Equivalently, every consistent theory has a model. Thus $⊢$ and $\models$ again coincide. (The standard proof is Henkin's: extend the theory with witnessing constants and build a term model out of the syntax itself.)
• Compactness Theorem: a theory $T$ has a model iff every finite subset of $T$ has a model. This follows from completeness, since proofs are finite. Compactness is the workhorse of model theory — it yields nonstandard models of arithmetic, infinite models from arbitrarily large finite ones, and much more.
• Löwenheim–Skolem Theorems: if a countable theory has an infinite model, it has models of every infinite cardinality. Downward: it has a countable model (the source of Skolem's paradox — a countable model of set theory that internally "believes" in uncountable sets; see Axiomatic Set Theory (ZFC)). Upward: it has arbitrarily large models. A corollary is that first-order logic cannot pin down an infinite structure up to isomorphism by its first-order theory alone.

These positive results are bounded by sharp limitations:

• Undecidability (Church–Turing): the set of first-order validities is not decidable — there is no algorithm that, given a sentence, always halts and correctly reports whether it is valid. It is, however, semidecidable (recursively enumerable): completeness guarantees a proof search that halts on every validity. This is the precise sense in which first-order logic is harder than sentential logic, whose validity is decidable by truth tables.
• Gödel's Incompleteness Theorems: any consistent, effectively axiomatized theory $T$ that interprets enough arithmetic is incomplete — there is a sentence $G$ with $T⊬G$ and $T⊬\neg G$ — and moreover $T$ cannot prove its own consistency. (Note the contrast: completeness is a property of the logic — every valid sentence is provable; incompleteness is a property of particular theories — they fail to decide every sentence in their language.)

Beyond first order

First-order quantifiers range only over individuals. Second-order logic also quantifies over relations and functions and can categorically characterize structures like the natural numbers (Peano's axioms with full second-order induction), but it pays for this expressiveness by losing completeness and compactness — there is no sound and complete effective proof system for full second-order semantics. This trade-off, expressiveness against metatheoretic tameness, is exactly why first-order logic is the default foundation for mathematics. See Second-Order and Higher-Order Logic for the full development.

Sentential vs. first-order logic

The recurring theme is the interplay of three layers — syntax, semantics, and proof — and the soundness/completeness theorems that lock provability ($⊢$) and truth ($\models$) together in both systems.