Extensional operators

An operator O on intensions W → α is extensional at w when its value at w depends on its argument only through the argument's extension at w, i.e. O · w factors through evaluation at w. The pointwise connectives are extensional; quantifiers over indices such as ModalLogic.nec are not. Extensionality is closed under the pointwise connectives and under composition, so scope-inertness lifts through a whole stack of extensional operators.

Main definitions

• IsExtensionalAt O w, IsExtensional O: local truth-functionality of an operator.

Main results

• IsExtensionalAt.and, IsExtensionalAt.or, IsExtensionalAt.not, IsExtensionalAt.comp: closure of extensional operators.

def ModalLogic.IsExtensionalAt {W : Type u_1} {α : Type u_2} {β : Type u_3} (O : (W → α) → W → β) (w : W) : Prop

O is extensional at w: its value at w depends on the argument intension only through the argument's extension at w, i.e. O · w factors through evaluation at w.

Equations

• ModalLogic.IsExtensionalAt O w = ∀ (p q : W → α), p w = q w → O p w = O q w

def ModalLogic.IsExtensional {W : Type u_1} {α : Type u_2} {β : Type u_3} (O : (W → α) → W → β) : Prop

O is extensional at every index.

Equations

• ModalLogic.IsExtensional O = ∀ (w : W), ModalLogic.IsExtensionalAt O w

theorem ModalLogic.isExtensionalAt_iff_factorsThrough {W : Type u_1} {α : Type u_2} {β : Type u_3} (O : (W → α) → W → β) (w : W) : IsExtensionalAt O w ↔ Function.FactorsThrough (fun (x : W → α) => O x w) fun (x : W → α) => x w

theorem ModalLogic.not_isExtensionalAt_iff_exists_witness {W : Type u_1} {α : Type u_2} {β : Type u_3} {O : (W → α) → W → β} {w : W} : ¬IsExtensionalAt O w ↔ ∃ (p : W → α), ∃ (q : W → α), p w = q w ∧ O p w ≠ O q w

theorem ModalLogic.IsExtensionalAt.eval {W : Type u_1} {α : Type u_2} {w : W} : IsExtensionalAt (fun (p : W → α) (w' : W) => p w') w

theorem ModalLogic.IsExtensionalAt.const {W : Type u_1} {α : Type u_2} {w : W} (P : W → Prop) : IsExtensionalAt (fun (x : W → α) (w' : W) => P w') w

theorem ModalLogic.IsExtensionalAt.neg {W : Type u_1} {w : W} : IsExtensionalAt (fun (p : W → Prop) (w' : W) => ¬p w') w

Pointwise negation is extensional: negation is not an intensional operator.

theorem ModalLogic.IsExtensionalAt.and {W : Type u_1} {α : Type u_2} {w : W} {O₁ O₂ : (W → α) → W → Prop} (h₁ : IsExtensionalAt O₁ w) (h₂ : IsExtensionalAt O₂ w) : IsExtensionalAt (fun (p : W → α) (w' : W) => O₁ p w' ∧ O₂ p w') w

theorem ModalLogic.IsExtensionalAt.or {W : Type u_1} {α : Type u_2} {w : W} {O₁ O₂ : (W → α) → W → Prop} (h₁ : IsExtensionalAt O₁ w) (h₂ : IsExtensionalAt O₂ w) : IsExtensionalAt (fun (p : W → α) (w' : W) => O₁ p w' ∨ O₂ p w') w

theorem ModalLogic.IsExtensionalAt.not {W : Type u_1} {α : Type u_2} {w : W} {O : (W → α) → W → Prop} (h : IsExtensionalAt O w) : IsExtensionalAt (fun (p : W → α) (w' : W) => ¬O p w') w

theorem ModalLogic.IsExtensionalAt.comp {W : Type u_1} {α : Type u_2} {β : Type u_3} {w : W} {O₁ : (W → α) → W → β} {O₂ : (W → β) → W → Prop} (h₂ : IsExtensionalAt O₂ w) (h₁ : IsExtensionalAt O₁ w) : IsExtensionalAt (fun (p : W → α) (w' : W) => O₂ (fun (s : W) => O₁ p s) w') w

Extensional operators compose: scope-inertness lifts through a stack of them.