Existential second-order conjunction and disjunction

existConj and existDisj combine formulas while collecting their leading existential relation quantifiers into one prefix. Their semantics hold for arbitrary open formulas; existential SO operands produce existential SO results. Each result has exactly the sum of the operand sizes plus one, so witness merging does not duplicate formulas.

This is the existential-prefix manipulation used in the second-order framework of Immerman's Descriptive Complexity, Section 7.1. It supplies logical closure before the machine characterization of existential SO is proved.

theorem Complexity.DescriptiveComplexity.SOFormula.mergeExist_sat {V : Vocabulary} {rctx : List Nat} {n : Nat} (isConjunction : Bool) (φ ψ : SOFormula V rctx n) (A : FinStruct V) (σ : Env A.card n) (ρ : REnv A.card rctx) : Sat A σ ρ (mergeExist isConjunction φ ψ) ↔ if isConjunction = true then Sat A σ ρ φ ∧ Sat A σ ρ ψ else Sat A σ ρ φ ∨ Sat A σ ρ ψ

Merging existential prefixes computes conjunction or disjunction as selected.

theorem Complexity.DescriptiveComplexity.SOFormula.isExistSO_mergeExist {V : Vocabulary} {rctx : List Nat} {n : Nat} (isConjunction : Bool) (φ ψ : SOFormula V rctx n) (hφ : φ.IsExistSO) (hψ : ψ.IsExistSO) : (mergeExist isConjunction φ ψ).IsExistSO

The merged prefix retains existential SO form.

@[simp]

theorem Complexity.DescriptiveComplexity.SOFormula.size_mergeExist {V : Vocabulary} {rctx : List Nat} {n : Nat} (isConjunction : Bool) (φ ψ : SOFormula V rctx n) : (mergeExist isConjunction φ ψ).size = φ.size + ψ.size + 1

Prefix merging adds one connective and preserves all other syntax nodes.

theorem Complexity.DescriptiveComplexity.SOFormula.existConj_sat {V : Vocabulary} {rctx : List Nat} {n : Nat} (φ ψ : SOFormula V rctx n) (A : FinStruct V) (σ : Env A.card n) (ρ : REnv A.card rctx) : Sat A σ ρ (φ.existConj ψ) ↔ Sat A σ ρ φ ∧ Sat A σ ρ ψ

Existential-prefix conjunction has the usual conjunction semantics.

theorem Complexity.DescriptiveComplexity.SOFormula.existDisj_sat {V : Vocabulary} {rctx : List Nat} {n : Nat} (φ ψ : SOFormula V rctx n) (A : FinStruct V) (σ : Env A.card n) (ρ : REnv A.card rctx) : Sat A σ ρ (φ.existDisj ψ) ↔ Sat A σ ρ φ ∨ Sat A σ ρ ψ

Existential-prefix disjunction has the usual disjunction semantics.

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

Existential SO form is closed under prefix-merging conjunction.

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

Existential SO form is closed under prefix-merging disjunction.

@[simp]

theorem Complexity.DescriptiveComplexity.SOFormula.size_existConj {V : Vocabulary} {rctx : List Nat} {n : Nat} (φ ψ : SOFormula V rctx n) : (φ.existConj ψ).size = φ.size + ψ.size + 1

Existential-prefix conjunction has additive size, with one new connective.

@[simp]

theorem Complexity.DescriptiveComplexity.SOFormula.size_existDisj {V : Vocabulary} {rctx : List Nat} {n : Nat} (φ ψ : SOFormula V rctx n) : (φ.existDisj ψ).size = φ.size + ψ.size + 1

Existential-prefix disjunction has additive size, with one new connective.