Documentation

Linglib.Phenomena.Reference.Studies.Elbourne2013

@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 Phenomena.Reference.Studies.Elbourne2013.SituationFrame :

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

Instances For

def Phenomena.Reference.Studies.Elbourne2013.SituationFrame.isWorld (F : SituationFrame) (s : F.Sit) :

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'

Instances For

def Phenomena.Reference.Studies.Elbourne2013.SituationFrame.isMinimal (F : SituationFrame) (P : F.Sit → Bool) (s : F.Sit) :

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)

Instances For

def Phenomena.Reference.Studies.Elbourne2013.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

Equations

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

Instances For

def Phenomena.Reference.Studies.Elbourne2013.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).

Equations

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

Instances For

theorem Phenomena.Reference.Studies.Elbourne2013.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 = Semantics.Lexical.Determiner.Definite.the_uniq_w domain restrictor scope

When situations ARE worlds, the_sit' = the_uniq_w.

theorem Phenomena.Reference.Studies.Elbourne2013.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.

theorem Phenomena.Reference.Studies.Elbourne2013.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.

theorem Phenomena.Reference.Studies.Elbourne2013.attributive_is_the_sit_bound {W E : Type} (domain : List E) [DecidableEq 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 Phenomena.Reference.Studies.Elbourne2013.DonkeyConfig (F : SituationFrame) :

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

Instances For

theorem Phenomena.Reference.Studies.Elbourne2013.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.

def Phenomena.Reference.Studies.Elbourne2013.useModeToSitVar :

Semantics.Reference.Donnellan.UseMode → Core.SitVarStatus.SitVarStatus

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

Equations

Instances For

theorem Phenomena.Reference.Studies.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 Phenomena.Reference.Studies.Elbourne2013.ExistenceEntailmentDatum :

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

Instances For

inductive Phenomena.Reference.Studies.Elbourne2013.IncompletenessSource :

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

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instDecidableEqIncompletenessSource :

DecidableEq IncompletenessSource

Equations

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

def Phenomena.Reference.Studies.Elbourne2013.instBEqIncompletenessSource.beq :

IncompletenessSource → IncompletenessSource → Bool

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqIncompletenessSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instBEqIncompletenessSource :

BEq IncompletenessSource

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqIncompletenessSource = { beq := Phenomena.Reference.Studies.Elbourne2013.instBEqIncompletenessSource.beq }

def Phenomena.Reference.Studies.Elbourne2013.instReprIncompletenessSource.repr :

IncompletenessSource → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instReprIncompletenessSource :

Repr IncompletenessSource

Equations

Phenomena.Reference.Studies.Elbourne2013.instReprIncompletenessSource = { reprPrec := Phenomena.Reference.Studies.Elbourne2013.instReprIncompletenessSource.repr }

def Phenomena.Reference.Studies.Elbourne2013.elbournePreferred :

IncompletenessSource

Equations

Phenomena.Reference.Studies.Elbourne2013.elbournePreferred = Phenomena.Reference.Studies.Elbourne2013.IncompletenessSource.situationVariable

Instances For

inductive Phenomena.Reference.Studies.Elbourne2013.NPDeletionSource :

How the deleted NP content is recovered.

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

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instDecidableEqNPDeletionSource :

DecidableEq NPDeletionSource

Equations

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

def Phenomena.Reference.Studies.Elbourne2013.instBEqNPDeletionSource.beq :

NPDeletionSource → NPDeletionSource → Bool

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqNPDeletionSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instBEqNPDeletionSource :

BEq NPDeletionSource

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqNPDeletionSource = { beq := Phenomena.Reference.Studies.Elbourne2013.instBEqNPDeletionSource.beq }

def Phenomena.Reference.Studies.Elbourne2013.instReprNPDeletionSource.repr :

NPDeletionSource → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instReprNPDeletionSource :

Repr NPDeletionSource

Equations

Phenomena.Reference.Studies.Elbourne2013.instReprNPDeletionSource = { reprPrec := Phenomena.Reference.Studies.Elbourne2013.instReprNPDeletionSource.repr }

structure Phenomena.Reference.Studies.Elbourne2013.PronounAsDefinite :

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

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instReprPronounAsDefinite :

Repr PronounAsDefinite

Equations

Phenomena.Reference.Studies.Elbourne2013.instReprPronounAsDefinite = { reprPrec := Phenomena.Reference.Studies.Elbourne2013.instReprPronounAsDefinite.repr }

def Phenomena.Reference.Studies.Elbourne2013.instReprPronounAsDefinite.repr :

PronounAsDefinite → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instBEqPronounAsDefinite :

BEq PronounAsDefinite

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqPronounAsDefinite = { beq := Phenomena.Reference.Studies.Elbourne2013.instBEqPronounAsDefinite.beq }

def Phenomena.Reference.Studies.Elbourne2013.instBEqPronounAsDefinite.beq :

PronounAsDefinite → PronounAsDefinite → Bool

Equations

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

Instances For

@[reducible, inline]

abbrev Phenomena.Reference.Studies.Elbourne2013.pronounDenot {W E : Type} (domain : List E) [DecidableEq E] (recoveredNP scope : E → W → Bool) :

Core.Presupposition.PrProp W

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

Equations

Phenomena.Reference.Studies.Elbourne2013.pronounDenot domain recoveredNP scope = Phenomena.Reference.Studies.Elbourne2013.the_sit' domain recoveredNP scope

Instances For

theorem Phenomena.Reference.Studies.Elbourne2013.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.

theorem Phenomena.Reference.Studies.Elbourne2013.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.

inductive Phenomena.Reference.Studies.Elbourne2013.SitBinder :

Elbourne's three situation binders.

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

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instDecidableEqSitBinder :

DecidableEq SitBinder

Equations

Phenomena.Reference.Studies.Elbourne2013.instDecidableEqSitBinder = Phenomena.Reference.Studies.Elbourne2013.instDecidableEqSitBinder.decEq

def Phenomena.Reference.Studies.Elbourne2013.instDecidableEqSitBinder.decEq (x✝ x✝¹ : SitBinder) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instBEqSitBinder :

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqSitBinder = { beq := Phenomena.Reference.Studies.Elbourne2013.instBEqSitBinder.beq }

def Phenomena.Reference.Studies.Elbourne2013.instBEqSitBinder.beq :

SitBinder → SitBinder → Bool

Equations

One or more equations did not get rendered due to their size.
Phenomena.Reference.Studies.Elbourne2013.instBEqSitBinder.beq x✝¹ x✝ = false

Instances For

def Phenomena.Reference.Studies.Elbourne2013.instReprSitBinder.repr :

SitBinder → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instReprSitBinder :

Equations

Phenomena.Reference.Studies.Elbourne2013.instReprSitBinder = { reprPrec := Phenomena.Reference.Studies.Elbourne2013.instReprSitBinder.repr }

inductive Phenomena.Reference.Studies.Elbourne2013.SitVar :

A situation variable — either free or indexed for binding.

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

Instances For

def Phenomena.Reference.Studies.Elbourne2013.instDecidableEqSitVar.decEq (x✝ x✝¹ : SitVar) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instDecidableEqSitVar :

DecidableEq SitVar

Equations

Phenomena.Reference.Studies.Elbourne2013.instDecidableEqSitVar = Phenomena.Reference.Studies.Elbourne2013.instDecidableEqSitVar.decEq

instance Phenomena.Reference.Studies.Elbourne2013.instBEqSitVar :

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqSitVar = { beq := Phenomena.Reference.Studies.Elbourne2013.instBEqSitVar.beq }

def Phenomena.Reference.Studies.Elbourne2013.instBEqSitVar.beq :

SitVar → SitVar → Bool

Equations

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instReprSitVar :

Equations

Phenomena.Reference.Studies.Elbourne2013.instReprSitVar = { reprPrec := Phenomena.Reference.Studies.Elbourne2013.instReprSitVar.repr }

def Phenomena.Reference.Studies.Elbourne2013.instReprSitVar.repr :

SitVar → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.Reference.Studies.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) :

