The language induced by a Boolean query

The bridge from descriptive complexity to the machine model: a Boolean query over finite structures induces a language (a set of bit strings) — the encodings of the structures satisfying it. This is where a logical characterization of a query becomes a statement about a machine-model Language, the connection Fagin's theorem (NP = ∃SO) and the other logic/complexity correspondences on track L6 ultimately rest on.

Main definitions and results

• DescriptiveComplexity.queryLanguage — the language of a query.
• DescriptiveComplexity.mem_queryLanguage — a Q-satisfying structure's encoding is in Q's language.

def Complexity.DescriptiveComplexity.queryLanguage {V : Vocabulary} (Q : BooleanQuery V) : Language

The language induced by a Boolean query Q: the set of bit strings that encode a (decidable) structure satisfying Q.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.DescriptiveComplexity.mem_queryLanguage {V : Vocabulary} (Q : BooleanQuery V) (A : DecFinStruct V) (hQ : Q A.toFinStruct) : encodeStruct A ∈ queryLanguage Q

Encoding a Q-satisfying structure lands in Q's induced language.