Satisfaction is the unique fixed point of the truth definition

The one lemma both halves of Trakhtenbrot's theorem rest on: on a well-formed instance (DescriptiveComplexity.FinSat.IsWF – the parse DAG descends along the order of the syntax) the least fixed point DescriptiveComplexity.FinSat.Gval of the truth definition is its only fixed point (DescriptiveComplexity.FinSat.IsEval.iff_Gval).

• the membership proof (DescriptiveComplexity.FinSat.Membership) guesses a relation and constrains it by the truth definition read as an equivalence; uniqueness is what forces the guess to be satisfaction, and is therefore what makes the ∃SO[new] sentence say what it should;
• the hardness proof (DescriptiveComplexity.FinSat.Hardness) has to evaluate the sentence it builds; it exhibits its intended valuation and concludes by the same uniqueness, never touching the fuel counter.

The proofs all go through one lemma, DescriptiveComplexity.FinSat.gstep_mono_child: the value of a node depends only on the values of nodes strictly below it in the order of the syntax. That is the only use well-formedness has here, and it is what replaces well-founded recursion on a decoded parse tree.

The rank of a node

noncomputable def DescriptiveComplexity.FinSat.orank {A : Type} [FirstOrder.Language.finsat.Structure A] (g : A) : ℕ

The rank of a node: how many nodes precede it in the order of the syntax. It bounds the depth of the parse DAG below the node, and so the fuel its evaluation needs.

Equations

• DescriptiveComplexity.FinSat.orank g = {x : A | DescriptiveComplexity.FinSat.OrdLt x g}.ncard

theorem DescriptiveComplexity.FinSat.orank_lt {A : Type} [FirstOrder.Language.finsat.Structure A] [Finite A] (hwf : IsWF A) {c g : A} (h : OrdLt c g) : orank c < orank g

theorem DescriptiveComplexity.FinSat.orank_child_lt {A : Type} [FirstOrder.Language.finsat.Structure A] [Finite A] (hwf : IsWF A) {g c : A} (h : ChildG g c) : orank c < orank g

Only the nodes below matter

theorem DescriptiveComplexity.FinSat.gstep_mono_child {A M : Type} [FirstOrder.Language.finsat.Structure A] (I : A → (A → M) → Prop) {rec rec' : (A → M) → A → Prop} (v : A → M) (g : A) (h : ∀ (v' : A → M) (c : A), ChildG g c → rec v' c → rec' v' c) : gstep I rec v g → gstep I rec' v g

The value of a node depends only on the values of the nodes strictly below it: every recursive occurrence in the truth definition is at a child, and on a well-formed instance a child comes strictly earlier in the order of the syntax. This is the whole use of well-formedness in the semantics.

theorem DescriptiveComplexity.FinSat.gval_orank {A M : Type} [FirstOrder.Language.finsat.Structure A] [Finite A] (hwf : IsWF A) (I : A → (A → M) → Prop) (k : ℕ) (v : A → M) (g : A) : gval I k v g → gval I (orank g + 1) v g

Rank many unfoldings suffice: whatever the fuel, a node that holds holds already with the fuel its rank gives it.

theorem DescriptiveComplexity.FinSat.Gval_iff_orank {A M : Type} [FirstOrder.Language.finsat.Structure A] [Finite A] (hwf : IsWF A) (I : A → (A → M) → Prop) (v : A → M) (g : A) : Gval I v g ↔ gval I (orank g + 1) v g

Fixed points of the truth definition

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

A valuation of the nodes satisfying the truth definition: the value of every node is what its clause says of the values of its children.

Equations

• DescriptiveComplexity.FinSat.IsEval I V = ∀ (v : A → M) (g : A), V v g ↔ DescriptiveComplexity.FinSat.gstep I V v g

theorem DescriptiveComplexity.FinSat.Gval_isEval {A M : Type} [FirstOrder.Language.finsat.Structure A] [Finite A] (hwf : IsWF A) (I : A → (A → M) → Prop) : IsEval I (Gval I)

Satisfaction is a fixed point of the truth definition.

theorem DescriptiveComplexity.FinSat.gval_of_isEval {A M : Type} [FirstOrder.Language.finsat.Structure A] {I : A → (A → M) → Prop} {V : (A → M) → A → Prop} (hV : IsEval I V) (k : ℕ) (v : A → M) (g : A) : gval I k v g → V v g

Every approximant of satisfaction is below any fixed point of the truth definition.

theorem DescriptiveComplexity.FinSat.IsEval.iff_Gval {A M : Type} [FirstOrder.Language.finsat.Structure A] [Finite A] (hwf : IsWF A) {I : A → (A → M) → Prop} {V : (A → M) → A → Prop} (hV : IsEval I V) (v : A → M) (g : A) : V v g ↔ Gval I v g

The fixed point is unique: any valuation satisfying the truth definition is satisfaction. On a well-formed instance the truth definition determines the value of a node from the values of the nodes below it, and there are no infinite descents.