Trakhtenbrot's Theorem states that the set of first-order sentences valid on every finite structure is not decidable, meaning no algorithm can determine in general whether a given first-order sentence holds in all finite models. Named for Boris Trakhtenbrot, it shows that finite model theory does not inherit the completeness and decidability properties available for first-order logic over arbitrary structures, since validity on finite models and validity in general diverge in this fundamental way.
Facts
StatementThe problem of validity in first-order logic on the class of all finite models is undecidable. 1 Classification
Statement Form Sources
1. Trakhtenbrot's theorem (Wikipedia)
Mathematical formulation section
The problem of validity in first-order logic on the class of all finite models is undecidable.
Opening section, publication sentence
The theorem was first published in 1950
View the SourceReader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.
Sign in to dispute this or suggest a correction.