Coppock & Beaver (2015): Definiteness and Determinacy

@cite{coppock-beaver-2015}

The central thesis of @cite{coppock-beaver-2015} is that the Russellian iota condition ∃!x. P x is not a primitive, but the conjunction of two logically independent components:

• Existence: ∃x. P x (asserted, scope-bearing)
• Uniqueness: ∀x y. P x → P y → x = y (presupposed, projects)

The empirical motivation is the projection contrast: under negation, "the King of France is bald" still presupposes that France has at most one king (Uniqueness), while leaving Existence in the scope of negation. The classical Russellian analysis collapses both into the assertion and loses this distinction.

What this file tests

The factorization is operationalized in Core.Nominal.Maximality as Existence, Uniqueness, and existsUnique over F.Denot .et. This study file builds three concrete restrictors over a tiny frame (sun / moon / mars; one index) and verifies:

1. Logical independence — Uniqueness can hold without Existence (the empty kingOfFrance extension), and Existence can hold without Uniqueness (the multi-witness planet extension).
2. Russellian collapse — existsUnique is true exactly for restrictors with a singleton extension (theSun).
3. Interpretation alignment — Core.Nominal.interpret on a .unique description returns none precisely in the Russellian failure cases (no extension, or non-unique extension).
4. Negation-projection contrast — the Uniqueness component projects through the assertion's polarity: ¬(the King of France is bald) still requires uniqueness of the King of France.

inductive Phenomena.Definiteness.Studies.CoppockBeaver2015.Body : Type

Three celestial bodies. sun is the unique satisfier of theSun; moon and mars jointly witness the multi-extension planet.

• sun : Body
• moon : Body
• mars : Body

@[implicit_reducible]

instance Phenomena.Definiteness.Studies.CoppockBeaver2015.instDecidableEqBody : DecidableEq Body

Equations

• Phenomena.Definiteness.Studies.CoppockBeaver2015.instDecidableEqBody x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Definiteness.Studies.CoppockBeaver2015.instReprBody : Repr Body

Equations

• Phenomena.Definiteness.Studies.CoppockBeaver2015.instReprBody = { reprPrec := Phenomena.Definiteness.Studies.CoppockBeaver2015.instReprBody.repr }

def Phenomena.Definiteness.Studies.CoppockBeaver2015.instReprBody.repr : Body → ℕ → Std.Format

Equations

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

def Phenomena.Definiteness.Studies.CoppockBeaver2015.F : Core.Logic.Intensional.Frame

One index suffices: the diagnostics are about predicate extensions, not about world-variability.

Equations

• Phenomena.Definiteness.Studies.CoppockBeaver2015.F = { Entity := Phenomena.Definiteness.Studies.CoppockBeaver2015.Body, Index := Unit }

def Phenomena.Definiteness.Studies.CoppockBeaver2015.theSun : F.Denot Core.Logic.Intensional.Ty.et

Singleton restrictor: theSun holds of exactly one entity.

Equations

• Phenomena.Definiteness.Studies.CoppockBeaver2015.theSun Phenomena.Definiteness.Studies.CoppockBeaver2015.Body.sun = True
• Phenomena.Definiteness.Studies.CoppockBeaver2015.theSun x✝ = False

def Phenomena.Definiteness.Studies.CoppockBeaver2015.planet : F.Denot Core.Logic.Intensional.Ty.et

Multi-witness restrictor: planet holds of two entities.

Equations

• Phenomena.Definiteness.Studies.CoppockBeaver2015.planet Phenomena.Definiteness.Studies.CoppockBeaver2015.Body.moon = True
• Phenomena.Definiteness.Studies.CoppockBeaver2015.planet Phenomena.Definiteness.Studies.CoppockBeaver2015.Body.mars = True
• Phenomena.Definiteness.Studies.CoppockBeaver2015.planet x✝ = False

def Phenomena.Definiteness.Studies.CoppockBeaver2015.kingOfFrance : F.Denot Core.Logic.Intensional.Ty.et

Empty restrictor: kingOfFrance has no satisfier. The @cite{coppock-beaver-2015} motivating case.

Equations

• Phenomena.Definiteness.Studies.CoppockBeaver2015.kingOfFrance x✝ = False

theorem Phenomena.Definiteness.Studies.CoppockBeaver2015.kingOfFrance_uniqueness_without_existence : Core.Nominal.Uniqueness kingOfFrance ∧ ¬Core.Nominal.Existence kingOfFrance

The empty restrictor satisfies Uniqueness vacuously, but not Existence. The exact configuration @cite{coppock-beaver-2015} use to argue that Uniqueness is a separate component, projecting through assertion polarity.

