FINSAT is in RE

The membership half of Trakhtenbrot's theorem: finite satisfiability of an encoded sentence is definable in ∃SO[new] (DescriptiveComplexity.finsat_sigmaSONewDefinable), the logic defining RE.

The mathematical content is DescriptiveComplexity.FinSat.finSatOn_iff_cert: an encoded sentence has a finite model exactly when a finite set of invented values carries a certificate – a model, environments with their graph, and truth values for the nodes and for the atoms. This file is that statement written out in syntax:

• the invented values are the extension A ⊕ Fin m of the universe, m unbounded – the only difference from a Σ₁ definition, and what puts the problem beyond NP;
• the five components of the certificate are the relation variables of a single existential second-order block (DescriptiveComplexity.FinSat.certBlock);
• every condition on them is a conjunct of the first-order kernel, with each quantifier guarded by its sort: the variables ranging over the instance by old, those ranging over the invented values by its negation. The guards are what make the kernel say exactly the certificate conditions, in both directions, rather than something stronger on one side.

The second-order block

inductive DescriptiveComplexity.FinSat.CertIx : Type

The relation variables of the ∃SO[new] definition of FINSAT: the model, the environments, the graph of an environment, the truth values of the nodes and the truth values of the atoms.

• elt : CertIx

  The elements of the model.

• env : CertIx

  The environments.

• val : CertIx

  val e x d: the environment e gives the variable x the value d.

• gv : CertIx

  gv g e: the node g holds under the environment e.

• hv : CertIx

  hv g e: the atom at g holds under the environment e.

@[instance_reducible]

instance DescriptiveComplexity.FinSat.instDecidableEqCertIx : DecidableEq CertIx

Equations

• DescriptiveComplexity.FinSat.instDecidableEqCertIx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.FinSat.instFintypeCertIx : Fintype CertIx

Equations

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

def DescriptiveComplexity.FinSat.certBlock : SOBlock

The single existential block of the definition.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.certLang : FirstOrder.Language

The vocabulary of the kernel: that of the instance, the marker old of the original elements, and the five relation variables.

Equations

• DescriptiveComplexity.FinSat.certLang = DescriptiveComplexity.soLang (DescriptiveComplexity.newLang FirstOrder.Language.finsat) [DescriptiveComplexity.FinSat.certBlock]

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.instSym {n : ℕ} (R : FirstOrder.Language.finsat.Relations n) : certLang.Relations n

A relation symbol of the instance, in the kernel's vocabulary.

Equations

• DescriptiveComplexity.FinSat.instSym R = Sum.inl (Sum.inl R)

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.oldSym : certLang.Relations 1

The marker of the original elements, in the kernel's vocabulary.

Equations

• DescriptiveComplexity.FinSat.oldSym = Sum.inl (Sum.inr FirstOrder.Language.oldSym)

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.eltSym : certLang.Relations 1

The relation variable of the model.

Equations

• DescriptiveComplexity.FinSat.eltSym = Sum.inr ⟨DescriptiveComplexity.FinSat.CertIx.elt, DescriptiveComplexity.FinSat.eltSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.envSym : certLang.Relations 1

The relation variable of the environments.

Equations

• DescriptiveComplexity.FinSat.envSym = Sum.inr ⟨DescriptiveComplexity.FinSat.CertIx.env, DescriptiveComplexity.FinSat.envSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.valSym : certLang.Relations 3

The relation variable of the graph of an environment.

Equations

• DescriptiveComplexity.FinSat.valSym = Sum.inr ⟨DescriptiveComplexity.FinSat.CertIx.val, DescriptiveComplexity.FinSat.valSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.gSym : certLang.Relations 2

The relation variable of the truth values of the nodes.

Equations

• DescriptiveComplexity.FinSat.gSym = Sum.inr ⟨DescriptiveComplexity.FinSat.CertIx.gv, DescriptiveComplexity.FinSat.gSym._proof_1⟩

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.hSym : certLang.Relations 2

The relation variable of the truth values of the atoms.

Equations

• DescriptiveComplexity.FinSat.hSym = Sum.inr ⟨DescriptiveComplexity.FinSat.CertIx.hv, DescriptiveComplexity.FinSat.hSym._proof_1⟩

The extended universe

@[instance_reducible]

noncomputable def DescriptiveComplexity.FinSat.extFinsat {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} : FirstOrder.Language.finsat.Structure (A ⊕ Fin m)

The vocabulary of the instance, read on the extended universe: a relation holds only of original elements, and there of what it holds of in the instance.

Equations

• DescriptiveComplexity.FinSat.extFinsat = DescriptiveComplexity.extBase FirstOrder.Language.finsat A m

@[instance_reducible]

noncomputable def DescriptiveComplexity.FinSat.certStr {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} (ρ : certBlock.Assignment (A ⊕ Fin m)) : certLang.Structure (A ⊕ Fin m)

