Iota

The iota operator takes a predicate to the individual it describes, when there is one: iota P is the unique satisfier of P, and none when P has no satisfier or several. Its definedness is unique existence, which splits into existence and uniqueness of the extension, the two components that Coppock and Beaver separate into an assertion and a presupposition. The determiner the asserts its scope of this referent.

Sharvy generalizes the definite article to individuals ordered by part-of, and Chierchia adopts the generalization: the definite picks out the largest member of a set, iota (IsGreatest X), since a set has at most one largest member. No atom is larger than another, so on a set of atoms the largest member exists only when there is exactly one member, while a finite nonempty set closed under sum always has one. Sending an individual to its parts, Set.Iic d, undoes the largest member.

Main definitions

• Reference.iota: the unique satisfier of a predicate, or none.

Main results

• iota_eq_some_iff, iota_isSome_iff, iota_eq_none_iff.
• existsUnique_iff_nonempty_subsingleton: ∃! is nonemptiness with subsingletonness.
• the_sem_iff_iota: the determiner the asserts its scope of the referent.
• iota_isGreatest_eq_some_iff: the largest member, Chierchia's (11a).
• IsAntichain.iota_isGreatest: on an antichain the largest member is the unique member, Chierchia's (11c), so an antichain with two members has none (IsAntichain.iota_isGreatest_eq_none).
• DirectedOn.iota_isGreatest_isSome: a finite nonempty directed set has a largest member.
• iota_isGreatest_elim_Iic, elim_Iic_iota_isGreatest: Chierchia's (17a) and (17b) at a single situation.

Implementation notes

A partial individual is an Option. Krifka, following Link, writes σ for the largest member and defines it as ιx[S(x) ∧ ∀x′[S(x′) → x′ ⊑ x]], which is iota (IsGreatest X). A kind in Chierchia's sense is a function S → Option E from situations to partial individuals. His ∩ is fun s ↦ iota (IsGreatest (P s)) where that is a kind, (16), and his ∪ is fun s ↦ (k s).elim ∅ Set.Iic, the ι and Id of his (25) applied at each situation (pp. 359–360). His (25e) prints Id(x) = λx[x ≤ y]; his footnote 14 shows that λy[y ≤ x] is meant.

References

• [Rus05]
• [CB15]
• [Par87]
• [Sha80]
• [Chi98]
• [Lin83]
• [Kri26]

theorem existsUnique_iff_nonempty_subsingleton {α : Type u_1} {p : α → Prop} : (∃! x : α, p x) ↔ {x : α | p x}.Nonempty ∧ {x : α | p x}.Subsingleton

Unique existence is nonemptiness together with subsingletonness of the extension.

noncomputable def Reference.iota {E : Type u_2} (P : E → Prop) : Option E

iota P is the unique satisfier of P, or none when P has no satisfier or several.

Equations

• Reference.iota P = if h : ∃! x : E, P x then some (Exists.choose h) else none

theorem Reference.iota_eq_some_iff {E : Type u_2} (P : E → Prop) {e : E} : iota P = some e ↔ P e ∧ ∀ (x : E), P x → x = e

theorem Reference.iota_isSome_iff {E : Type u_2} (P : E → Prop) : (iota P).isSome = true ↔ ∃! x : E, P x

theorem Reference.iota_eq_none_iff {E : Type u_2} (P : E → Prop) : iota P = none ↔ ¬∃! x : E, P x

The definite article

theorem Reference.iota_ident {E : Type u_2} (j : E) : iota (Quantifier.NP.ident j) = some j

The iota of Partee's singleton property ident j is j.

theorem Reference.the_sem_iff_iota {E : Type u_2} (P S : E → Prop) : Quantifier.GQ.the P S ↔ ∃ x ∈ iota P, S x

The determiner the asserts its scope of the Russellian referent.

Predicates with at most one satisfier

theorem Set.Subsingleton.iota_eq_some_iff {E : Type u_2} {P : E → Prop} {e : E} (h : {x : E | P x}.Subsingleton) : Reference.iota P = some e ↔ P e

theorem Set.Subsingleton.iota_isSome_iff {E : Type u_2} {P : E → Prop} (h : {x : E | P x}.Subsingleton) : (Reference.iota P).isSome = true ↔ ∃ (x : E), P x

The largest member

theorem Reference.iota_isGreatest_eq_some_iff {E : Type u_2} [PartialOrder E] {X : Set E} {d : E} : iota (IsGreatest X) = some d ↔ IsGreatest X d

theorem Reference.iota_isGreatest_isSome_iff {E : Type u_2} [PartialOrder E] {X : Set E} : (iota (IsGreatest X)).isSome = true ↔ ∃ (d : E), IsGreatest X d

theorem Reference.iota_isGreatest_eq_none_iff {E : Type u_2} [PartialOrder E] {X : Set E} : iota (IsGreatest X) = none ↔ ¬∃ (d : E), IsGreatest X d

theorem Reference.iota_isGreatest_Iic {E : Type u_2} [PartialOrder E] {d : E} : iota (IsGreatest (Set.Iic d)) = some d

theorem Reference.iota_isGreatest_empty {E : Type u_2} [PartialOrder E] : iota (IsGreatest ∅) = none

theorem Reference.iota_isGreatest_elim_Iic {E : Type u_2} [PartialOrder E] (o : Option E) : iota (IsGreatest (o.elim ∅ Set.Iic)) = o

The largest part of a partial individual is that individual.

theorem Reference.elim_Iic_iota_isGreatest {E : Type u_2} [PartialOrder E] {X : Set E} (hX : IsLowerSet X) (hd : X.Nonempty → ∃ (d : E), IsGreatest X d) : (iota (IsGreatest X)).elim ∅ Set.Iic = X

If X is closed downward and has a largest member wherever it is nonempty, then X is the set of parts of its largest member.

theorem IsAntichain.iota_isGreatest {E : Type u_2} [PartialOrder E] {X : Set E} (hs : IsAntichain (fun (x1 x2 : E) => x1 ≤ x2) X) : Reference.iota (IsGreatest X) = Reference.iota fun (x : E) => x ∈ X

On an antichain, such as a set of atoms, the largest member is the unique member.

theorem IsAntichain.iota_isGreatest_eq_none {E : Type u_2} [PartialOrder E] {X : Set E} (hs : IsAntichain (fun (x1 x2 : E) => x1 ≤ x2) X) {a b : E} (ha : a ∈ X) (hb : b ∈ X) (hab : a ≠ b) : Reference.iota (IsGreatest X) = none

An antichain with two members, such as a set of two atoms, has no largest member.

theorem DirectedOn.iota_isGreatest_isSome {E : Type u_2} [PartialOrder E] {X : Set E} (hs : DirectedOn (fun (x1 x2 : E) => x1 ≤ x2) X) (hfin : X.Finite) (hne : X.Nonempty) : (Reference.iota (IsGreatest X)).isSome = true

A finite nonempty directed set, such as a finite nonempty sup-closed set, has a largest member.