Elbourne (2013): Definite Descriptions

Elbourne gives the definite article a Fregean semantics over situations, the parts of possible worlds ordered by parthood. The article takes a property and a situation and, if exactly one thing has the property there, denotes that thing, so a description is a partial function from situations to individuals. Its situation pronoun is free, referring to a situation the context supplies, or bound by the abstractor of the containing proposition: free pronouns give Donnellan's referential use and bound ones the attributive use. Binding the pronoun below an intensional operator gives the de dicto reading, letting it refer to the actual world the de re reading, and binding it above the operator Kripke's attributive yet de re reading. Under an attitude verb the presupposition projects to the subject's beliefs, after Karttunen, and a donkey-anaphoric description is bound to the minimal situations of its restrictor, which gives donkey sentences their strong reading and a repeated description no sloppy reading.

Main definitions

• the, description, sentence: the article, a description with its situation pronoun, and a sentence as a trivalent proposition.
• deDicto, deRe, attributiveDeRe, attitude: descriptions under intensional operators and attitude verbs.
• Village: situations as finite sets of atomic facts.

Main results

• sentence_ne_zero_iff: a sentence presupposes exactly one satisfier at the situation its pronoun denotes.
• deDicto_ne_zero_iff, deRe_ne_zero_iff, attributiveDeRe_eq_one_iff: the three readings under an intensional operator.
• attitude_eq_zero_of_agnostic, russellian_consistent: the description, unlike its Russellian paraphrase, makes an agnostic subject's desire infelicitous.
• everyOwnerBeatsTheDonkey_iff, incomplete_description, everyOwnerBeatsTheDonkeyAndThePriestToo_iff: the strong donkey reading, incompleteness, and the strict reading of a repeated description in the village.

Implementation notes

• Situations are any partial order; minimality is mathlib's Minimal, and the lexical entries of §2.3.3 are transcribed with it. The article is iota at the situation, so its domain condition is ∃! (the_isSome_iff), and a sentence is Presupposition.presupOfReferent of the description. A situation pronoun is its value as a function of the situation the proposition is applied to, constant when free and the identity when bound. A description inside a scope contributes ∃ z ∈ the f s, the condition under which presupOfReferent is true, with Option membership.
• Intensional operators are universal over an accessibility relation and lift trivalent propositions by the Weak Kleene universal over the accessible situations (Trivalent.forallWeak); attitude verbs are defined where the complement is defined throughout the subject's doxastic alternatives and true where it is true throughout the verb's own, Karttunen's projection.
• The village of ch. 6 and ch. 9 is a concrete model: situations are finite sets of atomic facts ordered by inclusion, Kratzer's states of affairs, so minimal situations are computed and the strong reading of the donkey sentence is a theorem rather than a reading of the truth conditions.
• The examples are Data.Examples.Elbourne2013.

TODO

• Ch. 4's projection through possibility modals, disjunction and negation, ch. 7's modal subordination and counterfactuals, and ch. 10's descriptive indexicals are not represented.

References

• [Elb13]
• [Elb05]
• [Kra89]
• [BP83]
• [HK98]
• [Bur04]
• [Str50]
• [Rus05]
• [Don66]
• [Kri77]
• [Kar74a]
• [SGS00]
• [Gea62]

Quantification over minimal situations (§2.3.3)

def Elbourne2013.Q {S : Type u_1} [PartialOrder S] {E : Type u_2} (f : E → S → Prop) (x : E) (s s' : S) : Prop

The morpheme Q, (22), holds of x when there is an extended situation, a minimal situation between s' and s in which x has the property.

Equations

• Elbourne2013.Q f x s s' = ∃ (s'' : S), Minimal (fun (s'' : S) => s' ≤ s'' ∧ s'' ≤ s ∧ f x s'') s''

def Elbourne2013.every {S : Type u_1} [PartialOrder S] {E : Type u_2} (s₀ : S) (f : E → S → Prop) (g : E → S → S → Prop) (s : S) : Prop

every, (20), holds when every minimal situation, within the restrictor situation s₀ and the truth-supporting situation s, in which an individual has the restrictor property satisfies the nuclear scope.

Equations

