Intensional Properties: Rigidity, Reference, and Variable Interpretation

[Gal75] [Kri80] [Kap89]

Framework-agnostic types for intensional semantics: intensions as functions from indices (possible worlds) to extensions, rigid designators, evaluation, and referential interpretation modes.

These primitives are shared by Intensional.Defs, Semantics.Reference/, Semantics.Attitudes/, and RSA/ — any module that needs world-parameterized meanings.

Relationship to Denot

Denot E W (.intens a) = W → Denot E W a is an Intension W (Denot E W a). The up/down operators in Frame.lean are definitionally equal to rigid/evalAt here. This file provides the framework-agnostic versions; Frame.lean provides the IL-typed versions.

Key definitions

• Intension — world-to-extension functions (W → τ)
• IsRigid — constancy across indices
• CoRefer, CoExtensional — world-relative and world-universal agreement
• Kripke's necessity of identity theorems
• StableCharacter — Kaplan's stable character predicate
• ReferentialMode — Partee 1973's three-way classification
• SitVarStatus — Elbourne 2013's two-way classification
• IsExtensionalAt — operator extensionality (local truth-functionality); the operator-side dual of IsRigid

@[reducible, inline]

abbrev Intensional.Intension (W : Type u_1) (τ : Type u_2) : Type (max u_1 u_2)

An intension of type τ over indices W: a function from worlds to extensions. [Gal75]'s Ty2 type system: every type τ has an intensional counterpart (s,τ) interpreted as W → ⟦τ⟧.

Equations

• Intensional.Intension W τ = (W → τ)

def Intensional.Intension.rigid {W : Type u_1} {τ : Type u_2} (x : τ) : Intension W τ

A rigid designator: an intension that returns the same value at every world.

Equations

• Intensional.Intension.rigid x x✝ = x

def Intensional.Intension.evalAt {W : Type u_1} {τ : Type u_2} (f : Intension W τ) (w : W) : τ

Evaluate an intension at a world to get its extension.

Equations

• f.evalAt w = f w

def Intensional.Intension.IsRigid {W : Type u_1} {τ : Type u_2} (f : Intension W τ) : Prop

An intension is rigid iff it assigns the same extension at every world.

Equations

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

def Intensional.Intension.IsRigidOn {W : Type u_1} {τ : Type u_2} (f : Intension W τ) (S : Set W) : Prop

