Predicate Logic - Examples and Constructions

First-order logic provides the formal language for expressing mathematical statements across all areas of mathematics, from number theory to topology.

ExampleFormalizing Mathematical Statements

Number Theory: "Every even number greater than 2 can be expressed as the sum of two primes" (Goldbach's Conjecture):

\forall x \, (\text{Even}(x) \land x > 2 \to \exists y \, \exists z \, (\text{Prime}(y) \land \text{Prime}(z) \land x = y + z))

Analysis: "A function $f$ is continuous at $a$ ":

\forall \epsilon > 0 \, \exists \delta > 0 \, \forall x \, (|x - a| < \delta \to |f(x) - f(a)| < \epsilon)

Set Theory: "A set $X$ is infinite":

\forall n \in \mathbb{N} \, \exists f: \{1, \ldots, n\} \to X \, (\text{injective}(f))

DefinitionPrenex Normal Form

A formula is in prenex normal form (PNF) if it has the form:

Q_1 x_1 \, Q_2 x_2 \, \cdots \, Q_n x_n \, \psi

where each $Q_i$ is either $\forall$ or $\exists$ , and $\psi$ is quantifier-free. Every first-order formula is logically equivalent to a formula in prenex normal form.

ExampleConverting to Prenex Normal Form

Convert $\phi = \forall x \, P(x) \to \exists y \, Q(y)$ to PNF:

Eliminate implication: $\neg \forall x \, P(x) \lor \exists y \, Q(y)$
Move negation inward: $\exists x \, \neg P(x) \lor \exists y \, Q(y)$
Rename variables if needed: already distinct
Move quantifiers out: $\exists x \, \exists y \, (\neg P(x) \lor Q(y))$

The result is in PNF with two existential quantifiers.

DefinitionSkolemization

Skolemization is a transformation that eliminates existential quantifiers by introducing new function symbols (Skolem functions). Given a formula of the form $\forall x_1 \cdots \forall x_n \, \exists y \, \phi$ , replace it with $\forall x_1 \cdots \forall x_n \, \phi[y/f(x_1, \ldots, x_n)]$ where $f$ is a new $n$ -ary function symbol.

The resulting formula is not equivalent to the original but is equisatisfiable: one is satisfiable if and only if the other is.

ExampleSkolemization Process

Consider $\phi = \forall x \, \exists y \, \forall z \, \exists w \, P(x, y, z, w)$ :

Skolemize the first existential: replace $y$ with $f(x)$ where $f$ is a new unary function Result: $\forall x \, \forall z \, \exists w \, P(x, f(x), z, w)$
Skolemize the second existential: replace $w$ with $g(x, z)$ where $g$ is a new binary function Result: $\forall x \, \forall z \, P(x, f(x), z, g(x, z))$

The final formula is universal and quantifier-free in its matrix.

Remark

Skolemization is central to automated theorem proving. By eliminating existential quantifiers, we can focus on finding substitutions for universal variables. The resolution method, a complete refutation procedure for first-order logic, operates on Skolemized formulas in clause form, making it the workhorse of modern theorem provers.

DefinitionHerbrand Universe

For a first-order language $\mathcal{L}$ , the Herbrand universe $H(\mathcal{L})$ is the set of all ground terms (variable-free terms) constructible from the constants and function symbols of $\mathcal{L}$ . If $\mathcal{L}$ has no constants, add an arbitrary constant. The Herbrand universe provides a canonical domain for interpreting formulas.

These constructions transform first-order formulas into standard forms that facilitate both theoretical analysis and practical automated reasoning.