A QUD over worlds induces a "relevance" relation on situations.

Equations

Phenomena.Reference.Studies.Elbourne2013.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)

Instances For

theorem Phenomena.Reference.Studies.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 Phenomena.Reference.Studies.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₂.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₂

Bridge 1: "the" → the_sit #

theorem Phenomena.Reference.Studies.Elbourne2013.the_is_definite :

Fragments.English.Determiners.the.qforce = Fragments.English.Determiners.QForce.definite

theorem Phenomena.Reference.Studies.Elbourne2013.english_the_is_uniqueness :

Semantics.Lexical.Determiner.Definite.qforceToPresupType Fragments.English.Determiners.the.qforce = some Core.Definiteness.DefPresupType.uniqueness

theorem Phenomena.Reference.Studies.Elbourne2013.english_demonstratives_are_definite :

Fragments.English.Determiners.this.qforce = Fragments.English.Determiners.QForce.definite ∧ Fragments.English.Determiners.that.qforce = Fragments.English.Determiners.QForce.definite

Bridge 3: Pronouns → the_sit + NP-deletion #

theorem Phenomena.Reference.Studies.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

Bridge 4: Donnellan → Elbourne #

theorem Phenomena.Reference.Studies.Elbourne2013.referential_is_free :

useModeToSitVar Semantics.Reference.Donnellan.UseMode.referential = Core.SitVarStatus.SitVarStatus.free

