Distinguishing descriptions

A description distinguishes its referent from a contrast set when its compatibility with the referent strictly exceeds its compatibility with every distractor, compatibility taking values in a preorder. At truth values this is the distinguishing description of Dale and Reiter, which holds of the referent and of no distractor, and the Russellian uniqueness of Reference.iota over the domain the contrast set restricts. Under a graded semantics it says the referent is the literal listener's best guess, since a strictly monotone rescaling of compatibility such as the listener's normalization does not change it (Reference.distinguishes_comp_iff). A graded description distinguishes exactly when some level set of its compatibility does, so the truth-valued notion is the general one at a threshold.

Main definitions

• Reference.Distinguishes compat C r d: the compatibility of d with r strictly exceeds its compatibility with every member of C.

Main results

• distinguishes_prop_iff: at truth values, d holds of r and of no distractor.
• distinguishes_iff_iota, distinguishes_univ_erase_iff: identification is the definite's uniqueness on the domain, and r is the whole extension against everything else.
• distinguishes_comp_iff: invariance under strictly monotone rescaling of compatibility.
• distinguishes_iff_exists_threshold: a graded compatibility distinguishes exactly when some threshold of it does.

References

• [DR95]
• [Gri75]
• [EBF06]
• [DHG+20]

def Reference.Distinguishes {D : Type u_1} {E : Type u_2} {α : Type u_3} [Preorder α] (compat : D → E → α) (C : Finset E) (r : E) (d : D) : Prop

The compatibility of the description d with the referent r strictly exceeds its compatibility with every member of the contrast set C.

Equations

• Reference.Distinguishes compat C r d = ∀ c ∈ C, compat d c < compat d r

@[instance_reducible]

instance Reference.instDecidableDistinguishesOfDecidableLT {D : Type u_1} {E : Type u_2} {α : Type u_3} [Preorder α] (compat : D → E → α) (C : Finset E) (r : E) (d : D) [DecidableLT α] : Decidable (Distinguishes compat C r d)

Equations

• Reference.instDecidableDistinguishesOfDecidableLT compat C r d = id inferInstance

theorem Reference.Distinguishes.anti {D : Type u_1} {E : Type u_2} {α : Type u_3} [Preorder α] {compat : D → E → α} {C : Finset E} {r : E} {d : D} (h : Distinguishes compat C r d) {C' : Finset E} (hC : C' ⊆ C) : Distinguishes compat C' r d

A distinguishing description distinguishes against any smaller contrast set.

theorem Reference.distinguishes_comp_iff {D : Type u_1} {E : Type u_2} {α : Type u_3} {β : Type u_4} [LinearOrder α] {compat : D → E → α} {C : Finset E} {r : E} {d : D} [Preorder β] {compat' : D → E → β} {φ : α → β} {s : Set α} (hφ : StrictMonoOn φ s) (hs : ∀ (x : E), compat d x ∈ s) (h : ∀ (x : E), compat' d x = φ (compat d x)) : Distinguishes compat' C r d ↔ Distinguishes compat C r d

A rescaling of a description's compatibility that is strictly monotone on the values the description takes, such as the literal listener's normalization of a nonnegative meaning, preserves distinguishing.

theorem Reference.distinguishes_iff_exists_threshold {D : Type u_1} {E : Type u_2} {α : Type u_3} [LinearOrder α] {compat : D → E → α} {C : Finset E} {r : E} {d : D} : Distinguishes compat C r d ↔ ∃ (t : α), Distinguishes (fun (d : D) (x : E) => t ≤ compat d x) C r d

A graded compatibility distinguishes exactly when some threshold of it does, and the referent's own compatibility is such a threshold.

Truth-valued compatibility

@[instance_reducible]

instance Reference.instDecidableDistinguishes {D : Type u_1} {E : Type u_2} (compat : D → E → Prop) (C : Finset E) (r : E) (d : D) [(d : D) → (x : E) → Decidable (compat d x)] : Decidable (Distinguishes compat C r d)

Equations

• Reference.instDecidableDistinguishes compat C r d = id inferInstance

theorem Reference.distinguishes_prop_iff {D : Type u_1} {E : Type u_2} {compat : D → E → Prop} {C : Finset E} {r : E} {d : D} (hC : C.Nonempty) : Distinguishes compat C r d ↔ compat d r ∧ ∀ c ∈ C, ¬compat d c

At truth values, a description distinguishes r from a nonempty contrast set exactly when it holds of r and of no distractor.

theorem Reference.distinguishes_iff_iota {D : Type u_1} {E : Type u_2} {compat : D → E → Prop} {C : Finset E} {r : E} {d : D} [DecidableEq E] (hC : C.Nonempty) (hr : r ∉ C) : Distinguishes compat C r d ↔ (iota fun (x : E) => compat d x ∧ x ∈ insert r C) = some r

Identification against a nonempty contrast set that excludes the referent is the Russellian uniqueness of the description on the domain insert r C.

theorem Reference.distinguishes_univ_erase_iff {D : Type u_1} {E : Type u_2} {compat : D → E → Prop} {r : E} {d : D} [Fintype E] [DecidableEq E] [Nontrivial E] : Distinguishes compat (Finset.univ.erase r) r d ↔ {x : E | compat d x} = {r}

Against every other individual of a finite domain with at least two, a description distinguishes r exactly when r is its whole extension.