Trakhtenbrot's theorem

Trakhtenbrot's theorem states that finite satisfiability for first-order logic is undecidable. Unrestricted first-order satisfiability is semidecidable, so restricting models to finite structures changes the computational status.

Connect

Finite model theory: The study of logical properties of finite structures and the computational complexity of deciding them. The theorem is a foundational limit on what finite-model reasoning can decide.
Turing machine: An abstract model of computation that manipulates symbols on a tape according to finite rules. Undecidable halting behavior supplies the computational problem encoded by the theorem.
First-order satisfiability: The problem of determining whether a first-order sentence has any model, finite or infinite. It is semidecidable, unlike finite satisfiability, because proofs enumerate satisfiable cases.
Database finite-model semantics: The interpretation of database queries and theories over finite relational structures. It places automated reasoning about finite databases within the theorem's limits.
Finite satisfiability: The problem of determining whether a logical sentence has a model with a finite domain. This is the decision problem that Trakhtenbrot's theorem proves undecidable.
Halting problem: The problem of deciding whether an arbitrary program eventually stops on a given input. A reduction from halting explains why no algorithm decides finite satisfiability.
Finite validity: The problem of determining whether a sentence is true in every finite structure. By negation, deciding finite validity would decide finite satisfiability.
Finite model property: A property of a logic in which every satisfiable sentence has a finite model. The theorem concerns finite models, but this property alone does not make their existence decidable.
First-order logic: A formal language with variables, quantifiers, predicates, and rules for reasoning about structures. The theorem identifies a boundary between finite and unrestricted models of this logic.
Finite model: A finite structure that satisfies a sentence in a formal language. The reduction makes such a model exist exactly when the encoded computation halts.