Second-order logic: semantics

Satisfaction of a second-order formula needs, besides the first-order element environment Env, a relation environment REnv interpreting each relation variable in the de Bruijn context rctx as a relation of its arity on the universe. Second-order quantifiers range over all such relations, extending the relation environment with rCons.

This is step 2 of the Fagin decomposition (roadmap L6). The FO fragment embeds faithfully: SOFormula.ofFormula_sat shows the embedding preserves satisfaction, so first-order truth is a special case of second-order truth (SOSentence.models_ofFormula).

Main definitions and results

• DescriptiveComplexity.REnv, rCons, emptyREnv — relation environments.
• DescriptiveComplexity.SOFormula.Sat, SOSentence.Models — SO satisfaction.
• SOFormula.ofFormula_sat, SOSentence.models_ofFormula — the FO embedding is truth-preserving.

def Complexity.DescriptiveComplexity.REnv (card : Nat) (rctx : List Nat) : Type

A relation-variable assignment: interprets each relation variable in rctx as a relation of its arity on the universe Fin card.

Equations

• Complexity.DescriptiveComplexity.REnv card rctx = ((r : Fin rctx.length) → (Fin (rctx.get r) → Fin card) → Prop)

def Complexity.DescriptiveComplexity.rCons {card k : Nat} {rctx : List Nat} (S : (Fin k → Fin card) → Prop) (ρ : REnv card rctx) : REnv card (k :: rctx)

Extend a relation environment with a fresh arity-k relation at index 0.

Equations

• Complexity.DescriptiveComplexity.rCons S ρ ⟨0, isLt⟩ = S
• Complexity.DescriptiveComplexity.rCons S ρ ⟨i.succ, h⟩ = ρ ⟨i, ⋯⟩

def Complexity.DescriptiveComplexity.emptyREnv (card : Nat) : REnv card []

The empty relation environment (no relation variables).

Equations

• Complexity.DescriptiveComplexity.emptyREnv card r = absurd ⋯ ⋯

def Complexity.DescriptiveComplexity.SOFormula.Sat {V : Vocabulary} (A : FinStruct V) {rctx : List Nat} {n : Nat} : Env A.card n → REnv A.card rctx → SOFormula V rctx n → Prop

Satisfaction of a second-order formula in a structure under element and relation environments. Second-order quantifiers range over all relations of the quantified arity.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DescriptiveComplexity.SOFormula.Sat A x✝¹ x✝ φ.neg = ¬Complexity.DescriptiveComplexity.SOFormula.Sat A x✝¹ x✝ φ
• Complexity.DescriptiveComplexity.SOFormula.Sat A x✝¹ x✝ (φ.conj ψ) = (Complexity.DescriptiveComplexity.SOFormula.Sat A x✝¹ x✝ φ ∧ Complexity.DescriptiveComplexity.SOFormula.Sat A x✝¹ x✝ ψ)
• Complexity.DescriptiveComplexity.SOFormula.Sat A x✝¹ x✝ (φ.disj ψ) = (Complexity.DescriptiveComplexity.SOFormula.Sat A x✝¹ x✝ φ ∨ Complexity.DescriptiveComplexity.SOFormula.Sat A x✝¹ x✝ ψ)
• Complexity.DescriptiveComplexity.SOFormula.Sat A x✝¹ x✝ φ.exist = ∃ (a : Fin A.card), Complexity.DescriptiveComplexity.SOFormula.Sat A (Complexity.DescriptiveComplexity.envCons a x✝¹) x✝ φ
• Complexity.DescriptiveComplexity.SOFormula.Sat A x✝¹ x✝ φ.all = ∀ (a : Fin A.card), Complexity.DescriptiveComplexity.SOFormula.Sat A (Complexity.DescriptiveComplexity.envCons a x✝¹) x✝ φ

def Complexity.DescriptiveComplexity.SOSentence.Models {V : Vocabulary} (A : FinStruct V) (φ : SOSentence V) : Prop

A structure models a second-order sentence under the empty environments.

Equations

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

theorem Complexity.DescriptiveComplexity.SOFormula.ofFormula_sat {V : Vocabulary} (A : FinStruct V) {rctx : List Nat} (ρ : REnv A.card rctx) {n : Nat} (φ : Formula V n) (σ : Env A.card n) : Sat A σ ρ (ofFormula φ rctx) ↔ Formula.Sat A σ φ

The first-order embedding preserves satisfaction. An FO formula embedded into second-order logic is satisfied under (σ, ρ) exactly when the original is satisfied under σ — the relation environment ρ is irrelevant, since the embedded formula never mentions relation variables.

theorem Complexity.DescriptiveComplexity.SOSentence.models_ofFormula {V : Vocabulary} (A : FinStruct V) (φ : Sentence V) : Models A (SOFormula.ofFormula φ []) ↔ Sentence.Models A φ

First-order truth is a special case of second-order truth. A structure models an FO sentence iff it models its second-order embedding.