@cite{elbourne-2013}: Situation-Semantic Definite Descriptions @cite{elbourne-2013}

@cite{barwise-perry-1983} @cite{elbourne-2005} @cite{heim-1982} @cite{postal-1966} @cite{schwarz-2009} @cite{kamp-1981} @cite{stanley-szab-2000} @cite{tonhauser-beaver-roberts-simons-2013} @cite{roberts-2012}

Formalizes the core theoretical machinery from:

Elbourne, P. (2013). Definite Descriptions. Oxford Studies in Semantics and Pragmatics 1.

Elbourne argues that definite descriptions have a Fregean/Strawsonian semantics — they are type e, introduce a presupposition of existence + uniqueness, and are evaluated relative to situations (parts of worlds).

The single lexical entry ⟦the⟧ = λf.λs : ∃!x f(x)(s) = 1. ιx f(x)(s) = 1 unifies:

• Referential vs attributive uses (Ch 5): free vs bound situation pronoun
• Presupposition projection (Ch 4): domain conditions + λ-Conversion
• Donkey anaphora (Ch 6): pronouns = the + NP-deletion; minimal situations
• De re / de dicto (Ch 7): scope of situation binding, not DP scope
• Incomplete definites (Ch 9): situation restricts evaluation domain
• Existence entailments (Ch 8): presupposition projects to belief states

Key Results

• the_sit / the_sit': Elbourne's situation-relative ⟦the⟧
• the_sit_at_world_eq_the_uniq_w: specializes to existing the_uniq_w
• attributive_is_the_sit_bound: Donnellan's attributive = the_sit' (bound s)
• donkey_uniqueness_from_minimality: minimal situations yield uniqueness
• pronoun_is_definite_article: ⟦it⟧ = ⟦the⟧
• the_sit_assertion_implies_presup: assertion entails presupposition

structure Semantics.Intensional.Situations.Elbourne.SituationFrame : Type 1

A situation frame: the ontological foundation for Elbourne's system.

Situations are parts of worlds, ordered by a part-of relation ≤. Worlds are maximal situations. Properties and quantifiers are evaluated relative to situations rather than worlds, enabling situation-dependent uniqueness and domain restriction.

Based on @cite{barwise-perry-1983}: situations are "individuals having properties and standing in relations at various spatiotemporal locations". @cite{kratzer-1989}: situations are parts of worlds with a mereological structure.

• Sit : Type

  Domain of situations (D_s) — includes both partial situations and worlds

• Ent : Type

  Domain of entities (D_e)

• le : self.Sit → self.Sit → Prop

  Part-of relation (≤): s₁ ≤ s₂ means s₁ is part of s₂

• le_refl (s : self.Sit) : self.le s s

  Reflexivity: every situation is part of itself

• le_trans (s₁ s₂ s₃ : self.Sit) : self.le s₁ s₂ → self.le s₂ s₃ → self.le s₁ s₃

  Transitivity: part-of is transitive

• le_antisymm (s₁ s₂ : self.Sit) : self.le s₁ s₂ → self.le s₂ s₁ → s₁ = s₂

  Antisymmetry: mutual part-of implies identity

def Semantics.Intensional.Situations.Elbourne.SituationFrame.isWorld (F : SituationFrame) (s : F.Sit) : Prop

A world is a maximal situation — one that no other situation properly extends.

Equations

