Possessives and Relational Nouns

@cite{barker-2011}

Barker's type-shifting analysis: π relationalizes sortals, Ex detransitivizes relations.

Main definitions

π, ExProp, ExDecidable, PossessiveSemantics, possessiveRelational, possessiveSortal, naSemantics, bareSemantics

@[reducible, inline]

abbrev Semantics.ArgumentStructure.Relational.Pred1 (E S : Type) : Type

One-place predicates: E → S → Bool

Equations

• Semantics.ArgumentStructure.Relational.Pred1 E S = (E → S → Bool)

@[reducible, inline]

abbrev Semantics.ArgumentStructure.Relational.Pred2 (E S : Type) : Type

Two-place predicates (relations): E → E → S → Bool

Equations

• Semantics.ArgumentStructure.Relational.Pred2 E S = (E → E → S → Bool)

inductive Semantics.ArgumentStructure.Relational.SemType : Type

The semantic type of an expression, tracking arity.

• pred1 : SemType
• pred2 : SemType
• entity : SemType

@[implicit_reducible]

instance Semantics.ArgumentStructure.Relational.instDecidableEqSemType : DecidableEq SemType

Equations

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

@[implicit_reducible]

instance Semantics.ArgumentStructure.Relational.instReprSemType : Repr SemType

Equations

• Semantics.ArgumentStructure.Relational.instReprSemType = { reprPrec := Semantics.ArgumentStructure.Relational.instReprSemType.repr }

def Semantics.ArgumentStructure.Relational.instReprSemType.repr : SemType → ℕ → Std.Format

Equations

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

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

Barker's π (Relationalizer): λP.λx.λy. P(y) ∧ R(x,y)

Equations

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

def Semantics.ArgumentStructure.Relational.«termRelationalizer(_,_)» : Lean.ParserDescr

Equations

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

def Semantics.ArgumentStructure.Relational.ExProp {E S : Type} (R : Pred2 E S) : E → S → Prop

Ex (Existential Closure): λR.λx. ∃y. R(x,y)

Equations

• Semantics.ArgumentStructure.Relational.ExProp R x s = ∃ (y : E), R x y s = true

def Semantics.ArgumentStructure.Relational.ExDecidable {E S : Type} [Fintype E] [DecidableEq E] (R : Pred2 E S) : Pred1 E S

Equations

• Semantics.ArgumentStructure.Relational.ExDecidable R x s = decide (∃ (y : E), R x y s = true)

structure Semantics.ArgumentStructure.Relational.PossessiveSemantics (E S : Type) : Type

Semantic structure of possessive phrase

• possessor : E
• possesseePred : Pred1 E S
• relation : Pred2 E S
• relationIsLexical : Bool

def Semantics.ArgumentStructure.Relational.possessiveRelational {E S : Type} (possessor : E) (nounRel : Pred2 E S) : Pred1 E S

Equations

• Semantics.ArgumentStructure.Relational.possessiveRelational possessor nounRel y s = nounRel possessor y s

def Semantics.ArgumentStructure.Relational.possessiveSortal {E S : Type} (possessor : E) (nounPred : Pred1 E S) (R : Pred2 E S) : Pred1 E S

Equations

• Semantics.ArgumentStructure.Relational.possessiveSortal possessor nounPred R y s = Semantics.ArgumentStructure.Relational.π nounPred R possessor y s

theorem Semantics.ArgumentStructure.Relational.possessive_sortal_is_pi {E S : Type} (possessor : E) (P : Pred1 E S) (R : Pred2 E S) (y : E) (s : S) : possessiveSortal possessor P R y s = π P R possessor y s

def Semantics.ArgumentStructure.Relational.iotaPresupposition {E S : Type} (P : Pred1 E S) (s : S) : Prop

Equations

• Semantics.ArgumentStructure.Relational.iotaPresupposition P s = ∃ (x : E), P x s = true ∧ ∀ (y : E), P y s = true → y = x

structure Semantics.ArgumentStructure.Relational.DefinitePossessive (E S : Type) : Type

• possessor : E
• predicate : Pred1 E S
• presupposition (s : S) : iotaPresupposition self.predicate s

def Semantics.ArgumentStructure.Relational.naSemantics {E S : Type} (nounPred : Pred1 E S) (R : Pred2 E S) (relatum : E) : Pred1 E S

Equations

• Semantics.ArgumentStructure.Relational.naSemantics nounPred R relatum x s = Semantics.ArgumentStructure.Relational.π nounPred R relatum x s

def Semantics.ArgumentStructure.Relational.bareSemantics {E S : Type} (nounPred : Pred1 E S) : Pred1 E S

Equations

• Semantics.ArgumentStructure.Relational.bareSemantics nounPred = nounPred

theorem Semantics.ArgumentStructure.Relational.na_has_relatum_slot {E S : Type} (P : Pred1 E S) (R : Pred2 E S) (z x : E) (s : S) : naSemantics P R z x s = (P x s && R z x s)

