@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} @cite{donnellan-1966} @cite{kripke-1977} @cite{karttunen-1974}

Formalizes the core theoretical machinery and empirical predictions 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

Empirical Chain

Fragments/English/Determiners.lean
  "the": qforce =.definite → the_sit / the_sit'
Fragments/English/Pronouns.lean
  "it"/"he"/"she": pronounType =.personal, person =.third → the_sit' + NP-deletion
    ↓
(this file: theory + empirical predictions)
  referential/attributive → truth values → match empirical judgments
  incomplete definites → situation-relative uniqueness
  donkey anaphora → minimality → uniqueness

structure Elbourne2013.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 Elbourne2013.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 Elbourne2013.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 Elbourne2013.the_sit (F : SituationFrame) (domain : List 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.

Built from the canonical presupOfReferent combinator with russellIotaList as the per-situation referent selector.

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

Equations

• Elbourne2013.the_sit F domain restrictor scope = Core.Presupposition.PrProp.presupOfReferent (fun (s : F.Sit) => Core.Nominal.russellIotaList domain fun (e : F.Ent) => restrictor e s) scope

def Elbourne2013.the_sit' {W E : Type} (domain : List E) (restrictor scope : E → W → Bool) : Core.Presupposition.PrProp W

the_sit instantiated with bare type parameters (no SituationFrame). Coincides with Donnellan.definitePrProp — the same Russellian iota factored through presupOfReferent.

Equations

• Elbourne2013.the_sit' domain restrictor scope = Core.Presupposition.PrProp.presupOfReferent (fun (w : W) => Core.Nominal.russellIotaList domain fun (e : E) => restrictor e w) scope

theorem Elbourne2013.the_sit'_eq_definitePrProp {W E : Type} (domain : List E) (restrictor scope : E → W → Bool) : the_sit' domain restrictor scope = Semantics.Reference.Donnellan.definitePrProp domain restrictor scope

the_sit' and Donnellan.definitePrProp denote the same PrProp: both factor through presupOfReferent applied to a Russellian iota over the domain. The two names reflect different theoretical lineages (Elbourne's situation semantics vs. Donnellan's attributive use); the denotation is one and the same.

theorem Elbourne2013.the_sit_presup_depends_on_filter {W E : Type} (domain₁ domain₂ : List 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.

theorem Elbourne2013.the_sit_assertion_implies_presup {W E : Type} (domain : List E) (restrictor scope : E → W → Bool) (w : W) (h : (the_sit' domain restrictor scope).assertion w = (true = true)) : (the_sit' domain restrictor scope).presup w = (true = true)

A true assertion entails a satisfied presupposition.

theorem Elbourne2013.attributive_is_the_sit_bound {W E : Type} (domain : List E) (restrictor scope : E → W → Bool) : Semantics.Reference.Donnellan.definitePrProp domain restrictor scope = the_sit' domain restrictor scope

Donnellan's attributive semantics IS the_sit' with a bound situation variable.

structure Elbourne2013.DonkeyConfig (F : SituationFrame) : Type

In Elbourne's system, donkey pronouns are definite articles with phonologically null NP complements (NP-deletion).

• 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 Elbourne2013.donkey_uniqueness_from_minimality (F : SituationFrame) (domain : List 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

Uniqueness in donkey contexts derives from minimality of situations.

def Elbourne2013.useModeToSitVar : Semantics.Reference.Donnellan.UseMode → Core.SitVarStatus.SitVarStatus

Donnellan's referential/attributive distinction maps to Elbourne's free/bound situation variable distinction.

Equations

• Elbourne2013.useModeToSitVar Semantics.Reference.Donnellan.UseMode.referential = Core.SitVarStatus.SitVarStatus.free
• Elbourne2013.useModeToSitVar Semantics.Reference.Donnellan.UseMode.attributive = Core.SitVarStatus.SitVarStatus.bound

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

Mapping is total and injective.

structure Elbourne2013.ExistenceEntailmentDatum : Type

• 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

• source : String

  Source

inductive Elbourne2013.IncompletenessSource : Type

• situationVariable : IncompletenessSource
• relationVariable : IncompletenessSource
• pragmaticEnrichment : IncompletenessSource
• explicitApproach : IncompletenessSource
• lotRelationVariable : IncompletenessSource

@[implicit_reducible]

instance Elbourne2013.instDecidableEqIncompletenessSource : DecidableEq IncompletenessSource

Equations

• Elbourne2013.instDecidableEqIncompletenessSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Elbourne2013.instReprIncompletenessSource.repr : IncompletenessSource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Elbourne2013.instReprIncompletenessSource : Repr IncompletenessSource

Equations

• Elbourne2013.instReprIncompletenessSource = { reprPrec := Elbourne2013.instReprIncompletenessSource.repr }

def Elbourne2013.elbournePreferred : IncompletenessSource

Equations

• Elbourne2013.elbournePreferred = Elbourne2013.IncompletenessSource.situationVariable

inductive Elbourne2013.NPDeletionSource : Type

How the deleted NP content is recovered.

• antecedent : NPDeletionSource
• visualCue : NPDeletionSource
• generalKnowledge : NPDeletionSource
• donkeyRestrictor : NPDeletionSource

@[implicit_reducible]

instance Elbourne2013.instDecidableEqNPDeletionSource : DecidableEq NPDeletionSource

Equations

• Elbourne2013.instDecidableEqNPDeletionSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Elbourne2013.instReprNPDeletionSource.repr : NPDeletionSource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Elbourne2013.instReprNPDeletionSource : Repr NPDeletionSource

Equations

• Elbourne2013.instReprNPDeletionSource = { reprPrec := Elbourne2013.instReprNPDeletionSource.repr }

structure Elbourne2013.PronounAsDefinite : Type

• pronounForm : String
• deletedNP : String
• npSource : NPDeletionSource
• equivalentDefinite : String

@[implicit_reducible]

instance Elbourne2013.instReprPronounAsDefinite : Repr PronounAsDefinite

Equations

• Elbourne2013.instReprPronounAsDefinite = { reprPrec := Elbourne2013.instReprPronounAsDefinite.repr }

def Elbourne2013.instReprPronounAsDefinite.repr : PronounAsDefinite → ℕ → Std.Format

Equations

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

def Elbourne2013.instBEqPronounAsDefinite.beq : PronounAsDefinite → PronounAsDefinite → Bool

Equations

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

@[implicit_reducible]

instance Elbourne2013.instBEqPronounAsDefinite : BEq PronounAsDefinite

Equations

• Elbourne2013.instBEqPronounAsDefinite = { beq := Elbourne2013.instBEqPronounAsDefinite.beq }

@[reducible, inline]

abbrev Elbourne2013.pronounDenot {W E : Type} (domain : List E) (recoveredNP scope : E → W → Bool) : Core.Presupposition.PrProp W

Pronoun denotation: ⟦it⟧ = ⟦the⟧ + NP-deletion.

Equations

• Elbourne2013.pronounDenot domain recoveredNP scope = Elbourne2013.the_sit' domain recoveredNP scope

theorem Elbourne2013.pronoun_is_definite_article {W E : Type} (domain : List E) (restrictor scope : E → W → Bool) : pronounDenot domain restrictor scope = the_sit' domain restrictor scope

Pronouns = definite articles.

theorem Elbourne2013.pronoun_assertion_implies_presup {W E : Type} (domain : List E) (recoveredNP scope : E → W → Bool) (w : W) (h : (pronounDenot domain recoveredNP scope).assertion w = (true = true)) : (pronounDenot domain recoveredNP scope).presup w = (true = true)

Pronoun assertions entail pronoun presuppositions.

inductive Elbourne2013.SitBinder : Type

Elbourne's three situation binders.

• iota (index : ℕ) : SitBinder
• sigma (index : ℕ) : SitBinder
• sigmaSub (index : ℕ) : SitBinder

def Elbourne2013.instDecidableEqSitBinder.decEq (x✝ x✝¹ : SitBinder) : Decidable (x✝ = x✝¹)

Equations

• Elbourne2013.instDecidableEqSitBinder.decEq (Elbourne2013.SitBinder.iota a) (Elbourne2013.SitBinder.iota b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Elbourne2013.instDecidableEqSitBinder.decEq (Elbourne2013.SitBinder.iota index) (Elbourne2013.SitBinder.sigma index_1) = isFalse ⋯
• Elbourne2013.instDecidableEqSitBinder.decEq (Elbourne2013.SitBinder.iota index) (Elbourne2013.SitBinder.sigmaSub index_1) = isFalse ⋯
• Elbourne2013.instDecidableEqSitBinder.decEq (Elbourne2013.SitBinder.sigma index) (Elbourne2013.SitBinder.iota index_1) = isFalse ⋯
• Elbourne2013.instDecidableEqSitBinder.decEq (Elbourne2013.SitBinder.sigma a) (Elbourne2013.SitBinder.sigma b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Elbourne2013.instDecidableEqSitBinder.decEq (Elbourne2013.SitBinder.sigma index) (Elbourne2013.SitBinder.sigmaSub index_1) = isFalse ⋯
• Elbourne2013.instDecidableEqSitBinder.decEq (Elbourne2013.SitBinder.sigmaSub index) (Elbourne2013.SitBinder.iota index_1) = isFalse ⋯
• Elbourne2013.instDecidableEqSitBinder.decEq (Elbourne2013.SitBinder.sigmaSub index) (Elbourne2013.SitBinder.sigma index_1) = isFalse ⋯
• Elbourne2013.instDecidableEqSitBinder.decEq (Elbourne2013.SitBinder.sigmaSub a) (Elbourne2013.SitBinder.sigmaSub b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Elbourne2013.instDecidableEqSitBinder : DecidableEq SitBinder

Equations

• Elbourne2013.instDecidableEqSitBinder = Elbourne2013.instDecidableEqSitBinder.decEq

def Elbourne2013.instReprSitBinder.repr : SitBinder → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Elbourne2013.instReprSitBinder : Repr SitBinder

Equations

• Elbourne2013.instReprSitBinder = { reprPrec := Elbourne2013.instReprSitBinder.repr }

inductive Elbourne2013.SitVar : Type

A situation variable — either free or indexed for binding.

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

def Elbourne2013.instDecidableEqSitVar.decEq (x✝ x✝¹ : SitVar) : Decidable (x✝ = x✝¹)

Equations

• Elbourne2013.instDecidableEqSitVar.decEq (Elbourne2013.SitVar.free a) (Elbourne2013.SitVar.free b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Elbourne2013.instDecidableEqSitVar.decEq (Elbourne2013.SitVar.free salience) (Elbourne2013.SitVar.bound index) = isFalse ⋯
• Elbourne2013.instDecidableEqSitVar.decEq (Elbourne2013.SitVar.bound index) (Elbourne2013.SitVar.free salience) = isFalse ⋯
• Elbourne2013.instDecidableEqSitVar.decEq (Elbourne2013.SitVar.bound a) (Elbourne2013.SitVar.bound b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Elbourne2013.instDecidableEqSitVar : DecidableEq SitVar

Equations

• Elbourne2013.instDecidableEqSitVar = Elbourne2013.instDecidableEqSitVar.decEq

@[implicit_reducible]

instance Elbourne2013.instReprSitVar : Repr SitVar

Equations

• Elbourne2013.instReprSitVar = { reprPrec := Elbourne2013.instReprSitVar.repr }

def Elbourne2013.instReprSitVar.repr : SitVar → ℕ → Std.Format

Equations

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

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

Equations

• Elbourne2013.qudRelevantSituation F leDecide q w _hw s = (F.le s w ∧ q.r w s ∧ F.isMinimal (fun (s' : F.Sit) => leDecide s' w && q.sameAnswer w s') s)

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

theorem Elbourne2013.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₂.r a b → q₁.r a b) (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₁.r w s → F.le s₁ s) : F.le s₁ s₂

Bridge 1: "the" → the_sit

theorem Elbourne2013.the_is_definite : Fragments.English.Determiners.the.qforce = Theories.Semantics.Quantification.Lexicon.QForce.definite

theorem Elbourne2013.english_the_is_uniqueness : Semantics.Definiteness.qforceToPresupType Fragments.English.Determiners.the.qforce = some Features.Definiteness.DefPresupType.uniqueness

theorem Elbourne2013.english_demonstratives_are_definite : Fragments.English.Determiners.this.qforce = Theories.Semantics.Quantification.Lexicon.QForce.definite ∧ Fragments.English.Determiners.that.qforce = Theories.Semantics.Quantification.Lexicon.QForce.definite

Bridge 3: Pronouns → the_sit + NP-deletion

theorem Elbourne2013.it_entry_classification : Fragments.English.Pronouns.it.pronounType = Fragments.English.Pronouns.PronounType.personal ∧ Fragments.English.Pronouns.it.person = some UD.Person.third ∧ Fragments.English.Pronouns.it.number = some Number.sg

theorem Elbourne2013.he_entry_classification : Fragments.English.Pronouns.he.pronounType = Fragments.English.Pronouns.PronounType.personal ∧ Fragments.English.Pronouns.he.person = some UD.Person.third ∧ Fragments.English.Pronouns.he.number = some Number.sg ∧ Fragments.English.Pronouns.he.case_ = some UD.Case.nom

theorem Elbourne2013.she_entry_classification : Fragments.English.Pronouns.she.pronounType = Fragments.English.Pronouns.PronounType.personal ∧ Fragments.English.Pronouns.she.person = some UD.Person.third ∧ Fragments.English.Pronouns.she.number = some Number.sg ∧ Fragments.English.Pronouns.she.case_ = some UD.Case.nom

Bridge 4: Donnellan → Elbourne

theorem Elbourne2013.referential_is_free : useModeToSitVar Semantics.Reference.Donnellan.UseMode.referential = Core.SitVarStatus.SitVarStatus.free

theorem Elbourne2013.attributive_is_bound : useModeToSitVar Semantics.Reference.Donnellan.UseMode.attributive = Core.SitVarStatus.SitVarStatus.bound

Bridge 5: Pronoun-as-definite examples

def Elbourne2013.donkeyPronounExample : PronounAsDefinite

Equations

• Elbourne2013.donkeyPronounExample = { pronounForm := "it", deletedNP := "donkey", npSource := Elbourne2013.NPDeletionSource.donkeyRestrictor, equivalentDefinite := "the donkey" }

def Elbourne2013.anaphoricPronounExample : PronounAsDefinite

Equations

• Elbourne2013.anaphoricPronounExample = { pronounForm := "he", deletedNP := "Junior Dean", npSource := Elbourne2013.NPDeletionSource.antecedent, equivalentDefinite := "the Junior Dean" }

def Elbourne2013.voldemortExample : PronounAsDefinite

Equations

• Elbourne2013.voldemortExample = { pronounForm := "he", deletedNP := "person", npSource := Elbourne2013.NPDeletionSource.generalKnowledge, equivalentDefinite := "the person who hesitates" }

inductive Elbourne2013.Sit : Type

• sCourtroom : Sit
• sOffice : Sit
• wActual : Sit

@[implicit_reducible]

instance Elbourne2013.instDecidableEqSit : DecidableEq Sit

Equations

• Elbourne2013.instDecidableEqSit x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Elbourne2013.instReprSit.repr : Sit → ℕ → Std.Format

Equations

• Elbourne2013.instReprSit.repr Elbourne2013.Sit.sCourtroom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.Sit.sCourtroom")).group prec✝
• Elbourne2013.instReprSit.repr Elbourne2013.Sit.sOffice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.Sit.sOffice")).group prec✝
• Elbourne2013.instReprSit.repr Elbourne2013.Sit.wActual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.Sit.wActual")).group prec✝

@[implicit_reducible]

instance Elbourne2013.instReprSit : Repr Sit

Equations

• Elbourne2013.instReprSit = { reprPrec := Elbourne2013.instReprSit.repr }

inductive Elbourne2013.Ent : Type

• jones : Ent
• smith : Ent
• wilson : Ent
• table1 : Ent
• table2 : Ent
• table3 : Ent

@[implicit_reducible]

instance Elbourne2013.instDecidableEqEnt : DecidableEq Ent

Equations

• Elbourne2013.instDecidableEqEnt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Elbourne2013.instReprEnt : Repr Ent

Equations

• Elbourne2013.instReprEnt = { reprPrec := Elbourne2013.instReprEnt.repr }

def Elbourne2013.instReprEnt.repr : Ent → ℕ → Std.Format

Equations

• Elbourne2013.instReprEnt.repr Elbourne2013.Ent.jones prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.Ent.jones")).group prec✝
• Elbourne2013.instReprEnt.repr Elbourne2013.Ent.smith prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.Ent.smith")).group prec✝
• Elbourne2013.instReprEnt.repr Elbourne2013.Ent.wilson prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.Ent.wilson")).group prec✝
• Elbourne2013.instReprEnt.repr Elbourne2013.Ent.table1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.Ent.table1")).group prec✝
• Elbourne2013.instReprEnt.repr Elbourne2013.Ent.table2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.Ent.table2")).group prec✝
• Elbourne2013.instReprEnt.repr Elbourne2013.Ent.table3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.Ent.table3")).group prec✝

def Elbourne2013.allEnts : List Ent

Equations

• Elbourne2013.allEnts = [Elbourne2013.Ent.jones, Elbourne2013.Ent.smith, Elbourne2013.Ent.wilson, Elbourne2013.Ent.table1, Elbourne2013.Ent.table2, Elbourne2013.Ent.table3]

def Elbourne2013.isMurderer : Ent → Sit → Bool

Equations

• Elbourne2013.isMurderer Elbourne2013.Ent.jones Elbourne2013.Sit.sCourtroom = true
• Elbourne2013.isMurderer Elbourne2013.Ent.wilson Elbourne2013.Sit.wActual = true
• Elbourne2013.isMurderer x✝¹ x✝ = false

def Elbourne2013.isInsane : Ent → Sit → Bool

Equations

• Elbourne2013.isInsane Elbourne2013.Ent.jones x✝ = true
• Elbourne2013.isInsane x✝¹ x✝ = false

def Elbourne2013.theMurderer : Core.Presupposition.PrProp Sit

Equations

• Elbourne2013.theMurderer = Elbourne2013.the_sit' Elbourne2013.allEnts Elbourne2013.isMurderer Elbourne2013.isInsane

theorem Elbourne2013.referential_presup : theMurderer.presup Sit.sCourtroom = (true = true)

theorem Elbourne2013.referential_assertion : theMurderer.assertion Sit.sCourtroom = (true = true)

theorem Elbourne2013.attributive_presup : theMurderer.presup Sit.wActual = (true = true)

theorem Elbourne2013.attributive_assertion : theMurderer.assertion Sit.wActual = (false = true)

theorem Elbourne2013.ref_attr_diverge : theMurderer.assertion Sit.sCourtroom ≠ theMurderer.assertion Sit.wActual

def Elbourne2013.refSitVar : SitVar

Equations

• Elbourne2013.refSitVar = Elbourne2013.SitVar.free

def Elbourne2013.attrSitVar : SitVar

Equations

• Elbourne2013.attrSitVar = Elbourne2013.SitVar.bound 1

theorem Elbourne2013.same_entry_both_readings : theMurderer = theMurderer

def Elbourne2013.isTable : Ent → Sit → Bool

Equations

• Elbourne2013.isTable Elbourne2013.Ent.table1 Elbourne2013.Sit.sOffice = true
• Elbourne2013.isTable Elbourne2013.Ent.table1 Elbourne2013.Sit.wActual = true
• Elbourne2013.isTable Elbourne2013.Ent.table2 Elbourne2013.Sit.wActual = true
• Elbourne2013.isTable Elbourne2013.Ent.table3 Elbourne2013.Sit.wActual = true
• Elbourne2013.isTable x✝¹ x✝ = false

def Elbourne2013.isCoveredWithBooks : Ent → Sit → Bool

Equations

• Elbourne2013.isCoveredWithBooks Elbourne2013.Ent.table1 x✝ = true
• Elbourne2013.isCoveredWithBooks x✝¹ x✝ = false

def Elbourne2013.theTable : Core.Presupposition.PrProp Sit

Equations

• Elbourne2013.theTable = Elbourne2013.the_sit' Elbourne2013.allEnts Elbourne2013.isTable Elbourne2013.isCoveredWithBooks

theorem Elbourne2013.incomplete_presup_office : theTable.presup Sit.sOffice = (true = true)

theorem Elbourne2013.incomplete_presup_world : theTable.presup Sit.wActual = (false = true)

theorem Elbourne2013.incomplete_assertion_office : theTable.assertion Sit.sOffice = (true = true)

theorem Elbourne2013.incompleteness_is_situation_variable : elbournePreferred = IncompletenessSource.situationVariable

inductive Elbourne2013.DkEnt : Type

• farmer1 : DkEnt
• farmer2 : DkEnt
• donkey_a : DkEnt
• donkey_b : DkEnt
• donkey_c : DkEnt

@[implicit_reducible]

instance Elbourne2013.instDecidableEqDkEnt : DecidableEq DkEnt

Equations

• Elbourne2013.instDecidableEqDkEnt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Elbourne2013.instReprDkEnt : Repr DkEnt

Equations

• Elbourne2013.instReprDkEnt = { reprPrec := Elbourne2013.instReprDkEnt.repr }

def Elbourne2013.instReprDkEnt.repr : DkEnt → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Elbourne2013.instReprDkEnt.repr Elbourne2013.DkEnt.farmer1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.DkEnt.farmer1")).group prec✝
• Elbourne2013.instReprDkEnt.repr Elbourne2013.DkEnt.farmer2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.DkEnt.farmer2")).group prec✝

inductive Elbourne2013.DkSit : Type

• sMin1 : DkSit
• sMin2 : DkSit
• wActual : DkSit

@[implicit_reducible]

instance Elbourne2013.instDecidableEqDkSit : DecidableEq DkSit

Equations

• Elbourne2013.instDecidableEqDkSit x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Elbourne2013.instReprDkSit.repr : DkSit → ℕ → Std.Format

Equations

• Elbourne2013.instReprDkSit.repr Elbourne2013.DkSit.sMin1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.DkSit.sMin1")).group prec✝
• Elbourne2013.instReprDkSit.repr Elbourne2013.DkSit.sMin2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.DkSit.sMin2")).group prec✝
• Elbourne2013.instReprDkSit.repr Elbourne2013.DkSit.wActual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.DkSit.wActual")).group prec✝

@[implicit_reducible]

instance Elbourne2013.instReprDkSit : Repr DkSit

Equations

• Elbourne2013.instReprDkSit = { reprPrec := Elbourne2013.instReprDkSit.repr }

def Elbourne2013.dkLe : DkSit → DkSit → Prop

Equations

• Elbourne2013.dkLe x✝ Elbourne2013.DkSit.wActual = True
• Elbourne2013.dkLe Elbourne2013.DkSit.sMin1 Elbourne2013.DkSit.sMin1 = True
• Elbourne2013.dkLe Elbourne2013.DkSit.sMin2 Elbourne2013.DkSit.sMin2 = True
• Elbourne2013.dkLe x✝¹ x✝ = False

def Elbourne2013.DkF : SituationFrame

Equations

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

def Elbourne2013.dkEnts : List DkEnt

Equations

• Elbourne2013.dkEnts = [Elbourne2013.DkEnt.farmer1, Elbourne2013.DkEnt.farmer2, Elbourne2013.DkEnt.donkey_a, Elbourne2013.DkEnt.donkey_b, Elbourne2013.DkEnt.donkey_c]

def Elbourne2013.isDonkey : DkEnt → DkSit → Bool

Equations

• Elbourne2013.isDonkey Elbourne2013.DkEnt.donkey_a Elbourne2013.DkSit.sMin1 = true
• Elbourne2013.isDonkey Elbourne2013.DkEnt.donkey_b Elbourne2013.DkSit.sMin2 = true
• Elbourne2013.isDonkey Elbourne2013.DkEnt.donkey_a Elbourne2013.DkSit.wActual = true
• Elbourne2013.isDonkey Elbourne2013.DkEnt.donkey_b Elbourne2013.DkSit.wActual = true
• Elbourne2013.isDonkey Elbourne2013.DkEnt.donkey_c Elbourne2013.DkSit.wActual = true
• Elbourne2013.isDonkey x✝¹ x✝ = false

def Elbourne2013.isBeaten : DkEnt → DkSit → Bool

Equations

• Elbourne2013.isBeaten Elbourne2013.DkEnt.donkey_a x✝ = true
• Elbourne2013.isBeaten Elbourne2013.DkEnt.donkey_b x✝ = true
• Elbourne2013.isBeaten x✝¹ x✝ = false

def Elbourne2013.donkeyPronoun : Core.Presupposition.PrProp DkSit

Equations

• Elbourne2013.donkeyPronoun = Elbourne2013.the_sit' Elbourne2013.dkEnts Elbourne2013.isDonkey Elbourne2013.isBeaten

theorem Elbourne2013.donkey_presup_min1 : donkeyPronoun.presup DkSit.sMin1 = (true = true)

theorem Elbourne2013.donkey_presup_min2 : donkeyPronoun.presup DkSit.sMin2 = (true = true)

theorem Elbourne2013.donkey_presup_world_fails : donkeyPronoun.presup DkSit.wActual = (false = true)

theorem Elbourne2013.donkey_assertion_min1 : donkeyPronoun.assertion DkSit.sMin1 = (true = true)

theorem Elbourne2013.donkey_assertion_min2 : donkeyPronoun.assertion DkSit.sMin2 = (true = true)

def Elbourne2013.donkeyConfig1 : DonkeyConfig DkF

Equations

• Elbourne2013.donkeyConfig1 = { nounContent := Elbourne2013.isDonkey, sitVar := Elbourne2013.DkSit.sMin1, domain := Elbourne2013.dkEnts }

def Elbourne2013.donkeyConfig2 : DonkeyConfig DkF

Equations

• Elbourne2013.donkeyConfig2 = { nounContent := Elbourne2013.isDonkey, sitVar := Elbourne2013.DkSit.sMin2, domain := Elbourne2013.dkEnts }

theorem Elbourne2013.donkey_uniqueness_via_minimality_min1 : DkF.isMinimal (fun (s : DkF.Sit) => match List.filter (fun (e : DkEnt) => isDonkey e s) dkEnts with | [head] => true | x => false) DkSit.sMin1

theorem Elbourne2013.donkey_uniqueness_via_minimality_min2 : DkF.isMinimal (fun (s : DkF.Sit) => match List.filter (fun (e : DkEnt) => isDonkey e s) dkEnts with | [head] => true | x => false) DkSit.sMin2

inductive Elbourne2013.BSit : Type

• actual : BSit
• belief : BSit

@[implicit_reducible]

instance Elbourne2013.instDecidableEqBSit : DecidableEq BSit

Equations

• Elbourne2013.instDecidableEqBSit x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Elbourne2013.instReprBSit : Repr BSit

Equations

• Elbourne2013.instReprBSit = { reprPrec := Elbourne2013.instReprBSit.repr }

def Elbourne2013.instReprBSit.repr : BSit → ℕ → Std.Format

Equations

• Elbourne2013.instReprBSit.repr Elbourne2013.BSit.actual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.BSit.actual")).group prec✝
• Elbourne2013.instReprBSit.repr Elbourne2013.BSit.belief prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.BSit.belief")).group prec✝

inductive Elbourne2013.BEnt : Type

• jones : BEnt
• smith : BEnt
• mary : BEnt

@[implicit_reducible]

instance Elbourne2013.instDecidableEqBEnt : DecidableEq BEnt

Equations

• Elbourne2013.instDecidableEqBEnt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Elbourne2013.instReprBEnt.repr : BEnt → ℕ → Std.Format

Equations

• Elbourne2013.instReprBEnt.repr Elbourne2013.BEnt.jones prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.BEnt.jones")).group prec✝
• Elbourne2013.instReprBEnt.repr Elbourne2013.BEnt.smith prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.BEnt.smith")).group prec✝
• Elbourne2013.instReprBEnt.repr Elbourne2013.BEnt.mary prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Elbourne2013.BEnt.mary")).group prec✝

@[implicit_reducible]

instance Elbourne2013.instReprBEnt : Repr BEnt

Equations

• Elbourne2013.instReprBEnt = { reprPrec := Elbourne2013.instReprBEnt.repr }

def Elbourne2013.bEnts : List BEnt

Equations

• Elbourne2013.bEnts = [Elbourne2013.BEnt.jones, Elbourne2013.BEnt.smith, Elbourne2013.BEnt.mary]

def Elbourne2013.isPresident : BEnt → BSit → Bool

Equations

• Elbourne2013.isPresident Elbourne2013.BEnt.jones Elbourne2013.BSit.actual = true
• Elbourne2013.isPresident Elbourne2013.BEnt.smith Elbourne2013.BSit.belief = true
• Elbourne2013.isPresident x✝¹ x✝ = false

def Elbourne2013.isSpy : BEnt → BSit → Bool

Equations

• Elbourne2013.isSpy Elbourne2013.BEnt.smith x✝ = true
• Elbourne2013.isSpy x✝¹ x✝ = false

def Elbourne2013.thePresident : Core.Presupposition.PrProp BSit

Equations

• Elbourne2013.thePresident = Elbourne2013.the_sit' Elbourne2013.bEnts Elbourne2013.isPresident Elbourne2013.isSpy

theorem Elbourne2013.deRe_presup : thePresident.presup BSit.actual = (true = true)

theorem Elbourne2013.deRe_assertion : thePresident.assertion BSit.actual = (false = true)

theorem Elbourne2013.deDicto_presup : thePresident.presup BSit.belief = (true = true)

theorem Elbourne2013.deDicto_assertion : thePresident.assertion BSit.belief = (true = true)

theorem Elbourne2013.deRe_deDicto_diverge : thePresident.assertion BSit.actual ≠ thePresident.assertion BSit.belief

theorem Elbourne2013.deRe_is_free : Core.SitVarStatus.SitVarStatus.free = useModeToSitVar Semantics.Reference.Donnellan.UseMode.referential

theorem Elbourne2013.deDicto_is_bound : Core.SitVarStatus.SitVarStatus.bound = useModeToSitVar Semantics.Reference.Donnellan.UseMode.attributive

def Elbourne2013.deReVar : SitVar

Equations

• Elbourne2013.deReVar = Elbourne2013.SitVar.free

def Elbourne2013.deDictoVar : SitVar

Equations

• Elbourne2013.deDictoVar = Elbourne2013.SitVar.bound 1

def Elbourne2013.hansGhost : ExistenceEntailmentDatum

Equations

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

def Elbourne2013.ponceFountain : ExistenceEntailmentDatum

Equations

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

inductive Elbourne2013.GhostSit : Type

• actual : GhostSit
• belief : GhostSit

@[implicit_reducible]

instance Elbourne2013.instDecidableEqGhostSit : DecidableEq GhostSit

Equations

• Elbourne2013.instDecidableEqGhostSit x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Elbourne2013.instReprGhostSit.repr : GhostSit → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Elbourne2013.instReprGhostSit : Repr GhostSit

Equations

• Elbourne2013.instReprGhostSit = { reprPrec := Elbourne2013.instReprGhostSit.repr }

inductive Elbourne2013.GhostEnt : Type

• hans : GhostEnt
• ghost : GhostEnt

@[implicit_reducible]

instance Elbourne2013.instDecidableEqGhostEnt : DecidableEq GhostEnt

Equations

• Elbourne2013.instDecidableEqGhostEnt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Elbourne2013.instReprGhostEnt.repr : GhostEnt → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Elbourne2013.instReprGhostEnt : Repr GhostEnt

Equations

• Elbourne2013.instReprGhostEnt = { reprPrec := Elbourne2013.instReprGhostEnt.repr }

def Elbourne2013.ghostEnts : List GhostEnt

Equations

• Elbourne2013.ghostEnts = [Elbourne2013.GhostEnt.hans, Elbourne2013.GhostEnt.ghost]

def Elbourne2013.isGhost : GhostEnt → GhostSit → Bool

Equations

• Elbourne2013.isGhost Elbourne2013.GhostEnt.ghost Elbourne2013.GhostSit.belief = true
• Elbourne2013.isGhost x✝¹ x✝ = false

def Elbourne2013.isQuiet : GhostEnt → GhostSit → Bool

Equations

• Elbourne2013.isQuiet Elbourne2013.GhostEnt.ghost x✝ = true
• Elbourne2013.isQuiet x✝¹ x✝ = false

def Elbourne2013.theGhost : Core.Presupposition.PrProp GhostSit

Equations

• Elbourne2013.theGhost = Elbourne2013.the_sit' Elbourne2013.ghostEnts Elbourne2013.isGhost Elbourne2013.isQuiet

theorem Elbourne2013.ghost_presup_belief : theGhost.presup GhostSit.belief = (true = true)

theorem Elbourne2013.ghost_presup_actual : theGhost.presup GhostSit.actual = (false = true)

theorem Elbourne2013.ghost_matches_datum : hansGhost.speakerPresupposes = false ∧ hansGhost.subjectBelieves = true ∧ hansGhost.existenceActual = false

theorem Elbourne2013.ponce_matches_datum : ponceFountain.speakerPresupposes = false ∧ ponceFountain.subjectBelieves = true ∧ ponceFountain.existenceActual = false

def Elbourne2013.itAsDonkey : Core.Presupposition.PrProp DkSit

Equations

• Elbourne2013.itAsDonkey = Elbourne2013.pronounDenot Elbourne2013.dkEnts Elbourne2013.isDonkey Elbourne2013.isBeaten

theorem Elbourne2013.pronoun_matches_definite_min1 : itAsDonkey = donkeyPronoun

theorem Elbourne2013.pronoun_presup_min1 : itAsDonkey.presup DkSit.sMin1 = (true = true)

theorem Elbourne2013.pronoun_presup_world_fails : itAsDonkey.presup DkSit.wActual = (false = true)

theorem Elbourne2013.np_sources_exercised : donkeyPronounExample.npSource = NPDeletionSource.donkeyRestrictor ∧ anaphoricPronounExample.npSource = NPDeletionSource.antecedent ∧ voldemortExample.npSource = NPDeletionSource.generalKnowledge