Boolean Queries #
A boolean query over vocabulary V is a property of finite V-structures.
A query is order-independent if 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]
A boolean query over vocabulary V: a property of finite V-structures.
Equations
Instances For
def
Complexity.DescriptiveComplexity.BooleanQuery.IsOrderIndependent
{V : Vocabulary}
(Q : BooleanQuery V)
:
A boolean query is order-independent if isomorphic structures satisfy the same query. This is the key notion: a query defined by a logic is "legitimate" only if it is order-independent.
Equations
- Q.IsOrderIndependent = ∀ {A B : Complexity.DescriptiveComplexity.FinStruct V}, Nonempty (Complexity.DescriptiveComplexity.Iso A B) → (Q A ↔ Q B)
Instances For
def
Complexity.DescriptiveComplexity.BooleanQuery.complement
{V : Vocabulary}
(Q : BooleanQuery V)
:
The complement of a boolean query.
Equations
- Q.complement A = ¬Q A
Instances For
The intersection (conjunction) of two boolean queries.
Instances For
The union (disjunction) of two boolean queries.
Instances For
theorem
Complexity.DescriptiveComplexity.BooleanQuery.complement_orderIndependent
{V : Vocabulary}
{Q : BooleanQuery V}
(hQ : Q.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