theorem Semantics.ArgumentStructure.Relational.bare_has_no_relatum_slot {E S : Type} (P : Pred1 E S) (x : E) (s : S) : bareSemantics P x s = P x s

inductive Semantics.ArgumentStructure.Relational.InterpretationSource : Type

Source of the relational interpretation.

• lexicalRelation : InterpretationSource
• appliedPi : InterpretationSource
• noRelation : InterpretationSource

@[implicit_reducible]

instance Semantics.ArgumentStructure.Relational.instDecidableEqInterpretationSource : DecidableEq InterpretationSource

Equations

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

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

Equations

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

@[implicit_reducible]

instance Semantics.ArgumentStructure.Relational.instReprInterpretationSource : Repr InterpretationSource

Equations

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

def Semantics.ArgumentStructure.Relational.CanFillRelatum : InterpretationSource → Prop

Equations

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

@[implicit_reducible]

instance Semantics.ArgumentStructure.Relational.instDecidablePredInterpretationSourceCanFillRelatum : DecidablePred CanFillRelatum

Equations

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

theorem Semantics.ArgumentStructure.Relational.bridging_from_pi {E S : Type} (P : Pred1 E S) (R : Pred2 E S) : CanFillRelatum InterpretationSource.appliedPi ∧ ¬CanFillRelatum InterpretationSource.noRelation ∧ CanFillRelatum InterpretationSource.lexicalRelation

Bridging licensing follows from π-application.

Sortal nouns: π creates slot (bridging OK); no π means no slot (blocked). Relational nouns: lexical slot exists regardless of π.

inductive Semantics.ArgumentStructure.Relational.PossessionRelationType : Type

Vikner & Jensen's taxonomy of possession relations (Barker p. 9).

• inherent : PossessionRelationType

  Inherent: part-whole, properties (the car's speed, the table's leg)

