Every first-order property of an expansion is in the polynomial hierarchy

The immediate payoff of the translation lemma (DescriptiveComplexity.ExpExpansion.exists_translate), and the first check on DescriptiveComplexity.ExpExpansion in the direction nothing else tests: the other checks on the operator validate it from below (PSPACE ⊆ NL.exp ⊆ EXPTIME), while this bounds it from above. A property of the expanded universe that a first-order sentence can express is not exponentially hard: it is Σₖ over the base, hence in PH, hence in PSPACE.

Two steps, both off the shelf once the translation is available.

• The translated sentence is second-order over the ordered base – the expansion's own discipline, “the sentences see the order, the problem does not”. DescriptiveComplexity.sigmaSODefinable_of_orderPull re-quantifies the order inside the first block, which is legitimate here because the hypothesis holds for every linear order on the instance, so “for some” and “for every” agree.
• The prefix is padded by one trivial block (DescriptiveComplexity.sorealize_append_trivial), so that it has a first block to carry the order variable even when the sentence has no quantifiers at all.

theorem DescriptiveComplexity.ExpExpansion.mem_PH_of_fo_on_expansion {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (φ : (X.E.sum FirstOrder.Language.order).Sentence) (P : DecisionProblem L) (h : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [inst_2 : Finite A] [inst_3 : Nonempty A], P.Holds A ↔ X.Map A ⊨ φ) : PH.Mem P

A first-order property of an exponential expansion is in PH. The quantifiers of the sentence become second-order quantifier blocks over the base (DescriptiveComplexity.ExpExpansion.exists_translate), two per quantifier, and the order the expansion's sentences read is guessed inside the first block.

theorem DescriptiveComplexity.ExpExpansion.mem_PSPACE_of_fo_on_expansion {L : FirstOrder.Language} [L.IsRelational] (X : ExpExpansion L) (φ : (X.E.sum FirstOrder.Language.order).Sentence) (P : DecisionProblem L) (h : ∀ (A : Type) [inst : L.Structure A] [inst_1 : LinearOrder A] [inst_2 : Finite A] [inst_3 : Nonempty A], P.Holds A ↔ X.Map A ⊨ φ) : PSPACE.Mem P

A first-order property of an exponential expansion is in PSPACE.