Second-order logic: syntax

Second-order logic over a vocabulary V extends first-order logic with relation variables — quantifiable variables standing for relations on the universe — and second-order quantifiers. A formula is indexed by a de Bruijn context rctx : List ℕ giving the arities of the relation variables in scope (innermost first) and by the number n of first-order variables in scope, so soExist k pushes a fresh arity-k relation variable onto rctx.

This is step 1 of the Fagin decomposition (roadmap L6): the ∃SO fragment of this syntax is the one Fagin's theorem characterizes as NP.

Main definitions

• DescriptiveComplexity.SOFormula, SOSentence — second-order formulas and sentences.
• SOFormula.ofFormula — the embedding of first-order logic into second-order logic.
• SOFormula.size — the syntactic size.

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

Second-order formulas over vocabulary V, with a de Bruijn context rctx of relation-variable arities and n first-order variables. Extends first-order logic with relation-variable application (soRelApp) and second-order quantifiers (soExist/soAll), which push a fresh arity onto rctx.

• relApp {V : Vocabulary} {rctx : List Nat} {n : Nat} (i : Fin V.numRels) : (Fin (V.relArity i) → Term V n) → SOFormula V rctx n

  Apply a vocabulary relation symbol to terms.

• soRelApp {V : Vocabulary} {rctx : List Nat} {n : Nat} (r : Fin rctx.length) : (Fin (rctx.get r) → Term V n) → SOFormula V rctx n

  Apply a relation variable (de Bruijn index r, arity rctx.get r) to terms.

• eq {V : Vocabulary} {rctx : List Nat} {n : Nat} : Term V n → Term V n → SOFormula V rctx n

  Equality of terms.

• neg {V : Vocabulary} {rctx : List Nat} {n : Nat} : SOFormula V rctx n → SOFormula V rctx n

  Negation.

• conj {V : Vocabulary} {rctx : List Nat} {n : Nat} : SOFormula V rctx n → SOFormula V rctx n → SOFormula V rctx n

  Conjunction.

• disj {V : Vocabulary} {rctx : List Nat} {n : Nat} : SOFormula V rctx n → SOFormula V rctx n → SOFormula V rctx n

  Disjunction.

• exist {V : Vocabulary} {rctx : List Nat} {n : Nat} : SOFormula V rctx (n + 1) → SOFormula V rctx n

  First-order existential quantifier.

• all {V : Vocabulary} {rctx : List Nat} {n : Nat} : SOFormula V rctx (n + 1) → SOFormula V rctx n

  First-order universal quantifier.

• soExist {V : Vocabulary} {rctx : List Nat} {n : Nat} (k : Nat) : SOFormula V (k :: rctx) n → SOFormula V rctx n

  Second-order existential quantifier over a fresh arity-k relation.

• soAll {V : Vocabulary} {rctx : List Nat} {n : Nat} (k : Nat) : SOFormula V (k :: rctx) n → SOFormula V rctx n

  Second-order universal quantifier over a fresh arity-k relation.

@[reducible, inline]

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

A second-order sentence: no free relation or element variables.

Equations

• Complexity.DescriptiveComplexity.SOSentence V = Complexity.DescriptiveComplexity.SOFormula V [] 0

def Complexity.DescriptiveComplexity.SOFormula.ofFormula {V : Vocabulary} {n : Nat} : Formula V n → (rctx : List Nat) → SOFormula V rctx n

The first-order fragment embeds into second-order logic (over any relation context): every FO formula is an SO formula that never mentions relation variables.

Equations

