Modal Logic

Modal logic is a logic for reasoning about (possibly polyadic) relational structures, studying qualified statements through the use of modalities (like necessity, possibility, knowledge, belief, permission, etc.).

This module formalises general modal logic, parameterised over a signature of modal operators. A signature is formalised as a polynomial functor (PFunctor), generalising the concept of modal similarity types from the literature [BRV01].

Implementation notes

• Compared to [BRV01], a triangle takes a map of arguments (from the argument type given by the polynomial functor to propositions), instead of a sequence of arguments.
• The use of τ to range over signatures of modal operators comes from the literature [BRV01].

References

• P. Blackburn, M. de Rijke, Y. Venema, Modal Logic
• The definitions of theory equivalence and the denotational semantics of worlds are inspired by the development of Cslib.Logic.HML.

inductive Cslib.Logic.Modal.Proposition (τ : PFunctor.{u_1, u_2}) (Atom : Type u) : Type (max (max u u_1) u_2)

A modal proposition.

• atom {τ : PFunctor.{u_1, u_2}} {Atom : Type u} (p : Atom) : Proposition τ Atom

  Atomic proposition.

• false {τ : PFunctor.{u_1, u_2}} {Atom : Type u} : Proposition τ Atom

  Falsehood.

• not {τ : PFunctor.{u_1, u_2}} {Atom : Type u} (φ : Proposition τ Atom) : Proposition τ Atom

  Negation.

• or {τ : PFunctor.{u_1, u_2}} {Atom : Type u} (φ₁ φ₂ : Proposition τ Atom) : Proposition τ Atom

  Disjunction.

• triangle {τ : PFunctor.{u_1, u_2}} {Atom : Type u} (op : τ.A) (φs : τ.B op → Proposition τ Atom) : Proposition τ Atom

  Generalised possibility, or triangle.

@[reducible, inline]

abbrev Cslib.Logic.Modal.PropositionMap (τ : PFunctor.{u_1, u_2}) (op : τ.A) (Atom : Type u_3) : Type (max (max u_2 u_1) u_3)

A map of propositions for the operator op in the polynomial functor τ.

Equations

• Cslib.Logic.Modal.PropositionMap τ op Atom = (τ.B op → Cslib.Logic.Modal.Proposition τ Atom)

@[instance_reducible]

instance Cslib.Logic.Modal.instCoeProposition {Atom : Type u_1} {τ : PFunctor.{u_2, u_3}} : Coe Atom (Proposition τ Atom)

Utility to coerce atoms into atomic propositions.

Equations

• Cslib.Logic.Modal.instCoeProposition = { coe := Cslib.Logic.Modal.Proposition.atom }

@[instance_reducible]

instance Cslib.Logic.Modal.instBotProposition {τ : PFunctor.{u_2, u_3}} {Atom : Type u_1} : Bot (Proposition τ Atom)

Equations

• Cslib.Logic.Modal.instBotProposition = { bot := Cslib.Logic.Modal.Proposition.false }

@[instance_reducible]

instance Cslib.Logic.Modal.instHasNotProposition {τ : PFunctor.{u_2, u_3}} {Atom : Type u_1} : HasNot (Proposition τ Atom)

Equations

• Cslib.Logic.Modal.instHasNotProposition = { not := Cslib.Logic.Modal.Proposition.not }

@[instance_reducible]

instance Cslib.Logic.Modal.instHasOrProposition {τ : PFunctor.{u_2, u_3}} {Atom : Type u_1} : HasOr (Proposition τ Atom)

Equations

• Cslib.Logic.Modal.instHasOrProposition = { or := Cslib.Logic.Modal.Proposition.or }

@[instance_reducible]

instance Cslib.Logic.Modal.instHasTriangleProposition {τ : PFunctor.{u_2, u_3}} {Atom : Type u_1} : HasTriangle (Proposition τ Atom) τ

Equations

• Cslib.Logic.Modal.instHasTriangleProposition = { triangle := Cslib.Logic.Modal.Proposition.triangle }

theorem Cslib.Logic.Modal.Proposition.false_def {τ : PFunctor.{u_1, u_2}} {Atom : Type u_3} : false = ⊥

theorem Cslib.Logic.Modal.Proposition.not_def {τ : PFunctor.{u_1, u_2}} {Atom : Type u_3} (φ : Proposition τ Atom) : φ.not = HasNot.not φ

