The certificate: a finite model, invented

The mathematical content of FINSAT ∈ RE, ahead of any second-order syntax: an encoded sentence has a finite model exactly when a finite set of invented values carries one (DescriptiveComplexity.FinSat.finSatOn_iff_cert). The ∃SO[new] sentence of DescriptiveComplexity.FinSat.Membership is then this statement written out, the invented values being the extension A ⊕ Fin m of the universe and the five relations below the guessed relation variables.

What has to be invented, and why

• the elements of the model (Elt) – unbounded in the instance, which is exactly what ∃SO[new] adds to Σ₁ and what takes the problem out of NP;
• the environments (Env, with Val e x d reading the value of the variable x in the environment e). An environment is a function from the variables of the sentence to the model, so it cannot be a tuple: its arity would be the number of variables of the input. Reifying it as an invented value, with its graph as a guessed ternary relation, is the only way a first-order kernel can quantify over environments. val_update – every environment can be updated at one variable to any value – is what makes the reified environments cover all assignments, and it is used exactly where the truth definition updates the environment, at a quantifier node;
• the truth values of the nodes (G g e), constrained by the truth definition read as an equivalence (step). Well-formedness makes that fixed point unique (DescriptiveComplexity.FinSat.IsEval.iff_Gval), so the guess is forced to be satisfaction – this is where the acyclicity of the parse DAG is spent;
• the truth values of the atoms (H g e), not the interpretation of the relation symbols. An atom's arguments form a tuple of unbounded arity too, so the interpretation cannot be guessed directly; it is instead recovered from H by the coherence condition atom_coh – two atoms of the same symbol whose arguments have the same values get the same truth value – which is first-order and needs no tuples at all. The atom shape conditions of DescriptiveComplexity.FinSat.IsWF are what make that recovery sound.

Note that G must be given separately from H: a node that is a negated atom has the negation of the atom's truth value, so the two cannot be the same relation – the equation G g e ↔ ¬G g e has no solutions.

The certificate

