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.Problems.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.Problems.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.

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)

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)

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.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.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

Relabeling the invented values

The ∃SO[new] sentence of DescriptiveComplexity.Problems.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.

theorem DescriptiveComplexity.FinSat.forall_symm {D D' : Type} (σ : D ≃ D') (p : D → Prop) : (∀ (d : D'), p (σ.symm d)) ↔ ∀ (d : D), p d

theorem DescriptiveComplexity.FinSat.exists_symm {D D' : Type} (σ : D ≃ D') (p : D → Prop) : (∃ (d : D'), p (σ.symm d)) ↔ ∃ (d : D), p d

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

The graph of an environment, relabeled 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.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.Problems.FinSat.Membership turns into an ∃SO[new] sentence.