In
logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premis ...
,
finite model theory Finite model theory is a subarea of model theory. Model theory is the branch of logic which deals with the relation between a formal language (syntax) and its interpretations (semantics). Finite model theory is a restriction of model theory to inte ...
, and
computability theory
Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since ...
, Trakhtenbrot's theorem (due to
Boris Trakhtenbrot
Boris (Boaz) Abramovich Trakhtenbrot (russian: Борис Авраамович Трахтенброт, he, בועז טרכטנברוט; 19 February 1921 – 19 September 2016) was a Russian-Israeli mathematician in logic, algorithms, theory of co ...
) states that the problem of
validity
Validity or Valid may refer to:
Science/mathematics/statistics:
* Validity (logic), a property of a logical argument
* Scientific:
** Internal validity, the validity of causal inferences within scientific studies, usually based on experiments
...
in
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quanti ...
on the class of all finite models is
undecidable. In fact, the class of valid sentences over finite models is not
recursively enumerable
In computability theory, a set ''S'' of natural numbers is called computably enumerable (c.e.), recursively enumerable (r.e.), semidecidable, partially decidable, listable, provable or Turing-recognizable if:
*There is an algorithm such that the ...
(though it is
co-recursively enumerable).
Trakhtenbrot's theorem implies that
Gödel's completeness theorem
Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic.
The completeness theorem applies to any first-order theory: I ...
(that is fundamental to first-order logic) does not hold in the finite case. Also it seems counter-intuitive that being valid over all structures is 'easier' than over just the finite ones.
The theorem was first published in 1950: "The Impossibility of an Algorithm for the Decidability Problem on Finite Classes".
Mathematical formulation
We follow the formulations as in Ebbinghaus and Flum
Theorem
:
Satisfiability for finite structures is not decidable in
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quanti ...
.
:That is, the set is undecidable.
Corollary
Let σ be a relational vocabulary with one at least binary relation symbol.
:The set of
σ-sentences valid in all finite structures is not
recursively enumerable
In computability theory, a set ''S'' of natural numbers is called computably enumerable (c.e.), recursively enumerable (r.e.), semidecidable, partially decidable, listable, provable or Turing-recognizable if:
*There is an algorithm such that the ...
.
Remarks
# This implies that
Gödel's completeness theorem
Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic.
The completeness theorem applies to any first-order theory: I ...
fails in the finite since completeness implies recursive enumerability.
# It follows that there is no recursive function f such that: if φ has a finite model, then it has a model of size at most f(φ). In other words, there is no effective analogue to the
Löwenheim–Skolem theorem
In mathematical logic, the Löwenheim–Skolem theorem is a theorem on the existence and cardinality of models, named after Leopold Löwenheim and Thoralf Skolem.
The precise formulation is given below. It implies that if a countable first-orde ...
in the finite.
Intuitive proof
This proof is taken from Chapter 10, section 4, 5 of Mathematical Logic by H.-D. Ebbinghaus.
As in the most common proof of
Gödel's First Incompleteness Theorem through using the undecidability of the
halting problem
In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. Alan Turing proved in 1936 that a ...
, for each
Turing machine
A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algor ...
there is a corresponding arithmetical sentence
, effectively derivable from
, such that it is true if and only if
halts on the empty tape. Intuitively,
asserts "there exists a natural number that is the Gödel code for the computation record of
on the empty tape that ends with halting".
If the machine
does halt in finite steps, then the complete computation record is also finite, then there is a finite initial segment of the natural numbers such that the arithmetical sentence
is also true on this initial segment. Intuitively, this is because in this case, proving
requires the arithmetic properties of only finitely many numbers.
If the machine
does not halt in finite steps, then
is false in any finite model, since there's no finite computation record of
that ends with halting.
Thus, if
halts,
is true in some finite models. If
does not halt,
is false in all finite models. So,
does not halt if and only if
is true over all finite models.
The set of machines that does not halt is not recursively enumerable, so the set of valid sentences over finite models is not recursively enumerable.
Alternative proof
In this section we exhibit a more rigorous proof from Libkin.
Note in the above statement that the corollary also entails the theorem, and this is the direction we prove here.
Theorem
:For every relational vocabulary τ with at least one binary relation symbol, it is undecidable whether a sentence φ of vocabulary τ is finitely satisfiable.
Proof
According to the previous lemma, we can in fact use finitely many binary relation symbols. The idea of the proof is similar to the proof of Fagin's theorem, and we encode Turing machines in first-order logic. What we want to prove is that for every Turing machine M we construct a sentence φ
M of vocabulary τ such that φ
M is finitely satisfiable if and only if M halts on the empty input, which is equivalent to the halting problem and therefore undecidable.
Let M= ⟨Q, Σ, δ, q
0, Q
a, Q
r⟩ be a deterministic Turing machine with a single infinite tape.
* Q is the set of states,
* Σ is the input alphabet,
* Δ is the tape alphabet,
* δ is the transition function,
* q
0 is the initial state,
* Q
a and Q
r are the sets of accepting and rejecting states.
Since we are dealing with the problem of halting on an empty input we may assume w.l.o.g. that Δ= and that 0 represents a blank, while 1 represents some tape symbol. We define τ so that we can represent computations:
: τ :=
Where:
* < is a linear order and
min is a constant symbol for the minimal element with respect to < (our finite domain will be associated with an initial segment of the natural numbers).
* T
0 and T
1 are tape predicates. T
i(s,t) indicates that position s at time t contains i, where i ∈ .
* H
q's are head predicates. H
q(s,t) indicates that at time t the machine is in state q, and its head is in position s.
The sentence φ
M states that (i) <,
min, T
i's and H
q's are interpreted as above and (ii) that the machine eventually halts. The halting condition is equivalent to saying that H
q∗(s, t) holds for some s, t and q∗ ∈ Q
a ∪ Q
r and after that state, the configuration of the machine does not change. Configurations of a halting machine (the nonhalting is not finite) can be represented as a τ (finite) sentence (more precisely, a finite τ-structure which satisfies the sentence). The sentence φ
M is: φ ≡ α ∧ β ∧ γ ∧ η ∧ ζ ∧ θ.
We break it down by components:
* α states that < is a linear order and that
min is its minimal element
* γ defines the initial configuration of M: it is in state q
0, the head is in the first position and the tape contains only zeros: γ ≡ H
q0(
min,
min) ∧ ∀s T
0 (s,
min)
* η states that in every configuration of M, each tape cell contains exactly one element of Δ: ∀s∀t(T
0(s, t) ↔ ¬ T
1(s, t))
* β imposes a basic consistency condition on the predicates H
q's: at any time the machine is in exactly one state:
:
* ζ states that at some point M is in a halting state:
:
* θ consists of a conjunction of sentences stating that T
i's and H
q's are well behaved with respect to the transitions of M. As an example, let δ(q,0)=(q',1, left) meaning that if M is in state q reading 0, then it writes 1, moves the head one position to the left and goes into the state q'. We represent this condition by the disjunction of θ
0 and θ
1:
:
Where θ
2 is:
:
And:
:
Where θ
3 is:
s-1 and t+1 are first-order definable abbreviations for the predecessor and successor according to the ordering <. The sentence θ
0 assures that the tape content in position s changes from 0 to 1, the state changes from q to q', the rest of the tape remains the same and that the head moves to s-1 (i. e. one position to the left), assuming s is not the first position in the tape. If it is, then all is handled by θ
1: everything is the same, except the head does not move to the left but stays put.
If φ
M has a finite model, then such a model that represents a computation of M (that starts with the empty tape (i.e. tape containing all zeros) and ends in a halting state). If M halts on the empty input, then the set of all configurations of the halting computations of M (coded with <, T
i's and H
q's) is a model of φ
M, which is finite, since the set of all configurations of halting computations is finite. It follows that M halts on the empty input iff φ
M has a finite model. Since halting on the empty input is undecidable, so is the question of whether φ
M has a finite model
(equivalently, whether φ
M is finitely satisfiable) is also undecidable (recursively enumerable, but not recursive). This concludes the proof.
Corollary
: The set of finitely satisfiable sentences is recursively enumerable.
Proof
Enumerate all pairs
where
is finite and
.
Corollary
: For any vocabulary containing at least one binary relation symbol, the set of all finitely valid sentences is not recursively enumerable.
Proof
From the previous lemma, the set of finitely satisfiable sentences is recursively enumerable. Assume that the set of all finitely valid sentences is recursively enumerable. Since ¬φ is finitely valid iff φ is not finitely satisfiable, we conclude that the set of sentences which are not finitely satisfiable is recursively enumerable. If both a set A and its complement are recursively enumerable, then A is recursive. It follows that the set of finitely satisfiable sentences is recursive, which contradicts Trakhtenbrot's theorem.
References
* Boolos, Burgess, Jeffrey. ''Computability and Logic'', Cambridge University Press, 2002.
* Simpson, S. "Theorems of Church and Trakhtenbrot". 200
Finite model theory
Computability theory
Undecidable problems