An intension is rigid on a set S iff it assigns the same extension at every world in S. The set-relativized analog of IsRigid — used when only constancy across some restricted alternative set is required (e.g., a believer's doxastic alternatives, or a metaphysical-history slice).

IsRigid f is the special case S = Set.univ.

Equations

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

theorem Intensional.Intension.rigid_isRigid {W : Type u_1} {τ : Type u_2} (x : τ) : (rigid x).IsRigid

A rigid designator is rigid.

theorem Intensional.Intension.IsRigid.isRigidOn {W : Type u_1} {τ : Type u_2} {f : Intension W τ} (h : f.IsRigid) (S : Set W) : f.IsRigidOn S

A rigid intension is rigid on every set.

theorem Intensional.Intension.rigid_isRigidOn {W : Type u_1} {τ : Type u_2} (x : τ) (S : Set W) : (rigid x).IsRigidOn S

A rigid designator is rigid on every set.

theorem Intensional.Intension.isRigid_iff_isRigidOn_univ {W : Type u_1} {τ : Type u_2} (f : Intension W τ) : f.IsRigid ↔ f.IsRigidOn Set.univ

Full rigidity is rigidity on the universal set.

theorem Intensional.Intension.IsRigid.map {W : Type u_1} {τ₁ : Type u_2} {τ₂ : Type u_3} {f : Intension W τ₁} (h : f.IsRigid) (g : τ₁ → τ₂) : IsRigid fun (w : W) => g (f w)

Post-composition closure (Intension W is covariantly functorial in its target type, and rigidity is preserved by the functorial action). Given any g : τ₁ → τ₂, the post-composed intension g ∘ f : Intension W τ₂ is rigid whenever f is.

This is what makes the substrate's polymorphism in Res non-trivial: a rigid EntityConcept (Res = Agent) yields a rigid TimeConcept (Res = T) for any Agent → T function — the parallel between individual de re (Anand-Nevins shifty operators) and temporal de re (Abusch wide-scope tenses) is functorial.

def Intensional.Intension.precomp {W₁ : Type u_1} {W₂ : Type u_2} {τ : Type u_3} (g : W₂ → W₁) (f : Intension W₁ τ) : Intension W₂ τ

Pre-composition operator for intensions: given any g : W₂ → W₁, send f : Intension W₁ τ to f ∘ g : Intension W₂ τ. Equivalently Function.comp f g; named here to give the contravariant-functor action a domain-specific handle.

Equations

• Intensional.Intension.precomp g f w = f (g w)

@[simp]

theorem Intensional.Intension.precomp_apply {W₁ : Type u_1} {W₂ : Type u_2} {τ : Type u_3} (g : W₂ → W₁) (f : Intension W₁ τ) (w : W₂) : precomp g f w = f (g w)

theorem Intensional.Intension.IsRigid.precomp {W₁ : Type u_1} {W₂ : Type u_2} {τ : Type u_3} {f : Intension W₁ τ} (h : f.IsRigid) (g : W₂ → W₁) : (Intension.precomp g f).IsRigid

Pre-composition closure (Intension W is contravariantly functorial in its index type). Given any g : W₂ → W₁, the pre-composed intension f ∘ g : Intension W₂ τ is rigid whenever f is — constancy survives any relabeling of the input space.

Used by Semantics/Tense/DeRe.lean to lift a rigid TimeConcept over KContext to a rigid intension over the holder's WorldTimeIndex alternative-shift.

theorem Intensional.Intension.IsRigidOn.map {W : Type u_1} {τ₁ : Type u_2} {τ₂ : Type u_3} {f : Intension W τ₁} {S : Set W} (h : f.IsRigidOn S) (g : τ₁ → τ₂) : IsRigidOn (fun (w : W) => g (f w)) S

Set-relativized version of IsRigid.map: rigidity-on-a-set is preserved by post-composition with any function.

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

Set-relativized version of IsRigid.precomp: rigidity-on-S is preserved by pre-composition with g : W₂ → W₁, with the resulting intension rigid on the preimage Set.preimage g S. Mathlib idiom: precomp pulls back the constancy-set along g.

theorem Intensional.Intension.IsRigid.of_map_injective {W : Type u_1} {τ₁ : Type u_2} {τ₂ : Type u_3} {f : Intension W τ₁} {g : τ₁ → τ₂} (hg : Function.Injective g) (h : IsRigid fun (w : W) => g (f w)) : f.IsRigid

Reflection along injective post-composition: if g ∘ f is rigid and g is injective, then f was already rigid. Together with IsRigid.map, this establishes that IsRigid is preserved AND reflected by injective post-composition — i.e., injective g makes the lifting Intension W τ₁ → Intension W τ₂ rigidity-preserving in both directions.

theorem Intensional.Intension.IsRigid_iff_eq_const {W : Type u_1} {τ : Type u_2} [Nonempty W] (f : Intension W τ) : f.IsRigid ↔ ∃ (x : τ), f = Function.const W x

Mathlib-style characterization: over a nonempty index space, IsRigid is exactly "equals a constant function" via Function.const. The forward direction picks any witness w₀ : W and uses f w₀ as the constant value; the reverse is rfl-trivial.

The Nonempty W hypothesis is needed because without it IsRigid f is vacuously true (no two w₁ w₂ to compare), while ∃ x, f = Function.const W x requires some x : τ to exist as a witness — which fails when τ is also empty.

theorem Intensional.Intension.rigid_eq_const {W : Type u_1} {τ : Type u_2} (x : τ) : rigid x = Function.const W x

rigid x IS Function.const W x definitionally; this is the rigid-named bridge to mathlib's Function.const API.

theorem Intensional.Intension.evalAt_rigid {W : Type u_1} {τ : Type u_2} (x : τ) (w : W) : (rigid x).evalAt w = x

evalAt of rigid returns the original value.

theorem Intensional.Intension.rigid_section {W : Type u_1} {τ : Type u_2} (w : W) : (fun (x : τ) => (rigid x).evalAt w) = id

rigid is a section (right inverse) of world-evaluation: embedding an entity as a rigid intension and then evaluating recovers the entity.

Function-level formulation of evalAt_rigid. Together with rigid_evalAt_lossy, this establishes τ as a retract of Intension W τ via the section-retraction pair (rigid, evalAt · w).

theorem Intensional.Intension.rigid_evalAt_lossy {W : Type u_1} {τ : Type u_2} (f : Intension W τ) (w : W) (hNonRigid : ¬f.IsRigid) : rigid (f w) ≠ f

The reverse composition — evaluating and re-embedding — is lossy: it collapses non-rigid intensions to their value at w.

If f is non-rigid, rigid (f w) ≠ f because rigid (f w) is the constant function at f w, which disagrees with f at the worlds where f varies. Together with rigid_section, this shows that τ is a proper retract of Intension W τ: the round-trip rigid ∘ evalAt · w is the identity on the image of rigid but collapses everything else.

theorem Intensional.Intension.rigid_injective {W : Type u_1} {τ : Type u_2} [Inhabited W] : Function.Injective rigid

rigid is injective: different values give different intensions.

def Intensional.Intension.CoRefer {W : Type u_1} {τ : Type u_2} (f g : Intension W τ) (w : W) : Prop

Two intensions co-refer at world w.

Equations

• f.CoRefer g w = (f w = g w)

def Intensional.Intension.CoExtensional {W : Type u_1} {τ : Type u_2} (f g : Intension W τ) : Prop

Two intensions are co-extensional (agree at every world).

Equations

• f.CoExtensional g = ∀ (w : W), f w = g w

theorem Intensional.Intension.rigid_identity_necessary {W : Type u_1} {τ : Type u_2} (f g : Intension W τ) (hf : f.IsRigid) (hg : g.IsRigid) (w : W) (h : f.CoRefer g w) : f.CoExtensional g

Kripke's necessity of identity: if two rigid designators co-refer at any world, they are co-extensional (and hence the same intension).

This is the formal kernel of the [Kri80] argument: "Hesperus" and "Phosphorus" are both rigid; if they co-refer at the actual world then they pick out the same object at every world, so "Hesperus = Phosphorus" is necessary if true.

theorem Intensional.Intension.rigid_allOrNothing {W : Type u_1} {τ : Type u_2} (f g : Intension W τ) (hf : f.IsRigid) (hg : g.IsRigid) (w₁ w₂ : W) : f w₁ = g w₁ ↔ f w₂ = g w₂

Iff version of the necessity of identity: for rigid designators, co-reference at ANY world is equivalent to co-reference at EVERY world. Identity between rigid designators is never contingent — all or nothing.

theorem Intensional.Intension.varying_not_rigid {W : Type u_1} {τ : Type u_2} (f : Intension W τ) (w₁ w₂ : W) (h : f w₁ ≠ f w₂) : ¬f.IsRigid

An intension that takes different values at two worlds is not rigid. Contrapositive of IsRigid.

theorem Intensional.Intension.rigid_neq_nonrigid {W : Type u_1} {τ : Type u_2} (f g : Intension W τ) (hf : f.IsRigid) (hg : ¬g.IsRigid) : f ≠ g

A rigid intension is never equal to a non-rigid intension.

def Intensional.Intension.StableCharacter {C : Type u_1} {W : Type u_2} {τ : Type u_3} (char : C → Intension W τ) : Prop

A character is stable iff it assigns the same content at every context.

[Kap89] [vFH11] Remark 5: non-indexical expressions have stable character — their content does not depend on the context of utterance. This generalizes constantCharacter from Reference/Basic.lean to the framework-agnostic level.

Equations

• Intensional.Intension.StableCharacter char = ∀ (c₁ c₂ : C), char c₁ = char c₂

inductive Intensional.ReferentialMode.ReferentialMode : Type

[Par73]'s three-way interpretive classification for referential expressions. Applies uniformly to pronouns (entity variables) and tenses (temporal variables).

Mode	Pronouns	Tenses
indexical	"I" → agent of context	present → speech time
anaphoric	"he" → salient individual	past → salient narrative time
bound	"his" in ∀x...his...	tense in "whenever...is..."

[Elb13] collapses this to a two-way free/bound distinction (SitVarStatus); isFree provides the coarsening.

• indexical : ReferentialMode

  Anchored to utterance context (Kaplan's "I", Partee's deictic tense)

• anaphoric : ReferentialMode

  Resolved by discourse salience (3rd-person "he", narrative past)

• bound : ReferentialMode

  Bound by a c-commanding operator (∀x...his..., whenever...is...)

@[implicit_reducible]

instance Intensional.ReferentialMode.instDecidableEqReferentialMode : DecidableEq ReferentialMode

Equations

• Intensional.ReferentialMode.instDecidableEqReferentialMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Intensional.ReferentialMode.instReprReferentialMode : Repr ReferentialMode

Equations

• Intensional.ReferentialMode.instReprReferentialMode = { reprPrec := Intensional.ReferentialMode.instReprReferentialMode.repr }

def Intensional.ReferentialMode.instReprReferentialMode.repr : ReferentialMode → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Intensional.ReferentialMode.ReferentialMode.isFree : ReferentialMode → Bool

Coarsen to a two-way free/bound classification. Indexical and anaphoric are both "free" — they differ only in how the free variable is pragmatically resolved (utterance context vs. discourse salience).

Equations

• Intensional.ReferentialMode.ReferentialMode.indexical.isFree = true
• Intensional.ReferentialMode.ReferentialMode.anaphoric.isFree = true
• Intensional.ReferentialMode.ReferentialMode.bound.isFree = false

inductive Intensional.SitVarStatus.SitVarStatus : Type

[Elb13]'s two-way classification of situation variables. Coarsens ReferentialMode's three-way distinction: indexical and anaphoric both map to free.

• free : SitVarStatus

  Free: mapped to a contextually salient situation (→ de re)

• bound : SitVarStatus

  Bound: bound by an intensional operator (→ de dicto)

@[implicit_reducible]

instance Intensional.SitVarStatus.instDecidableEqSitVarStatus : DecidableEq SitVarStatus

Equations

• Intensional.SitVarStatus.instDecidableEqSitVarStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Intensional.SitVarStatus.instReprSitVarStatus : Repr SitVarStatus

Equations

• Intensional.SitVarStatus.instReprSitVarStatus = { reprPrec := Intensional.SitVarStatus.instReprSitVarStatus.repr }

def Intensional.SitVarStatus.instReprSitVarStatus.repr : SitVarStatus → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Intensional.SitVarStatus.SitVarStatus.toReferentialModes : SitVarStatus → List ReferentialMode.ReferentialMode

Expand Elbourne's two-way classification to Partee's three-way. Free situation variables correspond to either indexical or anaphoric interpretation; bound corresponds to bound.

Equations

• Intensional.SitVarStatus.SitVarStatus.free.toReferentialModes = [Intensional.ReferentialMode.ReferentialMode.indexical, Intensional.ReferentialMode.ReferentialMode.anaphoric]
• Intensional.SitVarStatus.SitVarStatus.bound.toReferentialModes = [Intensional.ReferentialMode.ReferentialMode.bound]

def Intensional.SitVarStatus.ReferentialMode.toSitVarStatus : ReferentialMode.ReferentialMode → SitVarStatus

Collapse Partee's three-way classification to Elbourne's two-way. Uses ReferentialMode.isFree for the coarsening.

Equations

• Intensional.SitVarStatus.ReferentialMode.toSitVarStatus m = if m.isFree = true then Intensional.SitVarStatus.SitVarStatus.free else Intensional.SitVarStatus.SitVarStatus.bound

theorem Intensional.SitVarStatus.sitVarStatus_roundtrip (s : SitVarStatus) (m : ReferentialMode.ReferentialMode) : m ∈ s.toReferentialModes → ReferentialMode.toSitVarStatus m = s

Round-trip: collapsing then expanding recovers the original status (as a member of the expanded list).

Operator extensionality

The operator-side dual of IsRigid: an operator on intensions is extensional at w when its value at w depends on its argument only through the argument's extension at w (local truth-functionality at β = Prop). Negation and the other pointwise connectives are extensional everywhere; quantifiers over indices (Core.Logic.Modal.box) are not. Semantics.Gradability.Classification.isExtensional (Kamp 1975's extensional adjective operators) is the entity-indexed ∀ w-closure of this notion.

