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

@[simp]

theorem DescriptiveComplexity.FinSat.relMap_inl₁ {A : Type} [FirstOrder.Language.finsat.Structure 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] {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] {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.

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

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.

The certificate

One conjunct per field of DescriptiveComplexity.FinSat.CertOK.

The kernel

The assignment a certificate determines

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.