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.

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.