Second-order logic: isomorphism invariance

Second-order satisfaction is preserved by isomorphisms, so second-order (and hence ∃SO) sentences define order-independent queries. This is the second-order analogue of Formula.sat_iso / Sentence.orderIndependent, and it is step 3 of the Fagin decomposition (roadmap L6).

The extra ingredient over the first-order case is transporting a relation environment across the isomorphism (REnv.map), together with the fact that this transport commutes with extending the environment by a fresh relation (rCons_map). Second-order quantifiers then match up by pushing/pulling the witnessing relations through the isomorphism.

Main definitions and results

• DescriptiveComplexity.REnv.map, rCons_map — transport of relation environments across an isomorphism, and its compatibility with rCons.
• SOFormula.sat_iso, SOSentence.models_iso — second-order satisfaction is isomorphism-invariant.
• SODefinable, SODefinable.orderIndependent — second-order definable queries are order-independent.

def Complexity.DescriptiveComplexity.REnv.map {V : Vocabulary} {A B : FinStruct V} (f : Iso A B) {rctx : List Nat} (ρ : REnv A.card rctx) : REnv B.card rctx

Transport a relation environment across an isomorphism: a relation on A is reinterpreted on B by pulling arguments back through f⁻¹.

Equations

• Complexity.DescriptiveComplexity.REnv.map f ρ r args = ρ r (f.invFun ∘ args)

theorem Complexity.DescriptiveComplexity.rCons_map {V : Vocabulary} {A B : FinStruct V} (f : Iso A B) {k : Nat} {rctx : List Nat} (S : (Fin k → Fin A.card) → Prop) (ρ : REnv A.card rctx) : REnv.map f (rCons S ρ) = rCons (fun (args : Fin k → Fin B.card) => S (f.invFun ∘ args)) (REnv.map f ρ)

Transport commutes with extending the environment by a fresh relation.

theorem Complexity.DescriptiveComplexity.SOFormula.sat_iso {V : Vocabulary} {A B : FinStruct V} (f : Iso A B) {rctx : List Nat} {n : Nat} (φ : SOFormula V rctx n) (σ : Env A.card n) (ρ : REnv A.card rctx) : Sat A σ ρ φ ↔ Sat B (f.toFun ∘ σ) (REnv.map f ρ) φ

Second-order satisfaction is isomorphism-invariant. Along an isomorphism f : A ≅ B, a formula holds at (σ, ρ) iff it holds at the transported environments (f ∘ σ, f₊ρ).

theorem Complexity.DescriptiveComplexity.SOSentence.models_iso {V : Vocabulary} {A B : FinStruct V} (f : Iso A B) (φ : SOSentence V) : Models A φ ↔ Models B φ

Second-order sentences are isomorphism-invariant.

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

A Boolean query is second-order definable if some SO sentence defines it.

Equations

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

theorem Complexity.DescriptiveComplexity.SODefinable.orderIndependent {V : Vocabulary} {Q : BooleanQuery V} (hQ : SODefinable Q) : Q.IsOrderIndependent

Second-order definable queries are order-independent — in particular every ∃SO query is legitimate, as Fagin's theorem requires.

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

Second-order definable queries are closed under complement (via ¬).

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

Second-order definable queries are closed under intersection (via ∧).

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

Second-order definable queries are closed under union (via ∨).