• Elbourne2013.every s₀ f g s = ∀ (x : E) (s' : S), Minimal (fun (s' : S) => s' ≤ s₀ ∧ s' ≤ s ∧ f x s') s' → g x s s'

def Elbourne2013.a {S : Type u_1} [PartialOrder S] {E : Type u_2} (s₀ : S) (f : E → S → Prop) (g : E → S → S → Prop) (s : S) : Prop

a, (21), holds when some minimal restrictor situation satisfies the nuclear scope.

Equations

• Elbourne2013.a s₀ f g s = ∃ (x : E) (s' : S), Minimal (fun (s' : S) => s' ≤ s₀ ∧ s' ≤ s ∧ f x s') s' ∧ g x s s'

def Elbourne2013.always {S : Type u_1} [PartialOrder S] (p : S → Prop) (q : S → S → Prop) (s : S) : Prop

always, (33), holds when every minimal situation in s satisfying the antecedent satisfies the consequent.

Equations

• Elbourne2013.always p q s = ∀ (s' : S), Minimal (fun (s' : S) => s' ≤ s ∧ p s') s' → q s s'

def Elbourne2013.QA {S : Type u_1} [PartialOrder S] (p : S → Prop) (s s' : S) : Prop

The morpheme Q_A, (34), is the propositional counterpart of Q.

Equations

• Elbourne2013.QA p s s' = ∃ (s'' : S), Minimal (fun (s'' : S) => s' ≤ s'' ∧ s'' ≤ s ∧ p s'') s''

The article and its situation pronoun (ch. 3–5)

noncomputable def Elbourne2013.the {S : Type u_1} {E : Type u_2} (f : E → S → Prop) (s : S) : Option E

The definite article, (3) of ch. 3, is λf.λs : ∃!x f(x)(s). ιx f(x)(s), a partial function from situations to the unique satisfier of the property in the situation.

Equations

• Elbourne2013.the f s = Reference.iota fun (x : E) => f x s

theorem Elbourne2013.the_isSome_iff {S : Type u_1} {E : Type u_2} (f : E → S → Prop) (s : S) : (the f s).isSome = true ↔ ∃! x : E, f x s

The domain condition of the article is that exactly one thing has the property in the situation.

theorem Elbourne2013.the_eq_some_iff {S : Type u_1} {E : Type u_2} (f : E → S → Prop) (s : S) (x : E) : the f s = some x ↔ f x s ∧ ∀ (y : E), f y s → y = x

noncomputable def Elbourne2013.pronoun {S : Type u_1} {E : Type u_2} (np : E → S → Prop) : S → Option E

A pronoun, (4b) of ch. 10, has the article's entry, its noun phrase supplied by NP-deletion.

Equations

• Elbourne2013.pronoun np = Elbourne2013.the np

noncomputable def Elbourne2013.description {S : Type u_1} {E : Type u_2} (σ : S → S) (f : E → S → Prop) (s : S) : Option E

[[the NP] sᵢ], (4) of ch. 3, is the description with its situation pronoun, whose value is the function σ of the situation the containing proposition is applied to. A free pronoun is constant, so that the referent enters via the context and is the same wherever the proposition is applied, the referential use of (11) of ch. 5; a bound one is the identity (Situation Binding I and λ-Conversion II), so that the individual described depends on the situation of evaluation, the attributive use of (15) of ch. 5.

Equations

• Elbourne2013.description σ f s = Elbourne2013.the f (σ s)

noncomputable def Elbourne2013.sentence {S : Type u_1} {E : Type u_2} (σ : S → S) (f vp : E → S → Prop) : S → SignType

[[[the NP] sᵢ] VP] is the sentence as a trivalent proposition, (3) of ch. 4 for a free pronoun and (4) for a bound one.

Equations

• Elbourne2013.sentence σ f vp = Presupposition.presupOfReferent (Elbourne2013.description σ f) vp

theorem Elbourne2013.sentence_ne_zero_iff {S : Type u_1} {E : Type u_2} (σ : S → S) (f vp : E → S → Prop) (s : S) : sentence σ f vp s ≠ 0 ↔ ∃! x : E, f x (σ s)

The sentence presupposes exactly one satisfier at the situation its pronoun denotes. A free pronoun discharges the domain condition at its referent, whatever situation the proposition is applied to; a bound one carries it to the situation where the proposition is applied.