theorem Phenomena.Reference.Studies.Elbourne2013.attributive_is_bound :

useModeToSitVar Semantics.Reference.Donnellan.UseMode.attributive = Core.SitVarStatus.SitVarStatus.bound

Bridge 5: Pronoun-as-definite examples #

def Phenomena.Reference.Studies.Elbourne2013.donkeyPronounExample :

PronounAsDefinite

Equations

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

Instances For

def Phenomena.Reference.Studies.Elbourne2013.anaphoricPronounExample :

PronounAsDefinite

Equations

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

Instances For

def Phenomena.Reference.Studies.Elbourne2013.voldemortExample :

PronounAsDefinite

Equations

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

Instances For

inductive Phenomena.Reference.Studies.Elbourne2013.Sit :

sCourtroom : Sit
sOffice : Sit
wActual : Sit

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instDecidableEqSit :

DecidableEq Sit

Equations

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

def Phenomena.Reference.Studies.Elbourne2013.instBEqSit.beq :

Sit → Sit → Bool

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqSit.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instBEqSit :

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqSit = { beq := Phenomena.Reference.Studies.Elbourne2013.instBEqSit.beq }

instance Phenomena.Reference.Studies.Elbourne2013.instReprSit :

Equations

Phenomena.Reference.Studies.Elbourne2013.instReprSit = { reprPrec := Phenomena.Reference.Studies.Elbourne2013.instReprSit.repr }

def Phenomena.Reference.Studies.Elbourne2013.instReprSit.repr :

Sit → ℕ → Std.Format

Equations

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

Instances For

inductive Phenomena.Reference.Studies.Elbourne2013.Ent :

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

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instDecidableEqEnt :

DecidableEq Ent

Equations

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

instance Phenomena.Reference.Studies.Elbourne2013.instBEqEnt :

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqEnt = { beq := Phenomena.Reference.Studies.Elbourne2013.instBEqEnt.beq }

def Phenomena.Reference.Studies.Elbourne2013.instBEqEnt.beq :

Ent → Ent → Bool

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqEnt.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Phenomena.Reference.Studies.Elbourne2013.instReprEnt.repr :

Ent → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instReprEnt :

Equations

Phenomena.Reference.Studies.Elbourne2013.instReprEnt = { reprPrec := Phenomena.Reference.Studies.Elbourne2013.instReprEnt.repr }

def Phenomena.Reference.Studies.Elbourne2013.allEnts :

Equations

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

Instances For

def Phenomena.Reference.Studies.Elbourne2013.isMurderer :

Ent → Sit → Bool

Equations

Instances For

def Phenomena.Reference.Studies.Elbourne2013.isInsane :

Ent → Sit → Bool

Equations

Instances For

def Phenomena.Reference.Studies.Elbourne2013.theMurderer :

Core.Presupposition.PrProp Sit

Equations

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

Instances For

theorem Phenomena.Reference.Studies.Elbourne2013.referential_presup :

theMurderer.presup Sit.sCourtroom = true

theorem Phenomena.Reference.Studies.Elbourne2013.referential_assertion :

theMurderer.assertion Sit.sCourtroom = true

theorem Phenomena.Reference.Studies.Elbourne2013.attributive_presup :

theMurderer.presup Sit.wActual = true

theorem Phenomena.Reference.Studies.Elbourne2013.attributive_assertion :

theMurderer.assertion Sit.wActual = false

theorem Phenomena.Reference.Studies.Elbourne2013.ref_attr_diverge :

theMurderer.assertion Sit.sCourtroom ≠ theMurderer.assertion Sit.wActual

def Phenomena.Reference.Studies.Elbourne2013.refSitVar :

Equations

Phenomena.Reference.Studies.Elbourne2013.refSitVar = Phenomena.Reference.Studies.Elbourne2013.SitVar.free

