Sahlqvist formulas

DefinitionPositive modal formulas#✓fully proved

Positive and negative modal formulas are defined by simultaneous recursion: every atom is positive, \(\bot\) is positive, \(\varphi \to \psi\) is positive if \(\varphi\) is negative and \(\psi\) is positive, and \(\Box\varphi\) is positive if \(\varphi\) is positive.

Positive formulas are closed under \(\wedge\), \(\vee\), \(\Box\) and \(\Diamond\), which are encoded through \(\to\), \(\bot\) and \(\Box\).

def IsPositive : Formula Atom → Prop
  | .atom _ => True
  | .bot => True
  | .imp φ ψ => IsNegative φ ∧ IsPositive ψ
  | .box φ => IsPositive φ

Uses 1 · Used by 2

Statement usesModal formulas

Used byThe B axiom is a Sahlqvist formula · Sahlqvist implications

DefinitionNegative modal formulas#✓fully proved

Negative and positive modal formulas are defined by simultaneous recursion: no atom is negative, \(\bot\) is negative, \(\varphi \to \psi\) is negative if \(\varphi\) is positive and \(\psi\) is negative, and \(\Box\varphi\) is negative if \(\varphi\) is negative.

Negative formulas are closed under \(\wedge\), \(\vee\), \(\Box\) and \(\Diamond\), which are encoded through \(\to\), \(\bot\) and \(\Box\).

def IsNegative : Formula Atom → Prop
  | .atom _ => False
  | .bot => True
  | .imp φ ψ => IsPositive φ ∧ IsNegative ψ
  | .box φ => IsNegative φ

Uses 1 · Used by 2

Statement usesModal formulas

Used bySahlqvist antecedents · The B axiom is a Sahlqvist formula

DefinitionIterated box#✓fully proved

For a natural number \(k\) and a modal formula \(\varphi\), the iterated box \(\Box^k \varphi\) is defined by \(\Box^0 \varphi = \varphi\) and \(\Box^{k+1} \varphi = \Box\,\Box^k \varphi\).

def boxPow : Nat → Formula Atom → Formula Atom
  | 0, φ => φ
  | k + 1, φ => .box (boxPow k φ)

Uses 1 · Used by 2

Statement usesModal formulas

Used bySahlqvist antecedents · The B axiom is a Sahlqvist formula

InductiveSahlqvist antecedents#✓fully proved

The Sahlqvist antecedents form the smallest class of modal formulas that contains every boxed atom \(\Box^k p\) (an atom \(p\) under \(k \ge 0\) boxes) and every negative formula, and is closed under \(\wedge\), \(\vee\) and \(\Diamond\).

Cslib.Modal.IsSahlqvistAntecedent · 17 lines

inductive IsSahlqvistAntecedent : Formula Atom → Prop
  /-- A boxed atom is a Sahlqvist antecedent. -/
  | boxedAtom (a : Atom) (k : Nat) :
      IsSahlqvistAntecedent (boxPow k (.atom a))
  /-- A negative formula is a Sahlqvist antecedent. -/
  | ofNegative (φ : Formula Atom) : IsNegative φ → IsSahlqvistAntecedent φ
  /-- Sahlqvist antecedents are closed under conjunction. -/
  | and (φ ψ : Formula Atom) :
      IsSahlqvistAntecedent φ → IsSahlqvistAntecedent ψ →
        IsSahlqvistAntecedent (φ.and ψ)
  /-- Sahlqvist antecedents are closed under disjunction. -/
  | or (φ ψ : Formula Atom) :
      IsSahlqvistAntecedent φ → IsSahlqvistAntecedent ψ →
        IsSahlqvistAntecedent (φ.or ψ)
  /-- Sahlqvist antecedents are closed under possibility. -/
  | dia (φ : Formula Atom) :
      IsSahlqvistAntecedent φ → IsSahlqvistAntecedent φ.dia

Uses 6 · Used by 2

Statement usesModal formulas · Conjunction · The possibility operator · Disjunction of modal formulas · Negative modal formulas · Iterated box

Used byThe B axiom is a Sahlqvist formula · Sahlqvist implications

DefinitionAtoms of a modal formula#✓fully proved

The set of atoms (propositional variables) occurring in a modal formula.

def Formula.atoms : Formula Atom → Set Atom
  | .atom a => {a}
  | .bot => ∅
  | .imp φ ψ => φ.atoms ∪ ψ.atoms
  | .box φ => φ.atoms

Uses 1 · Used by 1

Statement usesModal formulas

Used bySahlqvist formulas

DefinitionSahlqvist implications#✓fully proved

A modal formula is a Sahlqvist implication if it is an implication \(\alpha \to \beta\) whose antecedent \(\alpha\) is a Sahlqvist antecedent and whose consequent \(\beta\) is a positive formula.

def IsSahlqvistImplication (φ : Formula Atom) : Prop :=
  ∃ α β : Formula Atom, IsSahlqvistAntecedent α ∧ IsPositive β ∧ φ = α.imp β

Uses 3 · Used by 2

Statement usesModal formulas · Positive modal formulas · Sahlqvist antecedents

Used bySahlqvist formulas · The B axiom is a Sahlqvist formula

InductiveSahlqvist formulas#✓fully proved

The Sahlqvist formulas form the smallest class of modal formulas that contains every Sahlqvist implication, is closed under \(\wedge\) and \(\Box\), and contains \(\varphi \vee \psi\) whenever \(\varphi\) and \(\psi\) are Sahlqvist formulas with no atom in common.

The side condition on disjunction is essential: arbitrary disjunction leaves the correspondence class. \(\Diamond\) is not part of this outer closure; it belongs to the grammar of Sahlqvist antecedents. For example, the boxed Sahlqvist implication \(\Box(p \to \Box\Diamond p)\) is a Sahlqvist formula.

inductive IsSahlqvist : Formula Atom → Prop
  /-- A Sahlqvist implication is Sahlqvist. -/
  | impl {φ : Formula Atom} : IsSahlqvistImplication φ → IsSahlqvist φ
  /-- Sahlqvist formulas are closed under conjunction. -/
  | and {φ ψ : Formula Atom} :
      IsSahlqvist φ → IsSahlqvist ψ → IsSahlqvist (φ.and ψ)
  /-- Sahlqvist formulas are closed under disjunction with disjoint atoms. -/
  | or {φ ψ : Formula Atom} :
      IsSahlqvist φ → IsSahlqvist ψ → Disjoint φ.atoms ψ.atoms →
        IsSahlqvist (φ.or ψ)
  /-- Sahlqvist formulas are closed under boxing. -/
  | box {φ : Formula Atom} : IsSahlqvist φ → IsSahlqvist (.box φ)

Uses 5 · Used by 1

Statement usesModal formulas · Conjunction · Atoms of a modal formula · Disjunction of modal formulas · Sahlqvist implications

Used byThe B axiom is a Sahlqvist formula

TheoremThe B axiom is a Sahlqvist formula#✓fully proved

For every atom \(p\), the instance \(p \to \Box\Diamond p\) of the B axiom is a Sahlqvist formula: its antecedent \(p\) is a boxed atom with zero boxes and its consequent \(\Box\Diamond p\) is positive.

theorem isSahlqvist_axiomB (a : Atom) : IsSahlqvist (Formula.axiomB (.atom a))

Uses 10

Statement usesModal formulas · Axiom B · Sahlqvist formulas

Proof usesThe possibility operator · Negation of modal formulas · Negative modal formulas · Positive modal formulas · Sahlqvist antecedents · Sahlqvist implications · Iterated box

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.