The structure the kernel is read in: the extended structure together with an assignment of the relation variables.

Equations

• DescriptiveComplexity.FinSat.certStr ρ = (DescriptiveComplexity.newLang FirstOrder.Language.finsat).sumStructure DescriptiveComplexity.FinSat.certBlock.lang (A ⊕ Fin m)

The instance, read on the extended universe

A relation of the instance holds on the extended universe only of original elements, and there of what it holds of in the instance – so at original arguments the kernel reads the instance itself.

theorem DescriptiveComplexity.FinSat.relMap_inl {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m k : ℕ} (R : FirstOrder.Language.finsat.Relations k) (y : Fin k → A) : (FirstOrder.Language.Structure.RelMap R fun (i : Fin k) => Sum.inl (y i)) ↔ FirstOrder.Language.Structure.RelMap R y

@[simp]

theorem DescriptiveComplexity.FinSat.relMap_inl₁ {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} (R : FirstOrder.Language.finsat.Relations 1) (a : A) : FirstOrder.Language.Structure.RelMap R ![Sum.inl a] ↔ FirstOrder.Language.Structure.RelMap R ![a]

@[simp]

theorem DescriptiveComplexity.FinSat.relMap_inl₂ {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} (R : FirstOrder.Language.finsat.Relations 2) (a b : A) : FirstOrder.Language.Structure.RelMap R ![Sum.inl a, Sum.inl b] ↔ FirstOrder.Language.Structure.RelMap R ![a, b]

@[simp]

theorem DescriptiveComplexity.FinSat.relMap_inl₃ {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} (R : FirstOrder.Language.finsat.Relations 3) (a b c : A) : FirstOrder.Language.Structure.RelMap R ![Sum.inl a, Sum.inl b, Sum.inl c] ↔ FirstOrder.Language.Structure.RelMap R ![a, b, c]

The certificate an assignment carries

The five relation variables, read at the sorts they are meant for: the model and the environments among the invented values, the graph of an environment and the truth values across the two sorts. These are the components of the certificate DescriptiveComplexity.FinSat.CertOK the kernel says the assignment is.

def DescriptiveComplexity.FinSat.certElt {A : Type} {m : ℕ} (ρ : certBlock.Assignment (A ⊕ Fin m)) (d : Fin m) : Prop

The elements of the model an assignment carries.

Equations

• DescriptiveComplexity.FinSat.certElt ρ d = ρ DescriptiveComplexity.FinSat.CertIx.elt ![Sum.inr d]

def DescriptiveComplexity.FinSat.certEnv {A : Type} {m : ℕ} (ρ : certBlock.Assignment (A ⊕ Fin m)) (e : Fin m) : Prop

The environments an assignment carries.

Equations

• DescriptiveComplexity.FinSat.certEnv ρ e = ρ DescriptiveComplexity.FinSat.CertIx.env ![Sum.inr e]

def DescriptiveComplexity.FinSat.certVal {A : Type} {m : ℕ} (ρ : certBlock.Assignment (A ⊕ Fin m)) (e : Fin m) (x : A) (d : Fin m) : Prop

The graph of an environment, read off an assignment.

Equations

• DescriptiveComplexity.FinSat.certVal ρ e x d = ρ DescriptiveComplexity.FinSat.CertIx.val ![Sum.inr e, Sum.inl x, Sum.inr d]

def DescriptiveComplexity.FinSat.certG {A : Type} {m : ℕ} (ρ : certBlock.Assignment (A ⊕ Fin m)) (g : A) (e : Fin m) : Prop

The truth values of the nodes an assignment carries.

Equations

• DescriptiveComplexity.FinSat.certG ρ g e = ρ DescriptiveComplexity.FinSat.CertIx.gv ![Sum.inl g, Sum.inr e]

def DescriptiveComplexity.FinSat.certH {A : Type} {m : ℕ} (ρ : certBlock.Assignment (A ⊕ Fin m)) (g : A) (e : Fin m) : Prop

The truth values of the atoms an assignment carries.

Equations

• DescriptiveComplexity.FinSat.certH ρ g e = ρ DescriptiveComplexity.FinSat.CertIx.hv ![Sum.inl g, Sum.inr e]

Atomic formulas

noncomputable def DescriptiveComplexity.FinSat.instF₁ {γ : Type} (R : FirstOrder.Language.finsat.Relations 1) (x : γ) : certLang.Formula γ

An atom of a unary relation of the instance.

Equations

• DescriptiveComplexity.FinSat.instF₁ R x = (DescriptiveComplexity.FinSat.instSym R).formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.FinSat.instF₂ {γ : Type} (R : FirstOrder.Language.finsat.Relations 2) (x y : γ) : certLang.Formula γ

An atom of a binary relation of the instance.

Equations

• DescriptiveComplexity.FinSat.instF₂ R x y = (DescriptiveComplexity.FinSat.instSym R).formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

