Maximality and Coppock–Beaver Factorization

@cite{sharvy-1980} @cite{kriz-2015} @cite{coppock-beaver-2015} @cite{russell-1905}

Predicate operators consumed by the NominalKind interpretation function in Core/Nominal/Interpret.lean. All operators live over Core.Logic.Intensional.Frame.Denot so they slot directly into the IL stack.

What this module provides

• Coppock–Beaver factorization (@cite{coppock-beaver-2015}): 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 (@cite{sharvy-1980}): the maximal P-satisfier under a partial order on F.Entity. 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 (@cite{kriz-2015}): 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 @cite{kriz-2015} 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. Core/Nominal/Interpret.lean wires NominalKind constructors to them.

• Ord-free vs. order-relative. russellIota uses only Eq; sharvyMax requires PartialOrder F.Entity. This is the @cite{sharvy-1980} / @cite{link-1983} split: singular definites work over flat individuals, plural definites need the join-semilattice from mereology (@cite{link-1983}).

• 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 Core/Nominal/Interpret.lean lifts this to presupposition failure at the propositional level.

def Core.Nominal.Existence {F : Logic.Intensional.Frame} (P : F.Denot Logic.Intensional.Ty.et) : Prop

@cite{coppock-beaver-2015}'s Existence component. Asserted, not presupposed, in their factorization of the Russellian iota.

Equations

• Core.Nominal.Existence P = ∃ (x : F.Entity), P x

def Core.Nominal.Uniqueness {F : Logic.Intensional.Frame} (P : F.Denot Logic.Intensional.Ty.et) : Prop

@cite{coppock-beaver-2015}'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

• Core.Nominal.Uniqueness P = ∀ (x y : F.Entity), P x → P y → x = y

def Core.Nominal.existsUnique {F : Logic.Intensional.Frame} (P : F.Denot Logic.Intensional.Ty.et) : Prop

The classical Russellian condition: ∃!x. P x. By construction the conjunction of @cite{coppock-beaver-2015}'s two components.

Equations

• Core.Nominal.existsUnique P = (Core.Nominal.Existence P ∧ Core.Nominal.Uniqueness P)

theorem Core.Nominal.existsUnique_iff_existence_and_uniqueness {F : Logic.Intensional.Frame} (P : F.Denot Logic.Intensional.Ty.et) : existsUnique P ↔ Existence P ∧ Uniqueness P

Russellian existence-and-uniqueness is exactly the conjunction of Coppock–Beaver Existence and Uniqueness. By definition.

theorem Core.Nominal.uniqueness_does_not_imply_existence {F : Logic.Intensional.Frame} : (Uniqueness fun (x : F.Denot Logic.Intensional.Ty.e) => False) ∧ ¬Existence fun (x : F.Denot Logic.Intensional.Ty.e) => False

Existence and Uniqueness are logically independent. The empty predicate λ _ => False satisfies Uniqueness (vacuously) but not Existence — @cite{coppock-beaver-2015}'s key motivating data.

noncomputable def Core.Nominal.russellIota {F : Logic.Intensional.Frame} (P : F.Denot Logic.Intensional.Ty.et) : Option F.Entity

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 F.Entity.

Equations

• Core.Nominal.russellIota P = if h : Core.Nominal.existsUnique P then some (Exists.choose ⋯) else none

theorem Core.Nominal.russellIota_isSome_iff_existsUnique {F : Logic.Intensional.Frame} (P : F.Denot Logic.Intensional.Ty.et) : (russellIota P).isSome = true ↔ existsUnique P

russellIota returns some exactly when Russellian existence-and- uniqueness holds.

theorem Core.Nominal.russellIota_witness_satisfies {F : Logic.Intensional.Frame} (P : F.Denot Logic.Intensional.Ty.et) (e : F.Entity) (h : russellIota P = some e) : P e

The witness returned by russellIota satisfies the predicate.

theorem Core.Nominal.russellIota_witness_unique {F : Logic.Intensional.Frame} (P : F.Denot Logic.Intensional.Ty.et) (e₁ e₂ : F.Entity) (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 Core.Nominal.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 Core.Presupposition.presupOfReferent.

Equations

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

theorem Core.Nominal.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.

def Core.Nominal.IsMaximal {F : Logic.Intensional.Frame} [LE F.Entity] (P : F.Denot Logic.Intensional.Ty.et) (e : F.Entity) : Prop

@cite{sharvy-1980}: 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 @cite{link-1983}'s join semilattice) maximality returns the sum of all atoms.

Equations

• Core.Nominal.IsMaximal P e = (P e ∧ ∀ (x : F.Entity), P x → x ≤ e)

theorem Core.Nominal.isMaximal_unique {F : Logic.Intensional.Frame} [PartialOrder F.Entity] (P : F.Denot Logic.Intensional.Ty.et) (e₁ e₂ : F.Entity) (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 Core.Nominal.sharvyMax {F : Logic.Intensional.Frame} [PartialOrder F.Entity] (P : F.Denot Logic.Intensional.Ty.et) : Option F.Entity

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

• Core.Nominal.sharvyMax P = if h : ∃ (e : F.Entity), Core.Nominal.IsMaximal P e then some h.choose else none

theorem Core.Nominal.sharvyMax_isSome_iff_isMaximal {F : Logic.Intensional.Frame} [PartialOrder F.Entity] (P : F.Denot Logic.Intensional.Ty.et) : (sharvyMax P).isSome = true ↔ ∃ (e : F.Entity), IsMaximal P e

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

theorem Core.Nominal.sharvyMax_witness_isMaximal {F : Logic.Intensional.Frame} [PartialOrder F.Entity] (P : F.Denot Logic.Intensional.Ty.et) (e : F.Entity) (h : sharvyMax P = some e) : IsMaximal P e

The witness returned by sharvyMax is maximal.

theorem Core.Nominal.sharvyMax_witness_satisfies {F : Logic.Intensional.Frame} [PartialOrder F.Entity] (P : F.Denot Logic.Intensional.Ty.et) (e : F.Entity) (h : sharvyMax P = some e) : P e

The witness returned by sharvyMax satisfies P.

def Core.Nominal.Homogeneous {F : Logic.Intensional.Frame} (P S : F.Denot Logic.Intensional.Ty.et) : Prop

@cite{kriz-2015}: 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

• Core.Nominal.Homogeneous P S = ((∀ (x : F.Denot Core.Logic.Intensional.Ty.e), P x → S x) ∨ ∀ (x : F.Denot Core.Logic.Intensional.Ty.e), P x → ¬S x)

theorem Core.Nominal.homogeneous_symmetric_in_truth_value {F : Logic.Intensional.Frame} (P S : F.Denot Logic.Intensional.Ty.et) : Homogeneous P S ↔ (∀ (x : F.Denot Logic.Intensional.Ty.e), P x → S x) ∨ ∀ (x : F.Denot Logic.Intensional.Ty.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 Core.Nominal.uniqueness_implies_homogeneous_classical {F : Logic.Intensional.Frame} (P S : F.Denot Logic.Intensional.Ty.et) (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.