Invariant decision problems

A decision problem is a Boolean query together with its isomorphism invariance. Bundling this law lets structural reductions compose even when the intermediate universes have different canonical presentations. This is the decision-problem interface used by Senellart--Gnatenko (2026), Section 3.1, specialized to our FinStruct convention of at least two elements.

structure Complexity.DescriptiveComplexity.DecisionProblem (V : Vocabulary) : Type

An isomorphism-invariant property of finite structures.

• toQuery : BooleanQuery V

  The underlying query on structures.

• invariant : self.toQuery.IsOrderIndependent

  Renaming the universe does not affect the answer.

@[instance_reducible]

instance Complexity.DescriptiveComplexity.instCoeFunDecisionProblemForallFinStructProp {V : Vocabulary} : CoeFun (DecisionProblem V) fun (x : DecisionProblem V) => FinStruct V → Prop

Equations

• Complexity.DescriptiveComplexity.instCoeFunDecisionProblemForallFinStructProp = { coe := Complexity.DescriptiveComplexity.DecisionProblem.toQuery }

def Complexity.DescriptiveComplexity.DecisionProblem.ofFODefinable {V : Vocabulary} (Q : BooleanQuery V) (hQ : FODefinable Q) : DecisionProblem V

Bundle an FO-definable query as a decision problem.

Equations

• Complexity.DescriptiveComplexity.DecisionProblem.ofFODefinable Q hQ = { toQuery := Q, invariant := ⋯ }

def Complexity.DescriptiveComplexity.DecisionProblem.ofExistSODefinable {V : Vocabulary} (Q : BooleanQuery V) (hQ : ExistSODefinable Q) : DecisionProblem V

Bundle an existential SO-definable query as a decision problem.

Equations

• Complexity.DescriptiveComplexity.DecisionProblem.ofExistSODefinable Q hQ = { toQuery := Q, invariant := ⋯ }

def Complexity.DescriptiveComplexity.DecisionProblem.complement {V : Vocabulary} (P : DecisionProblem V) : DecisionProblem V

Complement of an invariant decision problem.

Equations

• P.complement = { toQuery := P.toQuery.complement, invariant := ⋯ }

def Complexity.DescriptiveComplexity.DecisionProblem.inter {V : Vocabulary} (P Q : DecisionProblem V) : DecisionProblem V

Intersection of invariant decision problems.

Equations

• P.inter Q = { toQuery := P.toQuery.inter Q.toQuery, invariant := ⋯ }

def Complexity.DescriptiveComplexity.DecisionProblem.union {V : Vocabulary} (P Q : DecisionProblem V) : DecisionProblem V

Union of invariant decision problems.

Equations

• P.union Q = { toQuery := P.toQuery.union Q.toQuery, invariant := ⋯ }