Coppock & Beaver (2015): Definiteness and Determinacy

[CB15]

The central thesis of [CB15] 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.

The factorization is operationalized in Semantics.Definiteness as Existence, Uniqueness, and existsUnique; this file tests it over a tiny frame (Body: sun / moon / mars, one situation index).

Main results

• kingOfFrance_uniqueness_without_existence, planet_existence_without_uniqueness: Existence and Uniqueness are logically independent.
• theSun_existsUnique, kingOfFrance_not_existsUnique, planet_not_existsUnique: Russellian existsUnique holds exactly for a singleton extension.
• interpret_theSun, interpret_kingOfFrance, interpret_planet: Semantics.Definiteness.interpret on a .unique description returns none precisely in the Russellian failure cases.
• uniqueness_projects_through_negation, existence_does_not_project_through_negation: the projection contrast — Uniqueness survives a scope operator, Existence does not.

A tiny frame for the projection diagnostics

inductive 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 CoppockBeaver2015.instDecidableEqBody : DecidableEq Body

Equations

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

def CoppockBeaver2015.instReprBody.repr : Body → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance CoppockBeaver2015.instReprBody : Repr Body

Equations

• CoppockBeaver2015.instReprBody = { reprPrec := CoppockBeaver2015.instReprBody.repr }

def CoppockBeaver2015.theSun : Intensional.Denot Body Unit Intensional.Ty.et

Singleton restrictor: theSun holds of exactly one entity. One index suffices — the diagnostics are about predicate extensions, not about world-variability.

Equations

• CoppockBeaver2015.theSun CoppockBeaver2015.Body.sun = True
• CoppockBeaver2015.theSun x✝ = False

def CoppockBeaver2015.planet : Intensional.Denot Body Unit Intensional.Ty.et

Multi-witness restrictor: planet holds of two entities.

Equations

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

def CoppockBeaver2015.kingOfFrance : Intensional.Denot Body Unit Intensional.Ty.et

Empty restrictor: kingOfFrance has no satisfier — the [CB15] motivating case.

Equations

• CoppockBeaver2015.kingOfFrance x✝ = False

Existence and Uniqueness are logically independent

theorem CoppockBeaver2015.kingOfFrance_uniqueness_without_existence : Semantics.Definiteness.Uniqueness kingOfFrance ∧ ¬Semantics.Definiteness.Existence kingOfFrance

The empty restrictor satisfies Uniqueness vacuously but not Existence — the configuration [CB15] use to argue that Uniqueness is a separate component, projecting through assertion polarity. A concrete instance of the substrate's uniqueness_does_not_imply_existence.

theorem CoppockBeaver2015.planet_existence_without_uniqueness : Semantics.Definiteness.Existence planet ∧ ¬Semantics.Definiteness.Uniqueness planet

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

theorem CoppockBeaver2015.theSun_existence_and_uniqueness : Semantics.Definiteness.Existence theSun ∧ Semantics.Definiteness.Uniqueness theSun

The singleton restrictor satisfies both components.

Russellian collapse: existsUnique is the conjunction

theorem CoppockBeaver2015.theSun_existsUnique : ∃! x : Intensional.Denot Body Unit Intensional.Ty.e, theSun x

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

theorem CoppockBeaver2015.kingOfFrance_not_existsUnique : ¬∃! x : Intensional.Denot Body Unit Intensional.Ty.e, kingOfFrance x

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

theorem CoppockBeaver2015.planet_not_existsUnique : ¬∃! x : Intensional.Denot Body Unit Intensional.Ty.e, planet x

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

Alignment with Semantics.Definiteness.interpret

def CoppockBeaver2015.g₀ : Core.Assignment Body

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

Equations

• CoppockBeaver2015.g₀ x✝ = CoppockBeaver2015.Body.sun

def CoppockBeaver2015.gs₀ : Intensional.Variables.SitAssignment Unit

Equations

• CoppockBeaver2015.gs₀ x✝ = ()

theorem CoppockBeaver2015.interpret_theSun : Semantics.Definiteness.interpret (Semantics.Definiteness.Description.unique (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 CoppockBeaver2015.interpret_kingOfFrance : Semantics.Definiteness.interpret (Semantics.Definiteness.Description.unique (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 §2 already isolated which component failed.

theorem CoppockBeaver2015.interpret_planet : Semantics.Definiteness.interpret (Semantics.Definiteness.Description.unique (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.

Negation-projection contrast

theorem CoppockBeaver2015.uniqueness_projects_through_negation (scope : Intensional.Denot Body Unit Intensional.Ty.et) : Semantics.Definiteness.Uniqueness kingOfFrance ∧ Semantics.Definiteness.Uniqueness fun (x : Intensional.Denot Body Unit Intensional.Ty.e) => ¬scope x ∧ kingOfFrance x

Predicate-level negation does not affect Uniqueness. This is the [CB15] projection diagnostic, expressed at the restrictor layer: whether the King of France is bald or non-bald, the Uniqueness presupposition on kingOfFrance survives. Uniqueness is a property of the restrictor, not the scope, so any sentential operator wrapping the description leaves it unchanged.

theorem CoppockBeaver2015.existence_does_not_project_through_negation (scope : Intensional.Denot Body Unit Intensional.Ty.et) : ¬Semantics.Definiteness.Existence fun (x : Intensional.Denot Body Unit Intensional.Ty.e) => scope x ∧ kingOfFrance x

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