Boolean Queries

A boolean query over vocabulary V is a property of finite V-structures. A query is order-independent if it is invariant under isomorphism: isomorphic structures give the same answer (Immerman, Chapter 1). The theorem that first-order sentences define order-independent queries is cited as Immerman Proposition 1.16 (Sentence.orderIndependent).

@[reducible, inline]

abbrev Complexity.DescriptiveComplexity.BooleanQuery (V : Vocabulary) : Type

A boolean query over vocabulary V: a property of finite V-structures.

Equations

• Complexity.DescriptiveComplexity.BooleanQuery V = (Complexity.DescriptiveComplexity.FinStruct V → Prop)

def Complexity.DescriptiveComplexity.BooleanQuery.IsOrderIndependent {V : Vocabulary} (Q : BooleanQuery V) : Prop

A boolean query is order-independent if it is invariant under isomorphism: isomorphic structures satisfy it equally. Despite the name, nothing here refers to an ordering of the universe. Iso preserves every relation of V, so when V contains an order symbol only order-preserving isomorphisms are quantified.

Equations

• Q.IsOrderIndependent = ∀ {A B : Complexity.DescriptiveComplexity.FinStruct V}, Nonempty (Complexity.DescriptiveComplexity.Iso A B) → (Q A ↔ Q B)

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

The complement of a boolean query.

Equations

• Q.complement A = ¬Q A

def Complexity.DescriptiveComplexity.BooleanQuery.inter {V : Vocabulary} (Q₁ Q₂ : BooleanQuery V) : BooleanQuery V

The intersection (conjunction) of two boolean queries.

Equations

• Q₁.inter Q₂ A = (Q₁ A ∧ Q₂ A)

def Complexity.DescriptiveComplexity.BooleanQuery.union {V : Vocabulary} (Q₁ Q₂ : BooleanQuery V) : BooleanQuery V

The union (disjunction) of two boolean queries.

Equations

• Q₁.union Q₂ A = (Q₁ A ∨ Q₂ A)

theorem Complexity.DescriptiveComplexity.BooleanQuery.complement_orderIndependent {V : Vocabulary} {Q : BooleanQuery V} (hQ : Q.IsOrderIndependent) : Q.complement.IsOrderIndependent

theorem Complexity.DescriptiveComplexity.BooleanQuery.inter_orderIndependent {V : Vocabulary} {Q₁ Q₂ : BooleanQuery V} (h₁ : Q₁.IsOrderIndependent) (h₂ : Q₂.IsOrderIndependent) : (Q₁.inter Q₂).IsOrderIndependent

theorem Complexity.DescriptiveComplexity.BooleanQuery.union_orderIndependent {V : Vocabulary} {Q₁ Q₂ : BooleanQuery V} (h₁ : Q₁.IsOrderIndependent) (h₂ : Q₂.IsOrderIndependent) : (Q₁.union Q₂).IsOrderIndependent