theorem Phenomena.Definiteness.Studies.CoppockBeaver2015.planet_existence_without_uniqueness : Core.Nominal.Existence planet ∧ ¬Core.Nominal.Uniqueness planet

The multi-witness restrictor satisfies Existence but not Uniqueness. Witnesses: moon and mars are both planets and are distinct.

theorem Phenomena.Definiteness.Studies.CoppockBeaver2015.theSun_existence_and_uniqueness : Core.Nominal.Existence theSun ∧ Core.Nominal.Uniqueness theSun

The singleton restrictor satisfies both components.

theorem Phenomena.Definiteness.Studies.CoppockBeaver2015.theSun_existsUnique : Core.Nominal.existsUnique theSun

For theSun, the Russellian condition holds: existsUnique is by construction the conjunction of Existence and Uniqueness.

theorem Phenomena.Definiteness.Studies.CoppockBeaver2015.kingOfFrance_not_existsUnique : ¬Core.Nominal.existsUnique kingOfFrance

For kingOfFrance, existsUnique fails — Existence is the missing conjunct. The factorization explains which component fails.

theorem Phenomena.Definiteness.Studies.CoppockBeaver2015.planet_not_existsUnique : ¬Core.Nominal.existsUnique planet

For planet, existsUnique fails — Uniqueness is the missing conjunct.

def Phenomena.Definiteness.Studies.CoppockBeaver2015.g₀ : Core.Assignment F.Entity

A trivial bi-assignment: every entity slot is sun, every situation slot is (). The diagnostics in this file do not bind anything.

Equations

• Phenomena.Definiteness.Studies.CoppockBeaver2015.g₀ x✝ = Phenomena.Definiteness.Studies.CoppockBeaver2015.Body.sun

def Phenomena.Definiteness.Studies.CoppockBeaver2015.gs₀ : Core.Logic.Intensional.Variables.SitAssignment F

Equations

• Phenomena.Definiteness.Studies.CoppockBeaver2015.gs₀ x✝ = ()

theorem Phenomena.Definiteness.Studies.CoppockBeaver2015.interpret_theSun : Core.Nominal.interpret (Core.Nominal.NominalKind.unique (Core.Logic.Intensional.Variables.DenotGS.const theSun) 0) g₀ gs₀ = some Body.sun

the sun (as a .unique description with restrictor theSun) interprets to some sun — the unique-witness case.

theorem Phenomena.Definiteness.Studies.CoppockBeaver2015.interpret_kingOfFrance : Core.Nominal.interpret (Core.Nominal.NominalKind.unique (Core.Logic.Intensional.Variables.DenotGS.const kingOfFrance) 0) g₀ gs₀ = none

the King of France interprets to none — Existence failure. The Russellian iota collapses the projection structure here, but the diagnostic in §2 already isolated which component failed.

theorem Phenomena.Definiteness.Studies.CoppockBeaver2015.interpret_planet : Core.Nominal.interpret (Core.Nominal.NominalKind.unique (Core.Logic.Intensional.Variables.DenotGS.const planet) 0) g₀ gs₀ = none

the planet interprets to none — Uniqueness failure. Same surface output as the Existence-failure case, even though the underlying presupposition violation is structurally different.

theorem Phenomena.Definiteness.Studies.CoppockBeaver2015.uniqueness_projects_through_negation (scope : F.Denot Core.Logic.Intensional.Ty.et) : Core.Nominal.Uniqueness kingOfFrance ∧ Core.Nominal.Uniqueness fun (x : F.Denot Core.Logic.Intensional.Ty.e) => ¬scope x ∧ kingOfFrance x

Predicate-level negation does not affect Uniqueness. This is the @cite{coppock-beaver-2015} projection diagnostic, expressed at the restrictor layer: whether the King of France is bald or non-bald, the Uniqueness presupposition on kingOfFrance survives. Operationalized here as: Uniqueness is a property of the restrictor, not the scope, so any sentential operator wrapping the description leaves it unchanged.

theorem Phenomena.Definiteness.Studies.CoppockBeaver2015.existence_does_not_project_through_negation (scope : F.Denot Core.Logic.Intensional.Ty.et) : ¬Core.Nominal.Existence fun (x : F.Denot Core.Logic.Intensional.Ty.e) => scope x ∧ kingOfFrance x

The Existence component, by contrast, can be negated independently: a non-existing King of France can satisfy or fail to satisfy any scope predicate vacuously. This is the contrast that motivates the factorization — Existence enters the scope of negation, Uniqueness does not.