FINSAT: finite satisfiability of a first-order sentence #

The problem of Trakhtenbrot's theorem (Trakhtenbrot 1950, Libkin 2004, ch. 9): does the given first-order sentence have a finite model? This file carries the instance encoding – a sentence, presented as a finite structure – and its semantics; membership in RE and RE-hardness live in the sibling files, and the completeness theorem in DescriptiveComplexity.Problems.FinSat.

The encoding #

An instance is a parse DAG in negation normal form. Its elements play several roles at once – nodes, variables, relation symbols, argument positions – and nothing forces those roles to be disjoint:

andN, orN mark the n-ary conjunction and disjunction nodes: such a node is the conjunction (disjunction) of all the nodes its child relation gives it. Nothing is a binary tree, which is what lets a reduction write an unbounded conjunction as a single node;
allN, exN mark the quantifier nodes, bind giving the variable quantified; a quantifier node is again read over all its children;
the leaves are literals: eqL g x y and neqL g x y for x = y and x ≠ y, and posL g s / negL g s for s(…) and ¬s(…), the arguments of the atom being given by arg g p x (“the argument at position p is the variable x”) and the argument positions of the symbol s by sig s p;
root marks the node the sentence starts at;
le is a linear order on the instance. A sentence is a string, so an encoding of one may certainly carry the order of its own syntax; what the order buys is that child g c → c < g – acyclicity of the parse DAG – becomes first-order, while acyclicity itself is not. The membership proof has to check well-formedness, so this matters.

Negation normal form is not a matter of economy: with negation confined to the leaves the value of a node is monotone in the values of its children, so satisfaction is a least fixed point (DescriptiveComplexity.FinSat.Gval, below) and no well-founded recursion on a decoded parse tree is needed anywhere. Every first-order formula has a negation normal form, and the hardness reduction produces one directly.

The semantics #

There is deliberately no decoding into a FirstOrder.Language.Sentence: the relation symbols of the encoded sentence are elements of the instance, so the decoded vocabulary would depend on the instance. Satisfaction is instead defined on the encoding, Tarski-style, by DescriptiveComplexity.FinSat.gstep – one clause per node kind, which is what a reader has to check anyway – iterated on a fuel counter (DescriptiveComplexity.FinSat.gval) and closed up (DescriptiveComplexity.FinSat.Gval).

A model is a finite nonempty type M together with an interpretation I : A → (A → M) → Prop reading a symbol and an assignment of argument positions, required to be local: I s may only look at the positions of the signature of s. Locality is what makes I s a relation of the arity of s rather than of the whole universe, and what makes the negative-atom clause unambiguous.

DescriptiveComplexity.FINSAT then holds of an instance when it is well-formed and the universal closure of the encoded formula has a finite model. Taking the universal closure costs nothing – the sentences the reduction produces are closed – and avoids conditioning on “every variable is bound by an ancestor”, which is a reachability property and so not first-order.

What is and is not claimed #

RE is the logically defined class of DescriptiveComplexity.RecursivelyEnumerable (definability in ∃SO[new]), so completeness of FINSAT for it is a statement about that logic. It becomes undecidability of finite satisfiability only through the bridge to Mathlib's computability layer (DescriptiveComplexity.finsat_not_computable).

FINSAT: finite satisfiability of a first-order sentence #

The encoding #

The semantics #

What is and is not claimed #

Reading the encoding #

Well-formedness #

Environments #

Satisfaction #

The problem #

Isomorphism-invariance #