theorem Cslib.Logic.Modal.Proposition.or_def {τ : PFunctor.{u_1, u_2}} {Atom : Type u_3} (φ₁ φ₂ : Proposition τ Atom) : φ₁.or φ₂ = HasOr.or φ₁ φ₂

theorem Cslib.Logic.Modal.Proposition.triangle_def {Atom : Type u_1} {τ : PFunctor.{u_2, u_3}} (op : τ.A) (φs : τ.B op → Proposition τ Atom) : triangle op φs = HasTriangle.triangle op φs

@[match_pattern]

def Cslib.Logic.Modal.Proposition.true {τ : PFunctor.{u_1, u_2}} {Atom : Type u_3} : Proposition τ Atom

Truth.

Equations

• Cslib.Logic.Modal.Proposition.true = Cslib.Logic.HasNot.not ⊥

@[instance_reducible]

instance Cslib.Logic.Modal.instTopProposition {τ : PFunctor.{u_2, u_3}} {Atom : Type u_1} : Top (Proposition τ Atom)

Equations

• Cslib.Logic.Modal.instTopProposition = { top := Cslib.Logic.Modal.Proposition.true }

theorem Cslib.Logic.Modal.Proposition.true_def {τ : PFunctor.{u_1, u_2}} {Atom : Type u_3} : true = ⊤

@[match_pattern]

def Cslib.Logic.Modal.Proposition.and {τ : PFunctor.{u_1, u_2}} {Atom : Type u_3} (φ₁ φ₂ : Proposition τ Atom) : Proposition τ Atom

Conjunction.

Equations

• φ₁.and φ₂ = Cslib.Logic.HasNot.not (Cslib.Logic.HasOr.or (Cslib.Logic.HasNot.not φ₁) (Cslib.Logic.HasNot.not φ₂))

@[instance_reducible]

instance Cslib.Logic.Modal.instHasAndProposition {τ : PFunctor.{u_2, u_3}} {Atom : Type u_1} : HasAnd (Proposition τ Atom)

Equations

• Cslib.Logic.Modal.instHasAndProposition = { and := Cslib.Logic.Modal.Proposition.and }

theorem Cslib.Logic.Modal.Proposition.and_def {τ : PFunctor.{u_1, u_2}} {Atom : Type u_3} (φ₁ φ₂ : Proposition τ Atom) : φ₁.and φ₂ = HasAnd.and φ₁ φ₂

@[match_pattern]

def Cslib.Logic.Modal.Proposition.imp {τ : PFunctor.{u_1, u_2}} {Atom : Type u_3} (φ₁ φ₂ : Proposition τ Atom) : Proposition τ Atom

Implication.

Equations

• φ₁.imp φ₂ = Cslib.Logic.HasOr.or (Cslib.Logic.HasNot.not φ₁) φ₂

@[instance_reducible]

instance Cslib.Logic.Modal.instHasImpProposition {τ : PFunctor.{u_2, u_3}} {Atom : Type u_1} : HasImp (Proposition τ Atom)

Equations

• Cslib.Logic.Modal.instHasImpProposition = { imp := Cslib.Logic.Modal.Proposition.imp }

theorem Cslib.Logic.Modal.Proposition.imp_def {τ : PFunctor.{u_1, u_2}} {Atom : Type u_3} (φ₁ φ₂ : Proposition τ Atom) : φ₁.imp φ₂ = HasImp.imp φ₁ φ₂

@[match_pattern]

def Cslib.Logic.Modal.Proposition.iff {τ : PFunctor.{u_1, u_2}} {Atom : Type u_3} (φ₁ φ₂ : Proposition τ Atom) : Proposition τ Atom

Bi-implication.

Equations

• φ₁.iff φ₂ = Cslib.Logic.HasAnd.and (Cslib.Logic.HasImp.imp φ₁ φ₂) (Cslib.Logic.HasImp.imp φ₂ φ₁)

@[instance_reducible]

instance Cslib.Logic.Modal.instHasIffProposition {τ : PFunctor.{u_2, u_3}} {Atom : Type u_1} : HasIff (Proposition τ Atom)

Equations

• Cslib.Logic.Modal.instHasIffProposition = { iff := Cslib.Logic.Modal.Proposition.iff }

theorem Cslib.Logic.Modal.Proposition.iff_def {τ : PFunctor.{u_1, u_2}} {Atom : Type u_3} (φ₁ φ₂ : Proposition τ Atom) : φ₁.iff φ₂ = HasIff.iff φ₁ φ₂

def Cslib.Logic.Modal.PropositionMap.not {τ : PFunctor.{u_1, u_2}} {op : τ.A} {Atom : Type u_3} (φs : PropositionMap τ op Atom) (i : τ.B op) : Proposition τ Atom