noncomputable def DescriptiveComplexity.FinSat.instF₃ {γ : Type} (R : FirstOrder.Language.finsat.Relations 3) (x y z : γ) : certLang.Formula γ

An atom of a ternary relation of the instance.

Equations

• DescriptiveComplexity.FinSat.instF₃ R x y z = (DescriptiveComplexity.FinSat.instSym R).formula ![FirstOrder.Language.var x, FirstOrder.Language.var y, FirstOrder.Language.var z]

noncomputable def DescriptiveComplexity.FinSat.oldF {γ : Type} (x : γ) : certLang.Formula γ

x is an original element.

Equations

• DescriptiveComplexity.FinSat.oldF x = DescriptiveComplexity.FinSat.oldSym.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.FinSat.eltF {γ : Type} (x : γ) : certLang.Formula γ

x is an element of the model.

Equations

• DescriptiveComplexity.FinSat.eltF x = DescriptiveComplexity.FinSat.eltSym.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.FinSat.envF {γ : Type} (x : γ) : certLang.Formula γ

x is an environment.

Equations

• DescriptiveComplexity.FinSat.envF x = DescriptiveComplexity.FinSat.envSym.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.FinSat.valF {γ : Type} (e x d : γ) : certLang.Formula γ

The environment e gives the variable x the value d.

Equations

• DescriptiveComplexity.FinSat.valF e x d = DescriptiveComplexity.FinSat.valSym.formula ![FirstOrder.Language.var e, FirstOrder.Language.var x, FirstOrder.Language.var d]

noncomputable def DescriptiveComplexity.FinSat.gF {γ : Type} (g e : γ) : certLang.Formula γ

The node g holds under the environment e.

Equations

• DescriptiveComplexity.FinSat.gF g e = DescriptiveComplexity.FinSat.gSym.formula₂ (FirstOrder.Language.var g) (FirstOrder.Language.var e)

noncomputable def DescriptiveComplexity.FinSat.hF {γ : Type} (g e : γ) : certLang.Formula γ

The atom at g holds under the environment e.

Equations

• DescriptiveComplexity.FinSat.hF g e = DescriptiveComplexity.FinSat.hSym.formula₂ (FirstOrder.Language.var g) (FirstOrder.Language.var e)

@[simp]