theorem Elbourne2013.sentence_eq_one_iff {S : Type u_1} {E : Type u_2} (σ : S → S) (f vp : E → S → Prop) {s : S} {x : E} (h : description σ f s = some x) : sentence σ f vp s = 1 ↔ vp x s

Where the description denotes, the sentence says of that individual what the predicate says of it; a referential description makes the proposition object-dependent, (12) of ch. 5.

Intensional operators: de re, de dicto, attributive de re (ch. 7)

noncomputable def Elbourne2013.box {S : Type u_1} (R : S → Set S) (p : S → SignType) : S → SignType

A universal intensional operator over an accessibility relation is the Weak Kleene universal over the accessible situations, defined where the proposition is defined throughout them and true where it is true throughout them, as in (12) and (14) of ch. 7.

Equations

• Elbourne2013.box R p s = Trivalent.forallWeak fun (w : ↑(R s)) => p ↑w

theorem Elbourne2013.box_ne_zero_iff {S : Type u_1} (R : S → Set S) (p : S → SignType) (s : S) : box R p s ≠ 0 ↔ ∀ w ∈ R s, p w ≠ 0

noncomputable def Elbourne2013.deDicto {S : Type u_1} {E : Type u_2} (R : S → Set S) (f vp : E → S → Prop) : S → SignType

De dicto, (11) of ch. 7, the situation pronoun is bound by ς immediately below the operator.

Equations

• Elbourne2013.deDicto R f vp = Elbourne2013.box R (Elbourne2013.sentence id f vp)

noncomputable def Elbourne2013.deRe {S : Type u_1} {E : Type u_2} (R : S → Set S) (w₀ : S) (f vp : E → S → Prop) : S → SignType

De re, (13) of ch. 7, the situation pronoun inside the operator refers to the actual world w₀.

Equations

• Elbourne2013.deRe R w₀ f vp = Elbourne2013.box R (Elbourne2013.sentence (fun (x : S) => w₀) f vp)

noncomputable def Elbourne2013.attributiveDeRe {S : Type u_1} {E : Type u_2} (R : S → Set S) (f vp : E → S → Prop) : S → SignType

Attributive de re, (17) and (25) of ch. 7, the pronoun is bound above the operator, so the description is evaluated at the topic situation and only the predicate is modalized.

Equations

• Elbourne2013.attributiveDeRe R f vp = Presupposition.presupOfReferent (Elbourne2013.the f) fun (x : E) (s : S) => ∀ w ∈ R s, vp x w

theorem Elbourne2013.deDicto_ne_zero_iff {S : Type u_1} {E : Type u_2} (R : S → Set S) (f vp : E → S → Prop) (s : S) : deDicto R f vp s ≠ 0 ↔ ∀ w ∈ R s, ∃! x : E, f x w

De dicto, every accessible situation must contain exactly one satisfier, and the satisfiers may differ.

theorem Elbourne2013.deRe_ne_zero_iff {S : Type u_1} {E : Type u_2} (R : S → Set S) (w₀ : S) (f vp : E → S → Prop) (s : S) : deRe R w₀ f vp s ≠ 0 ↔ ∀ w ∈ R s, ∃! x : E, f x w₀

De re, the satisfier is fixed in the actual world, and need not satisfy the property in the accessible situations.

theorem Elbourne2013.attributiveDeRe_ne_zero_iff {S : Type u_1} {E : Type u_2} (R : S → Set S) (f vp : E → S → Prop) (s : S) : attributiveDeRe R f vp s ≠ 0 ↔ ∃! x : E, f x s

Attributive de re presupposes exactly one satisfier in the topic situation.

theorem Elbourne2013.attributiveDeRe_eq_one_iff {S : Type u_1} {E : Type u_2} (R : S → Set S) (f vp : E → S → Prop) {s : S} {x : E} (h : the f s = some x) : attributiveDeRe R f vp s = 1 ↔ ∀ w ∈ R s, vp x w

Kripke's number of the planets, (16) of ch. 7, is attributive, since the speaker need not know which number, yet de re, since the number in the topic situation is what is odd in every accessible world.

Existence entailments (ch. 8)

noncomputable def Elbourne2013.attitude {S : Type u_1} (dox R : S → Set S) (p : S → SignType) : S → SignType