Point-wise negation of a proposition map.

Equations

• φs.not i = Cslib.Logic.HasNot.not (φs i)

@[instance_reducible]

instance Cslib.Logic.Modal.instHasNotPropositionMap {τ : PFunctor.{u_2, u_3}} {op : τ.A} {Atom : Type u_1} : HasNot (PropositionMap τ op Atom)

Equations

• Cslib.Logic.Modal.instHasNotPropositionMap = { not := Cslib.Logic.Modal.PropositionMap.not }

@[simp]

theorem Cslib.Logic.Modal.PropositionMap.not_apply {τ : PFunctor.{u_1, u_2}} {op : τ.A} {Atom : Type u_3} {φs : PropositionMap τ op Atom} (i : τ.B op) : HasNot.not φs i = HasNot.not (φs i)

def Cslib.Logic.Modal.PropositionMap.and {τ : PFunctor.{u_1, u_2}} {op : τ.A} {Atom : Type u_3} (φs₁ φs₂ : PropositionMap τ op Atom) (i : τ.B op) : Proposition τ Atom

Point-wise conjunction of proposition maps.

Equations

• φs₁.and φs₂ i = Cslib.Logic.HasAnd.and (φs₁ i) (φs₂ i)

@[instance_reducible]

instance Cslib.Logic.Modal.instHasAndPropositionMap {τ : PFunctor.{u_2, u_3}} {op : τ.A} {Atom : Type u_1} : HasAnd (PropositionMap τ op Atom)

Equations

• Cslib.Logic.Modal.instHasAndPropositionMap = { and := Cslib.Logic.Modal.PropositionMap.and }

theorem Cslib.Logic.Modal.PropositionMap.and_apply {τ : PFunctor.{u_1, u_2}} {op : τ.A} {Atom : Type u_3} (φs₁ φs₂ : PropositionMap τ op Atom) (i : τ.B op) : HasAnd.and φs₁ φs₂ i = HasAnd.and (φs₁ i) (φs₂ i)

def Cslib.Logic.Modal.PropositionMap.or {τ : PFunctor.{u_1, u_2}} {op : τ.A} {Atom : Type u_3} (φs₁ φs₂ : PropositionMap τ op Atom) (i : τ.B op) : Proposition τ Atom

Point-wise disjunction of proposition maps.

Equations

• φs₁.or φs₂ i = Cslib.Logic.HasOr.or (φs₁ i) (φs₂ i)

@[instance_reducible]

instance Cslib.Logic.Modal.instHasOrPropositionMap {τ : PFunctor.{u_2, u_3}} {op : τ.A} {Atom : Type u_1} : HasOr (PropositionMap τ op Atom)

Equations

• Cslib.Logic.Modal.instHasOrPropositionMap = { or := Cslib.Logic.Modal.PropositionMap.or }

def Cslib.Logic.Modal.PropositionMap.imp {τ : PFunctor.{u_1, u_2}} {op : τ.A} {Atom : Type u_3} (φs₁ φs₂ : PropositionMap τ op Atom) (i : τ.B op) : Proposition τ Atom

Point-wise implication of proposition maps.

Equations

• φs₁.imp φs₂ i = Cslib.Logic.HasImp.imp (φs₁ i) (φs₂ i)

@[instance_reducible]

instance Cslib.Logic.Modal.instHasImpPropositionMap {τ : PFunctor.{u_2, u_3}} {op : τ.A} {Atom : Type u_1} : HasImp (PropositionMap τ op Atom)

Equations

• Cslib.Logic.Modal.instHasImpPropositionMap = { imp := Cslib.Logic.Modal.PropositionMap.imp }

def Cslib.Logic.Modal.PropositionMap.iff {τ : PFunctor.{u_1, u_2}} {op : τ.A} {Atom : Type u_3} (φs₁ φs₂ : PropositionMap τ op Atom) (i : τ.B op) : Proposition τ Atom

Point-wise bi-implication of proposition maps.

Equations

• φs₁.iff φs₂ i = Cslib.Logic.HasIff.iff (φs₁ i) (φs₂ i)

@[instance_reducible]

instance Cslib.Logic.Modal.instHasIffPropositionMap {τ : PFunctor.{u_2, u_3}} {op : τ.A} {Atom : Type u_1} : HasIff (PropositionMap τ op Atom)

Equations