theorem DescriptiveComplexity.FinSat.realize_instF₁ {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (R : FirstOrder.Language.finsat.Relations 1) (x : γ) (v : γ → A ⊕ Fin m) : (instF₁ R x).Realize v ↔ FirstOrder.Language.Structure.RelMap R ![v x]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_instF₂ {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (R : FirstOrder.Language.finsat.Relations 2) (x y : γ) (v : γ → A ⊕ Fin m) : (instF₂ R x y).Realize v ↔ FirstOrder.Language.Structure.RelMap R ![v x, v y]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_instF₃ {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (R : FirstOrder.Language.finsat.Relations 3) (x y z : γ) (v : γ → A ⊕ Fin m) : (instF₃ R x y z).Realize v ↔ FirstOrder.Language.Structure.RelMap R ![v x, v y, v z]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_oldF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (oldF x).Realize v ↔ IsOld (v x)

@[simp]

theorem DescriptiveComplexity.FinSat.realize_eltF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (eltF x).Realize v ↔ ρ CertIx.elt ![v x]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_envF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x : γ) (v : γ → A ⊕ Fin m) : (envF x).Realize v ↔ ρ CertIx.env ![v x]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_valF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (e x d : γ) (v : γ → A ⊕ Fin m) : (valF e x d).Realize v ↔ ρ CertIx.val ![v e, v x, v d]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_gF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (g e : γ) (v : γ → A ⊕ Fin m) : (gF g e).Realize v ↔ ρ CertIx.gv ![v g, v e]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_hF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (g e : γ) (v : γ → A ⊕ Fin m) : (hF g e).Realize v ↔ ρ CertIx.hv ![v g, v e]

noncomputable def DescriptiveComplexity.FinSat.eqF {γ : Type} (x y : γ) : certLang.Formula γ

Equality of two variables.

Equations

• DescriptiveComplexity.FinSat.eqF x y = (FirstOrder.Language.var x).equal (FirstOrder.Language.var y)

@[simp]

theorem DescriptiveComplexity.FinSat.realize_eqF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y : γ) (v : γ → A ⊕ Fin m) : (eqF x y).Realize v ↔ v x = v y

Naming the symbols of the instance

noncomputable def DescriptiveComplexity.FinSat.leF {γ : Type} (x y : γ) : certLang.Formula γ

The order of the syntax.

Equations

• DescriptiveComplexity.FinSat.leF x y = DescriptiveComplexity.FinSat.instF₂ FirstOrder.Language.finsatLeSym x y

noncomputable def DescriptiveComplexity.FinSat.andNF {γ : Type} (g : γ) : certLang.Formula γ

The node g is a conjunction.

Equations

• DescriptiveComplexity.FinSat.andNF g = DescriptiveComplexity.FinSat.instF₁ FirstOrder.Language.finsatAndSym g

noncomputable def DescriptiveComplexity.FinSat.orNF {γ : Type} (g : γ) : certLang.Formula γ

The node g is a disjunction.

Equations

• DescriptiveComplexity.FinSat.orNF g = DescriptiveComplexity.FinSat.instF₁ FirstOrder.Language.finsatOrSym g

noncomputable def DescriptiveComplexity.FinSat.allNF {γ : Type} (g : γ) : certLang.Formula γ

The node g is a universal quantifier.

Equations

• DescriptiveComplexity.FinSat.allNF g = DescriptiveComplexity.FinSat.instF₁ FirstOrder.Language.finsatAllSym g

noncomputable def DescriptiveComplexity.FinSat.exNF {γ : Type} (g : γ) : certLang.Formula γ

The node g is an existential quantifier.

Equations

• DescriptiveComplexity.FinSat.exNF g = DescriptiveComplexity.FinSat.instF₁ FirstOrder.Language.finsatExSym g

noncomputable def DescriptiveComplexity.FinSat.childF {γ : Type} (g c : γ) : certLang.Formula γ

The node c is a child of the node g.

Equations

• DescriptiveComplexity.FinSat.childF g c = DescriptiveComplexity.FinSat.instF₂ FirstOrder.Language.finsatChildSym g c

noncomputable def DescriptiveComplexity.FinSat.bindF {γ : Type} (g x : γ) : certLang.Formula γ

The quantifier node g binds the variable x.

Equations

• DescriptiveComplexity.FinSat.bindF g x = DescriptiveComplexity.FinSat.instF₂ FirstOrder.Language.finsatBindSym g x

noncomputable def DescriptiveComplexity.FinSat.eqLF {γ : Type} (g x y : γ) : certLang.Formula γ

The node g is the literal x = y.

Equations

• DescriptiveComplexity.FinSat.eqLF g x y = DescriptiveComplexity.FinSat.instF₃ FirstOrder.Language.finsatEqSym g x y

noncomputable def DescriptiveComplexity.FinSat.neqLF {γ : Type} (g x y : γ) : certLang.Formula γ

The node g is the literal x ≠ y.

Equations

• DescriptiveComplexity.FinSat.neqLF g x y = DescriptiveComplexity.FinSat.instF₃ FirstOrder.Language.finsatNeqSym g x y

noncomputable def DescriptiveComplexity.FinSat.posLF {γ : Type} (g s : γ) : certLang.Formula γ

The node g is a positive atom of the symbol s.

Equations

• DescriptiveComplexity.FinSat.posLF g s = DescriptiveComplexity.FinSat.instF₂ FirstOrder.Language.finsatPosSym g s

noncomputable def DescriptiveComplexity.FinSat.negLF {γ : Type} (g s : γ) : certLang.Formula γ

The node g is a negated atom of the symbol s.

Equations

• DescriptiveComplexity.FinSat.negLF g s = DescriptiveComplexity.FinSat.instF₂ FirstOrder.Language.finsatNegSym g s

noncomputable def DescriptiveComplexity.FinSat.argF {γ : Type} (g p x : γ) : certLang.Formula γ

The argument of the atom g at position p is the variable x.

Equations

• DescriptiveComplexity.FinSat.argF g p x = DescriptiveComplexity.FinSat.instF₃ FirstOrder.Language.finsatArgSym g p x

noncomputable def DescriptiveComplexity.FinSat.sigF {γ : Type} (s p : γ) : certLang.Formula γ

The symbol s has an argument position p.

Equations

• DescriptiveComplexity.FinSat.sigF s p = DescriptiveComplexity.FinSat.instF₂ FirstOrder.Language.finsatSigSym s p

noncomputable def DescriptiveComplexity.FinSat.rootF {γ : Type} (g : γ) : certLang.Formula γ

The node g is the root of the encoded sentence.

Equations

• DescriptiveComplexity.FinSat.rootF g = DescriptiveComplexity.FinSat.instF₁ FirstOrder.Language.finsatRootSym g

@[simp]

theorem DescriptiveComplexity.FinSat.realize_leF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (x y : γ) (v : γ → A ⊕ Fin m) : (leF x y).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.finsatLeSym ![v x, v y]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_andNF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (g : γ) (v : γ → A ⊕ Fin m) : (andNF g).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.finsatAndSym ![v g]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_orNF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (g : γ) (v : γ → A ⊕ Fin m) : (orNF g).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.finsatOrSym ![v g]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_allNF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (g : γ) (v : γ → A ⊕ Fin m) : (allNF g).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.finsatAllSym ![v g]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_exNF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (g : γ) (v : γ → A ⊕ Fin m) : (exNF g).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.finsatExSym ![v g]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_childF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (g c : γ) (v : γ → A ⊕ Fin m) : (childF g c).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.finsatChildSym ![v g, v c]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_bindF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (g x : γ) (v : γ → A ⊕ Fin m) : (bindF g x).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.finsatBindSym ![v g, v x]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_eqLF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (g x y : γ) (v : γ → A ⊕ Fin m) : (eqLF g x y).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.finsatEqSym ![v g, v x, v y]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_neqLF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (g x y : γ) (v : γ → A ⊕ Fin m) : (neqLF g x y).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.finsatNeqSym ![v g, v x, v y]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_posLF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (g s : γ) (v : γ → A ⊕ Fin m) : (posLF g s).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.finsatPosSym ![v g, v s]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_negLF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (g s : γ) (v : γ → A ⊕ Fin m) : (negLF g s).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.finsatNegSym ![v g, v s]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_argF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (g p x : γ) (v : γ → A ⊕ Fin m) : (argF g p x).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.finsatArgSym ![v g, v p, v x]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_sigF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (s p : γ) (v : γ → A ⊕ Fin m) : (sigF s p).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.finsatSigSym ![v s, v p]

@[simp]

theorem DescriptiveComplexity.FinSat.realize_rootF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (g : γ) (v : γ → A ⊕ Fin m) : (rootF g).Realize v ↔ FirstOrder.Language.Structure.RelMap FirstOrder.Language.finsatRootSym ![v g]

Guarded quantifiers

Every quantifier of the kernel ranges over one of the two sorts of the extended universe – the original elements, marked by old, and the invented values – and is guarded accordingly. The guards are not decoration: one missing in a hypothesis position (inside the update relation of the universal-quantifier clause, or in the agreement hypotheses of g_ext and atom_coh) makes the kernel demand of an assignment more than the certificate gives, and that direction of the correspondence no longer closes.

A variable is named by its distance from its binder: vr0 is bound by the innermost guarded quantifier, vr1 by the one just outside it, and so on – so passing under one more quantifier increments every index, and up is that same shift applied to a variable given by name.

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.up {γ : Type} (x : γ) : γ ⊕ Unit

A variable of the enclosing scope, seen from inside one guarded quantifier.

Equations

• DescriptiveComplexity.FinSat.up x = Sum.inl x

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.vr0 {γ : Type} : γ ⊕ Unit

The variable bound by the innermost guarded quantifier.

Equations

• DescriptiveComplexity.FinSat.vr0 = Sum.inr ()

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.vr1 {γ : Type} : (γ ⊕ Unit) ⊕ Unit

The variable bound one guarded quantifier further out.

Equations

• DescriptiveComplexity.FinSat.vr1 = DescriptiveComplexity.FinSat.up DescriptiveComplexity.FinSat.vr0

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.vr2 {γ : Type} : ((γ ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound two guarded quantifiers further out.

Equations

• DescriptiveComplexity.FinSat.vr2 = DescriptiveComplexity.FinSat.up DescriptiveComplexity.FinSat.vr1

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.vr3 {γ : Type} : (((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound three guarded quantifiers further out.

Equations

• DescriptiveComplexity.FinSat.vr3 = DescriptiveComplexity.FinSat.up DescriptiveComplexity.FinSat.vr2

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.vr4 {γ : Type} : ((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound four guarded quantifiers further out.

Equations

• DescriptiveComplexity.FinSat.vr4 = DescriptiveComplexity.FinSat.up DescriptiveComplexity.FinSat.vr3

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.vr5 {γ : Type} : (((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound five guarded quantifiers further out.

Equations

• DescriptiveComplexity.FinSat.vr5 = DescriptiveComplexity.FinSat.up DescriptiveComplexity.FinSat.vr4

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.vr6 {γ : Type} : ((((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound six guarded quantifiers further out.

Equations

• DescriptiveComplexity.FinSat.vr6 = DescriptiveComplexity.FinSat.up DescriptiveComplexity.FinSat.vr5

@[reducible, inline]

abbrev DescriptiveComplexity.FinSat.vr7 {γ : Type} : (((((((γ ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit) ⊕ Unit

The variable bound seven guarded quantifiers further out.

Equations

• DescriptiveComplexity.FinSat.vr7 = DescriptiveComplexity.FinSat.up DescriptiveComplexity.FinSat.vr6

noncomputable def DescriptiveComplexity.FinSat.exOldF {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) : certLang.Formula γ

∃ x, old x ∧ φ: a quantifier over the original elements.

Equations

• DescriptiveComplexity.FinSat.exOldF φ = FirstOrder.Language.Formula.iExs Unit (DescriptiveComplexity.FinSat.oldF DescriptiveComplexity.FinSat.vr0 ⊓ φ)

noncomputable def DescriptiveComplexity.FinSat.allOldF {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) : certLang.Formula γ

∀ x, old x → φ: a quantifier over the original elements.

Equations

• DescriptiveComplexity.FinSat.allOldF φ = FirstOrder.Language.Formula.iAlls Unit (FirstOrder.Language.BoundedFormula.imp (DescriptiveComplexity.FinSat.oldF DescriptiveComplexity.FinSat.vr0) φ)

noncomputable def DescriptiveComplexity.FinSat.exNewF {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) : certLang.Formula γ

∃ d, ¬old d ∧ φ: a quantifier over the invented values.

Equations

• DescriptiveComplexity.FinSat.exNewF φ = FirstOrder.Language.Formula.iExs Unit (FirstOrder.Language.BoundedFormula.not (DescriptiveComplexity.FinSat.oldF DescriptiveComplexity.FinSat.vr0) ⊓ φ)

noncomputable def DescriptiveComplexity.FinSat.allNewF {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) : certLang.Formula γ

∀ d, ¬old d → φ: a quantifier over the invented values.

Equations

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

theorem DescriptiveComplexity.FinSat.exists_inr_of_not_isOld {A : Type} {m : ℕ} {x : A ⊕ Fin m} (h : ¬IsOld x) : ∃ (j : Fin m), x = Sum.inr j

@[simp]

theorem DescriptiveComplexity.FinSat.realize_exOldF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) (v : γ → A ⊕ Fin m) : (exOldF φ).Realize v ↔ ∃ (a : A), φ.Realize (Sum.elim v fun (x : Unit) => Sum.inl a)

@[simp]

theorem DescriptiveComplexity.FinSat.realize_allOldF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) (v : γ → A ⊕ Fin m) : (allOldF φ).Realize v ↔ ∀ (a : A), φ.Realize (Sum.elim v fun (x : Unit) => Sum.inl a)

@[simp]

theorem DescriptiveComplexity.FinSat.realize_exNewF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) (v : γ → A ⊕ Fin m) : (exNewF φ).Realize v ↔ ∃ (j : Fin m), φ.Realize (Sum.elim v fun (x : Unit) => Sum.inr j)

@[simp]

theorem DescriptiveComplexity.FinSat.realize_allNewF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (φ : certLang.Formula (γ ⊕ Unit)) (v : γ → A ⊕ Fin m) : (allNewF φ).Realize v ↔ ∀ (j : Fin m), φ.Realize (Sum.elim v fun (x : Unit) => Sum.inr j)

Well-formedness

The kernel has to check well-formedness, since junk instances are no-instances: each condition of DescriptiveComplexity.FinSat.IsWF is one conjunct, every quantifier ranging over the original elements.

noncomputable def DescriptiveComplexity.FinSat.ordReflS : certLang.Sentence

The order of the syntax is reflexive.

Equations

• DescriptiveComplexity.FinSat.ordReflS = DescriptiveComplexity.FinSat.allOldF (DescriptiveComplexity.FinSat.leF DescriptiveComplexity.FinSat.vr0 DescriptiveComplexity.FinSat.vr0)

noncomputable def DescriptiveComplexity.FinSat.ordTransS : certLang.Sentence

The order of the syntax is transitive.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.ordAntisymmS : certLang.Sentence

The order of the syntax is antisymmetric.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.ordTotalS : certLang.Sentence

The order of the syntax is total.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.childLtS : certLang.Sentence

Children come strictly earlier in the order of the syntax.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.argFunS : certLang.Sentence

An atom has at most one argument at each position.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.atomSymS : certLang.Sentence

An atom has at most one relation symbol.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.argSigS : certLang.Sentence

An atom only has arguments at the positions of its symbol's signature.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.argTotS : certLang.Sentence

An atom has an argument at every position of its symbol's signature.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.wfS : certLang.Sentence

The instance is well-formed: the nine conditions of DescriptiveComplexity.FinSat.IsWF, conjoined.

Equations

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

theorem DescriptiveComplexity.FinSat.realize_wfS {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} : (A ⊕ Fin m) ⊨ wfS ↔ IsWF A

The truth definition

DescriptiveComplexity.FinSat.CertStep written out: one disjunct per kind of node, the environments and the values of the model ranging over the invented values and everything read off the encoding over the original elements.

noncomputable def DescriptiveComplexity.FinSat.updF {γ : Type} (e e' x d : γ) : certLang.Formula γ

e' is the environment e with the variable x set to the value d (DescriptiveComplexity.FinSat.UpdAt). Its inner quantifiers carry guards like every other, and here it matters: this clause occurs in a hypothesis position inside the universal-quantifier disjunct below.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.stepBodyF {γ : Type} (g e : γ) : certLang.Formula γ

The value of the node g under the environment e, one disjunct per kind of node.

Equations

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

theorem DescriptiveComplexity.FinSat.realize_stepBodyF {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} {γ : Type} (g e : γ) (v : γ → A ⊕ Fin m) (a : A) (i : Fin m) (hg : v g = Sum.inl a) (he : v e = Sum.inr i) : (stepBodyF g e).Realize v ↔ CertStep (certElt ρ) (certEnv ρ) (certVal ρ) (certG ρ) (certH ρ) a i

The disjunction is the truth definition read on the certificate the assignment carries.

The certificate

One conjunct per field of DescriptiveComplexity.FinSat.CertOK.

noncomputable def DescriptiveComplexity.FinSat.eltNeS : certLang.Sentence

The model is nonempty.

Equations

• DescriptiveComplexity.FinSat.eltNeS = DescriptiveComplexity.FinSat.exNewF (DescriptiveComplexity.FinSat.eltF DescriptiveComplexity.FinSat.vr0)

noncomputable def DescriptiveComplexity.FinSat.envNeS : certLang.Sentence

There is at least one environment.

Equations

• DescriptiveComplexity.FinSat.envNeS = DescriptiveComplexity.FinSat.exNewF (DescriptiveComplexity.FinSat.envF DescriptiveComplexity.FinSat.vr0)

noncomputable def DescriptiveComplexity.FinSat.valTotalS : certLang.Sentence

An environment gives every variable a value in the model.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.valFunS : certLang.Sentence

An environment gives every variable at most one value.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.valUpdateS : certLang.Sentence

Environments are closed under updating one variable.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.gExtS : certLang.Sentence

The truth value of a node depends on the environment only through the values it gives.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.stepS : certLang.Sentence

The truth values obey the truth definition.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.atomCohS : certLang.Sentence

Two atoms of the same relation symbol whose arguments have the same values have the same truth value.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.rootHoldsS : certLang.Sentence

The root holds under every environment.

Equations

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

noncomputable def DescriptiveComplexity.FinSat.certS : certLang.Sentence

The assignment is a certificate: the nine conditions of DescriptiveComplexity.FinSat.CertOK, conjoined.

Equations

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

theorem DescriptiveComplexity.FinSat.realize_eltNeS {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} : (A ⊕ Fin m) ⊨ eltNeS ↔ ∃ (d : Fin m), certElt ρ d

theorem DescriptiveComplexity.FinSat.realize_envNeS {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} : (A ⊕ Fin m) ⊨ envNeS ↔ ∃ (e : Fin m), certEnv ρ e

theorem DescriptiveComplexity.FinSat.realize_valTotalS {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} : (A ⊕ Fin m) ⊨ valTotalS ↔ ∀ (e : Fin m), certEnv ρ e → ∀ (x : A), ∃ (d : Fin m), certElt ρ d ∧ certVal ρ e x d

theorem DescriptiveComplexity.FinSat.realize_valFunS {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} : (A ⊕ Fin m) ⊨ valFunS ↔ ∀ (e : Fin m), certEnv ρ e → ∀ (x : A) (d d' : Fin m), certVal ρ e x d → certVal ρ e x d' → d = d'

theorem DescriptiveComplexity.FinSat.realize_valUpdateS {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} : (A ⊕ Fin m) ⊨ valUpdateS ↔ ∀ (e : Fin m), certEnv ρ e → ∀ (x : A) (d : Fin m), certElt ρ d → ∃ (e' : Fin m), certEnv ρ e' ∧ UpdAt (certVal ρ) e e' x d

theorem DescriptiveComplexity.FinSat.realize_gExtS {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} : (A ⊕ Fin m) ⊨ gExtS ↔ ∀ (g : A) (e e' : Fin m), certEnv ρ e → certEnv ρ e' → (∀ (x : A) (d : Fin m), certVal ρ e x d ↔ certVal ρ e' x d) → (certG ρ g e ↔ certG ρ g e')

theorem DescriptiveComplexity.FinSat.realize_stepS {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} : (A ⊕ Fin m) ⊨ stepS ↔ ∀ (g : A) (e : Fin m), certEnv ρ e → (certG ρ g e ↔ CertStep (certElt ρ) (certEnv ρ) (certVal ρ) (certG ρ) (certH ρ) g e)

theorem DescriptiveComplexity.FinSat.realize_atomCohS {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} : (A ⊕ Fin m) ⊨ atomCohS ↔ ∀ (g g' s : A) (e e' : Fin m), certEnv ρ e → certEnv ρ 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 : Fin m), certVal ρ e x d ↔ certVal ρ e' x' d) → (certH ρ g e ↔ certH ρ g' e')

theorem DescriptiveComplexity.FinSat.realize_rootHoldsS {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} : (A ⊕ Fin m) ⊨ rootHoldsS ↔ ∀ (g : A), RootG g → ∀ (e : Fin m), certEnv ρ e → certG ρ g e

theorem DescriptiveComplexity.FinSat.realize_certS {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} : (A ⊕ Fin m) ⊨ certS ↔ CertOK (certElt ρ) (certEnv ρ) (certVal ρ) (certG ρ) (certH ρ)

The kernel

noncomputable def DescriptiveComplexity.FinSat.kernelS : certLang.Sentence

The first-order kernel of the ∃SO[new] definition of FINSAT: the instance is a well-formed encoding, and the guessed relations are a certificate of finite satisfiability.

Equations

• DescriptiveComplexity.FinSat.kernelS = DescriptiveComplexity.FinSat.wfS ⊓ DescriptiveComplexity.FinSat.certS

theorem DescriptiveComplexity.FinSat.realize_kernelS {A : Type} [FirstOrder.Language.finsat.Structure A] [Nonempty A] {m : ℕ} {ρ : certBlock.Assignment (A ⊕ Fin m)} : (A ⊕ Fin m) ⊨ kernelS ↔ IsWF A ∧ CertOK (certElt ρ) (certEnv ρ) (certVal ρ) (certG ρ) (certH ρ)

The assignment a certificate determines

def DescriptiveComplexity.FinSat.certAssign {A : Type} {m : ℕ} (Elt Env : Fin m → Prop) (Val : Fin m → A → Fin m → Prop) (G H : A → Fin m → Prop) : certBlock.Assignment (A ⊕ Fin m)

The assignment of the relation variables a certificate determines: each variable holds exactly at the sort its component is meant for, and nowhere else – which is what makes the sort guards of the kernel harmless in this direction.

Equations

• One or more equations did not get rendered due to their size.
• DescriptiveComplexity.FinSat.certAssign Elt Env Val G H DescriptiveComplexity.FinSat.CertIx.elt = fun (x : Fin 1 → A ⊕ Fin m) => ∃ (d : Fin m), x 0 = Sum.inr d ∧ Elt d
• DescriptiveComplexity.FinSat.certAssign Elt Env Val G H DescriptiveComplexity.FinSat.CertIx.env = fun (x : Fin 1 → A ⊕ Fin m) => ∃ (e : Fin m), x 0 = Sum.inr e ∧ Env e
• DescriptiveComplexity.FinSat.certAssign Elt Env Val G H DescriptiveComplexity.FinSat.CertIx.gv = fun (x : Fin 2 → A ⊕ Fin m) => ∃ (g : A) (e : Fin m), x 0 = Sum.inl g ∧ x 1 = Sum.inr e ∧ G g e
• DescriptiveComplexity.FinSat.certAssign Elt Env Val G H DescriptiveComplexity.FinSat.CertIx.hv = fun (x : Fin 2 → A ⊕ Fin m) => ∃ (g : A) (e : Fin m), x 0 = Sum.inl g ∧ x 1 = Sum.inr e ∧ H g e

theorem DescriptiveComplexity.FinSat.certElt_certAssign {A : Type} {m : ℕ} (Elt Env : Fin m → Prop) (Val : Fin m → A → Fin m → Prop) (G H : A → Fin m → Prop) : certElt (certAssign Elt Env Val G H) = Elt

theorem DescriptiveComplexity.FinSat.certEnv_certAssign {A : Type} {m : ℕ} (Elt Env : Fin m → Prop) (Val : Fin m → A → Fin m → Prop) (G H : A → Fin m → Prop) : certEnv (certAssign Elt Env Val G H) = Env

theorem DescriptiveComplexity.FinSat.certVal_certAssign {A : Type} {m : ℕ} (Elt Env : Fin m → Prop) (Val : Fin m → A → Fin m → Prop) (G H : A → Fin m → Prop) : certVal (certAssign Elt Env Val G H) = Val

theorem DescriptiveComplexity.FinSat.certG_certAssign {A : Type} {m : ℕ} (Elt Env : Fin m → Prop) (Val : Fin m → A → Fin m → Prop) (G H : A → Fin m → Prop) : certG (certAssign Elt Env Val G H) = G

theorem DescriptiveComplexity.FinSat.certH_certAssign {A : Type} {m : ℕ} (Elt Env : Fin m → Prop) (Val : Fin m → A → Fin m → Prop) (G H : A → Fin m → Prop) : certH (certAssign Elt Env Val G H) = H

Membership

theorem DescriptiveComplexity.finsat_sigmaSONewDefinable : SigmaSONewDefinable FINSAT

FINSAT is definable in ∃SO[new], the logic defining RE: the invented values carry a finite model of the encoded sentence together with the environments – a certificate (DescriptiveComplexity.FinSat.finSatOn_iff_certFin) – and the first-order kernel DescriptiveComplexity.FinSat.kernelS checks that the encoding is well formed and that the guessed relations are one.

The number of invented values is unbounded in the instance, which is exactly what takes the problem beyond NP: a finite model of a satisfiable sentence can be arbitrarily larger than the sentence.

theorem DescriptiveComplexity.finsat_mem_RE : RE.Mem FINSAT

FINSAT is in RE.