• F.isWorld s = ∀ (s' : F.Sit), F.le s s' → s = s'

def Semantics.Intensional.Situations.Elbourne.SituationFrame.isMinimal (F : SituationFrame) (P : F.Sit → Bool) (s : F.Sit) : Prop

A situation s is minimal for property P iff P holds at s and at no proper part of s. Minimality is key for donkey anaphora (Ch 6): in a minimal situation where "a farmer owns a donkey", there is exactly one farmer and one donkey, securing uniqueness.

Equations

• F.isMinimal P s = (P s = true ∧ ∀ (s' : F.Sit), F.le s' s → P s' = true → s' = s)

def Semantics.Intensional.Situations.Elbourne.the_sit (F : SituationFrame) (domain : List F.Ent) [DecidableEq F.Ent] (restrictor scope : F.Ent → F.Sit → Bool) : Core.Presupposition.PrProp F.Sit

⟦the⟧ in Elbourne's system: the situation-relative Fregean definite.

⟦the⟧ = λf_{⟨e,st⟩}.λs : s ∈ D_s ∧ ∃!x f(x)(s) = 1. ιx f(x)(s) = 1

Takes a restrictor (property of entities relative to situations) and a situation, presupposes existence+uniqueness in that situation, and returns the unique satisfier.

The situation parameter s may be:

• Free (referential use, Ch 5): mapped to a contextually salient s*
• Bound (attributive use, Ch 5): bound by a higher operator (ς, Σ)
• Bound by quantifier (donkey anaphora, Ch 6): bound by always/GEN

This single entry, combined with situation binding, replaces the need for separate the_uniq (uniqueness) and the_fam (familiarity) denotations. The "two types of definites" arise from which situation the pronoun refers to, not from lexical ambiguity.

For compositionality with the existing PrProp infrastructure, we package the result as a presuppositional proposition indexed by situations.

Equations

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

def Semantics.Intensional.Situations.Elbourne.the_sit' {W E : Type} (domain : List E) [DecidableEq E] (restrictor scope : E → W → Bool) : Core.Presupposition.PrProp W

the_sit instantiated with bare type parameters (no SituationFrame) is definitionally equal to the_uniq_w. This shows that the existing the_uniq_w is literally a special case of Elbourne's system.

Equations

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

theorem Semantics.Intensional.Situations.Elbourne.the_sit_at_world_eq_the_uniq_w {W E : Type} (domain : List E) [DecidableEq E] (restrictor scope : E → W → Bool) : the_sit' domain restrictor scope = Lexical.Determiner.Definite.the_uniq_w domain restrictor scope

When situations ARE worlds, the_sit' = the_uniq_w.

This is the key integration theorem: the_sit is strictly more general than the_uniq_w. The existing formalization is a special case of Elbourne's system, not a competing theory.

theorem Semantics.Intensional.Situations.Elbourne.the_sit_presup_depends_on_filter {W E : Type} (domain₁ domain₂ : List E) [DecidableEq E] (restrictor scope : E → W → Bool) (w : W) (h : List.filter (fun (e : E) => restrictor e w) domain₁ = List.filter (fun (e : E) => restrictor e w) domain₂) : (the_sit' domain₁ restrictor scope).presup w = (the_sit' domain₂ restrictor scope).presup w

The presupposition of the_sit' is determined solely by the filter result.

The weak/strong article distinction reduces to situation size:

• Weak article: evaluated at a world-sized situation (global uniqueness)
• Strong article: evaluated at a discourse-restricted situation (familiarity)

Since both are instances of the_sit', the presupposition behavior depends only on which entities satisfy the restrictor at the evaluation situation — not on the full domain. Two domains yielding the same satisfiers produce identical presupposition behavior.

theorem Semantics.Intensional.Situations.Elbourne.the_sit_assertion_implies_presup {W E : Type} (domain : List E) [DecidableEq E] (restrictor scope : E → W → Bool) (w : W) (h : (the_sit' domain restrictor scope).assertion w = true) : (the_sit' domain restrictor scope).presup w = true

A true assertion entails a satisfied presupposition.

This is the formal content of Frege/Strawson: the_sit' cannot assert anything about an entity unless the presupposition of existence+uniqueness holds. Failure of the presupposition forces the assertion to false.

theorem Semantics.Intensional.Situations.Elbourne.attributive_is_the_sit_bound {W E : Type} (domain : List E) [DecidableEq E] (restrictor scope : E → W → Bool) : Reference.Donnellan.definitePrProp domain restrictor scope = the_sit' domain restrictor scope

Donnellan's attributive semantics IS the_sit' with a bound situation variable. Both filter the domain for the unique restrictor-satisfier, varying the evaluation index.

This formalizes Elbourne's central argument against Donnellan's ambiguity: referential and attributive uses arise from the SAME lexical entry. The difference is whether the situation pronoun is free (referential) or bound (attributive).

• Free s → s mapped to a salient restrictor situation s* (= referential)
• Bound s → s bound by an operator (attitude verb, modal, quantifier) (= attributive)

@cite{donnellan-1966} identified a real pragmatic phenomenon (use-types) but was wrong to posit a semantic ambiguity.

structure Semantics.Intensional.Situations.Elbourne.DonkeyConfig (F : SituationFrame) : Type

In Elbourne's system, donkey pronouns are definite articles with phonologically null NP complements (NP-deletion). The NP content is recovered from the restrictor of the quantifier that binds the situation variable.

"Every man who owns a donkey beats it." → LF: every [man s₃ who owns [a s₁ donkey] s₃] [beats [the donkey s₃] s₃]

The pronoun "it" = [the donkey s₃], where:

• "the" = the definite article (the_sit)
• "donkey" = the deleted NP (recovered from the indefinite's restrictor)
• s₃ = a situation variable bound by the quantifier every

• nounContent : F.Ent → F.Sit → Bool

  The restrictor property (e.g., "donkey")

• sitVar : F.Sit

  The pronoun's situation variable

• domain : List F.Ent

  The domain of entities

theorem Semantics.Intensional.Situations.Elbourne.donkey_uniqueness_from_minimality (F : SituationFrame) (domain : List F.Ent) [DecidableEq F.Ent] (restrictor scope : F.Ent → F.Sit → Bool) (s : F.Sit) (h_minimal : F.isMinimal (fun (s : F.Sit) => match List.filter (fun (e : F.Ent) => restrictor e s) domain with | [head] => true | x => false) s) : (the_sit F domain restrictor scope).presup s = true

Uniqueness in donkey contexts derives from minimality of situations.

In a minimal situation where "a farmer owns a donkey", there is exactly one farmer and exactly one donkey. The definite article's uniqueness presupposition is thus automatically satisfied.

This replaces dynamic-semantic approaches that use discourse referents and file cards. Elbourne achieves the same covariation effect through situation binding + minimality.

TODO: prove this fully — requires showing that in a minimal situation s satisfying P, the filter domain.filter (λ e => P e s) yields a singleton. This depends on the definition of minimality for the specific predicate and the relationship between domain and situations.

inductive Semantics.Intensional.Situations.Elbourne.SitVarStatus : Type

The de re / de dicto ambiguity is NOT a matter of DP scope (contra @cite{russell-1905}). It is a matter of situation variable scope.

• De dicto: situation variable BOUND by attitude verb → restrictor evaluated in belief-worlds → referent varies
• De re: situation variable FREE (referential) → restrictor evaluated in actual world → referent fixed

"Mary believes the president is a spy."

• De dicto: [Mary believes [the president s₁] is a spy] where s₁ is bound by believes → president in Mary's belief worlds
• De re: [Mary believes [the president s*] is a spy] where s* refers to actual world → the actual president

This analysis is empirically superior to scope-based approaches because it handles Bäuerle's (1983) puzzle where the indefinite takes narrow scope but the situation pronoun scopes out.

• free : SitVarStatus

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

• bound : SitVarStatus

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

instance Semantics.Intensional.Situations.Elbourne.instDecidableEqSitVarStatus : DecidableEq SitVarStatus

Equations

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

instance Semantics.Intensional.Situations.Elbourne.instBEqSitVarStatus : BEq SitVarStatus

Equations

• Semantics.Intensional.Situations.Elbourne.instBEqSitVarStatus = { beq := Semantics.Intensional.Situations.Elbourne.instBEqSitVarStatus.beq }

def Semantics.Intensional.Situations.Elbourne.instBEqSitVarStatus.beq : SitVarStatus → SitVarStatus → Bool

Equations

• Semantics.Intensional.Situations.Elbourne.instBEqSitVarStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Intensional.Situations.Elbourne.instReprSitVarStatus.repr : SitVarStatus → ℕ → Std.Format

Equations

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

instance Semantics.Intensional.Situations.Elbourne.instReprSitVarStatus : Repr SitVarStatus

Equations

• Semantics.Intensional.Situations.Elbourne.instReprSitVarStatus = { reprPrec := Semantics.Intensional.Situations.Elbourne.instReprSitVarStatus.repr }

def Semantics.Intensional.Situations.Elbourne.sitVarToReading : SitVarStatus → String

The de re / de dicto distinction reduces to situation variable scope.

Equations

• Semantics.Intensional.Situations.Elbourne.sitVarToReading Semantics.Intensional.Situations.Elbourne.SitVarStatus.free = "de re"
• Semantics.Intensional.Situations.Elbourne.sitVarToReading Semantics.Intensional.Situations.Elbourne.SitVarStatus.bound = "de dicto"

structure Semantics.Intensional.Situations.Elbourne.ExistenceEntailmentDatum : Type

Elbourne's key argument against Russell: the definite article introduces a PRESUPPOSITION of existence+uniqueness, not an ASSERTION.

Evidence: "Hans wants the ghost in his attic to be quiet tonight."

• Presupposes: Hans BELIEVES there is exactly one ghost in his attic.
• Does NOT presuppose: there IS a ghost in Hans's attic.

Un@cite{karttunen-1974}'s generalization, the presupposition of the embedded definite projects to the matrix subject's beliefs. This is exactly what the_sit predicts: the situation variable s is bound within the scope of wants, so uniqueness is evaluated in Hans's belief/desire situations, not in the actual world.

Russell's analysis wrongly predicts an assertion of existence, which should then be part of what Hans wants. But "Hans wants the ghost to be quiet" ≠ "Hans wants there to be a ghost and it to be quiet."

• sentence : String

  The sentence

• speakerPresupposes : Bool

  Does the speaker presuppose existence?

• subjectBelieves : Bool

  Does the subject believe in existence?

• existenceActual : Bool

  Is existence actually the case?

• elbournePrediction : String

  Elbourne's prediction: presupposition projects to subject's beliefs

• source : String

  Source

inductive Semantics.Intensional.Situations.Elbourne.IncompletenessSource : Type

Incomplete definite descriptions are definites whose restrictor does not uniquely determine a referent in the global domain, but does in a situationally restricted domain.

"The table is covered with books."

• There are many tables in the world.
• But in the relevant situation s, there is exactly one table.
• Uniqueness is relative to s, not the global domain.

Elbourne (Ch 9 §9.2.5) argues for the "syntactic situation variable approach": the situation parameter on the definite article IS the mechanism of domain restriction. No covert relation variable (contra @cite{von-fintel-1994}), no pragmatic enrichment (contra @cite{sperber-wilson-1986}), no language-of-thought variables (contra @cite{stanley-szab-2000}). Just situations.

This is the simplest account: the situation variable that EVERY definite already has (for uniqueness) also handles incompleteness for free.

• situationVariable : IncompletenessSource

  Situation variable restricts domain

• relationVariable : IncompletenessSource

  Covert relation variable

• pragmaticEnrichment : IncompletenessSource

  Pragmatic enrichment

• explicitApproach : IncompletenessSource

  Explicit approach

• lotRelationVariable : IncompletenessSource

  Language of thought relation variable

instance Semantics.Intensional.Situations.Elbourne.instDecidableEqIncompletenessSource : DecidableEq IncompletenessSource

Equations

• Semantics.Intensional.Situations.Elbourne.instDecidableEqIncompletenessSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Intensional.Situations.Elbourne.instBEqIncompletenessSource : BEq IncompletenessSource

Equations

• Semantics.Intensional.Situations.Elbourne.instBEqIncompletenessSource = { beq := Semantics.Intensional.Situations.Elbourne.instBEqIncompletenessSource.beq }

def Semantics.Intensional.Situations.Elbourne.instBEqIncompletenessSource.beq : IncompletenessSource → IncompletenessSource → Bool

Equations

• Semantics.Intensional.Situations.Elbourne.instBEqIncompletenessSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Intensional.Situations.Elbourne.instReprIncompletenessSource.repr : IncompletenessSource → ℕ → Std.Format

Equations

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

instance Semantics.Intensional.Situations.Elbourne.instReprIncompletenessSource : Repr IncompletenessSource

Equations

• Semantics.Intensional.Situations.Elbourne.instReprIncompletenessSource = { reprPrec := Semantics.Intensional.Situations.Elbourne.instReprIncompletenessSource.repr }

def Semantics.Intensional.Situations.Elbourne.elbournePreferred : IncompletenessSource

Elbourne's argument: situation variables handle incompleteness AND sloppy identity (Ch 9 §9.3) simultaneously. The other approaches fail to account for the strict/sloppy pattern in donkey sentences with downstressed continuations.

Equations

• Semantics.Intensional.Situations.Elbourne.elbournePreferred = Semantics.Intensional.Situations.Elbourne.IncompletenessSource.situationVariable

inductive Semantics.Intensional.Situations.Elbourne.NPDeletionSource : Type

How the deleted NP content is recovered.

• antecedent : NPDeletionSource

  Linguistic antecedent (anaphoric)

• visualCue : NPDeletionSource

  Visual cue in environment (deictic/referential)

• generalKnowledge : NPDeletionSource

  General knowledge, e.g., "person" (Voldemort phrases)

• donkeyRestrictor : NPDeletionSource

  Donkey: recovered from indefinite's restrictor

instance Semantics.Intensional.Situations.Elbourne.instDecidableEqNPDeletionSource : DecidableEq NPDeletionSource

Equations

• Semantics.Intensional.Situations.Elbourne.instDecidableEqNPDeletionSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Intensional.Situations.Elbourne.instBEqNPDeletionSource.beq : NPDeletionSource → NPDeletionSource → Bool

Equations

• Semantics.Intensional.Situations.Elbourne.instBEqNPDeletionSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Intensional.Situations.Elbourne.instBEqNPDeletionSource : BEq NPDeletionSource

Equations

• Semantics.Intensional.Situations.Elbourne.instBEqNPDeletionSource = { beq := Semantics.Intensional.Situations.Elbourne.instBEqNPDeletionSource.beq }

instance Semantics.Intensional.Situations.Elbourne.instReprNPDeletionSource : Repr NPDeletionSource

Equations

• Semantics.Intensional.Situations.Elbourne.instReprNPDeletionSource = { reprPrec := Semantics.Intensional.Situations.Elbourne.instReprNPDeletionSource.repr }

def Semantics.Intensional.Situations.Elbourne.instReprNPDeletionSource.repr : NPDeletionSource → ℕ → Std.Format

Equations

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

structure Semantics.Intensional.Situations.Elbourne.PronounAsDefinite : Type

• pronounForm : String

  The pronoun form

• deletedNP : String

  The deleted NP content (recovered from context)

• npSource : NPDeletionSource

  Source of NP content

• equivalentDefinite : String

  Equivalent overt definite description

def Semantics.Intensional.Situations.Elbourne.instReprPronounAsDefinite.repr : PronounAsDefinite → ℕ → Std.Format

Equations

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

instance Semantics.Intensional.Situations.Elbourne.instReprPronounAsDefinite : Repr PronounAsDefinite

Equations

• Semantics.Intensional.Situations.Elbourne.instReprPronounAsDefinite = { reprPrec := Semantics.Intensional.Situations.Elbourne.instReprPronounAsDefinite.repr }

instance Semantics.Intensional.Situations.Elbourne.instBEqPronounAsDefinite : BEq PronounAsDefinite

Equations

• Semantics.Intensional.Situations.Elbourne.instBEqPronounAsDefinite = { beq := Semantics.Intensional.Situations.Elbourne.instBEqPronounAsDefinite.beq }

def Semantics.Intensional.Situations.Elbourne.instBEqPronounAsDefinite.beq : PronounAsDefinite → PronounAsDefinite → Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Intensional.Situations.Elbourne.instBEqPronounAsDefinite.beq x✝¹ x✝ = false

@[reducible, inline]

abbrev Semantics.Intensional.Situations.Elbourne.pronounDenot {W E : Type} (domain : List E) [DecidableEq E] (recoveredNP scope : E → W → Bool) : Core.Presupposition.PrProp W

Pronoun denotation in Elbourne's system (@cite{postal-1966}, @cite{elbourne-2005}, 2013 Ch 10).

A pronoun with recovered NP content R has the SAME denotation as the definite article applied to R:

⟦pronoun⟧(R)(scope)(s) = ⟦the⟧(R)(scope)(s) = the_sit'(domain)(R)(scope)(s)

The only difference between "the dog" and "it" (with recovered NP "dog") is phonological: the pronoun has a deleted NP complement. The semantic function is literally the_sit' in both cases.

Equations

• Semantics.Intensional.Situations.Elbourne.pronounDenot domain recoveredNP scope = Semantics.Intensional.Situations.Elbourne.the_sit' domain recoveredNP scope

theorem Semantics.Intensional.Situations.Elbourne.pronoun_is_definite_article {W E : Type} (domain : List E) [DecidableEq E] (restrictor scope : E → W → Bool) : pronounDenot domain restrictor scope = the_sit' domain restrictor scope

Pronouns = definite articles: ⟦it⟧ = ⟦the⟧ (@cite{postal-1966}, @cite{elbourne-2005}, 2013 Ch 10).

A pronoun's denotation, given a contextually recovered NP restrictor, is extensionally identical to the definite article applied to the same restrictor. There is no semantic distinction — only a phonological one (NP-deletion).

This is the formal statement of Elbourne's unification: the same function the_sit' serves as the denotation of both "the [NP]" and "pronoun [∅_NP]". The surface difference between definite descriptions and pronouns is entirely syntactic (overt vs deleted NP).

theorem Semantics.Intensional.Situations.Elbourne.pronoun_assertion_implies_presup {W E : Type} (domain : List E) [DecidableEq E] (recoveredNP scope : E → W → Bool) (w : W) (h : (pronounDenot domain recoveredNP scope).assertion w = true) : (pronounDenot domain recoveredNP scope).presup w = true

Pronoun assertions entail pronoun presuppositions (inherits from the_sit'). This confirms that the Frege/Strawson property carries over to Elbourne's analysis of pronouns: "it" presupposes existence+uniqueness of the deleted NP's referent, just like "the [NP]" does.

def Semantics.Intensional.Situations.Elbourne.presupTypeToSitDescription : Core.Definiteness.DefPresupType → String

The weak/strong article distinction is a distinction in which situation the definite is evaluated at, not a lexical ambiguity.

• Weak article (uniqueness): evaluated at a WORLD-SIZED situation → global uniqueness required
• Strong article (familiarity): evaluated at a DISCOURSE-RESTRICTED situation → uniqueness among salient entities only

This connects Core/Definiteness.lean's DefPresupType to Elbourne's system: both.uniqueness and.familiarity are generated by the_sit, differing only in the size of the evaluation situation.

Equations

• Semantics.Intensional.Situations.Elbourne.presupTypeToSitDescription Core.Definiteness.DefPresupType.uniqueness = "world-sized situation (global uniqueness)"
• Semantics.Intensional.Situations.Elbourne.presupTypeToSitDescription Core.Definiteness.DefPresupType.familiarity = "discourse-restricted situation (salience-based uniqueness)"

def Semantics.Intensional.Situations.Elbourne.useModeToSitVar : Reference.Donnellan.UseMode → SitVarStatus

Donnellan's referential/attributive distinction is subsumed by Elbourne's situation-binding analysis.

• Donnellan's UseMode.referential = Elbourne's free situation pronoun Both yield rigid reference to a contextually fixed individual.
• Donnellan's UseMode.attributive = Elbourne's bound situation pronoun Both yield world-varying reference to whoever satisfies the description.

The key advance: Elbourne derives the distinction from independently needed situation variables, while Donnellan posits a semantic ambiguity that @cite{kripke-1977} argued against.

Equations

• Semantics.Intensional.Situations.Elbourne.useModeToSitVar Semantics.Reference.Donnellan.UseMode.referential = Semantics.Intensional.Situations.Elbourne.SitVarStatus.free
• Semantics.Intensional.Situations.Elbourne.useModeToSitVar Semantics.Reference.Donnellan.UseMode.attributive = Semantics.Intensional.Situations.Elbourne.SitVarStatus.bound

theorem Semantics.Intensional.Situations.Elbourne.useMode_sitVar_roundtrip (m : Reference.Donnellan.UseMode) : (match useModeToSitVar m with | SitVarStatus.free => Reference.Donnellan.UseMode.referential | SitVarStatus.bound => Reference.Donnellan.UseMode.attributive) = m

Mapping is total and injective: the two systems are isomorphic.

inductive Semantics.Intensional.Situations.Elbourne.SitBinder : Type

Elbourne's three situation binders. These bind situation variables at different semantic types:

• ς_i (iota-binder): binds situation variables in ⟨s,t⟩ constituents (sentences, propositions). Used by quantificational adverbs (always, sometimes) and the GEN operator.

• Σ_i (Sigma-binder): binds situation variables in ⟨e,st⟩ constituents (verb phrases, predicates). Used by quantificational determiners (every, some) — these need to bind situations within their nuclear scope.

• σ_i (sigma-binder): binds situation variables in ⟨e,sst⟩ constituents (relational nouns). Used for relational readings where the noun relates an entity to a situation.

In practice, ς_i does most of the work. The situation variable s_i in the definite article is typically bound by ς_i placed by a quantifier (every, always) just above the nuclear scope.

• iota (index : ℕ) : SitBinder

  ς_i: binds in ⟨s,t⟩

• sigma (index : ℕ) : SitBinder

  Σ_i: binds in ⟨e,st⟩

• sigmaSub (index : ℕ) : SitBinder

  σ_i: binds in ⟨e,sst⟩

def Semantics.Intensional.Situations.Elbourne.instDecidableEqSitBinder.decEq (x✝ x✝¹ : SitBinder) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Intensional.Situations.Elbourne.instDecidableEqSitBinder : DecidableEq SitBinder

Equations

• Semantics.Intensional.Situations.Elbourne.instDecidableEqSitBinder = Semantics.Intensional.Situations.Elbourne.instDecidableEqSitBinder.decEq

instance Semantics.Intensional.Situations.Elbourne.instBEqSitBinder : BEq SitBinder

Equations

• Semantics.Intensional.Situations.Elbourne.instBEqSitBinder = { beq := Semantics.Intensional.Situations.Elbourne.instBEqSitBinder.beq }

def Semantics.Intensional.Situations.Elbourne.instBEqSitBinder.beq : SitBinder → SitBinder → Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Intensional.Situations.Elbourne.instBEqSitBinder.beq x✝¹ x✝ = false

def Semantics.Intensional.Situations.Elbourne.instReprSitBinder.repr : SitBinder → ℕ → Std.Format

Equations

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

instance Semantics.Intensional.Situations.Elbourne.instReprSitBinder : Repr SitBinder

Equations

• Semantics.Intensional.Situations.Elbourne.instReprSitBinder = { reprPrec := Semantics.Intensional.Situations.Elbourne.instReprSitBinder.repr }

inductive Semantics.Intensional.Situations.Elbourne.SitVar : Type

A situation variable — either free (referential) or indexed for binding.

• free (salience : ℕ := 0) : SitVar

  Free situation pronoun: mapped to a contextually salient situation s*

• bound (index : ℕ) : SitVar

  Bound situation variable with index i — bound by a SitBinder

def Semantics.Intensional.Situations.Elbourne.instDecidableEqSitVar.decEq (x✝ x✝¹ : SitVar) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Intensional.Situations.Elbourne.instDecidableEqSitVar : DecidableEq SitVar

Equations

• Semantics.Intensional.Situations.Elbourne.instDecidableEqSitVar = Semantics.Intensional.Situations.Elbourne.instDecidableEqSitVar.decEq

def Semantics.Intensional.Situations.Elbourne.instBEqSitVar.beq : SitVar → SitVar → Bool

Equations

• Semantics.Intensional.Situations.Elbourne.instBEqSitVar.beq (Semantics.Intensional.Situations.Elbourne.SitVar.free a) (Semantics.Intensional.Situations.Elbourne.SitVar.free b) = (a == b)
• Semantics.Intensional.Situations.Elbourne.instBEqSitVar.beq (Semantics.Intensional.Situations.Elbourne.SitVar.bound a) (Semantics.Intensional.Situations.Elbourne.SitVar.bound b) = (a == b)
• Semantics.Intensional.Situations.Elbourne.instBEqSitVar.beq x✝¹ x✝ = false

instance Semantics.Intensional.Situations.Elbourne.instBEqSitVar : BEq SitVar

Equations

• Semantics.Intensional.Situations.Elbourne.instBEqSitVar = { beq := Semantics.Intensional.Situations.Elbourne.instBEqSitVar.beq }

instance Semantics.Intensional.Situations.Elbourne.instReprSitVar : Repr SitVar

Equations

• Semantics.Intensional.Situations.Elbourne.instReprSitVar = { reprPrec := Semantics.Intensional.Situations.Elbourne.instReprSitVar.repr }

def Semantics.Intensional.Situations.Elbourne.instReprSitVar.repr : SitVar → ℕ → Std.Format

Equations

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

inductive Semantics.Intensional.Situations.Elbourne.UnifiedPhenomenon : Type

Summary of phenomena unified by Elbourne's single lexical entry. Each phenomenon was previously handled by separate mechanisms in the literature; Elbourne derives them all from the_sit + situation binding.

• fregeStrawsonPresupposition : UnifiedPhenomenon

  Ch 3: Basic Fregean presupposition of existence+uniqueness

• presuppositionProjection : UnifiedPhenomenon

  Ch 4: Presupposition projection through connectives

• referentialAttributive : UnifiedPhenomenon

  Ch 5: Referential vs attributive uses

• donkeyAnaphora : UnifiedPhenomenon

  Ch 6: Donkey anaphora covariation

• deReDeDicto : UnifiedPhenomenon

  Ch 7: De re / de dicto ambiguity

• existenceEntailments : UnifiedPhenomenon

  Ch 8: Existence entailments under attitude verbs

• incompleteDefinites : UnifiedPhenomenon

  Ch 9: Incomplete definite descriptions

• pronounsAsDefinites : UnifiedPhenomenon

  Ch 10: Pronouns as definite descriptions

instance Semantics.Intensional.Situations.Elbourne.instDecidableEqUnifiedPhenomenon : DecidableEq UnifiedPhenomenon

Equations

• Semantics.Intensional.Situations.Elbourne.instDecidableEqUnifiedPhenomenon x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Intensional.Situations.Elbourne.instBEqUnifiedPhenomenon : BEq UnifiedPhenomenon

Equations

• Semantics.Intensional.Situations.Elbourne.instBEqUnifiedPhenomenon = { beq := Semantics.Intensional.Situations.Elbourne.instBEqUnifiedPhenomenon.beq }

def Semantics.Intensional.Situations.Elbourne.instBEqUnifiedPhenomenon.beq : UnifiedPhenomenon → UnifiedPhenomenon → Bool

Equations

• Semantics.Intensional.Situations.Elbourne.instBEqUnifiedPhenomenon.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Intensional.Situations.Elbourne.instReprUnifiedPhenomenon.repr : UnifiedPhenomenon → ℕ → Std.Format

Equations

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

instance Semantics.Intensional.Situations.Elbourne.instReprUnifiedPhenomenon : Repr UnifiedPhenomenon

Equations

• Semantics.Intensional.Situations.Elbourne.instReprUnifiedPhenomenon = { reprPrec := Semantics.Intensional.Situations.Elbourne.instReprUnifiedPhenomenon.repr }

def Semantics.Intensional.Situations.Elbourne.phenomenonMechanism : UnifiedPhenomenon → String

All phenomena derive from the same lexical entry + situation binding.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Intensional.Situations.Elbourne.phenomenonMechanism Semantics.Intensional.Situations.Elbourne.UnifiedPhenomenon.fregeStrawsonPresupposition = "Domain condition on the_sit"
• Semantics.Intensional.Situations.Elbourne.phenomenonMechanism Semantics.Intensional.Situations.Elbourne.UnifiedPhenomenon.referentialAttributive = "Free vs bound situation variable"
• Semantics.Intensional.Situations.Elbourne.phenomenonMechanism Semantics.Intensional.Situations.Elbourne.UnifiedPhenomenon.donkeyAnaphora = "Minimal situations + the_sit + NP-deletion"
• Semantics.Intensional.Situations.Elbourne.phenomenonMechanism Semantics.Intensional.Situations.Elbourne.UnifiedPhenomenon.deReDeDicto = "Situation variable scope under attitude verbs"
• Semantics.Intensional.Situations.Elbourne.phenomenonMechanism Semantics.Intensional.Situations.Elbourne.UnifiedPhenomenon.existenceEntailments = "Presupposition projects to subject's beliefs"
• Semantics.Intensional.Situations.Elbourne.phenomenonMechanism Semantics.Intensional.Situations.Elbourne.UnifiedPhenomenon.incompleteDefinites = "Situation restricts evaluation domain"
• Semantics.Intensional.Situations.Elbourne.phenomenonMechanism Semantics.Intensional.Situations.Elbourne.UnifiedPhenomenon.pronounsAsDefinites = "⟦it⟧ = ⟦the⟧ + NP-deletion (Postal 1966)"

def Semantics.Intensional.Situations.Elbourne.qudRelevantSituation (F : SituationFrame) [DecidableEq F.Sit] (leDecide : F.Sit → F.Sit → Bool) (q : QUD F.Sit) (w : F.Sit) (_hw : F.isWorld w) (s : F.Sit) : Prop

A QUD over worlds induces a "relevance" relation on situations: a situation is Q-relevant at world w if it is the smallest part of w that settles which QUD-cell w belongs to.

This is a conjecture — the bridge between epistemological partitions (QUD cells) and ontological restrictions (situations).

Equations

• Semantics.Intensional.Situations.Elbourne.qudRelevantSituation F leDecide q w _hw s = (F.le s w ∧ q.sameAnswer w s = true ∧ F.isMinimal (fun (s' : F.Sit) => leDecide s' w && q.sameAnswer w s') s)

theorem Semantics.Intensional.Situations.Elbourne.situation_pronoun_tracks_qud (F : SituationFrame) [DecidableEq F.Sit] (leDecide : F.Sit → F.Sit → Bool) (q : QUD F.Sit) (w : F.Sit) (hw : F.isWorld w) (s : F.Sit) (hs : qudRelevantSituation F leDecide q w hw s) (domain : List F.Ent) [DecidableEq F.Ent] (restrictor scope : F.Ent → F.Sit → Bool) (hRestr : ∀ (e : F.Ent), restrictor e s = restrictor e w) (hScope : ∀ (e : F.Ent), scope e s = scope e w) : (the_sit F domain restrictor scope).assertion s = (the_sit F domain restrictor scope).assertion w

The QUD–situation bridge: Elbourne's situation pronoun, when resolved by discourse, picks out the QUD-relevant situation.

The original conjecture (universally quantified over all restrictors/scopes) was false: the_sit filters by restrictor e s vs restrictor e w and uses scope e s vs scope e w, which can differ across situations.

The correct version requires persistence: both the restrictor and scope must be invariant between the QUD-relevant situation s and the world w. This captures the intuition that a Q-compatible predicate has the same extension in the relevant situation as in the full world.

theorem Semantics.Intensional.Situations.Elbourne.qud_refinement_monotone (F : SituationFrame) [DecidableEq F.Sit] (leDecide : F.Sit → F.Sit → Bool) (q₁ q₂ : QUD F.Sit) (w : F.Sit) (hw : F.isWorld w) (s₁ s₂ : F.Sit) (hRefine : ∀ (a b : F.Sit), q₂.sameAnswer a b = true → q₁.sameAnswer a b = true) (hs₁ : qudRelevantSituation F leDecide q₁ w hw s₁) (hs₂ : qudRelevantSituation F leDecide q₂ w hw s₂) (hUniq : ∀ (s : F.Sit), F.le s w → q₁.sameAnswer w s = true → F.le s₁ s) : F.le s₁ s₂

QUD refinement corresponds to situation enlargement, given that the coarser QUD's minimal situation is unique (below the finer one).

The original conjecture was false without uniqueness: isMinimal gives a minimal element, not the minimum. In a partial order, s₁ and s₂ can be incomparable minimal elements of their respective sets. The hypothesis hUniq below ensures s₁ is the unique minimal situation for q₁ below s₂, which holds when the part-of relation on sub-world situations is well-founded and the Q₁-resolving set is a filter (closed under finite meets).

def Semantics.Intensional.Situations.Elbourne.SitVarStatus.toReferentialModes : SitVarStatus → List Core.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

• Semantics.Intensional.Situations.Elbourne.SitVarStatus.free.toReferentialModes = [Core.ReferentialMode.ReferentialMode.indexical, Core.ReferentialMode.ReferentialMode.anaphoric]
• Semantics.Intensional.Situations.Elbourne.SitVarStatus.bound.toReferentialModes = [Core.ReferentialMode.ReferentialMode.bound]

def Semantics.Intensional.Situations.Elbourne.ReferentialMode.toSitVarStatus : Core.ReferentialMode.ReferentialMode → SitVarStatus

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

Equations

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

theorem Semantics.Intensional.Situations.Elbourne.sitVarStatus_roundtrip (s : SitVarStatus) (m : Core.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).