Possessive-of as a Kleisli arrow

The possessive denotation in the unified referential currency NominalDenot (Semantics/Reference/Nominal.lean), which is a monad. NP's N is Kleisli bind into the definite possessee of the possessor: re-point the possessor denotation's selector through the possession relation (russellIota of the relation), inheriting the possessor's intrinsic presupposition. So:

• possessive nesting (John's mother's friend) is bind associativity;
• the possessor's φ-features (when it is a pronoun) ride along to the whole possessive, by applyTo_presup;
• the existence/uniqueness presupposition is selector definedness (russellIota_isSome_iff_exists_unique), not a separate intrinsic presup.

Main declarations

• Possessive.theOf R — the Kleisli arrow: the unique R-possessee of a possessor, as a NominalDenot.
• Possessive.applyTo nd R = nd >>= theOf R — NP's N.
• Possessive.Definite.toNominalDenot — a definite carrier as a NominalDenot (always-defined selector, from HasIotaWitness).

Main statements

• applyTo_presup — the possessive's presupposition is the possessor's.
• applyTo_selector — the selector binds through the iota of the relation.
• applyTo_applyTo — nesting, from bind_assoc.

The Kleisli arrow

noncomputable def Possessive.theOf {Ctx : Type u_1} {W E : Type} (R : E → E → Prop) (possessor : E) : Semantics.Reference.NominalDenot Ctx W E

The unique entity the possessor stands in relation R to, as a NominalDenot: a definite referent (russellIota) with vacuous intrinsic presupposition — definedness is its only presupposition.

Equations

• Possessive.theOf R possessor = { presup := fun (x : Ctx) (x_1 : W) => True, selector := fun (x : Ctx) (x_1 : W) => Semantics.Definiteness.russellIota fun (y : E) => R possessor y }

noncomputable def Possessive.applyTo {Ctx : Type u_1} {W E : Type} (nd : Semantics.Reference.NominalDenot Ctx W E) (R : E → E → Prop) : Semantics.Reference.NominalDenot Ctx W E

NP's N: re-select the possessor denotation through the possession relation R.

Equations

• Possessive.applyTo nd R = nd >>= Possessive.theOf R

Composition laws

@[simp]

theorem Possessive.applyTo_presup {Ctx : Type u_1} {W E : Type} (nd : Semantics.Reference.NominalDenot Ctx W E) (R : E → E → Prop) (c : Ctx) (w : W) : (applyTo nd R).presup c w = nd.presup c w

The possessive's intrinsic presupposition is the possessor's — a possessor pronoun's φ-features ride along to the whole possessive.

@[simp]

theorem Possessive.applyTo_selector {Ctx : Type u_1} {W E : Type} (nd : Semantics.Reference.NominalDenot Ctx W E) (R : E → E → Prop) (c : Ctx) (w : W) : (applyTo nd R).selector c w = (nd.selector c w).bind fun (p : E) => Semantics.Definiteness.russellIota fun (y : E) => R p y

The possessive's selector binds the possessor through the iota of the relation: defined exactly when the possessor is defined and has a unique R-possessee.

theorem Possessive.applyTo_applyTo {Ctx : Type u_1} {W E : Type} (nd : Semantics.Reference.NominalDenot Ctx W E) (R₁ R₂ : E → E → Prop) : applyTo (applyTo nd R₁) R₂ = do let p ← nd applyTo (theOf R₁ p) R₂

Nesting (John's mother's friend) — from bind associativity.

Definite carriers as nominal denotations

noncomputable def Possessive.Definite.toNominalDenot {Ctx : Type u_1} {E S : Type} (d : Definite E S) : Semantics.Reference.NominalDenot Ctx S E

A definite possessive carrier as a NominalDenot over its situations: the selector is russellIota of the possessee predicate, always defined because the carrier bears the iota-presupposition (HasIotaWitness).

Equations

• d.toNominalDenot = { presup := fun (x : Ctx) (x_1 : S) => True, selector := fun (x : Ctx) (s : S) => Semantics.Definiteness.russellIota fun (y : E) => d.predicate y s }