Intensional Properties: Rigidity, Reference, and Variable Interpretation

@cite{gallin-1975} @cite{kripke-1980} @cite{kaplan-1989}

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 Core.Logic.Intensional.Frame, Semantics.Reference/, Semantics.Attitudes/, and RSA/ — any module that needs world-parameterized meanings.

Relationship to Frame

Frame.Denot (.intens a) = F.Index → F.Denot a is an Intension F.Index (F.Denot 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

@[reducible, inline]

abbrev Core.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. @cite{gallin-1975}'s Ty2 type system: every type τ has an intensional counterpart (s,τ) interpreted as W → ⟦τ⟧.

Equations

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

def Core.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

• Core.Intension.rigid x x✝ = x

def Core.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 Core.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 Core.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 Core.Intension.rigid_isRigid {W : Type u_1} {τ : Type u_2} (x : τ) : (rigid x).IsRigid

A rigid designator is rigid.

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

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

@[simp]

theorem Core.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 Core.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 Theories/Semantics/Tense/DeRe.lean to lift a rigid TimeConcept over KContext to a rigid intension over the holder's WorldTimeIndex alternative-shift.

theorem Core.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 Core.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 Core.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 Core.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 Core.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 Core.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 Core.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 Core.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 Core.Intension.rigid_injective {W : Type u_1} {τ : Type u_2} [Inhabited W] : Function.Injective rigid

rigid is injective: different values give different intensions.

def Core.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 Core.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 Core.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 @cite{kripke-1980} 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 Core.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 Core.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 Core.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 Core.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.

@cite{kaplan-1989} @cite{von-fintel-heim-2011} 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

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

inductive Core.ReferentialMode.ReferentialMode : Type

@cite{partee-1973}'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..."

@cite{elbourne-2013} 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 Core.ReferentialMode.instDecidableEqReferentialMode : DecidableEq ReferentialMode

Equations

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

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

Equations

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

@[implicit_reducible]

instance Core.ReferentialMode.instReprReferentialMode : Repr ReferentialMode

Equations

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

def Core.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

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

inductive Core.SitVarStatus.SitVarStatus : Type

@cite{elbourne-2013}'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 Core.SitVarStatus.instDecidableEqSitVarStatus : DecidableEq SitVarStatus

Equations

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

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

Equations

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

@[implicit_reducible]

instance Core.SitVarStatus.instReprSitVarStatus : Repr SitVarStatus

Equations

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

def Core.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

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

def Core.SitVarStatus.ReferentialMode.toSitVarStatus : ReferentialMode.ReferentialMode → SitVarStatus

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

Equations

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

theorem Core.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).