Rigid designation

import Linglib.Semantics.Reference.Rigidity

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. The designator whose reference f fixes at w is the constant intension fun _ ↦ f w, and f is rigid iff it is the designator whose reference it fixes at every index. Rigidity is subsingletonness of the range, and rigid intensions that agree at one index agree everywhere, which is the necessity of identity.

An operator O governing the predication of P of a designator f has a large scope reading, which evaluates f at the index of the whole sentence, and a small scope reading, which evaluates it at each index the operator reaches. The large scope reading of f is the small scope reading of the designator whose reference f fixes at that index. The two readings coincide when f is constant on the indices on which the operator's value depends: under every operator when f is rigid, and for every designator when the operator is extensional.

Main definitions

IsRigid f: constancy of f : W → τ.
largeScope O P f, smallScope O P f: the two scope readings of O over P of f.

Main results

isRigid_iff_forall_eq_const: a rigid designator is the one whose reference it fixes.
isRigid_iff_subsingleton_range: the mathlib face.
IsRigid.eq_of_apply_eq: the necessity of identity.
largeScope_eq_smallScope_const: the large scope reading as fixing the reference.
largeScope_eq_smallScope_of_dependsOn: the scope readings coincide for a designator constant on the indices the operator reads.
largeScope_eq_smallScope: the scope readings coincide for a rigid designator.
Montague.IsExtensionalAt.largeScope_eq_smallScope: the scope readings coincide under an extensional operator.

References

Declarations

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

def IsRigid L56–57

{W : Type u_1} {τ : Type u_2} (f : W → τ) :

Prop

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

Used by isRigid_iff_forall_eq_const, IsRigid.eq_const, isRigid_iff_subsingleton_range, isRigid_const, isRigid_of_subsingleton, IsRigid.eq_of_apply_eq, IsRigid.ne, IsRigid.map, Function.Injective.isRigid_comp_iff, largeScope_eq_smallScope

Used in Semantics/Reference/Character, Semantics/Reference/Nominal, Semantics/Reference/Pronoun, Aloni2001, Kripke1980 and 5 more

theorem isRigid_iff_forall_eq_const L59–60

{W : Type u_1} {τ : Type u_2} {f : W → τ} :

IsRigid f ↔ ∀ (w : W), f = fun (x : W) => f w

Built from

L62–63

theorem isRigid_iff_subsingleton_range L65–66

{W : Type u_1} {τ : Type u_2} {f : W → τ} :

IsRigid f ↔ (Set.range f).Subsingleton

Built from

L68

L70–72

Rigid intensions that agree at one index are equal, which is the necessity of identity.

theorem IsRigid.eq_of_apply_eq L74–77

{W : Type u_1} {τ : Type u_2} {f g : W → τ} (hf : IsRigid f) (hg : IsRigid g) {w : W} (h : f w = g w) :

f = g

Built from

L79–80

L82–83

L85–87

Scope

The large scope reading of the operator O over the predication of P of f, which evaluates f at the index of the whole sentence.

def largeScope L91–94

{W : Type u_1} {τ : Type u_2} (O : (W → Prop) → W → Prop) (P : τ → W → Prop) (f : W → τ) (w : W) :

Prop

largeScope O P f w = O (P (f w)) w

Used by largeScope_eq_smallScope_const, largeScope_eq_smallScope_of_dependsOn, largeScope_eq_smallScope, Montague.IsExtensionalAt.largeScope_eq_smallScope

Used in Almog2014, Kripke1980, Zimmermann2026

The small scope reading, which evaluates f at each index the operator reaches.

def smallScope L96–98

{W : Type u_1} {τ : Type u_2} (O : (W → Prop) → W → Prop) (P : τ → W → Prop) (f : W → τ) :

W → Prop

smallScope O P f = O fun (v : W) => P (f v) v

Used by largeScope_eq_smallScope_const, largeScope_eq_smallScope_of_dependsOn, largeScope_eq_smallScope, Montague.IsExtensionalAt.largeScope_eq_smallScope

Used in Almog2014, Kripke1980, Zimmermann2026

The large scope reading of f is the small scope reading of the designator whose reference f fixes at the index of the whole sentence.

theorem largeScope_eq_smallScope_const L100–104

{W : Type u_1} {τ : Type u_2} (O : (W → Prop) → W → Prop) (P : τ → W → Prop) (f : W → τ) (w : W) :

largeScope O P f w = smallScope O P (fun (x : W) => f w) w

Built from ,

The two scope readings of f coincide at w when f is constant on a set of indices on which the operator's value at w depends.

theorem largeScope_eq_smallScope_of_dependsOn L106–111

{W : Type u_1} {τ : Type u_2} {f : W → τ} {O : (W → Prop) → W → Prop} {s : Set W} {w : W} (hO : DependsOn (fun (x : W → Prop) => O x w) s) (hf : Set.EqOn f (fun (x : W) => f w) s) (P : τ → W → Prop) :

largeScope O P f w = smallScope O P f w

Built from ,

theorem largeScope_eq_smallScope L113–115

{W : Type u_1} {τ : Type u_2} {f : W → τ} (h : IsRigid f) (O : (W → Prop) → W → Prop) (P : τ → W → Prop) :

largeScope O P f = smallScope O P f

Built from , ,

The two scope readings of every designator coincide under an operator extensional at w.

theorem Montague.IsExtensionalAt.largeScope_eq_smallScope L117–122

{W : Type u_1} {τ : Type u_2} {O : (W → Prop) → W → Prop} {w : W} (h : IsExtensionalAt O w) (P : τ → W → Prop) (f : W → τ) :

largeScope O P f w = smallScope O P f w

Built from ,