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 carriers, 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: existential closure of a relation.
• 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).

Tags

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

Predicates and arity

@[reducible, inline]

abbrev ArgumentStructure.Relational.Pred1 (E : Type u_1) (S : Type u_2) : Type (max u_1 u_2)

One-place predicate over entities and states.

Equations

• ArgumentStructure.Relational.Pred1 E S = (E → S → Prop)

@[reducible, inline]

abbrev ArgumentStructure.Relational.Pred2 (E : Type u_1) (S : Type u_2) : Type (max u_1 u_2)

Two-place predicate over entities and states.

Equations

• ArgumentStructure.Relational.Pred2 E S = (E → E → S → Prop)

Type shifters

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

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 : Pred2 E S) : Pred1 E S

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

theorem ArgumentStructure.Relational.ex_pi_retraction {E : Type u_1} {S : Type u_2} [Nonempty E] (P : Pred1 E S) (R : Pred2 E S) (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 : Pred1 E S) (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 : Pred1 E S) (R : Pred2 E S) (relatum : E) : Pred1 E S

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 : Pred1 E S) : Pred1 E S

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).

@[implicit_reducible]

instance ArgumentStructure.Relational.instDecidableEqInterpretationSource : DecidableEq InterpretationSource

Equations

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

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

Equations

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

@[implicit_reducible]

instance ArgumentStructure.Relational.instReprInterpretationSource : Repr InterpretationSource

Equations

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

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

@[implicit_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.

• pred1 : NominalInterpType

  Pred1: no relatum slot (sortal, no π).

• pred2 : NominalInterpType

  Pred2: relatum slot (relational or π-shifted).

@[implicit_reducible]

instance ArgumentStructure.Relational.instDecidableEqNominalInterpType : DecidableEq NominalInterpType

Equations

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

@[implicit_reducible]

instance ArgumentStructure.Relational.instReprNominalInterpType : Repr NominalInterpType

Equations

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

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

Equations

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

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

Whether the interpretation type has a relatum slot.

Equations

• ArgumentStructure.Relational.NominalInterpType.pred1.hasRelatumSlot = False
• ArgumentStructure.Relational.NominalInterpType.pred2.hasRelatumSlot = True

@[implicit_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.pred1.canTakePossessor = False
• ArgumentStructure.Relational.NominalInterpType.pred2.canTakePossessor = True

@[implicit_reducible]

instance ArgumentStructure.Relational.NominalInterpType.instDecidablePredCanTakePossessor : DecidablePred canTakePossessor

Equations

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