Trakhtenbrot's theorem: finite satisfiability is RE-complete

The umbrella of the FINSAT files. The problem (DescriptiveComplexity.FINSAT) is: given a first-order sentence, encoded as a finite structure, does it have a finite model? Its two halves are

• membership – DescriptiveComplexity.finsat_mem_RE: the model is invented, which is exactly what ∃SO[new] (and nothing weaker) can do;
• hardness – DescriptiveComplexity.finsat_hard_of_sigmaSONewDefinable: an ∃SO[new] certificate is “a finite extension of the universe plus relations on it satisfying a fixed first-order kernel”, and a finite model of a sentence is “a finite universe plus relations on it satisfying a given first-order sentence”; the reduction is the translation of the first into the second.

Together: DescriptiveComplexity.FINSAT_RE_complete.

Where the work is

The mathematical content of hardness is DescriptiveComplexity.FinSat.finsat_hard_of_sigmaSONewDefinable, which builds the sentence σ_A – an existential prefix naming the elements of the instance, a diagram forcing them apart, and the negation-normal-form translation of the kernel, whose atoms of the instance's own vocabulary are read by the interpretation and never mentioned by the sentence. The construction works because the source vocabulary is relational – as every vocabulary of a DescriptiveComplexity.DecisionProblem is: the encoded sentence carries its own quantifiers and would otherwise have to name what a function symbol does on an invented value – an undefinable junk element.

What the theorem does and does not say

RE here is the logically defined class of DescriptiveComplexity.RecursivelyEnumerable, so this is “finite satisfiability is complete for ∃SO[new]”. It becomes undecidability of finite satisfiability only through the bridge to Mathlib's computability layer, DescriptiveComplexity.Computability, where the encoding of finite structures as numbers turns it into DescriptiveComplexity.finsat_not_computable.

theorem DescriptiveComplexity.finsat_hard_of_sigmaSONewDefinable {L : FirstOrder.Language} [L.IsRelational] (Q : DecisionProblem L) : SigmaSONewDefinable Q → Nonempty (RelOrderedFOReduction Q FINSAT)

The hardness half of Trakhtenbrot's theorem: every ∃SO[new]-definable problem admits an ordered first-order reduction to finite satisfiability – DescriptiveComplexity.FinSat.finsat_hard_of_sigmaSONewDefinable, the encoded sentence σ_A, in the relativized form hardness is stated in.

theorem DescriptiveComplexity.FINSAT_RE_complete : RE.Complete FINSAT

Trakhtenbrot's theorem, in the logical form: finite satisfiability of a first-order sentence is RE-complete.

Membership is DescriptiveComplexity.finsat_mem_RE, hardness DescriptiveComplexity.finsat_hard_of_sigmaSONewDefinable.

theorem DescriptiveComplexity.finsat_RE_hard : RE.Hard FINSAT

FINSAT is RE-hard.