First-order logic semantics: term evaluation, formula satisfaction, models.

Follows Immerman Definition 1.11 (semantics part).

def Complexity.DescriptiveComplexity.Term.eval {V : Vocabulary} {n : Nat} (A : FinStruct V) (σ : Env A.card n) : Term V n → Fin A.card

Evaluate a term in a structure under an environment.

Equations

• Complexity.DescriptiveComplexity.Term.eval A σ (Complexity.DescriptiveComplexity.Term.var i) = σ i
• Complexity.DescriptiveComplexity.Term.eval A σ (Complexity.DescriptiveComplexity.Term.const j) = A.const j

def Complexity.DescriptiveComplexity.Formula.Sat {V : Vocabulary} {n : Nat} (A : FinStruct V) (σ : Env A.card n) : Formula V n → Prop

Satisfaction of a formula in a structure under an environment.

Equations

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

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

A structure models a sentence if it is satisfied under the empty environment.

Equations

• Complexity.DescriptiveComplexity.Sentence.Models A φ = Complexity.DescriptiveComplexity.Formula.Sat A (Complexity.DescriptiveComplexity.emptyEnv A.card) φ

def Complexity.DescriptiveComplexity.«term_⊨_» : Lean.TrailingParserDescr

Notation: A ⊨ φ for Sentence.Models A φ.

Equations

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

theorem Complexity.DescriptiveComplexity.Formula.verum_sat {V : Vocabulary} {n : Nat} (A : FinStruct V) (σ : Env A.card n) : Sat A σ verum ↔ True

theorem Complexity.DescriptiveComplexity.Formula.falsum_sat {V : Vocabulary} {n : Nat} (A : FinStruct V) (σ : Env A.card n) : Sat A σ falsum ↔ False