Maximality and Coppock–Beaver Factorization

[Sha80] [Kri15b] [CB15] [Rus05]

Predicate operators consumed by the Description interpretation function in Semantics/Definiteness/Interpret.lean. They operate over entity predicates E → Prop — the extensional fragment of Intensional.Denot E W .et. At type .et a denotation reduces to E → Prop with no occurrence of the situation type W, so these world-blind operators do not bind it: they apply to any IL denotation of type .et by defeq, with E inferred from the predicate's domain.

What this module provides

• Coppock–Beaver factorization ([CB15]): the Russellian iota is split into two independent predicates over restrictors — Existence (∃x. P x) and Uniqueness (∀ x y. P x → P y → x = y). The classical Russellian condition existsUnique is the conjunction.

• Sharvy maximality ([Sha80]): the maximal P-satisfier under a partial order on E. For singular count nouns this collapses to Russellian iota; for plurals (with a join-semilattice on entities) it returns the join of all satisfiers. We supply both:

  • russellIota — order-free unique-element selector
  • sharvyMax — preorder-relative maximal-element selector

• Križ homogeneity ([Kri15b]): the predicate homogeneous P S holds when the scope predicate is either uniformly true or uniformly false on the satisfiers of P. Required for the [Kri15b] semantics of plural definites, where "the boys are tall" presupposes homogeneity rather than universality.

Design notes

• No semantic interpretation here. This file provides only the operators. Semantics/Definiteness/Interpret.lean wires Description constructors to them.

• Ord-free vs. order-relative. russellIota uses only Eq; sharvyMax requires PartialOrder E. This is the [Sha80] / [Lin83] split: singular definites work over flat individuals, plural definites need the join-semilattice from mereology ([Lin83]).

• Option is the right return type. A definite description with an unsatisfied uniqueness presupposition has no referent; rather than throw an exception or produce an arbitrary witness, we return none. The interpretation function in Semantics/Definiteness/Interpret.lean lifts this to presupposition failure at the propositional level.

Coppock–Beaver factorization

def Semantics.Definiteness.Existence {E : Type u_1} (P : E → Prop) : Prop

[CB15]'s Existence component. Asserted, not presupposed, in their factorization of the Russellian iota.

Equations

• Semantics.Definiteness.Existence P = ∃ (x : E), P x

def Semantics.Definiteness.Uniqueness {E : Type u_1} (P : E → Prop) : Prop

[CB15]'s Uniqueness component. Presupposed (rather than asserted) on their account; this is the projection contrast that distinguishes "the King of France isn't bald" (uniqueness presupposed) from a plain Russellian negation (uniqueness in scope of negation).

Equations

• Semantics.Definiteness.Uniqueness P = ∀ (x y : E), P x → P y → x = y

theorem Semantics.Definiteness.existsUnique_iff_existence_and_uniqueness {E : Type u_1} (P : E → Prop) : (∃! x : E, P x) ↔ Existence P ∧ Uniqueness P

The Russellian condition ∃! x, P x factors into Coppock–Beaver's two components: Existence (asserted) and Uniqueness (presupposed). A genuine iff, not rfl — mathlib's ∃! bundles the components under one existential, CB splits them. Uniqueness is mathlib ∃! everywhere in this subsystem (there is no separate existsUnique def); this theorem is the bridge to the CB components, and Relational.iotaPresupposition is ∃! by abbrev.

theorem Semantics.Definiteness.uniqueness_does_not_imply_existence {E : Type u_1} : (Uniqueness fun (x : E) => False) ∧ ¬Existence fun (x : E) => False

Existence and Uniqueness are logically independent. The empty predicate λ _ => False satisfies Uniqueness (vacuously) but not Existence — [CB15]'s key motivating data.

Russellian iota (order-free)

noncomputable def Semantics.Definiteness.russellIota {E : Type u_1} (P : E → Prop) : Option E

The order-free unique-element selector: returns the witness when there is exactly one P-satisfier. Order-free version usable when no preorder is declared on E.

Equations

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

theorem Semantics.Definiteness.russellIota_isSome_iff_exists_unique {E : Type u_1} (P : E → Prop) : (russellIota P).isSome = true ↔ ∃! x : E, P x

russellIota returns some exactly when mathlib's ∃! holds.

theorem Semantics.Definiteness.russellIota_witness_satisfies {E : Type u_1} (P : E → Prop) (e : E) (h : russellIota P = some e) : P e

The witness returned by russellIota satisfies the predicate.

