Second-order transport through first-order interpretations

Pull back second-order formulas along the existing universe-preserving FOInterpretation. Vocabulary atoms are replaced by their defining first-order formulas; relation variables and their quantifiers retain their arities and scope. The transport theorem holds for arbitrary open formulas and relation environments. It preserves both FO matrices and existential second-order prefixes.

This supplies reduction closure for the logical classes before a machine capture theorem is available. For tagged tuple interpretations, relation variables instead need blocks of larger-arity variables; that generalization is separate work.

The pullback approach is standard in descriptive complexity; see Immerman, Descriptive Complexity (1999), and Senellart and Gnatenko, Descriptive Complexity in Lean: Completeness by First-Order Reductions (2026), Sections 3.3 and 4.1, https://arxiv.org/abs/2609.18261. These proofs use Complexitylib's own syntax.

def Complexity.DescriptiveComplexity.FOInterpretation.translateSO {V W : Vocabulary} (I : FOInterpretation V W) {rctx : List Nat} {n : Nat} : SOFormula W rctx n → SOFormula V rctx n

Pull back an SO formula along a universe-preserving FO interpretation.

Equations

• One or more equations did not get rendered due to their size.
• I.translateSO (Complexity.DescriptiveComplexity.SOFormula.soRelApp r ts) = Complexity.DescriptiveComplexity.SOFormula.soRelApp r fun (k : Fin (x✝¹.get r)) => I.translateTerm (ts k)
• I.translateSO (Complexity.DescriptiveComplexity.SOFormula.eq t₁ t₂) = Complexity.DescriptiveComplexity.SOFormula.eq (I.translateTerm t₁) (I.translateTerm t₂)
• I.translateSO φ.neg = (I.translateSO φ).neg
• I.translateSO (φ.conj ψ) = (I.translateSO φ).conj (I.translateSO ψ)
• I.translateSO (φ.disj ψ) = (I.translateSO φ).disj (I.translateSO ψ)
• I.translateSO φ.exist = (I.translateSO φ).exist
• I.translateSO φ.all = (I.translateSO φ).all
• I.translateSO (Complexity.DescriptiveComplexity.SOFormula.soExist k φ) = Complexity.DescriptiveComplexity.SOFormula.soExist k (I.translateSO φ)
• I.translateSO (Complexity.DescriptiveComplexity.SOFormula.soAll k φ) = Complexity.DescriptiveComplexity.SOFormula.soAll k (I.translateSO φ)

theorem Complexity.DescriptiveComplexity.FOInterpretation.translateSO_sat {V W : Vocabulary} (I : FOInterpretation V W) (A : FinStruct V) {rctx : List Nat} {n : Nat} (φ : SOFormula W rctx n) (σ : Env A.card n) (ρ : REnv A.card rctx) : SOFormula.Sat (I.apply A) σ ρ φ ↔ SOFormula.Sat A σ ρ (I.translateSO φ)

SO transport, including open element and relation environments.

theorem Complexity.DescriptiveComplexity.FOInterpretation.isFOMatrix_translateSO {V W : Vocabulary} (I : FOInterpretation V W) {rctx : List Nat} {n : Nat} (φ : SOFormula W rctx n) : (I.translateSO φ).IsFOMatrix ↔ φ.IsFOMatrix

Pullback preserves and reflects the absence of second-order quantifiers.

theorem Complexity.DescriptiveComplexity.FOInterpretation.isExistSO_translateSO {V W : Vocabulary} (I : FOInterpretation V W) {rctx : List Nat} {n : Nat} (φ : SOFormula W rctx n) : (I.translateSO φ).IsExistSO ↔ φ.IsExistSO

Pullback preserves existential second-order prefix form.

theorem Complexity.DescriptiveComplexity.SODefinable.of_reduces {V W : Vocabulary} {Q₁ : BooleanQuery V} {Q₂ : BooleanQuery W} (hQ₂ : SODefinable Q₂) (hred : FOReduces Q₁ Q₂) : SODefinable Q₁

Second-order definability is closed under the existing FO reductions.