Instances For

def Phenomena.Reference.Studies.Elbourne2013.attrSitVar :

Equations

Phenomena.Reference.Studies.Elbourne2013.attrSitVar = Phenomena.Reference.Studies.Elbourne2013.SitVar.bound 1

Instances For

theorem Phenomena.Reference.Studies.Elbourne2013.same_entry_both_readings :

theMurderer = theMurderer

def Phenomena.Reference.Studies.Elbourne2013.isCoveredWithBooks :

Ent → Sit → Bool

Equations

Instances For

def Phenomena.Reference.Studies.Elbourne2013.theTable :

Core.Presupposition.PrProp Sit

Equations

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

Instances For

theorem Phenomena.Reference.Studies.Elbourne2013.incomplete_presup_office :

theTable.presup Sit.sOffice = true

theorem Phenomena.Reference.Studies.Elbourne2013.incomplete_presup_world :

theTable.presup Sit.wActual = false

theorem Phenomena.Reference.Studies.Elbourne2013.incomplete_assertion_office :

theTable.assertion Sit.sOffice = true

theorem Phenomena.Reference.Studies.Elbourne2013.incompleteness_is_situation_variable :

elbournePreferred = IncompletenessSource.situationVariable

inductive Phenomena.Reference.Studies.Elbourne2013.DkEnt :

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

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instDecidableEqDkEnt :

DecidableEq DkEnt

Equations

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

instance Phenomena.Reference.Studies.Elbourne2013.instBEqDkEnt :

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqDkEnt = { beq := Phenomena.Reference.Studies.Elbourne2013.instBEqDkEnt.beq }

def Phenomena.Reference.Studies.Elbourne2013.instBEqDkEnt.beq :

DkEnt → DkEnt → Bool

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqDkEnt.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instReprDkEnt :

Equations

Phenomena.Reference.Studies.Elbourne2013.instReprDkEnt = { reprPrec := Phenomena.Reference.Studies.Elbourne2013.instReprDkEnt.repr }

def Phenomena.Reference.Studies.Elbourne2013.instReprDkEnt.repr :

DkEnt → ℕ → Std.Format

Equations

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

Instances For

inductive Phenomena.Reference.Studies.Elbourne2013.DkSit :

sMin1 : DkSit
sMin2 : DkSit
wActual : DkSit

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instDecidableEqDkSit :

DecidableEq DkSit

Equations

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

def Phenomena.Reference.Studies.Elbourne2013.instBEqDkSit.beq :

DkSit → DkSit → Bool

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqDkSit.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instBEqDkSit :

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqDkSit = { beq := Phenomena.Reference.Studies.Elbourne2013.instBEqDkSit.beq }

instance Phenomena.Reference.Studies.Elbourne2013.instReprDkSit :

Equations

Phenomena.Reference.Studies.Elbourne2013.instReprDkSit = { reprPrec := Phenomena.Reference.Studies.Elbourne2013.instReprDkSit.repr }

def Phenomena.Reference.Studies.Elbourne2013.instReprDkSit.repr :

DkSit → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.Reference.Studies.Elbourne2013.DkF :

Equations

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

Instances For

def Phenomena.Reference.Studies.Elbourne2013.dkEnts :

Equations

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

Instances For

def Phenomena.Reference.Studies.Elbourne2013.isDonkey :

DkEnt → DkSit → Bool

Equations

Instances For

def Phenomena.Reference.Studies.Elbourne2013.isBeaten :

DkEnt → DkSit → Bool

Equations

Instances For

def Phenomena.Reference.Studies.Elbourne2013.donkeyPronoun :

Core.Presupposition.PrProp DkSit

Equations

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

Instances For

theorem Phenomena.Reference.Studies.Elbourne2013.donkey_presup_min1 :

donkeyPronoun.presup DkSit.sMin1 = true

theorem Phenomena.Reference.Studies.Elbourne2013.donkey_presup_min2 :

donkeyPronoun.presup DkSit.sMin2 = true

theorem Phenomena.Reference.Studies.Elbourne2013.donkey_presup_world_fails :

donkeyPronoun.presup DkSit.wActual = false

theorem Phenomena.Reference.Studies.Elbourne2013.donkey_assertion_min1 :

donkeyPronoun.assertion DkSit.sMin1 = true

theorem Phenomena.Reference.Studies.Elbourne2013.donkey_assertion_min2 :

