First-order logic syntax: terms, formulas, sentences, derived connectives.

Follows Immerman Definition 1.11. Terms are variables (de Bruijn indexed) or vocabulary constants. Formulas are indexed by the number of free variables.

inductive Complexity.DescriptiveComplexity.Term (V : Vocabulary) (n : Nat) : Type

Terms of first-order logic over vocabulary V with n free variables.

• var {V : Vocabulary} {n : Nat} : Fin n → Term V n
• const {V : Vocabulary} {n : Nat} : Fin V.numConsts → Term V n

inductive Complexity.DescriptiveComplexity.Formula (V : Vocabulary) : Nat → Type

Formulas of first-order logic over vocabulary V with n free variables.

• relApp {V : Vocabulary} {n : Nat} (i : Fin V.numRels) : (Fin (V.relArity i) → Term V n) → Formula V n
• eq {V : Vocabulary} {n : Nat} : Term V n → Term V n → Formula V n
• neg {V : Vocabulary} {n : Nat} : Formula V n → Formula V n
• conj {V : Vocabulary} {n : Nat} : Formula V n → Formula V n → Formula V n
• disj {V : Vocabulary} {n : Nat} : Formula V n → Formula V n → Formula V n
• exist {V : Vocabulary} {n : Nat} : Formula V (n + 1) → Formula V n
• all {V : Vocabulary} {n : Nat} : Formula V (n + 1) → Formula V n

@[reducible, inline]

abbrev Complexity.DescriptiveComplexity.Sentence (V : Vocabulary) : Type

A sentence is a formula with no free variables.

Equations

• Complexity.DescriptiveComplexity.Sentence V = Complexity.DescriptiveComplexity.Formula V 0

def Complexity.DescriptiveComplexity.Formula.impl {V : Vocabulary} {n : Nat} (φ ψ : Formula V n) : Formula V n

Material implication.

Equations

• φ.impl ψ = φ.neg.disj ψ

def Complexity.DescriptiveComplexity.Formula.biconditional {V : Vocabulary} {n : Nat} (φ ψ : Formula V n) : Formula V n

Biconditional (if and only if).

Equations

• φ.biconditional ψ = (φ.impl ψ).conj (ψ.impl φ)

def Complexity.DescriptiveComplexity.Formula.verum {V : Vocabulary} {n : Nat} : Formula V n

Verum (always true): ∀x₀. x₀ = x₀. Works at any n including 0.

Equations

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

def Complexity.DescriptiveComplexity.Formula.falsum {V : Vocabulary} {n : Nat} : Formula V n

Falsum (always false): ¬⊤.

Equations

• Complexity.DescriptiveComplexity.Formula.falsum = Complexity.DescriptiveComplexity.Formula.verum.neg

def Complexity.DescriptiveComplexity.Formula.quantifierRank {V : Vocabulary} {n : Nat} : Formula V n → Nat

Quantifier rank of a formula.

Equations

• (Complexity.DescriptiveComplexity.Formula.relApp i a).quantifierRank = 0
• (Complexity.DescriptiveComplexity.Formula.eq a a_1).quantifierRank = 0
• φ.neg.quantifierRank = φ.quantifierRank
• (φ.conj ψ).quantifierRank = max φ.quantifierRank ψ.quantifierRank
• (φ.disj ψ).quantifierRank = max φ.quantifierRank ψ.quantifierRank
• φ.exist.quantifierRank = φ.quantifierRank + 1
• φ.all.quantifierRank = φ.quantifierRank + 1

def Complexity.DescriptiveComplexity.Formula.size {V : Vocabulary} {n : Nat} : Formula V n → Nat

Size (number of nodes) of a formula.

Equations

• (Complexity.DescriptiveComplexity.Formula.relApp i a).size = 1
• (Complexity.DescriptiveComplexity.Formula.eq a a_1).size = 1
• φ.neg.size = φ.size + 1
• (φ.conj ψ).size = φ.size + ψ.size + 1
• (φ.disj ψ).size = φ.size + ψ.size + 1
• φ.exist.size = φ.size + 1
• φ.all.size = φ.size + 1