Relational nouns: the relationalizer and its closures

Type shifters for relational nouns and possessive constructions, following [barker-2011]. A noun with a relatum slot denotes a situation-indexed relation E → Y → S → Prop, possessor first, over a possessum type Y that is the entity type for ordinary possession and the state type when the possessum is a quality ([hanink-koontz-garboden-2025]); a sortal noun denotes Y → S → Prop. The relationalizer π P R opens a slot on a sortal P with a free relation R, and applied to a possessor x it is the modifier genitive λy. P y ∧ R x y, the noun conjoined with the bare predicate possessive R x (pi_apply). The argument genitive is application itself: a relational noun R applied to its possessor is R x. Ex and ExPossessor close the relatum and the possessor slot, the domain and codomain of the relation at each situation.

Main declarations

• π P R: Barker's relationalizer, π P R x y s ↔ P y s ∧ R x y s.
• Ex R, ExPossessor R: existential closure of the relatum (Ex R x s ↔ ∃ y, R x y s) and of the possessor (ExPossessor R y s ↔ ∃ x, R x y s), the alienator of [adamson-2024].

Main statements

• pi_apply: π P R x = P ⊓ R x, the modifier genitive as intersective modification by the predicate possessive ([PB01]).
• pi_top: π ⊤ R = R.
• exPossessor_pi: the alienator over a relationalized noun keeps the sortal core.

References

• [barker-2011]
• [adamson-2024]
• [PB01]
• [hanink-koontz-garboden-2025]

The relationalizer

def Possession.π {E : Type u_1} {Y : Type u_2} {S : Type u_3} (P : Y → S → Prop) (R : E → Y → S → Prop) : E → Y → S → Prop

Barker's relationalizer: π P R x y s ↔ P y s ∧ R x y s. Applied to a possessor x it is the modifier genitive λy. P y ∧ R x y; coercing the sortal to a relation and taking the possessor as its argument ([JV94]) and modifying the sortal by the possessor's free relation ([Par97]) assemble the same term π P R x.

Equations

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

theorem Possession.pi_apply {E : Type u_1} {Y : Type u_2} {S : Type u_3} (P : Y → S → Prop) (R : E → Y → S → Prop) (x : E) : π P R x = P ⊓ R x

The modifier genitive is the noun conjoined with the bare predicate possessive R x.

@[simp]

theorem Possession.pi_top {E : Type u_1} {Y : Type u_2} {S : Type u_3} (R : E → Y → S → Prop) : π ⊤ R = R

Over the trivial restrictor the relationalizer is the relation itself.

Existential closures

def Possession.Ex {E : Type u_1} {Y : Type u_2} {S : Type u_3} (R : E → Y → S → Prop) : E → S → Prop

Existential closure of the relatum, Ex R x s ↔ ∃ y, R x y s: the domain of R at s.

Equations

• Possession.Ex R x s = ∃ (y : Y), R x y s

def Possession.ExPossessor {E : Type u_1} {Y : Type u_2} {S : Type u_3} (R : E → Y → S → Prop) : Y → S → Prop

Existential closure of the possessor, ExPossessor R y s ↔ ∃ x, R x y s: the codomain of R at s, the alienator nominalizer of [adamson-2024] that closes a relational noun's possessor slot.

Equations

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

theorem Possession.exPossessor_pi {E : Type u_1} {Y : Type u_2} {S : Type u_3} (P : Y → S → Prop) (R : E → Y → S → Prop) (y : Y) (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.