donkeyPronoun.assertion DkSit.sMin2 = true

def Phenomena.Reference.Studies.Elbourne2013.donkeyConfig1 :

DonkeyConfig DkF

Equations

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

Instances For

def Phenomena.Reference.Studies.Elbourne2013.donkeyConfig2 :

DonkeyConfig DkF

Equations

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

Instances For

theorem Phenomena.Reference.Studies.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 Phenomena.Reference.Studies.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 Phenomena.Reference.Studies.Elbourne2013.BSit :

actual : BSit
belief : BSit

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instDecidableEqBSit :

DecidableEq BSit

Equations

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

instance Phenomena.Reference.Studies.Elbourne2013.instBEqBSit :

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqBSit = { beq := Phenomena.Reference.Studies.Elbourne2013.instBEqBSit.beq }

def Phenomena.Reference.Studies.Elbourne2013.instBEqBSit.beq :

BSit → BSit → Bool

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqBSit.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instReprBSit :

Equations

Phenomena.Reference.Studies.Elbourne2013.instReprBSit = { reprPrec := Phenomena.Reference.Studies.Elbourne2013.instReprBSit.repr }

def Phenomena.Reference.Studies.Elbourne2013.instReprBSit.repr :

BSit → ℕ → Std.Format

Equations

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

Instances For

inductive Phenomena.Reference.Studies.Elbourne2013.BEnt :

jones : BEnt
smith : BEnt
mary : BEnt

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instDecidableEqBEnt :

DecidableEq BEnt

Equations

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

instance Phenomena.Reference.Studies.Elbourne2013.instBEqBEnt :

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqBEnt = { beq := Phenomena.Reference.Studies.Elbourne2013.instBEqBEnt.beq }

def Phenomena.Reference.Studies.Elbourne2013.instBEqBEnt.beq :

BEnt → BEnt → Bool

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqBEnt.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instReprBEnt :

Equations

Phenomena.Reference.Studies.Elbourne2013.instReprBEnt = { reprPrec := Phenomena.Reference.Studies.Elbourne2013.instReprBEnt.repr }

def Phenomena.Reference.Studies.Elbourne2013.instReprBEnt.repr :

BEnt → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.Reference.Studies.Elbourne2013.bEnts :

Equations

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

Instances For

def Phenomena.Reference.Studies.Elbourne2013.isPresident :

BEnt → BSit → Bool

Equations

Instances For

def Phenomena.Reference.Studies.Elbourne2013.isSpy :

BEnt → BSit → Bool

Equations

Instances For

def Phenomena.Reference.Studies.Elbourne2013.thePresident :

Core.Presupposition.PrProp BSit

Equations

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

Instances For

theorem Phenomena.Reference.Studies.Elbourne2013.deRe_presup :

thePresident.presup BSit.actual = true

theorem Phenomena.Reference.Studies.Elbourne2013.deRe_assertion :

thePresident.assertion BSit.actual = false

theorem Phenomena.Reference.Studies.Elbourne2013.deDicto_presup :

thePresident.presup BSit.belief = true

theorem Phenomena.Reference.Studies.Elbourne2013.deDicto_assertion :

thePresident.assertion BSit.belief = true

theorem Phenomena.Reference.Studies.Elbourne2013.deRe_deDicto_diverge :

thePresident.assertion BSit.actual ≠ thePresident.assertion BSit.belief

theorem Phenomena.Reference.Studies.Elbourne2013.deRe_is_free :

Core.SitVarStatus.SitVarStatus.free = useModeToSitVar Semantics.Reference.Donnellan.UseMode.referential

theorem Phenomena.Reference.Studies.Elbourne2013.deDicto_is_bound :

Core.SitVarStatus.SitVarStatus.bound = useModeToSitVar Semantics.Reference.Donnellan.UseMode.attributive

def Phenomena.Reference.Studies.Elbourne2013.deReVar :

Equations

Phenomena.Reference.Studies.Elbourne2013.deReVar = Phenomena.Reference.Studies.Elbourne2013.SitVar.free

Instances For

def Phenomena.Reference.Studies.Elbourne2013.deDictoVar :

Equations

Phenomena.Reference.Studies.Elbourne2013.deDictoVar = Phenomena.Reference.Studies.Elbourne2013.SitVar.bound 1

Instances For

def Phenomena.Reference.Studies.Elbourne2013.hansGhost :

ExistenceEntailmentDatum

Equations

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

Instances For

