LogicalZooAn atlas of formal logics

Classical Logics

FOL

First-Order Logic

Classical predicate logic with quantification over individuals, relational structures, and Tarskian semantics.

Overview

First-order logic (FOL) extends propositional logic with variables, quantifiers, equality (when included in the signature), and interpretations of relation and function symbols. Its semantics is defined over structures with a nonempty domain of individuals.

Syntax

Terms are built from variables, constants, and function symbols. Atomic formulas apply predicate symbols to terms or compare terms for equality. Formulas are closed under Boolean connectives and the quantifiers \forall x and \exists x.

For a binary relation R, the sentence

\forall x\,\exists y\,R(x,y)

asserts that every element has an R-successor. This does not by itself require the domain to be infinite.

Semantics

A structure \mathcal M provides a nonempty domain and interpretations of the nonlogical symbols. Satisfaction \mathcal M,s\models\varphi is defined relative to a variable assignment s. Quantifiers range over the domain of \mathcal M.

The distinction between satisfaction over arbitrary structures and satisfaction over finite structures is crucial. For example, FOL has the compactness property on arbitrary structures, but finite satisfiability behaves differently.

Proof Theory and Model Theory

Gödel's completeness theorem identifies semantic validity with derivability in a sound complete first-order calculus. The Löwenheim–Skolem theorems and compactness are central model-theoretic results. Neither should be mistaken for a general finite-model principle.

Decidability and Complexity

Unrestricted first-order validity is recursively enumerable but undecidable. Finite satisfiability is also undecidable; by Trakhtenbrot's theorem, finite validity is not recursively enumerable for sufficiently expressive relational signatures.

Relationships to Other Logics

FO² restricts the number of variable symbols. The guarded fragment restricts quantifier use through atomic guards. ALC corresponds to a restricted first-order language under a standard translation. Higher-order logic quantifies over objects of additional types.

References

  1. Herbert B. Enderton (2001). A Mathematical Introduction to Logic, 2nd ed. Academic Press.
  2. Leonid Libkin (2004). Elements of Finite Model Theory. Springer.

Related logics

  • ALC — Attributive Concept Language with Complements
  • FO² — Two-Variable First-Order Logic
  • GF — Guarded Fragment
  • HOL — Classical Higher-Order Logic
  • PL — Classical Propositional Logic

Links to this entry

  • ALC — Attributive Concept Language with Complements
  • B — Brouwer Modal Logic B
  • DLP — Description Logic Programs (DLP)
  • FO² — Two-Variable First-Order Logic
  • GF — Guarded Fragment
  • HOL — Classical Higher-Order Logic
  • K — Basic Normal Modal Logic K
  • K4 — Transitive Modal Logic K4
  • K45 — Transitive Euclidean Modal Logic K45
  • K5 — Euclidean Modal Logic K5
  • KB — Normal Modal Logic KB
  • KB5 — Symmetric Euclidean Modal Logic KB5
  • KD — Normal Modal Logic KD
  • KD4 — Serial Transitive Modal Logic KD4
  • KD45 — Serial Transitive Euclidean Modal Logic KD45
  • KD5 — Serial Euclidean Modal Logic KD5
  • KDB — Normal Modal Logic KDB
  • KT — Normal Modal Logic T
  • PL — Classical Propositional Logic
  • S4 — Normal Modal Logic S4
  • S5 — Normal Modal Logic S5
  • SROIQ — SROIQ: An Expressive Description Logic

Published on Oct. 31, 2026 · Version 1