Rigid designation

An intension over an index type W is a function W → τ, and it is rigid when it takes the same value at every index: a rigid designator in the sense of Kripke, a stable content in the sense of Kaplan. Rigidity is subsingletonness of the range (isRigid_iff_subsingleton_range), and rigidity on a set is subsingletonness of the image (isRigidOn_iff_subsingleton_image); the closure properties are those of Set.Subsingleton. Rigid intensions that agree at one index agree everywhere, which is the necessity of identity.

Main definitions

• IsRigid f, IsRigidOn f S: constancy of f : W → τ everywhere, or on S.

Main results

• isRigid_iff_subsingleton_range, isRigidOn_iff_subsingleton_image: the mathlib face.
• IsRigid.eq_of_apply_eq: rigid intensions that agree at one index are equal.
• IsRigid.map, IsRigid.of_comp_injective, IsRigid.precomp, IsRigidOn.precomp, IsRigidOn.mono: closure under composition and restriction.

References

• [S. Kripke, Naming and Necessity (1980)][kripke-1980]
• [D. Kaplan, Demonstratives (1989)][kaplan-1989]
• D. Gallin, Intensional and Higher-Order Modal Logic (1975)

def Reference.IsRigid {W : Type u_1} {τ : Type u_3} (f : W → τ) : Prop

An intension is rigid when it takes the same value at every index.

Equations

• Reference.IsRigid f = ∀ (w₁ w₂ : W), f w₁ = f w₂

def Reference.IsRigidOn {W : Type u_1} {τ : Type u_3} (f : W → τ) (S : Set W) : Prop

An intension is rigid on S when it takes the same value at every index in S.

Equations

• Reference.IsRigidOn f S = ∀ (w₁ : W), w₁ ∈ S → ∀ (w₂ : W), w₂ ∈ S → f w₁ = f w₂

theorem Reference.isRigid_iff_subsingleton_range {W : Type u_1} {τ : Type u_3} {f : W → τ} : IsRigid f ↔ (Set.range f).Subsingleton

theorem Reference.isRigidOn_iff_subsingleton_image {W : Type u_1} {τ : Type u_3} {f : W → τ} {S : Set W} : IsRigidOn f S ↔ (f '' S).Subsingleton

theorem Reference.isRigid_const {W : Type u_1} {τ : Type u_3} (x : τ) : IsRigid fun (x_1 : W) => x

theorem Reference.IsRigidOn.mono {W : Type u_1} {τ : Type u_3} {f : W → τ} {S T : Set W} (h : IsRigidOn f S) (hT : T ⊆ S) : IsRigidOn f T

theorem Reference.IsRigid.isRigidOn {W : Type u_1} {τ : Type u_3} {f : W → τ} (h : IsRigid f) (S : Set W) : IsRigidOn f S

theorem Reference.IsRigid.eq_const {W : Type u_1} {τ : Type u_3} {f : W → τ} (h : IsRigid f) (w : W) : f = fun (x : W) => f w

A rigid intension is the constant function of its value at any index.

theorem Reference.IsRigid.eq_of_apply_eq {W : Type u_1} {τ : Type u_3} {f g : W → τ} (hf : IsRigid f) (hg : IsRigid g) {w : W} (h : f w = g w) : f = g

Necessity of identity: rigid intensions that agree at one index are equal.

theorem Reference.const_ne_of_not_isRigid {W : Type u_1} {τ : Type u_3} {f : W → τ} (h : ¬IsRigid f) (w : W) : (fun (x : W) => f w) ≠ f

A non-rigid intension differs from the constant function of any of its values.

theorem Reference.IsRigid.map {W : Type u_1} {τ : Type u_3} {τ' : Type u_4} {f : W → τ} (h : IsRigid f) (g : τ → τ') : IsRigid (g ∘ f)

theorem Reference.IsRigid.of_comp_injective {W : Type u_1} {τ : Type u_3} {τ' : Type u_4} {f : W → τ} {g : τ → τ'} (hg : Function.Injective g) (h : IsRigid (g ∘ f)) : IsRigid f

theorem Reference.IsRigid.precomp {W : Type u_1} {W' : Type u_2} {τ : Type u_3} {f : W → τ} (h : IsRigid f) (g : W' → W) : IsRigid (f ∘ g)

theorem Reference.IsRigidOn.precomp {W : Type u_1} {W' : Type u_2} {τ : Type u_3} {f : W → τ} {S : Set W} (h : IsRigidOn f S) (g : W' → W) : IsRigidOn (f ∘ g) (g ⁻¹' S)