def DescriptiveComplexity.FinSat.UpdAt {A D : Type} (Val : D → A → D → Prop) (e e' : D) (x : A) (d : D) : Prop

e' is the environment e with the variable x set to the value d.

Equations

• DescriptiveComplexity.FinSat.UpdAt Val e e' x d = (Val e' x d ∧ ∀ (y : A), y ≠ x → ∀ (c : D), Val e' y c ↔ Val e y c)

def DescriptiveComplexity.FinSat.CertStep {A : Type} [FirstOrder.Language.finsat.Structure A] {D : Type} (Elt Env : D → Prop) (Val : D → A → D → Prop) (G H : A → D → Prop) (g : A) (e : D) : Prop

The truth definition of DescriptiveComplexity.FinSat.gstep, read on a certificate: environments are invented values, an updated environment is any invented value that updates the given one, and the two atom clauses read the guessed truth value of the atom rather than an interpretation.

Equations

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

structure DescriptiveComplexity.FinSat.CertOK {A : Type} [FirstOrder.Language.finsat.Structure A] {D : Type} (Elt Env : D → Prop) (Val : D → A → D → Prop) (G H : A → D → Prop) : Prop

A certificate of finite satisfiability, over a set D of invented values: a nonempty model Elt, environments Env with their graph Val, truth values G of the nodes and H of the atoms, subject to the conditions of the module docstring. Every condition is first-order in the vocabulary of the instance together with the five relations, which is what makes the ∃SO[new] sentence of DescriptiveComplexity.FinSat.Membership possible.

• elt_nonempty : ∃ (d : D), Elt d

  The model is nonempty.

• env_nonempty : ∃ (e : D), Env e

  There is at least one environment.

• val_total (e : D) : Env e → ∀ (x : A), ∃ (d : D), Elt d ∧ Val e x d

  An environment gives every variable a value in the model.

• val_fun (e : D) : Env e → ∀ (x : A) (d d' : D), Val e x d → Val e x d' → d = d'

  An environment gives every variable at most one value.

• val_update (e : D) : Env e → ∀ (x : A) (d : D), Elt d → ∃ (e' : D), Env e' ∧ UpdAt Val e e' x d

  Environments are closed under updating one variable: this is what makes the invented environments cover every assignment.

• g_ext (g : A) (e e' : D) : Env e → Env e' → (∀ (x : A) (d : D), Val e x d ↔ Val e' x d) → (G g e ↔ G g e')

  The truth value of a node depends on the environment only through the values it gives: two environments with the same graph agree.

• step (g : A) (e : D) : Env e → (G g e ↔ CertStep Elt Env Val G H g e)

  The truth values obey the truth definition.

• atom_coh (g g' s : A) (e e' : D) : Env e → Env e' → PosG g s ∨ NegG g s → PosG g' s ∨ NegG g' s → (∀ (p x x' : A), ArgG g p x → ArgG g' p x' → ∀ (d : D), Val e x d ↔ Val e' x' d) → (H g e ↔ H g' e')

  Atoms cohere: two atoms of the same relation symbol whose arguments have the same values have the same truth value. This is what an interpretation of the symbol is, written without tuples.

• root_holds (g : A) : RootG g → ∀ (e : D), Env e → G g e

  The root holds under every environment.

Matching the arguments of an atom

An assignment of the argument positions matches an atom under an environment when it gives each argument position the value of the variable the atom has there. The shape conditions of DescriptiveComplexity.FinSat.IsWF make such an assignment exist, and make any two of them agree wherever the symbol's signature can see – so “some matching assignment satisfies the symbol” and “every matching assignment does” coincide, which is what the negated atom clause of the truth definition needs.

theorem DescriptiveComplexity.FinSat.matching_exists {A : Type} [FirstOrder.Language.finsat.Structure A] (hwf : IsWF A) (g : A) {M : Type} (v : A → M) : ∃ (w : A → M), ∀ (p x : A), ArgG g p x → w p = v x

Some assignment of the argument positions matches the arguments of an atom: they are functional.

theorem DescriptiveComplexity.FinSat.matching_agree {A : Type} [FirstOrder.Language.finsat.Structure A] (hwf : IsWF A) {g s : A} (hs : PosG g s ∨ NegG g s) {M : Type} {v w w' : A → M} (hw : ∀ (p x : A), ArgG g p x → w p = v x) (hw' : ∀ (p x : A), ArgG g p x → w' p = v x) (p : A) : SigG s p → w p = w' p

Two assignments matching the arguments of an atom agree on every position of its symbol's signature: the atom has an argument at each of them.

From a certificate to a model

def DescriptiveComplexity.FinSat.Represents {A D : Type} (Val : D → A → D → Prop) {Elt : D → Prop} (e : D) (v : A → { d : D // Elt d }) : Prop

The environment object e represents the assignment v.

Equations

• DescriptiveComplexity.FinSat.Represents Val e v = ∀ (x : A), Val e x ↑(v x)

def DescriptiveComplexity.FinSat.CertI {A : Type} [FirstOrder.Language.finsat.Structure A] {D : Type} (Env : D → Prop) (Val : D → A → D → Prop) (H : A → D → Prop) {Elt : D → Prop} (s : A) (w : A → { d : D // Elt d }) : Prop

The interpretation a certificate carries: a symbol holds of an assignment of its argument positions when some atom of that symbol, whose arguments have those values under some environment, is guessed true.

Equations

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

def DescriptiveComplexity.FinSat.CertV {A D : Type} (Env : D → Prop) (Val : D → A → D → Prop) (G : A → D → Prop) {Elt : D → Prop} (v : A → { d : D // Elt d }) (g : A) : Prop

The valuation of the nodes a certificate carries.

Equations

• DescriptiveComplexity.FinSat.CertV Env Val G v g = ∃ (e : D), Env e ∧ DescriptiveComplexity.FinSat.Represents Val e v ∧ G g e

theorem DescriptiveComplexity.FinSat.val_iff_of_represents {A : Type} [FirstOrder.Language.finsat.Structure A] {D : Type} {Elt Env : D → Prop} {Val : D → A → D → Prop} {G H : A → D → Prop} (hc : CertOK Elt Env Val G H) {e : D} (he : Env e) {v : A → { d : D // Elt d }} (hv : Represents Val e v) (x : A) (d : D) : Val e x d ↔ d = ↑(v x)

theorem DescriptiveComplexity.FinSat.represents_exists {A : Type} [FirstOrder.Language.finsat.Structure A] {D : Type} {Elt Env : D → Prop} {Val : D → A → D → Prop} {G H : A → D → Prop} (hc : CertOK Elt Env Val G H) [Finite A] (v : A → { d : D // Elt d }) : ∃ (e : D), Env e ∧ Represents Val e v

Every assignment is represented: the environments are closed under updating one variable, and the instance has finitely many of them.

theorem DescriptiveComplexity.FinSat.certV_iff {A : Type} [FirstOrder.Language.finsat.Structure A] {D : Type} {Elt Env : D → Prop} {Val : D → A → D → Prop} {G H : A → D → Prop} (hc : CertOK Elt Env Val G H) {e : D} (he : Env e) {v : A → { d : D // Elt d }} (hv : Represents Val e v) (g : A) : CertV Env Val G v g ↔ G g e

theorem DescriptiveComplexity.FinSat.certI_local {A : Type} [FirstOrder.Language.finsat.Structure A] {D : Type} {Elt Env : D → Prop} {Val : D → A → D → Prop} {H : A → D → Prop} (hwf : IsWF A) : Local (CertI Env Val H)

The interpretation a certificate carries is local: an atom only has arguments at the positions its symbol declares.

theorem DescriptiveComplexity.FinSat.certH_iff {A : Type} [FirstOrder.Language.finsat.Structure A] {D : Type} {Elt Env : D → Prop} {Val : D → A → D → Prop} {G H : A → D → Prop} (hc : CertOK Elt Env Val G H) (hwf : IsWF A) {g s : A} (hs : PosG g s ∨ NegG g s) {e : D} (he : Env e) {v : A → { d : D // Elt d }} (hv : Represents Val e v) : H g e ↔ ∃ (w : A → { d : D // Elt d }), (∀ (p x : A), ArgG g p x → w p = v x) ∧ CertI Env Val H s w

The guessed truth value of an atom is the truth of that atom in the interpretation the certificate carries: coherence one way, the arguments of the atom the other.

theorem DescriptiveComplexity.FinSat.certH_iff_forall {A : Type} [FirstOrder.Language.finsat.Structure A] {D : Type} {Elt Env : D → Prop} {Val : D → A → D → Prop} {G H : A → D → Prop} (hc : CertOK Elt Env Val G H) (hwf : IsWF A) {g s : A} (hs : PosG g s ∨ NegG g s) {e : D} (he : Env e) {v : A → { d : D // Elt d }} (hv : Represents Val e v) : H g e ↔ ∀ (w : A → { d : D // Elt d }), (∀ (p x : A), ArgG g p x → w p = v x) → CertI Env Val H s w

The same, read universally: all the assignments matching the arguments of an atom give it the same value, so “some matching assignment” and “every matching assignment” agree.

theorem DescriptiveComplexity.FinSat.represents_upd {A D : Type} {Elt : D → Prop} {Val : D → A → D → Prop} {e e' : D} {v : A → { d : D // Elt d }} (hv : Represents Val e v) {x : A} {d : { d : D // Elt d }} (hu : UpdAt Val e e' x ↑d) : Represents Val e' (upd v x d)

theorem DescriptiveComplexity.FinSat.certStep_iff {A : Type} [FirstOrder.Language.finsat.Structure A] {D : Type} {Elt Env : D → Prop} {Val : D → A → D → Prop} {G H : A → D → Prop} (hc : CertOK Elt Env Val G H) [Finite A] (hwf : IsWF A) {e : D} (he : Env e) {v : A → { d : D // Elt d }} (hv : Represents Val e v) (g : A) : CertStep Elt Env Val G H g e ↔ gstep (CertI Env Val H) (CertV Env Val G) v g

The certificate's truth values obey the truth definition of the model it carries: one clause at a time, the invented environments standing for the assignments they represent.

theorem DescriptiveComplexity.FinSat.certV_isEval {A : Type} [FirstOrder.Language.finsat.Structure A] {D : Type} {Elt Env : D → Prop} {Val : D → A → D → Prop} {G H : A → D → Prop} (hc : CertOK Elt Env Val G H) [Finite A] (hwf : IsWF A) : IsEval (CertI Env Val H) (CertV Env Val G)

theorem DescriptiveComplexity.FinSat.finSatOn_of_cert {A : Type} [FirstOrder.Language.finsat.Structure A] {D : Type} {Elt Env : D → Prop} {Val : D → A → D → Prop} {G H : A → D → Prop} (hc : CertOK Elt Env Val G H) [Finite A] [Finite D] (hwf : IsWF A) : FinSatOn A

A certificate gives a finite model: its marked values are the universe, its coherent atom values the interpretation, and its node values satisfaction – by uniqueness of the fixed point of the truth definition.

From a model to a certificate

The invented values are the assignments themselves: an environment is an assignment, and an element of the model is the constant assignment at it.

def DescriptiveComplexity.FinSat.EnvElt {A M : Type} (d : A → M) : Prop

The invented values standing for elements of the model: the constant assignments.

Equations

• DescriptiveComplexity.FinSat.EnvElt d = ∃ (z : M), d = fun (x : A) => z

def DescriptiveComplexity.FinSat.EnvVal {A M : Type} (e : A → M) (x : A) (d : A → M) : Prop

The graph of an environment, when environments are assignments.

Equations

• DescriptiveComplexity.FinSat.EnvVal e x d = (d = fun (x_1 : A) => e x)

def DescriptiveComplexity.FinSat.EnvG {A : Type} [FirstOrder.Language.finsat.Structure A] {M : Type} (I : A → (A → M) → Prop) (g : A) (e : A → M) : Prop

The truth values of the nodes read off satisfaction.

Equations

• DescriptiveComplexity.FinSat.EnvG I g e = DescriptiveComplexity.FinSat.Gval I e g

def DescriptiveComplexity.FinSat.EnvH {A : Type} [FirstOrder.Language.finsat.Structure A] {M : Type} (I : A → (A → M) → Prop) (g : A) (e : A → M) : Prop

The truth values of the atoms read off the interpretation.

Equations

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

theorem DescriptiveComplexity.FinSat.envVal_eq {A M : Type} [Nonempty A] {e e' : A → M} {x x' : A} (h : ∀ (d : A → M), EnvVal e x d ↔ EnvVal e' x' d) : e x = e' x'

theorem DescriptiveComplexity.FinSat.updAt_upd {A M : Type} (e : A → M) (x : A) (z : M) : UpdAt EnvVal e (upd e x z) x fun (x : A) => z

theorem DescriptiveComplexity.FinSat.eq_upd_of_updAt {A M : Type} [Nonempty A] {e e' : A → M} {x : A} {z : M} (hu : UpdAt EnvVal e e' x fun (x : A) => z) : e' = upd e x z

theorem DescriptiveComplexity.FinSat.envH_iff {A : Type} [FirstOrder.Language.finsat.Structure A] {M : Type} {I : A → (A → M) → Prop} (hwf : IsWF A) {g s : A} (hs : PosG g s ∨ NegG g s) (e : A → M) : EnvH I g e ↔ ∃ (w : A → M), (∀ (p x : A), ArgG g p x → w p = e x) ∧ I s w

theorem DescriptiveComplexity.FinSat.envH_iff_forall {A : Type} [FirstOrder.Language.finsat.Structure A] {M : Type} {I : A → (A → M) → Prop} (hwf : IsWF A) (hloc : Local I) {g s : A} (hs : PosG g s ∨ NegG g s) (e : A → M) : EnvH I g e ↔ ∀ (w : A → M), (∀ (p x : A), ArgG g p x → w p = e x) → I s w

The same, read universally: every assignment matching the arguments of an atom gives it the same value.

theorem DescriptiveComplexity.FinSat.envH_coh {A : Type} [FirstOrder.Language.finsat.Structure A] {M : Type} [Nonempty A] {I : A → (A → M) → Prop} (hwf : IsWF A) (hloc : Local I) {g g' s : A} {e e' : A → M} (hs : PosG g s ∨ NegG g s) (hs' : PosG g' s ∨ NegG g' s) (hval : ∀ (p x x' : A), ArgG g p x → ArgG g' p x' → ∀ (d : A → M), EnvVal e x d ↔ EnvVal e' x' d) : EnvH I g e → EnvH I g' e'

The atom values read off a local interpretation cohere: an atom's arguments cover exactly the argument positions of its symbol, so two atoms of that symbol whose arguments have the same values are read at the same tuple.

theorem DescriptiveComplexity.FinSat.cert_of_model {A : Type} [FirstOrder.Language.finsat.Structure A] {M : Type} [Nonempty A] {I : A → (A → M) → Prop} [Finite A] [Finite M] [Nonempty M] (hwf : IsWF A) (hloc : Local I) (hroot : ∀ (v : A → M) (g : A), RootG g → Gval I v g) : CertOK EnvElt (fun (x : A → M) => True) EnvVal (EnvG I) (EnvH I)

A finite model gives a certificate: invent the assignments.

Relabelling the invented values

The ∃SO[new] sentence of DescriptiveComplexity.FinSat.Membership guesses its relations over A ⊕ Fin m, so it needs the invented values indexed. Nothing in DescriptiveComplexity.FinSat.CertOK looks at the set of invented values beyond its elements, so a bijection carries a certificate over one such set to a certificate over another, one field at a time.

def DescriptiveComplexity.FinSat.mapVal {A D D' : Type} (σ : D ≃ D') (Val : D → A → D → Prop) : D' → A → D' → Prop

The graph of an environment, relabelled along a bijection of the invented values.

Equations

• DescriptiveComplexity.FinSat.mapVal σ Val e x d = Val (σ.symm e) x (σ.symm d)

theorem DescriptiveComplexity.FinSat.updAt_map {A D D' : Type} (σ : D ≃ D') (Val : D → A → D → Prop) (e e' : D') (x : A) (d : D') : UpdAt (mapVal σ Val) e e' x d ↔ UpdAt Val (σ.symm e) (σ.symm e') x (σ.symm d)

theorem DescriptiveComplexity.FinSat.certStep_map {A : Type} [FirstOrder.Language.finsat.Structure A] {D D' : Type} (σ : D ≃ D') {Elt Env : D → Prop} {Val : D → A → D → Prop} {G H : A → D → Prop} (g : A) (e : D') : CertStep (fun (d : D') => Elt (σ.symm d)) (fun (e : D') => Env (σ.symm e)) (mapVal σ Val) (fun (g : A) (e : D') => G g (σ.symm e)) (fun (g : A) (e : D') => H g (σ.symm e)) g e ↔ CertStep Elt Env Val G H g (σ.symm e)

The truth definition, read on a relabelled certificate.

theorem DescriptiveComplexity.FinSat.CertOK.map {A : Type} [FirstOrder.Language.finsat.Structure A] {D D' : Type} (σ : D ≃ D') {Elt Env : D → Prop} {Val : D → A → D → Prop} {G H : A → D → Prop} (hc : CertOK Elt Env Val G H) : CertOK (fun (d : D') => Elt (σ.symm d)) (fun (e : D') => Env (σ.symm e)) (mapVal σ Val) (fun (g : A) (e : D') => G g (σ.symm e)) fun (g : A) (e : D') => H g (σ.symm e)

A certificate can be carried to any equinumerous set of invented values, which is what lets the ∃SO[new] sentence guess its relations over the extension A ⊕ Fin m of the universe.

The characterization

theorem DescriptiveComplexity.FinSat.finSatOn_iff_cert (A : Type) [FirstOrder.Language.finsat.Structure A] [Finite A] [Nonempty A] : FinSatOn A ↔ IsWF A ∧ ∃ (D : Type) (_ : Finite D) (Elt : D → Prop) (Env : D → Prop) (Val : D → A → D → Prop) (G : A → D → Prop) (H : A → D → Prop), CertOK Elt Env Val G H

An encoded sentence has a finite model exactly when a finite set of invented values carries one. The right-hand side is first-order in the instance together with five guessed relations, which is what DescriptiveComplexity.FinSat.Membership turns into an ∃SO[new] sentence.

theorem DescriptiveComplexity.FinSat.finSatOn_iff_certFin (A : Type) [FirstOrder.Language.finsat.Structure A] [Finite A] [Nonempty A] : FinSatOn A ↔ IsWF A ∧ ∃ (m : ℕ) (Elt : Fin m → Prop) (Env : Fin m → Prop) (Val : Fin m → A → Fin m → Prop) (G : A → Fin m → Prop) (H : A → Fin m → Prop), CertOK Elt Env Val G H

The same, with the invented values indexed: exactly the form the ∃SO[new] sentence of DescriptiveComplexity.FinSat.Membership needs, its relation variables ranging over the extension A ⊕ Fin m of the universe.