def Intensional.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. Equivalently, O · w factors through evaluation at w (isExtensionalAt_iff_factorsThrough).

Equations

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

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

O is extensional: extensional at every index.

Equations

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

theorem Intensional.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

Extensionality at w is O · w factoring through evaluation at w.

theorem Intensional.isExtensionalAt_iff {W : Type u_1} {α : Type u_2} (O : (W → α) → W → Prop) (w : W) : IsExtensionalAt O w ↔ ∀ (p q : W → α), p w = q w → (O p w ↔ O q w)

The iff form at β = Prop, the shape semantic theorems consume.

theorem Intensional.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

Refutation by witness: a pair agreeing at w on which O differs.

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

Evaluation itself is extensional.

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

Constant operators are extensional.

theorem Intensional.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 Intensional.IsExtensionalAt.and {W : Type u_1} {w : W} {α : Type u_2} {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

Extensional operators are closed under pointwise conjunction.

theorem Intensional.IsExtensionalAt.or {W : Type u_1} {w : W} {α : Type u_2} {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

Extensional operators are closed under pointwise disjunction.

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

Extensional operators are closed under pointwise negation.

theorem Intensional.IsExtensionalAt.comp {W : Type u_1} {w : W} {α : Type u_2} {β : Type u_3} {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

Towers of extensional operators are extensional: if O₁, O₂ are extensional at w, so is O₂ applied over O₁'s output intension. Scope-inertness lifts through whole stacks of extensional operators.