def Phenomena.Reference.Studies.Elbourne2013.ponceFountain :

ExistenceEntailmentDatum

Equations

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

Instances For

inductive Phenomena.Reference.Studies.Elbourne2013.GhostSit :

actual : GhostSit
belief : GhostSit

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instDecidableEqGhostSit :

DecidableEq GhostSit

Equations

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

def Phenomena.Reference.Studies.Elbourne2013.instBEqGhostSit.beq :

GhostSit → GhostSit → Bool

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqGhostSit.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instBEqGhostSit :

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqGhostSit = { beq := Phenomena.Reference.Studies.Elbourne2013.instBEqGhostSit.beq }

def Phenomena.Reference.Studies.Elbourne2013.instReprGhostSit.repr :

GhostSit → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instReprGhostSit :

Equations

Phenomena.Reference.Studies.Elbourne2013.instReprGhostSit = { reprPrec := Phenomena.Reference.Studies.Elbourne2013.instReprGhostSit.repr }

inductive Phenomena.Reference.Studies.Elbourne2013.GhostEnt :

hans : GhostEnt
ghost : GhostEnt

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instDecidableEqGhostEnt :

DecidableEq GhostEnt

Equations

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

def Phenomena.Reference.Studies.Elbourne2013.instBEqGhostEnt.beq :

GhostEnt → GhostEnt → Bool

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqGhostEnt.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Reference.Studies.Elbourne2013.instBEqGhostEnt :

Equations

Phenomena.Reference.Studies.Elbourne2013.instBEqGhostEnt = { beq := Phenomena.Reference.Studies.Elbourne2013.instBEqGhostEnt.beq }

instance Phenomena.Reference.Studies.Elbourne2013.instReprGhostEnt :

Equations

Phenomena.Reference.Studies.Elbourne2013.instReprGhostEnt = { reprPrec := Phenomena.Reference.Studies.Elbourne2013.instReprGhostEnt.repr }

def Phenomena.Reference.Studies.Elbourne2013.instReprGhostEnt.repr :

GhostEnt → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.Reference.Studies.Elbourne2013.ghostEnts :

Equations

Phenomena.Reference.Studies.Elbourne2013.ghostEnts = [Phenomena.Reference.Studies.Elbourne2013.GhostEnt.hans , Phenomena.Reference.Studies.Elbourne2013.GhostEnt.ghost ]

Instances For

def Phenomena.Reference.Studies.Elbourne2013.isGhost :

GhostEnt → GhostSit → Bool

Equations

Instances For

def Phenomena.Reference.Studies.Elbourne2013.isQuiet :

GhostEnt → GhostSit → Bool

Equations

Instances For

def Phenomena.Reference.Studies.Elbourne2013.theGhost :

Core.Presupposition.PrProp GhostSit

Equations

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

Instances For

theorem Phenomena.Reference.Studies.Elbourne2013.ghost_presup_belief :

theGhost.presup GhostSit.belief = true

theorem Phenomena.Reference.Studies.Elbourne2013.ghost_presup_actual :

theGhost.presup GhostSit.actual = false

theorem Phenomena.Reference.Studies.Elbourne2013.ghost_matches_datum :

hansGhost.speakerPresupposes = false ∧ hansGhost.subjectBelieves = true ∧ hansGhost.existenceActual = false

theorem Phenomena.Reference.Studies.Elbourne2013.ponce_matches_datum :

ponceFountain.speakerPresupposes = false ∧ ponceFountain.subjectBelieves = true ∧ ponceFountain.existenceActual = false

def Phenomena.Reference.Studies.Elbourne2013.itAsDonkey :

Core.Presupposition.PrProp DkSit

Equations

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

Instances For

theorem Phenomena.Reference.Studies.Elbourne2013.pronoun_matches_definite_min1 :

itAsDonkey = donkeyPronoun

theorem Phenomena.Reference.Studies.Elbourne2013.pronoun_presup_min1 :

itAsDonkey.presup DkSit.sMin1 = true

theorem Phenomena.Reference.Studies.Elbourne2013.pronoun_presup_world_fails :

itAsDonkey.presup DkSit.wActual = false

theorem Phenomena.Reference.Studies.Elbourne2013.np_sources_exercised :

donkeyPronounExample.npSource = NPDeletionSource.donkeyRestrictor ∧ anaphoricPronounExample.npSource = NPDeletionSource.antecedent ∧ voldemortExample.npSource = NPDeletionSource.generalKnowledge