Possessives and relational nouns

Type-shifting operators for the analysis of possessive constructions and relational nouns, following [Bar11].

The relationalizer π takes a sortal predicate P and a relation R and returns the relational predicate fun x y ↦ P y ∧ R x y. Its quasi-adjoint Ex collapses a relation back to a property by existentially closing the second argument.

The structural condition having a relatum slot controls two surface phenomena — possessor licensing and demonstrative anaphora. They are tracked as separate predicates (hasRelatumSlot, canTakePossessor) over NominalInterpType because they describe distinct linguistic facts, even though they coincide by construction.

The possessive-specific descriptions, capability mixins, and quantificational layer live in the unified Possessive namespace (Semantics/Possessive/), built on this substrate.

Main definitions

• π P R: Barker's relationalizer.
• Ex R, ExPossessor R: existential closure of a relation in its second argument, and in its first — the possessor of π P R.
• iotaPresupposition P: Russellian uniqueness presupposition for definites.
• naSemantics, bareSemantics: demonstrative and bare nominal denotations.
• NominalInterpType: relational arity of a nominal denotation.

Main statements

• ex_pi_retraction: Ex recovers a witness of π P R from witnesses of P and R.

References

• [Bar11]: Possessives and relational nouns (von Heusinger/Maienborn/Portner handbook, pp. 1109–1130; π and Ex at p. 1114).
• [Ada24]: the alienator nominalizer, ExPossessor.

Tags

relational noun, type shifting, bridging, definite description, demonstrative

Predicates and arity

Type shifters

def ArgumentStructure.Relational.π {E : Type u_1} {S : Type u_2} (P : E → S → Prop) (R : E → E → S → Prop) : E → E → S → Prop

Barker's relationalizer: π P R x y s ↔ P y s ∧ R x y s.

Equations

• ArgumentStructure.Relational.π P R x y s = (P y s ∧ R x y s)

def ArgumentStructure.Relational.Ex {E : Type u_1} {S : Type u_2} (R : E → E → S → Prop) : E → S → Prop

Existential closure of a relation in its second argument: Ex R x s ↔ ∃ y, R x y s.

Equations

• ArgumentStructure.Relational.Ex R x s = ∃ (y : E), R x y s

def ArgumentStructure.Relational.ExPossessor {E : Type u_1} {S : Type u_2} (R : E → E → S → Prop) : E → S → Prop

Existential closure of a relation in its first argument — the possessor of π P R: ExPossessor R y s ↔ ∃ x, R x y s. The alienator nominalizer of [Ada24], which closes a relational noun's possessor slot.

Equations

• ArgumentStructure.Relational.ExPossessor R y s = ∃ (x : E), R x y s

theorem ArgumentStructure.Relational.exPossessor_pi {E : Type u_1} {S : Type u_2} (P : E → S → Prop) (R : E → E → S → Prop) (y : E) (s : S) : ExPossessor (π P R) y s ↔ P y s ∧ ∃ (x : E), R x y s

The alienator over a relationalized noun keeps the sortal core and closes the relation.

theorem ArgumentStructure.Relational.ex_pi_retraction {E : Type u_1} {S : Type u_2} [Nonempty E] (P : E → S → Prop) (R : E → E → S → Prop) (y z : E) (s : S) (hP : P y s) (hR : R z y s) : Ex (π P R) z s

Ex (π P R) z s is witnessed whenever some y satisfies both P y s and R z y s.

Definiteness and demonstratives

@[reducible, inline]

abbrev ArgumentStructure.Relational.iotaPresupposition {E : Type u_1} {S : Type u_2} (P : E → S → Prop) (s : S) : Prop

Russellian uniqueness presupposition: ∃! x, P x s. This is mathlib's ExistsUnique (the body unfolds to ∃ x, P x s ∧ ∀ y, P y s → y = x), so the full ExistsUnique.* API is available; the name records the linguistic role — the presupposition a definite description carries.

Equations

• ArgumentStructure.Relational.iotaPresupposition P s = ∃! x : E, P x s

def ArgumentStructure.Relational.naSemantics {E : Type u_1} {S : Type u_2} (nounPred : E → S → Prop) (R : E → E → S → Prop) (relatum : E) : E → S → Prop

