The small-model property of ∃*∀* sentences

What makes EPR a bounded problem: a satisfiable ∃*∀* sentence has a model whose universe is the instance itself. The witnesses of the existential variables are the only elements a model needs – everything else the sentence says is universally quantified, and a universal statement survives passing to a subuniverse containing those witnesses.

The proof counts nothing. Map the instance onto the model by x ↦ ε x at an existential variable and by a fixed element elsewhere (DescriptiveComplexity.Epr.collapse); read the interpretation back through that map, and let every variable stand for itself. What makes the reading legitimate is locality together with well-formedness: the value of a symbol is decided by the argument positions its signature declares, an atom names exactly one variable at each of them, and those variables' values are the ones the collapse carries.

This is the form the membership proof uses: with the universe fixed to the instance, an interpretation is a relation on the instance and an assignment of the universal variables is a function on it – one point of an exponential expansion.

def DescriptiveComplexity.Epr.SelfModel (A : Type) [FirstOrder.Language.epr.Structure A] : Prop

A model on the instance itself: an interpretation of the symbols by relations on the instance, and a witness for the existential variables among its elements.

Equations

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

noncomputable def DescriptiveComplexity.Epr.collapse {A : Type} [FirstOrder.Language.epr.Structure A] {M : Type} (ε : A → M) (m₀ : M) : A → M

The instance, mapped into a model: the witness of an existential variable, and a fixed element elsewhere. Its image is the subuniverse the sentence can speak of.

Equations

• DescriptiveComplexity.Epr.collapse ε m₀ x = if DescriptiveComplexity.Epr.EVarG x then ε x else m₀

theorem DescriptiveComplexity.Epr.collapse_eVar {A : Type} [FirstOrder.Language.epr.Structure A] {M : Type} {ε : A → M} {m₀ : M} {x : A} (h : EVarG x) : collapse ε m₀ x = ε x

theorem DescriptiveComplexity.Epr.collapse_val {A : Type} [FirstOrder.Language.epr.Structure A] {M : Type} (ε : A → M) (m₀ : M) (u : A → A) (x : A) : collapse ε m₀ (eprVal (fun (y : A) => y) u x) = eprVal ε (fun (y : A) => collapse ε m₀ (u y)) x

The collapse commutes with the two environments: the value a variable takes when it stands for itself, mapped into the model, is the value it takes in the model.

noncomputable def DescriptiveComplexity.Epr.argAssign {A : Type} [FirstOrder.Language.epr.Structure A] (u : A → A) (l : A) : A → A

The arguments of a literal, as an assignment of its positions: the value of the variable the encoding names there, when every variable stands for itself. Well-formedness makes the choice unambiguous.

Equations

• DescriptiveComplexity.Epr.argAssign u l p = if h : ∃ (x : A), DescriptiveComplexity.Epr.ArgG l p x then DescriptiveComplexity.Epr.eprVal (fun (y : A) => y) u h.choose else u p

theorem DescriptiveComplexity.Epr.argAssign_eq {A : Type} [FirstOrder.Language.epr.Structure A] (hwf : IsWF A) (u : A → A) {l p x : A} (h : ArgG l p x) : argAssign u l p = eprVal (fun (y : A) => y) u x

theorem DescriptiveComplexity.Epr.selfModel_of_eprSatOn {A : Type} [FirstOrder.Language.epr.Structure A] (hwf : IsWF A) (h : EprSatOn A) : SelfModel A

A model becomes one on the instance: read every symbol through the collapse, and take each variable to stand for itself.

theorem DescriptiveComplexity.Epr.eprSatOn_of_selfModel {A : Type} [FirstOrder.Language.epr.Structure A] [Finite A] [Nonempty A] (h : SelfModel A) : EprSatOn A

And a model on the instance is a model: the instance is a finite nonempty universe like any other.

theorem DescriptiveComplexity.Epr.eprSatOn_iff_selfModel {A : Type} [FirstOrder.Language.epr.Structure A] [Finite A] [Nonempty A] (hwf : IsWF A) : EprSatOn A ↔ SelfModel A

The small-model property: a well-formed instance is satisfiable exactly when it is satisfiable on its own universe.