theorem Semantics.Definiteness.russellIota_witness_unique {E : Type u_1} (P : E → Prop) (e₁ e₂ : E) (h₁ : russellIota P = some e₁) (h₂ : russellIota P = some e₂) : e₁ = e₂

Two witnesses returned by russellIota (over the same predicate) must coincide. By Uniqueness.

def Semantics.Definiteness.russellIotaList {E : Type u_1} (domain : List E) (P : E → Bool) : Option E

Computable list-based Russellian iota: returns the unique witness when domain.filter P is a singleton, none otherwise. This is the concrete operational counterpart to russellIota and the canonical referent selector used by Semantics.Presupposition.presupOfReferent.

Equations

• Semantics.Definiteness.russellIotaList domain P = match List.filter P domain with | [e] => some e | x => none

theorem Semantics.Definiteness.russellIotaList_eq_some_iff {E : Type u_1} (domain : List E) (P : E → Bool) (e : E) : russellIotaList domain P = some e ↔ List.filter P domain = [e]

russellIotaList returns some e iff domain.filter P is the singleton [e]. By definition, modulo the match reduction.

Sharvy maximality (preorder-relative)

def Semantics.Definiteness.IsMaximal {E : Type u_1} [LE E] (P : E → Prop) (e : E) : Prop

[Sha80]: an entity e is maximal among the P-satisfiers when e satisfies P and dominates every other P-satisfier under ≤. For singular count nouns the order is flat (only e ≤ e) so maximality coincides with Russellian uniqueness; for plurals (with [Lin83]'s join semilattice) maximality returns the sum of all atoms.

Equations

• Semantics.Definiteness.IsMaximal P e = (P e ∧ ∀ (x : E), P x → x ≤ e)

theorem Semantics.Definiteness.isMaximal_unique {E : Type u_1} [PartialOrder E] (P : E → Prop) (e₁ e₂ : E) (h₁ : IsMaximal P e₁) (h₂ : IsMaximal P e₂) : e₁ = e₂

Sharvy maximality is unique: at most one entity is IsMaximal P under a partial order. Antisymmetry collapses two maxima into one.

noncomputable def Semantics.Definiteness.sharvyMax {E : Type u_1} [PartialOrder E] (P : E → Prop) : Option E

The Sharvy maximal-element selector. Returns the unique maximal P-satisfier when one exists; none otherwise (no satisfier, or no upper bound among the satisfiers).

Equations

• Semantics.Definiteness.sharvyMax P = if h : ∃ (e : E), Semantics.Definiteness.IsMaximal P e then some h.choose else none

theorem Semantics.Definiteness.sharvyMax_isSome_iff_isMaximal {E : Type u_1} [PartialOrder E] (P : E → Prop) : (sharvyMax P).isSome = true ↔ ∃ (e : E), IsMaximal P e

sharvyMax returns some exactly when a maximal P-satisfier exists.

theorem Semantics.Definiteness.sharvyMax_witness_isMaximal {E : Type u_1} [PartialOrder E] (P : E → Prop) (e : E) (h : sharvyMax P = some e) : IsMaximal P e

The witness returned by sharvyMax is maximal.

theorem Semantics.Definiteness.sharvyMax_witness_satisfies {E : Type u_1} [PartialOrder E] (P : E → Prop) (e : E) (h : sharvyMax P = some e) : P e

The witness returned by sharvyMax satisfies P.

Križ homogeneity

def Semantics.Definiteness.Homogeneous {E : Type u_1} (P S : E → Prop) : Prop

[Kri15b]: a scope predicate S is homogeneous on the P-satisfiers when it holds either of all of them or of none of them. This is what licenses "the boys are tall" — Križ argues uniformity is presupposed, so partial-truth cases (some boys tall, others not) yield presupposition failure rather than False.

Equations

• Semantics.Definiteness.Homogeneous P S = ((∀ (x : E), P x → S x) ∨ ∀ (x : E), P x → ¬S x)

theorem Semantics.Definiteness.homogeneous_symmetric_in_truth_value {E : Type u_1} (P S : E → Prop) : Homogeneous P S ↔ (∀ (x : E), P x → S x) ∨ ∀ (x : E), P x → ¬S x

Homogeneity is symmetric in its two failure modes (uniformly-S vs uniformly-¬S). Both yield well-defined truth values; only the split case is presupposition failure. By definition.

theorem Semantics.Definiteness.uniqueness_implies_homogeneous_classical {E : Type u_1} (P S : E → Prop) (hU : Uniqueness P) : Homogeneous P S

Russellian uniqueness implies Križ homogeneity (vacuously beyond the unique witness): if there is exactly one P-satisfier, then any S is trivially uniform on the (singleton) extension of P.