Syntax and Semantics of First-Order Logic

Motivation: Speaking About Structures, Not Just Propositions

Propositional logic cannot express “all natural numbers are even” or “there exists a prime number.” First-order logic (FOL) adds quantifiers ∀ and ∃, predicate symbols, and function symbols—this is the language of modern mathematics. FOL is used to formulate group theory, arithmetic, set theory.

Syntax of FOL

Signature σ: a set of predicate symbols P (of arity n), function symbols f (of arity n), and constants c (nullary functions).

Terms (recursive definition):

• Variables x, y, z, ... are terms.
• Constants c are terms.
• If f is a function symbol of arity n and t₁,...,tₙ are terms, then f(t₁,...,tₙ) is a term.

Formulas:

• P(t₁,...,tₙ) is an atomic formula (predicate P applied to terms).
• t₁ = t₂ is an atomic equality formula.
• ¬φ, φ∧ψ, φ∨ψ, φ→ψ come from propositional connectives.
• ∀x φ is the universal quantifier: “for all x, φ holds.”
• ∃x φ is the existential quantifier: “there exists x such that φ holds.”

Free and bound variables: x is free in φ if it is not within the scope of quantifiers over x. In ∀x P(x, y): x is bound, y is free.

Semantics: First-Order Structures

Structure M = (D, P^M, f^M, c^M):

• D ≠ ∅ is the domain (universe), e.g., ℕ, ℤ, ℝ, a graph, etc.
• For each predicate P of arity n: P^M ⊆ Dⁿ is a relation.
• For each function f of arity n: f^M: Dⁿ → D is a function.
• For each constant c: c^M ∈ D.

Variable assignment: μ: {variables} → D.

Truth in M ⊨ φ[μ] (recursively):

• M ⊨ P(t₁,...,tₙ)[μ] ⟺ (t₁^M[μ],...,tₙ^M[μ]) ∈ P^M
• M ⊨ ∀x φ[μ] ⟺ M ⊨ φ[μ[x↦d]] for all d ∈ D
• M ⊨ ∃x φ[μ] ⟺ M ⊨ φ[μ[x↦d]] for some d ∈ D

Key Concepts

Sentence (closed formula): no free variables. Truth does not depend on assignment.

Theory T: a set of sentences. M is a model of T if M ⊨ φ for all φ ∈ T.

Logically valid formula: M ⊨ φ in every structure M.

Numerical Example

Problem: Let M = (ℤ, <, S), where < is the standard order, S(x) = x+1. Check the truth of: (a) ∀x ∃y (x < y), (b) ∃x ∀y (x < y), (c) ∀x ∀y (x < y → S(x) < S(y)).

Step 1. (a) ∀x ∃y (x < y): for any integer x we need y > x. Take y = x+1 ∈ ℤ. True ✓.

Step 2. (b) ∃x ∀y (x < y): need the minimal element of ℤ. But ℤ has no least integer. False ✓.

Step 3. (c) ∀x ∀y (x < y → S(x) < S(y)): if x < y, then x+1 < y+1. This is an obvious property of the integers. True ✓.

Additionally. Let us write “density of order” in FOL: ∀x ∀y (x < y → ∃z (x < z ∧ z < y)). In (ℤ, <): for x=0, y=1 there is no z with 0 < z < 1 in ℤ. False in ℤ. In (ℚ, <) or (ℝ, <)—true.

Real-World Application

Databases: SQL is practically first-order logic. The query “select all employees whose salary is above average” is ∀x (Empl(x) ∧ Sal(x) > Avg → Result(x)). Query optimizers use logical formula transformations.

Additional Aspects

First-order predicate logic adds the quantifiers ∀ and ∃ and predicates of variables to propositional logic. This gives enough expressiveness to axiomatize number theory (Peano arithmetic), set theory (ZFC), and most of standard mathematics. The Löwenheim–Skolem theorem that every satisfiable theory has a countable model leads to Skolem’s paradox (the uncountability of the set of real numbers in a countable model of ZFC). In practice, first-order resolution provers such as E, Vampire, Prover9 solve problems in group theory, rings, relational databases, program verification, and algebraic geometry.

Connection with Other Areas of Mathematics

In the theory of differential equations, first-order logic underlies the formalization of the concept of solutions in various models. For example, the concept of elementary equivalence of fields of real numbers and formal power series fields is used in Robinson’s nonstandard analysis: solutions of equations are considered in elementary extensions, and properties such as “there exists an integral curve” are formulated logically. In algebra, the theorem on the classification of models of the theory of algebraically closed fields of a given characteristic plays a central role: Łoś and Tarski showed that all such fields of the same transcendence degree are isomorphic, and model-theoretic arguments allow transferring results from one field (e.g., the algebraic closure of a subfield of the complex numbers) to another.

In topology, first-order logic appears in the description of structures where properties such as compactness or connectedness are formulated through predicates on open sets. The works of Tarski and Cheitin on topological semigroups rely on elementary theories of these structures. In probability theory, FOL is used in the axiomatization of Kolmogorov’s probability spaces: sigma-algebras, events, and random variables are described by predicates, and results such as Lévy’s monotone convergence theorem are formalized in logic with quantifiers over events. In numerical methods, the logical language is applied to specification of algorithm correctness: properties such as convergence of iterative schemes, stability of finite difference schemes, and correctness of Monte Carlo methods are written as universal and existential statements about sequences of approximations and probabilistic estimates.

Historical Background and Concept Development

The roots of first-order logic go back to Frege, who published in 1879 “Begriffsschrift,” where for the first time a formal theory of predicates was proposed. Peano in “Arithmetices principia” (1899) used a similar language to axiomatize the natural numbers. The modern syntax and semantics of FOL were systematized by Hilbert and Ackermann in the book “Grundzüge der theoretischen Logik” (1928), where the notions of model and consequence were discussed. Tarski in his 1935 article “Der Wahrheitsbegriff in den formalisierten Sprachen” formulated the model-theoretic definition of truth, initiating the semantic approach. In the 1930s, Löwenheim, Skolem, and Malcev developed techniques for scaling models and proved theorems on the compactness and countability of models of satisfiable theories. A turning point was Gödel’s work: the completeness theorem (1930) showed the coincidence of syntactic and semantic consequence, and the incompleteness theorems (1931) revealed the limitations of the axiomatization of arithmetic.