Combining existential second-order prefixes

Pull the leading existential relation quantifiers of both operands outward, weakening the other operand at each binder. Once both prefixes are exhausted, join the matrices by conjunction or disjunction. This is the usual closure construction for existential second-order logic, implemented on de Bruijn syntax.

@[irreducible]

def Complexity.DescriptiveComplexity.SOFormula.mergeExist {V : Vocabulary} (isConjunction : Bool) {rctx : List Nat} {n : Nat} : SOFormula V rctx n → SOFormula V rctx n → SOFormula V rctx n

Merge leading existential SO prefixes, then combine their matrices. isConjunction = true selects conjunction and false selects disjunction.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DescriptiveComplexity.SOFormula.mergeExist isConjunction x✝¹ x✝ = if isConjunction = true then x✝¹.conj x✝ else x✝¹.disj x✝

def Complexity.DescriptiveComplexity.SOFormula.existConj {V : Vocabulary} {rctx : List Nat} {n : Nat} (φ ψ : SOFormula V rctx n) : SOFormula V rctx n

Conjoin existential SO formulas with their relation quantifiers in one prefix.

Equations

• φ.existConj ψ = Complexity.DescriptiveComplexity.SOFormula.mergeExist true φ ψ

def Complexity.DescriptiveComplexity.SOFormula.existDisj {V : Vocabulary} {rctx : List Nat} {n : Nat} (φ ψ : SOFormula V rctx n) : SOFormula V rctx n

Disjoin existential SO formulas with their relation quantifiers in one prefix.

Equations

• φ.existDisj ψ = Complexity.DescriptiveComplexity.SOFormula.mergeExist false φ ψ