An attitude verb with [Kar74a]'s projection (§8.6) is defined where the complement is defined throughout the subject's doxastic alternatives, and true where the complement is true throughout the verb's own alternatives, doxastic for believe and bouletic for want.

Equations

• Elbourne2013.attitude dox R p = {s : S | ∀ w ∈ dox s, p w ≠ 0}.indicator fun (s : S) => SignType.ofProp (∀ w ∈ R s, p w = 1)

theorem Elbourne2013.attitude_ne_zero_iff {S : Type u_1} {E : Type u_2} (dox R : S → Set S) (f vp : E → S → Prop) (s : S) : attitude dox R (sentence id f vp) s ≠ 0 ↔ ∀ w ∈ dox s, ∃! x : E, f x w

Hans wants the ghost in his attic to be quiet, (40)–(41) of ch. 8, presupposes that Hans believes there is exactly one ghost in his attic.

theorem Elbourne2013.attitude_eq_zero_of_agnostic {S : Type u_1} {E : Type u_2} (dox R : S → Set S) (f vp : E → S → Prop) {s : S} (h : ∃ w ∈ dox s, ¬∃ (x : E), f x w) : attitude dox R (sentence id f vp) s = 0

A subject unsure whether there is a ghost in his attic cannot felicitously want the ghost in his attic to be quiet, (31) with (33b), since the presupposition attributes the belief to him.

def Elbourne2013.russellian {S : Type u_1} {E : Type u_2} (R : S → Set S) (f vp : E → S → Prop) (s : S) : Prop

The Russellian paraphrase (33a) asserts existence and uniqueness inside the attitude.

Equations

• Elbourne2013.russellian R f vp s = ∀ w ∈ R s, ∃ (x : E), f x w ∧ (∀ (y : E), f y w → y = x) ∧ vp x w

theorem Elbourne2013.conditional_ne_zero_iff {S : Type u_1} {E : Type u_2} (f vp : E → S → Prop) (q : S → SignType) (s : S) : (-sentence id f vp s).joinWeak (q s) ≠ 0 ↔ (∃! x : E, f x s) ∧ q s ≠ 0

The antecedent of a conditional is a hole, (39) of ch. 8, so the existence presupposition of the description projects to the whole conditional, here the Weak Kleene material conditional.

theorem Elbourne2013.russellian_consistent : ∃ (dox : Bool → Set Bool) (R : Bool → Set Bool) (f : Unit → Bool → Prop) (vp : Unit → Bool → Prop), (∃ w ∈ dox true, ¬∃ (x : Unit), f x w) ∧ russellian R f vp true

The Russellian paraphrase is consistent with agnosticism, (31) with (33a), since the existence claim sits inside the bouletic alternatives. The witness has two situations, one without a ghost that the subject leaves open and one with a quiet ghost that he wants.

theorem Elbourne2013.attitude_ne_zero_not_speaker : ∃ (dox : Bool → Set Bool) (R : Bool → Set Bool) (f : Unit → Bool → Prop) (vp : Unit → Bool → Prop) (s : Bool), attitude dox R (sentence id f vp) s ≠ 0 ∧ ¬∃ (x : Unit), f x s

Under an attitude verb the description commits the subject, not the speaker, to a fountain of youth, (36) of ch. 8. The presupposition holds although there is none in the topic situation.

The village: situations as sets of facts (ch. 6, ch. 9)

inductive Elbourne2013.Fact (E : Type u_1) : Type u_1

The atomic facts of a village are [Kra89]'s states of affairs, thin particulars instantiating properties and relations.

• farmer {E : Type u_1} (x : E) : Fact E
• donkey {E : Type u_1} (x : E) : Fact E
• priest {E : Type u_1} (x : E) : Fact E
• table {E : Type u_1} (x : E) : Fact E
• covered {E : Type u_1} (x : E) : Fact E
• owns {E : Type u_1} (x y : E) : Fact E
• beats {E : Type u_1} (x y : E) : Fact E

def Elbourne2013.instDecidableEqFact.decEq {E✝ : Type u_1} [DecidableEq E✝] (x✝ x✝¹ : Fact E✝) : Decidable (x✝ = x✝¹)