• Cslib.Logic.Modal.instHasIffPropositionMap = { iff := Cslib.Logic.Modal.PropositionMap.iff }

@[simp]

theorem Cslib.Logic.Modal.PropositionMap.or_apply {τ : PFunctor.{u_1, u_2}} {op : τ.A} {Atom : Type u_3} (φs ψs : PropositionMap τ op Atom) (i : τ.B op) : HasOr.or φs ψs i = HasOr.or (φs i) (ψs i)

@[simp]

theorem Cslib.Logic.Modal.PropositionMap.imp_apply {τ : PFunctor.{u_1, u_2}} {op : τ.A} {Atom : Type u_3} (φs ψs : PropositionMap τ op Atom) (i : τ.B op) : HasImp.imp φs ψs i = HasImp.imp (φs i) (ψs i)

@[simp]

theorem Cslib.Logic.Modal.PropositionMap.iff_apply {τ : PFunctor.{u_1, u_2}} {op : τ.A} {Atom : Type u_3} (φs ψs : PropositionMap τ op Atom) (i : τ.B op) : HasIff.iff φs ψs i = HasIff.iff (φs i) (ψs i)

@[match_pattern]

def Cslib.Logic.Modal.Proposition.nabla {Atom : Type u_1} {τ : PFunctor.{u_2, u_3}} (op : τ.A) (φs : τ.B op → Proposition τ Atom) : Proposition τ Atom

Generalised necessity, or nabla (∇), dual of triangle.

Equations

• Cslib.Logic.Modal.Proposition.nabla op φs = Cslib.Logic.HasNot.not (Cslib.Logic.HasTriangle.triangle op (Cslib.Logic.HasNot.not φs))

@[instance_reducible]

instance Cslib.Logic.Modal.instHasNablaProposition {τ : PFunctor.{u_2, u_3}} {Atom : Type u_1} : HasNabla (Proposition τ Atom) τ

Equations

• Cslib.Logic.Modal.instHasNablaProposition = { nabla := Cslib.Logic.Modal.Proposition.nabla }

theorem Cslib.Logic.Modal.Proposition.nabla_def {Atom : Type u_1} {τ : PFunctor.{u_2, u_3}} (op : τ.A) (φs : τ.B op → Proposition τ Atom) : nabla op φs = HasNabla.nabla op φs

@[reducible, inline]

abbrev Cslib.Logic.Modal.PropositionMap.const {Atom : Type u_1} {τ : PFunctor.{u_2, u_3}} (op : τ.A) (φ : Proposition τ Atom) : PropositionMap τ op Atom

The constant proposition map for the operator op, used for applying a modality uniformly. This supplies the same proposition φ to every argument position of op.

Equations

• Cslib.Logic.Modal.PropositionMap.const op φ = PFunctor.const op φ

@[simp]

theorem Cslib.Logic.Modal.PropositionMap.const_not {Atom : Type u_1} {τ : PFunctor.{u_2, u_3}} (op : τ.A) (φ : Proposition τ Atom) : const op (HasNot.not φ) = HasNot.not (const op φ)

Negation commutes with constant proposition maps.

@[simp]

theorem Cslib.Logic.Modal.PropositionMap.const_and {Atom : Type u_1} {τ : PFunctor.{u_2, u_3}} (op : τ.A) (φ ψ : Proposition τ Atom) : const op (HasAnd.and φ ψ) = HasAnd.and (const op φ) (const op ψ)

Conjunction commutes with constant proposition maps.

@[simp]

theorem Cslib.Logic.Modal.PropositionMap.const_or {Atom : Type u_1} {τ : PFunctor.{u_2, u_3}} (op : τ.A) (φ ψ : Proposition τ Atom) : const op (HasOr.or φ ψ) = HasOr.or (const op φ) (const op ψ)

Disjunction commutes with constant proposition maps.

@[simp]

theorem Cslib.Logic.Modal.PropositionMap.const_imp {Atom : Type u_1} {τ : PFunctor.{u_2, u_3}} (op : τ.A) (φ ψ : Proposition τ Atom) : const op (HasImp.imp φ ψ) = HasImp.imp (const op φ) (const op ψ)

Implication commutes with constant proposition maps.

@[simp]

theorem Cslib.Logic.Modal.PropositionMap.const_iff {Atom : Type u_1} {τ : PFunctor.{u_2, u_3}} (op : τ.A) (φ ψ : Proposition τ Atom) : const op (HasIff.iff φ ψ) = HasIff.iff (const op φ) (const op ψ)

Bi-implication commutes with constant proposition maps.