Demonstrative-headed nominal: π applied to a sortal noun with the demonstrative supplying the relatum.

Equations

• ArgumentStructure.Relational.naSemantics nounPred R relatum = ArgumentStructure.Relational.π nounPred R relatum

def ArgumentStructure.Relational.bareSemantics {E : Type u_1} {S : Type u_2} (nounPred : E → S → Prop) : E → S → Prop

Bare nominal: identity on the predicate (no relatum slot).

Equations

• ArgumentStructure.Relational.bareSemantics nounPred = nounPred

Interpretation sources and bridging

inductive ArgumentStructure.Relational.InterpretationSource : Type

Source of a noun's relational interpretation.

• lexicalRelation : InterpretationSource

  Noun is lexically relational (e.g. brother, author).

• appliedPi : InterpretationSource

  π was applied (e.g. possessive, demonstrative).

• noRelation : InterpretationSource

  No relation available (bare sortal).

@[instance_reducible]

instance ArgumentStructure.Relational.instDecidableEqInterpretationSource : DecidableEq InterpretationSource

Equations

• ArgumentStructure.Relational.instDecidableEqInterpretationSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ArgumentStructure.Relational.instReprInterpretationSource : Repr InterpretationSource

Equations

• ArgumentStructure.Relational.instReprInterpretationSource = { reprPrec := ArgumentStructure.Relational.instReprInterpretationSource.repr }

def ArgumentStructure.Relational.instReprInterpretationSource.repr : InterpretationSource → ℕ → Std.Format

Equations

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

def ArgumentStructure.Relational.CanFillRelatum : InterpretationSource → Prop

Whether an interpretation source provides a relatum slot.

Equations

• ArgumentStructure.Relational.CanFillRelatum ArgumentStructure.Relational.InterpretationSource.lexicalRelation = True
• ArgumentStructure.Relational.CanFillRelatum ArgumentStructure.Relational.InterpretationSource.appliedPi = True
• ArgumentStructure.Relational.CanFillRelatum ArgumentStructure.Relational.InterpretationSource.noRelation = False

@[instance_reducible]

instance ArgumentStructure.Relational.instDecidablePredInterpretationSourceCanFillRelatum : DecidablePred CanFillRelatum

Equations

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

Nominal interpretation type

inductive ArgumentStructure.Relational.NominalInterpType : Type

Interpretation type of a nominal: with or without a relatum slot.

• sortal : NominalInterpType

  No relatum slot (one-place; no π).

• relational : NominalInterpType

  Relatum slot (two-place: lexically relational or π-shifted).

@[instance_reducible]

instance ArgumentStructure.Relational.instDecidableEqNominalInterpType : DecidableEq NominalInterpType

Equations

• ArgumentStructure.Relational.instDecidableEqNominalInterpType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ArgumentStructure.Relational.instReprNominalInterpType.repr : NominalInterpType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ArgumentStructure.Relational.instReprNominalInterpType : Repr NominalInterpType

Equations

• ArgumentStructure.Relational.instReprNominalInterpType = { reprPrec := ArgumentStructure.Relational.instReprNominalInterpType.repr }

def ArgumentStructure.Relational.NominalInterpType.hasRelatumSlot : NominalInterpType → Prop

Whether the interpretation type has a relatum slot.

Equations

• ArgumentStructure.Relational.NominalInterpType.sortal.hasRelatumSlot = False
• ArgumentStructure.Relational.NominalInterpType.relational.hasRelatumSlot = True

@[instance_reducible]

instance ArgumentStructure.Relational.NominalInterpType.instDecidablePredHasRelatumSlot : DecidablePred hasRelatumSlot

Equations

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

def ArgumentStructure.Relational.NominalInterpType.canTakePossessor : NominalInterpType → Prop

Whether the interpretation type can take a possessor argument.

Equations

• ArgumentStructure.Relational.NominalInterpType.sortal.canTakePossessor = False
• ArgumentStructure.Relational.NominalInterpType.relational.canTakePossessor = True

@[instance_reducible]

instance ArgumentStructure.Relational.NominalInterpType.instDecidablePredCanTakePossessor : DecidablePred canTakePossessor

Equations

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