• agentive : PossessionRelationType

  Agentive: agent relation (John's poem = poem John wrote)

• control : PossessionRelationType

  Control: ownership, legal control (John's house)

• pragmatic : PossessionRelationType

  Pragmatic: any contextually salient relation

@[implicit_reducible]

instance Semantics.ArgumentStructure.Relational.instDecidableEqPossessionRelationType : DecidableEq PossessionRelationType

Equations

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

def Semantics.ArgumentStructure.Relational.instReprPossessionRelationType.repr : PossessionRelationType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.ArgumentStructure.Relational.instReprPossessionRelationType : Repr PossessionRelationType

Equations

• Semantics.ArgumentStructure.Relational.instReprPossessionRelationType = { reprPrec := Semantics.ArgumentStructure.Relational.instReprPossessionRelationType.repr }

def Semantics.ArgumentStructure.Relational.relationSource (isNounRelational : Bool) : String

Lexical possession (relational noun) vs pragmatic possession (sortal noun).

Equations

• Semantics.ArgumentStructure.Relational.relationSource isNounRelational = if isNounRelational = true then "lexical" else "pragmatic (from π)"

def Semantics.ArgumentStructure.Relational.derivation_johns_brother {E S : Type} (john : E) (brother : Pred2 E S) : Pred1 E S

Derivation: "John's brother" (relational noun, no π needed).

Equations

• Semantics.ArgumentStructure.Relational.derivation_johns_brother john brother = Semantics.ArgumentStructure.Relational.possessiveRelational john brother

def Semantics.ArgumentStructure.Relational.derivation_johns_cloud {E S : Type} (john : E) (cloud : Pred1 E S) (R : Pred2 E S) : Pred1 E S

Derivation: "John's cloud" (sortal noun, π required).

Equations

• Semantics.ArgumentStructure.Relational.derivation_johns_cloud john cloud R = Semantics.ArgumentStructure.Relational.possessiveSortal john cloud R

def Semantics.ArgumentStructure.Relational.derivation_na_author {E S : Type} (author : Pred2 E S) (relatum : E) : Pred1 E S

Derivation: Mandarin "na zuozhe" (that author; relational noun).

Equations

• Semantics.ArgumentStructure.Relational.derivation_na_author author relatum x s = author relatum x s

def Semantics.ArgumentStructure.Relational.derivation_na_seat {E S : Type} (seat : Pred1 E S) (R : Pred2 E S) (car : E) : Pred1 E S

Derivation: Mandarin "na zuoyi" (that seat; sortal noun, π from na).

Equations

• Semantics.ArgumentStructure.Relational.derivation_na_seat seat R car = Semantics.ArgumentStructure.Relational.naSemantics seat R car

def Semantics.ArgumentStructure.Relational.derivation_bare_seat {E S : Type} (seat : Pred1 E S) : Pred1 E S

Derivation: Bare Mandarin "zuoyi" (seat; no π, no bridging slot).

Equations

• Semantics.ArgumentStructure.Relational.derivation_bare_seat seat = Semantics.ArgumentStructure.Relational.bareSemantics seat

Algebraic Structure

@cite{ahn-zhu-2025} @cite{barker-2011}

π and Ex form a pseudo-adjoint pair: Ex(π(P, R)) ≈ P (when R is satisfied by some entity).

theorem Semantics.ArgumentStructure.Relational.ex_pi_retraction {E S : Type} [Nonempty E] (P : Pred1 E S) (R : Pred2 E S) (y z : E) (s : S) (hP : P y s = true) (hR : R z y s = true) : ExProp (π P R) z s

Retraction: Ex(π(P, R)) holds when both P(y) and R(z,y) hold.

Unification of Possessives, Demonstratives, and Bridging

Three questions are equivalent:

1. Can "John's N" be interpreted? (possessive licensing)
2. Can "na N" accommodate a bridging antecedent? (bridging licensing)
3. Does the interpretation of N have type Pred2? (structural question)

inductive Semantics.ArgumentStructure.Relational.NominalInterpType : Type

The interpretation type of a nominal

• pred1 : NominalInterpType

  Pred1: No relatum slot (sortal, no π)

• pred2 : NominalInterpType

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

@[implicit_reducible]

instance Semantics.ArgumentStructure.Relational.instDecidableEqNominalInterpType : DecidableEq NominalInterpType

Equations

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

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

Equations

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

@[implicit_reducible]

instance Semantics.ArgumentStructure.Relational.instReprNominalInterpType : Repr NominalInterpType

Equations

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

def Semantics.ArgumentStructure.Relational.NominalInterpType.hasRelatumSlot : NominalInterpType → Bool

Does this interpretation type have a relatum slot?

Equations

• Semantics.ArgumentStructure.Relational.NominalInterpType.pred1.hasRelatumSlot = false
• Semantics.ArgumentStructure.Relational.NominalInterpType.pred2.hasRelatumSlot = true

def Semantics.ArgumentStructure.Relational.NominalInterpType.canTakePossessor : NominalInterpType → Bool

Can this interpretation type take a possessor?

Equations

• Semantics.ArgumentStructure.Relational.NominalInterpType.pred1.canTakePossessor = false
• Semantics.ArgumentStructure.Relational.NominalInterpType.pred2.canTakePossessor = true

def Semantics.ArgumentStructure.Relational.NominalInterpType.canBridge : NominalInterpType → Bool

Can this interpretation type accommodate bridging?

Equations

• Semantics.ArgumentStructure.Relational.NominalInterpType.pred1.canBridge = false
• Semantics.ArgumentStructure.Relational.NominalInterpType.pred2.canBridge = true

theorem Semantics.ArgumentStructure.Relational.unification_principle (t : NominalInterpType) : t.hasRelatumSlot = t.canTakePossessor ∧ t.canTakePossessor = t.canBridge

hasRelatumSlot ⟺ canTakePossessor ⟺ canBridge.

theorem Semantics.ArgumentStructure.Relational.bridging_is_possession (t : NominalInterpType) : t.canBridge = t.canTakePossessor

Bridging asymmetry = possessive asymmetry.

theorem Semantics.ArgumentStructure.Relational.pi_creates_slot {E S : Type} (P : Pred1 E S) (R : Pred2 E S) (z x : E) (s : S) : π P R z x s = (P x s && R z x s)

π always creates a relatum slot (π : Pred1 → Pred2).

theorem Semantics.ArgumentStructure.Relational.structural_explanation (t : NominalInterpType) : t.canBridge = true ↔ t.hasRelatumSlot = true

Bridging ↔ having a relatum slot.

def Semantics.ArgumentStructure.Relational.possessiveAsNPQ {E : Type} (possessor : E) (R : E → E → Bool) : Core.Quantification.NPQ E

A possessive like "John's" produces a type ⟨1⟩ quantifier (NPQ): ⟦John's⟧ = λR.λP. ∃y. R(possessor, y) ∧ P(y). When the possessum is unique, this is a Montagovian individual.

Possessive GQs are NON-ISOM: "John's cat" depends on the identity of John, not just cardinalities. This connects Barker's type-shifting analysis to the GQ framework in Core.Quantification.

Equations

• Semantics.ArgumentStructure.Relational.possessiveAsNPQ possessor R P = ∃ (y : E), R possessor y = true ∧ P y

theorem Semantics.ArgumentStructure.Relational.possessive_individual_eval {E : Type} (b : E) (P : E → Prop) : Core.Quantification.individual b P = P b

When the possessum is unique, the possessive NP denotes a Montagovian individual: ⟦John's brother⟧ = I_{b} where b is John's unique brother. The Montagovian individual I_b maps any property P to P(b). Cross-ref: Core.Quantification.individual.