@[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₂

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

A rigid designator is rigid.

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.

Stable Character (@cite{kaplan-1989} §XIX Remarks 5-8)

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

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.

instance Core.ReferentialMode.instReprReferentialMode : Repr ReferentialMode

Equations

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

instance Core.ReferentialMode.instBEqReferentialMode : BEq ReferentialMode

Equations

• Core.ReferentialMode.instBEqReferentialMode = { beq := Core.ReferentialMode.instBEqReferentialMode.beq }

def Core.ReferentialMode.instBEqReferentialMode.beq : ReferentialMode → ReferentialMode → Bool

Equations

• Core.ReferentialMode.instBEqReferentialMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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)

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.instBEqSitVarStatus.beq : SitVarStatus → SitVarStatus → Bool

Equations

• Core.SitVarStatus.instBEqSitVarStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.SitVarStatus.instBEqSitVarStatus : BEq SitVarStatus

Equations

• Core.SitVarStatus.instBEqSitVarStatus = { beq := Core.SitVarStatus.instBEqSitVarStatus.beq }

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

Equations

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

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

@[reducible, inline]

abbrev Core.VarAssignment.VarAssignment (D : Type u_1) : Type u_1

Generic variable assignment: maps indices to values in domain D. Instantiate with D = Entity for pronoun interpretation (@cite{heim-kratzer-1998}) or D = Time for temporal variable interpretation.

Equations

• Core.VarAssignment.VarAssignment D = (ℕ → D)

def Core.VarAssignment.updateVar {D : Type u_1} (g : VarAssignment D) (n : ℕ) (d : D) : VarAssignment D

Modified assignment g[n ↦ d]: update index n to value d.

Equations

• Core.VarAssignment.updateVar g n d i = if i = n then d else g i

def Core.VarAssignment.lookupVar {D : Type u_1} (n : ℕ) (g : VarAssignment D) : D

Variable denotation: ⟦xₙ⟧^g = g(n).

Equations

• Core.VarAssignment.lookupVar n g = g n

def Core.VarAssignment.varLambdaAbs {D : Type u_1} {α : Type u_2} (n : ℕ) (body : VarAssignment D → α) : VarAssignment D → D → α

Lambda abstraction over variable n: bind a variable in body.

Equations

• Core.VarAssignment.varLambdaAbs n body g d = body (Core.VarAssignment.updateVar g n d)

@[simp]

theorem Core.VarAssignment.update_lookup_same {D : Type u_1} (g : VarAssignment D) (n : ℕ) (d : D) : lookupVar n (updateVar g n d) = d

@[simp]

theorem Core.VarAssignment.update_lookup_other {D : Type u_1} (g : VarAssignment D) (n i : ℕ) (d : D) (h : i ≠ n) : lookupVar i (updateVar g n d) = lookupVar i g

theorem Core.VarAssignment.update_update_same {D : Type u_1} (g : VarAssignment D) (n : ℕ) (d₁ d₂ : D) : updateVar (updateVar g n d₁) n d₂ = updateVar g n d₂

theorem Core.VarAssignment.update_self {D : Type u_1} (g : VarAssignment D) (n : ℕ) : updateVar g n (g n) = g