Modal Frames

A frame is a structure of relations, each with its own arity.

Implementation notes

Frames for general modal logic were formulated with modal similarity types [Blackburn2001], which we generalise here to arbitrary polynomial functors.

References

• [P. Blackburn, M. de Rijke, Y. Venema, Modal Logic][Blackburn2001]

structure Cslib.Frame (World : Type u) (τ : PFunctor.{u_1, u_2}) : Type (max (max u u_1) u_2)

A frame is an indexed structure of general relations that can differ in argument positions.

Frames are typically used in combination with modal logics or akin concepts. This is why we use op (for operator) to range over relation indexes.

The definition generalises Definition 1.23 in [Blackburn2001] to general operator signatures given as PFunctors and possibly-empty world types.

• r (op : τ.A) : World → (τ.B op → World) → Prop

  Accessibility relations.

def Cslib.Frame.project {World : Type u_1} {τ : PFunctor.{u_2, u_3}} (f : Frame World τ) (op : τ.A) (i : τ.B op) : World → World → Prop

The binary relation obtained by observing position i of the worlds accessible via op.

Equations

• f.project op i w w' = ∃ (ws : τ.B op → World), f.r op w ws ∧ ws i = w'

@[instance_reducible]

def Cslib.Frame.diagonal {World : Type u_1} {τ : PFunctor.{u_2, u_3}} (f : Frame World τ) (op : τ.A) : World → World → Prop

The binary relation induced by restricting the accessibility relation of op to constant tuples of worlds.

Equations

• f.diagonal op w w' = f.r op w fun (x : τ.B op) => w'

theorem Cslib.Frame.r_const_of_diagonal {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {op : τ.A} {w w' : World} {f : Frame World τ} (h : f.diagonal op w w') : f.r op w fun (x : τ.B op) => w'

theorem Cslib.Frame.diagonal_of_r {τ : PFunctor.{u_1, u_2}} {World : Type u_3} {op : τ.A} {w : World} {ws : τ.B op → World} [τ.Unary] {f : Frame World τ} (h : f.r op w ws) : f.diagonal op w (ws default)

class Cslib.Frame.DiagonalSymm {World : Type u_1} {τ : PFunctor.{u_2, u_3}} (f : Frame World τ) (op : τ.A) : Prop

A frame is diagonally symmetric at op if, whenever w accesses ws, some component of ws accesses the constant sequence at w.

• symm (w : World) (ws : τ.B op → World) : f.r op w ws → ∃ (i : τ.B op), f.r op (ws i) fun (x : τ.B op) => w

class Cslib.Frame.Trans {World : Type u_1} {τ : PFunctor.{u_2, u_3}} (f : Frame World τ) (op : τ.A) : Prop

A frame is transitive at op if accessibility can be composed through any accessible component: whenever w accesses ws₁ and ws₁ i accesses ws₂, then w accesses ws₂.

• trans (w : World) (ws₁ : τ.B op → World) (i : τ.B op) (ws₂ : τ.B op → World) : f.r op w ws₁ → f.r op (ws₁ i) ws₂ → f.r op w ws₂

instance Cslib.Frame.instIsTransProjectOfTrans {World : Type u_1} {τ : PFunctor.{u_2, u_3}} {op : τ.A} (f : Frame World τ) [f.Trans op] (i : τ.B op) : IsTrans World (f.project op i)

Frame transitivity at op implies transitivity of all its projected binary relations.

class Cslib.Frame.RightEuclidean {World : Type u_1} {τ : PFunctor.{u_2, u_3}} (f : Frame World τ) (op : τ.A) : Prop

A frame is right Euclidean at op if, whenever a world w accesses two tuples ws₁ and ws₂, some component of ws₂ accesses ws₁.

• rightEuclidean (w : World) (ws₁ ws₂ : τ.B op → World) : f.r op w ws₁ → f.r op w ws₂ → ∃ (i : τ.B op), f.r op (ws₂ i) ws₁

def Cslib.Frame.PreservesMap {α : Type u_1} {τ : PFunctor.{u_2, u_3}} (f : Frame α τ) (op : τ.A) (P : α → Prop) (Ps : τ.B op → α → Prop) : Prop

A predicate map Ps is preserved from P by op if, whenever P holds at a world w, then for every tuple ws accessible from w via op, each component ws i satisfies the corresponding predicate Ps i.

Equations

• f.PreservesMap op P Ps = ∀ (w : α) (ws : τ.B op → α), f.r op w ws → P w → ∃ (i : τ.B op), Ps i (ws i)

def Cslib.Frame.ofRelations {World : Type u_1} {τ : PFunctor.{u_2, u_3}} [τ.Unary] (r : τ.A → World → World → Prop) : Frame World τ

Builds a unary frame from an indexed family of binary relations.

Equations

• Cslib.Frame.ofRelations r = { r := fun (i : τ.A) (w : World) (ws : τ.B i → World) => r i w (ws default) }

theorem Cslib.Frame.ofRelations_iff {World : Type u_1} {τ : PFunctor.{u_2, u_3}} [τ.Unary] (r : τ.A → World → World → Prop) (i : τ.A) (w : World) (ws : τ.B i → World) : (ofRelations r).r i w ws ↔ r i w (ws default)

@[simp]

theorem Cslib.Frame.ofRelations_diagonal_iff {World : Type u_1} {τ : PFunctor.{u_2, u_3}} [τ.Unary] (r : τ.A → World → World → Prop) (i : τ.A) (w w' : World) : (ofRelations r).diagonal i w w' ↔ r i w w'