Equations

• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.farmer a) (Elbourne2013.Fact.farmer b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.farmer x_2) (Elbourne2013.Fact.donkey x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.farmer x_2) (Elbourne2013.Fact.priest x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.farmer x_2) (Elbourne2013.Fact.table x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.farmer x_2) (Elbourne2013.Fact.covered x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.farmer x_2) (Elbourne2013.Fact.owns x_3 y) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.farmer x_2) (Elbourne2013.Fact.beats x_3 y) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.donkey x_2) (Elbourne2013.Fact.farmer x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.donkey a) (Elbourne2013.Fact.donkey b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.donkey x_2) (Elbourne2013.Fact.priest x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.donkey x_2) (Elbourne2013.Fact.table x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.donkey x_2) (Elbourne2013.Fact.covered x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.donkey x_2) (Elbourne2013.Fact.owns x_3 y) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.donkey x_2) (Elbourne2013.Fact.beats x_3 y) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.priest x_2) (Elbourne2013.Fact.farmer x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.priest x_2) (Elbourne2013.Fact.donkey x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.priest a) (Elbourne2013.Fact.priest b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.priest x_2) (Elbourne2013.Fact.table x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.priest x_2) (Elbourne2013.Fact.covered x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.priest x_2) (Elbourne2013.Fact.owns x_3 y) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.priest x_2) (Elbourne2013.Fact.beats x_3 y) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.table x_2) (Elbourne2013.Fact.farmer x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.table x_2) (Elbourne2013.Fact.donkey x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.table x_2) (Elbourne2013.Fact.priest x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.table a) (Elbourne2013.Fact.table b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.table x_2) (Elbourne2013.Fact.covered x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.table x_2) (Elbourne2013.Fact.owns x_3 y) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.table x_2) (Elbourne2013.Fact.beats x_3 y) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.covered x_2) (Elbourne2013.Fact.farmer x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.covered x_2) (Elbourne2013.Fact.donkey x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.covered x_2) (Elbourne2013.Fact.priest x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.covered x_2) (Elbourne2013.Fact.table x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.covered a) (Elbourne2013.Fact.covered b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.covered x_2) (Elbourne2013.Fact.owns x_3 y) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.covered x_2) (Elbourne2013.Fact.beats x_3 y) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.owns x_2 y) (Elbourne2013.Fact.farmer x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.owns x_2 y) (Elbourne2013.Fact.donkey x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.owns x_2 y) (Elbourne2013.Fact.priest x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.owns x_2 y) (Elbourne2013.Fact.table x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.owns x_2 y) (Elbourne2013.Fact.covered x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.owns a a_1) (Elbourne2013.Fact.owns b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.owns x_2 y) (Elbourne2013.Fact.beats x_3 y_1) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.beats x_2 y) (Elbourne2013.Fact.farmer x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.beats x_2 y) (Elbourne2013.Fact.donkey x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.beats x_2 y) (Elbourne2013.Fact.priest x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.beats x_2 y) (Elbourne2013.Fact.table x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.beats x_2 y) (Elbourne2013.Fact.covered x_3) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.beats x_2 y) (Elbourne2013.Fact.owns x_3 y_1) = isFalse ⋯
• Elbourne2013.instDecidableEqFact.decEq (Elbourne2013.Fact.beats a a_1) (Elbourne2013.Fact.beats b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Elbourne2013.instDecidableEqFact {E✝ : Type u_1} [DecidableEq E✝] : DecidableEq (Fact E✝)

Equations

• Elbourne2013.instDecidableEqFact = Elbourne2013.instDecidableEqFact.decEq

@[reducible, inline]

abbrev Elbourne2013.Village (E : Type u_1) : Type u_1

A situation is a finite set of facts, parthood is inclusion, and a world is the set of all the facts that hold in it.

Equations

• Elbourne2013.Village E = Finset (Elbourne2013.Fact E)

theorem Elbourne2013.exists_minimal_singleton_iff {E : Type u_1} {t u : Village E} (φ : Fact E) (g : Village E → Prop) : (∃ (s : Village E), Minimal (fun (s : Village E) => s ⊆ t ∧ s ⊆ u ∧ φ ∈ s) s ∧ g s) ↔ φ ∈ t ∧ φ ∈ u ∧ g {φ}

The minimal situations containing a fact within two bounds are the singleton.

theorem Elbourne2013.Q_subset_iff {E : Type u_1} [DecidableEq E] (Φ : E → Village E) (x : E) (s s' : Village E) : Q (fun (x : E) (s'' : Village E) => Φ x ⊆ s'') x s s' ↔ s' ⊆ s ∧ Φ x ⊆ s

An extended situation for a set of facts exists exactly when s' is part of s and the facts hold in s.

theorem Elbourne2013.Q_mem_iff {E : Type u_1} [DecidableEq E] (φ : E → Fact E) (x : E) (s s' : Village E) : Q (fun (x : E) (s'' : Village E) => φ x ∈ s'') x s s' ↔ s' ⊆ s ∧ φ x ∈ s

An extended situation for a single fact exists exactly when s' is part of s and the fact holds in s.

def Elbourne2013.ownsADonkey {E : Type u_1} (s₀ : Village E) (x : E) (s' : Village E) : Prop

man who owns a donkey is the restrictor of (4) in ch. 6, with a and Q inside the relative clause.

Equations

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

theorem Elbourne2013.ownsADonkey_iff {E : Type u_1} [DecidableEq E] (s₀ : Village E) (x : E) {s' : Village E} (h : s' ⊆ s₀) : ownsADonkey s₀ x s' ↔ Fact.farmer x ∈ s' ∧ ∃ (y : E), Fact.donkey y ∈ s' ∧ Fact.owns x y ∈ s'

The relative clause unfolds to facts in the situation.

theorem Elbourne2013.minimal_ownsADonkey_iff {E : Type u_1} [DecidableEq E] (w : Village E) (x : E) (s' : Village E) : Minimal (fun (s' : Village E) => s' ⊆ w ∧ s' ⊆ w ∧ ownsADonkey w x s') s' ↔ ∃ (y : E), Fact.farmer x ∈ w ∧ Fact.donkey y ∈ w ∧ Fact.owns x y ∈ w ∧ s' = {Fact.farmer x, Fact.donkey y, Fact.owns x y}

Within the world there is one minimal situation of a farmer owning a donkey per owned donkey, consisting of the farmer, the donkey and the owning.

theorem Elbourne2013.the_donkey_minimal {E : Type u_1} [DecidableEq E] (x y : E) : the (fun (z : E) (s : Village E) => Fact.donkey z ∈ s) {Fact.farmer x, Fact.donkey y, Fact.owns x y} = some y

In the minimal situation of a farmer owning a donkey, the donkey denotes that donkey, unique by minimality.

theorem Elbourne2013.existsUnique_donkey_of_minimal {E : Type u_1} [DecidableEq E] (w : Village E) (x : E) {s' : Village E} (hs : Minimal (fun (s' : Village E) => s' ⊆ w ∧ s' ⊆ w ∧ ownsADonkey w x s') s') : ∃! z : E, Fact.donkey z ∈ s'

The domain condition of the donkey-anaphoric description is met by minimality, since every minimal situation of a farmer owning a donkey contains exactly one donkey, §6.2.

noncomputable def Elbourne2013.beatsTheDonkey {E : Type u_1} (x : E) (s s' : Village E) : Prop

The nuclear scope of (4) in ch. 6 is σ₃ [Q [beats [the donkey s₃]]]. Situation Binding III binds the description to the restrictor's minimal situation s', and Q extends s' to a situation in which the beating holds.

Equations

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

noncomputable def Elbourne2013.everyOwnerBeatsTheDonkey {E : Type u_1} (s₀ s : Village E) : Prop

This is (3) of ch. 6, every man who owns a donkey beats the donkey, with the LF (4).

Equations

• Elbourne2013.everyOwnerBeatsTheDonkey s₀ s = Elbourne2013.every s₀ (Elbourne2013.ownsADonkey s₀) Elbourne2013.beatsTheDonkey s

noncomputable def Elbourne2013.everyOwnerBeatsIt {E : Type u_1} (s₀ s : Village E) : Prop

In (10a) of ch. 10, every man who owns a donkey beats it, the pronoun with its deleted noun phrase stands in place of the description.

Equations

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

theorem Elbourne2013.everyOwnerBeatsTheDonkey_iff {E : Type u_1} [DecidableEq E] (w : Village E) : everyOwnerBeatsTheDonkey w w ↔ ∀ (x y : E), Fact.farmer x ∈ w → Fact.donkey y ∈ w → Fact.owns x y ∈ w → Fact.beats x y ∈ w

On the neat semantics for donkey sentences (§6.2), the sentence is true in the village world iff every farmer beats every donkey he owns. The bound description picks out the unique donkey of each minimal owning situation, so the reading is the strong one.

theorem Elbourne2013.everyOwnerBeatsIt_iff {E : Type u_1} [DecidableEq E] (w : Village E) : everyOwnerBeatsIt w w ↔ ∀ (x y : E), Fact.farmer x ∈ w → Fact.donkey y ∈ w → Fact.owns x y ∈ w → Fact.beats x y ∈ w

The pronoun sentence has the same meaning, being the same LF up to the null noun phrase.

Incompleteness and the argument from sloppy identity (ch. 9)

def Elbourne2013.room : Village Bool

The room of (4) in ch. 9 has one table, covered with books.

Equations

• Elbourne2013.room = {Elbourne2013.Fact.table true, Elbourne2013.Fact.covered true}

def Elbourne2013.world : Village Bool

The world contains the room and a second table.

Equations

• Elbourne2013.world = {Elbourne2013.Fact.table true, Elbourne2013.Fact.table false, Elbourne2013.Fact.covered true}

theorem Elbourne2013.room_le_world : room ⊆ world

theorem Elbourne2013.incomplete_description : sentence (fun (x : Village Bool) => room) (fun (x : Bool) (s : Village Bool) => Fact.table x ∈ s) (fun (x : Bool) (s : Village Bool) => Fact.covered x ∈ s) world ≠ 0 ∧ ¬∃! x : Bool, Fact.table x ∈ world

Incompleteness, (4) of ch. 9, arises when the table is covered with books is said in a room with one table. The referential situation pronoun to the room satisfies the domain condition although the world contains two tables.

noncomputable def Elbourne2013.relDescription {E : Type u_1} {S : Type u_2} (rel : E → E → S → Prop) (np : E → S → Prop) (v : E) (s : S) : Option E

A relation-variable description the [f v] NP, §9.2.1, denotes the unique NP-satisfier standing in the covert relation to the individual variable v, which a higher quantifier may bind.

Equations

• Elbourne2013.relDescription rel np v s = Reference.iota fun (x : E) => np x s ∧ rel x v s

theorem Elbourne2013.relDescription_eq_some_iff {E : Type u_1} {S : Type u_2} (rel : E → E → S → Prop) (np : E → S → Prop) (v : E) (s : S) (x : E) : relDescription rel np v s = some x ↔ (np x s ∧ rel x v s) ∧ ∀ (y : E), np y s → rel y v s → y = x

The relation-variable description covaries with its individual variable. Read as the donkey v owns, the donkey denotes each owner's own donkey, which licenses the sloppy reading of (17b) in ch. 9 and would wrongly license one for (17a).

noncomputable def Elbourne2013.everyOwnerBeatsTheDonkeyAndThePriestToo {E : Type u_1} (s₀ s : Village E) : Prop

In (29) of ch. 9, every farmer who owns a donkey beats the donkey, and the priest beats the donkey too, with the LF (31), the quantifier scopes over the conjunction, and both occurrences of the donkey are bound by σ to the same minimal situation.

Equations

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

theorem Elbourne2013.everyOwnerBeatsTheDonkeyAndThePriestToo_iff {E : Type u_1} [DecidableEq E] (w : Village E) {p : E} (hp : the (fun (p : E) (s : Village E) => Fact.priest p ∈ s) w = some p) : everyOwnerBeatsTheDonkeyAndThePriestToo w w ↔ ∀ (x y : E), Fact.farmer x ∈ w → Fact.donkey y ∈ w → Fact.owns x y ∈ w → Fact.beats x y ∈ w ∧ Fact.beats p y ∈ w

On the strict reading, (32) of ch. 9, the priest beats each farmer's donkey. A sloppy reading, on which the priest beats his own donkey, would need the description to depend on an individual variable, which the situation-variable description lacks.