• Complexity.DescriptiveComplexity.SOFormula.ofFormula (Complexity.DescriptiveComplexity.Formula.relApp i args) x✝ = Complexity.DescriptiveComplexity.SOFormula.relApp i args
• Complexity.DescriptiveComplexity.SOFormula.ofFormula (Complexity.DescriptiveComplexity.Formula.eq a b) x✝ = Complexity.DescriptiveComplexity.SOFormula.eq a b
• Complexity.DescriptiveComplexity.SOFormula.ofFormula φ.neg x✝ = (Complexity.DescriptiveComplexity.SOFormula.ofFormula φ x✝).neg
• Complexity.DescriptiveComplexity.SOFormula.ofFormula (φ.conj ψ) x✝ = (Complexity.DescriptiveComplexity.SOFormula.ofFormula φ x✝).conj (Complexity.DescriptiveComplexity.SOFormula.ofFormula ψ x✝)
• Complexity.DescriptiveComplexity.SOFormula.ofFormula (φ.disj ψ) x✝ = (Complexity.DescriptiveComplexity.SOFormula.ofFormula φ x✝).disj (Complexity.DescriptiveComplexity.SOFormula.ofFormula ψ x✝)
• Complexity.DescriptiveComplexity.SOFormula.ofFormula φ.exist x✝ = (Complexity.DescriptiveComplexity.SOFormula.ofFormula φ x✝).exist
• Complexity.DescriptiveComplexity.SOFormula.ofFormula φ.all x✝ = (Complexity.DescriptiveComplexity.SOFormula.ofFormula φ x✝).all

def Complexity.DescriptiveComplexity.SOFormula.size {V : Vocabulary} {rctx : List Nat} {n : Nat} : SOFormula V rctx n → Nat

Syntactic size (number of nodes) of a second-order formula.

Equations

• (Complexity.DescriptiveComplexity.SOFormula.relApp i a).size = 1
• (Complexity.DescriptiveComplexity.SOFormula.soRelApp r a).size = 1
• (Complexity.DescriptiveComplexity.SOFormula.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
• (Complexity.DescriptiveComplexity.SOFormula.soExist k φ).size = φ.size + 1
• (Complexity.DescriptiveComplexity.SOFormula.soAll k φ).size = φ.size + 1

def Complexity.DescriptiveComplexity.SOFormula.IsFOMatrix {V : Vocabulary} {rctx : List Nat} {n : Nat} : SOFormula V rctx n → Prop

A formula has no second-order quantifiers — an FO matrix over the relation variables in scope.

Equations

• (Complexity.DescriptiveComplexity.SOFormula.relApp i a).IsFOMatrix = True
• (Complexity.DescriptiveComplexity.SOFormula.soRelApp r a).IsFOMatrix = True
• (Complexity.DescriptiveComplexity.SOFormula.eq a a_1).IsFOMatrix = True
• φ.neg.IsFOMatrix = φ.IsFOMatrix
• (φ.conj ψ).IsFOMatrix = (φ.IsFOMatrix ∧ ψ.IsFOMatrix)
• (φ.disj ψ).IsFOMatrix = (φ.IsFOMatrix ∧ ψ.IsFOMatrix)
• φ.exist.IsFOMatrix = φ.IsFOMatrix
• φ.all.IsFOMatrix = φ.IsFOMatrix
• (Complexity.DescriptiveComplexity.SOFormula.soExist k a).IsFOMatrix = False
• (Complexity.DescriptiveComplexity.SOFormula.soAll k a).IsFOMatrix = False

def Complexity.DescriptiveComplexity.SOFormula.IsExistSO {V : Vocabulary} {rctx : List Nat} {n : Nat} : SOFormula V rctx n → Prop

A formula is in existential second-order (∃SO) form: a block of second-order existential quantifiers over an FO matrix. This is the exact fragment Fagin's theorem characterizes as NP.

Equations

• (Complexity.DescriptiveComplexity.SOFormula.soExist k ψ).IsExistSO = ψ.IsExistSO
• x✝.IsExistSO = x✝.IsFOMatrix

theorem Complexity.DescriptiveComplexity.SOFormula.ofFormula_isFOMatrix {V : Vocabulary} {n : Nat} (φ : Formula V n) (rctx : List Nat) : (ofFormula φ rctx).IsFOMatrix

The first-order embedding of any formula is an FO matrix.

theorem Complexity.DescriptiveComplexity.SOFormula.ofFormula_isExistSO {V : Vocabulary} {n : Nat} (φ : Formula V n) (rctx : List Nat) : (ofFormula φ rctx).IsExistSO

The first-order fragment sits inside ∃SO: an embedded FO formula is a (quantifier-free-in-second-order) ∃SO formula.