@[reducible, inline]

abbrev Semantics.Lexical.Noun.Relational.Barker2011.Pred1 (E S : Type) : Type

One-place predicates: E → S → Bool

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.Pred1 E S = (E → S → Bool)

@[reducible, inline]

abbrev Semantics.Lexical.Noun.Relational.Barker2011.Pred2 (E S : Type) : Type

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

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.Pred2 E S = (E → E → S → Bool)

inductive Semantics.Lexical.Noun.Relational.Barker2011.SemType : Type

The semantic type of an expression, tracking arity.

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

instance Semantics.Lexical.Noun.Relational.Barker2011.instDecidableEqSemType : DecidableEq SemType

Equations

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

instance Semantics.Lexical.Noun.Relational.Barker2011.instReprSemType : Repr SemType

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.instReprSemType = { reprPrec := Semantics.Lexical.Noun.Relational.Barker2011.instReprSemType.repr }

def Semantics.Lexical.Noun.Relational.Barker2011.instReprSemType.repr : SemType → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Noun.Relational.Barker2011.instBEqSemType : BEq SemType

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.instBEqSemType = { beq := Semantics.Lexical.Noun.Relational.Barker2011.instBEqSemType.beq }

def Semantics.Lexical.Noun.Relational.Barker2011.instBEqSemType.beq : SemType → SemType → Bool

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.instBEqSemType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Lexical.Noun.Relational.Barker2011.π {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.Lexical.Noun.Relational.Barker2011.π P R x y s = (P y s && R x y s)

def Semantics.Lexical.Noun.Relational.Barker2011.«termRelationalizer(_,_)» : Lean.ParserDescr

Equations

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

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

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

Equations

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

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

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.ExDecidable R x s = Fintype.elems.toList.any fun (y : E) => R x y s

structure Semantics.Lexical.Noun.Relational.Barker2011.PossessiveSemantics (E S : Type) : Type

Semantic structure of possessive phrase

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

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

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.possessiveRelational possessor nounRel y s = nounRel possessor y s

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

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.possessiveSortal possessor nounPred R y s = Semantics.Lexical.Noun.Relational.Barker2011.π nounPred R possessor y s

theorem Semantics.Lexical.Noun.Relational.Barker2011.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.Lexical.Noun.Relational.Barker2011.iotaPresupposition {E S : Type} (P : Pred1 E S) (s : S) : Prop

Equations

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

structure Semantics.Lexical.Noun.Relational.Barker2011.DefinitePossessive (E S : Type) : Type

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

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

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.naSemantics nounPred R relatum x s = Semantics.Lexical.Noun.Relational.Barker2011.π nounPred R relatum x s

def Semantics.Lexical.Noun.Relational.Barker2011.bareSemantics {E S : Type} (nounPred : Pred1 E S) : Pred1 E S

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.bareSemantics nounPred = nounPred

theorem Semantics.Lexical.Noun.Relational.Barker2011.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.Lexical.Noun.Relational.Barker2011.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.Lexical.Noun.Relational.Barker2011.InterpretationSource : Type

Source of the relational interpretation.

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

instance Semantics.Lexical.Noun.Relational.Barker2011.instDecidableEqInterpretationSource : DecidableEq InterpretationSource

Equations

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

def Semantics.Lexical.Noun.Relational.Barker2011.instReprInterpretationSource.repr : InterpretationSource → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Noun.Relational.Barker2011.instReprInterpretationSource : Repr InterpretationSource

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.instReprInterpretationSource = { reprPrec := Semantics.Lexical.Noun.Relational.Barker2011.instReprInterpretationSource.repr }

instance Semantics.Lexical.Noun.Relational.Barker2011.instBEqInterpretationSource : BEq InterpretationSource

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.instBEqInterpretationSource = { beq := Semantics.Lexical.Noun.Relational.Barker2011.instBEqInterpretationSource.beq }

def Semantics.Lexical.Noun.Relational.Barker2011.instBEqInterpretationSource.beq : InterpretationSource → InterpretationSource → Bool

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.instBEqInterpretationSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Lexical.Noun.Relational.Barker2011.canFillRelatum : InterpretationSource → Bool

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.canFillRelatum Semantics.Lexical.Noun.Relational.Barker2011.InterpretationSource.lexicalRelation = true
• Semantics.Lexical.Noun.Relational.Barker2011.canFillRelatum Semantics.Lexical.Noun.Relational.Barker2011.InterpretationSource.appliedPi = true
• Semantics.Lexical.Noun.Relational.Barker2011.canFillRelatum Semantics.Lexical.Noun.Relational.Barker2011.InterpretationSource.noRelation = false

theorem Semantics.Lexical.Noun.Relational.Barker2011.bridging_from_pi {E S : Type} (P : Pred1 E S) (R : Pred2 E S) : canFillRelatum InterpretationSource.appliedPi = true ∧ canFillRelatum InterpretationSource.noRelation = false ∧ canFillRelatum InterpretationSource.lexicalRelation = true

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.Lexical.Noun.Relational.Barker2011.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

instance Semantics.Lexical.Noun.Relational.Barker2011.instDecidableEqPossessionRelationType : DecidableEq PossessionRelationType

Equations

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

def Semantics.Lexical.Noun.Relational.Barker2011.instReprPossessionRelationType.repr : PossessionRelationType → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Noun.Relational.Barker2011.instReprPossessionRelationType : Repr PossessionRelationType

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.instReprPossessionRelationType = { reprPrec := Semantics.Lexical.Noun.Relational.Barker2011.instReprPossessionRelationType.repr }

instance Semantics.Lexical.Noun.Relational.Barker2011.instBEqPossessionRelationType : BEq PossessionRelationType

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.instBEqPossessionRelationType = { beq := Semantics.Lexical.Noun.Relational.Barker2011.instBEqPossessionRelationType.beq }

def Semantics.Lexical.Noun.Relational.Barker2011.instBEqPossessionRelationType.beq : PossessionRelationType → PossessionRelationType → Bool

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.instBEqPossessionRelationType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Lexical.Noun.Relational.Barker2011.relationSource (isNounRelational : Bool) : String

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

Equations

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

def Semantics.Lexical.Noun.Relational.Barker2011.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.Lexical.Noun.Relational.Barker2011.derivation_johns_brother john brother = Semantics.Lexical.Noun.Relational.Barker2011.possessiveRelational john brother

def Semantics.Lexical.Noun.Relational.Barker2011.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.Lexical.Noun.Relational.Barker2011.derivation_johns_cloud john cloud R = Semantics.Lexical.Noun.Relational.Barker2011.possessiveSortal john cloud R

def Semantics.Lexical.Noun.Relational.Barker2011.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.Lexical.Noun.Relational.Barker2011.derivation_na_author author relatum x s = author relatum x s

def Semantics.Lexical.Noun.Relational.Barker2011.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.Lexical.Noun.Relational.Barker2011.derivation_na_seat seat R car = Semantics.Lexical.Noun.Relational.Barker2011.naSemantics seat R car

def Semantics.Lexical.Noun.Relational.Barker2011.derivation_bare_seat {E S : Type} (seat : Pred1 E S) : Pred1 E S

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

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.derivation_bare_seat seat = Semantics.Lexical.Noun.Relational.Barker2011.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.Lexical.Noun.Relational.Barker2011.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.Lexical.Noun.Relational.Barker2011.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)

instance Semantics.Lexical.Noun.Relational.Barker2011.instDecidableEqNominalInterpType : DecidableEq NominalInterpType

Equations

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

def Semantics.Lexical.Noun.Relational.Barker2011.instReprNominalInterpType.repr : NominalInterpType → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Noun.Relational.Barker2011.instReprNominalInterpType : Repr NominalInterpType

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.instReprNominalInterpType = { reprPrec := Semantics.Lexical.Noun.Relational.Barker2011.instReprNominalInterpType.repr }

def Semantics.Lexical.Noun.Relational.Barker2011.instBEqNominalInterpType.beq : NominalInterpType → NominalInterpType → Bool

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.instBEqNominalInterpType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Noun.Relational.Barker2011.instBEqNominalInterpType : BEq NominalInterpType

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.instBEqNominalInterpType = { beq := Semantics.Lexical.Noun.Relational.Barker2011.instBEqNominalInterpType.beq }

def Semantics.Lexical.Noun.Relational.Barker2011.NominalInterpType.hasRelatumSlot : NominalInterpType → Bool

Does this interpretation type have a relatum slot?

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.NominalInterpType.pred1.hasRelatumSlot = false
• Semantics.Lexical.Noun.Relational.Barker2011.NominalInterpType.pred2.hasRelatumSlot = true

def Semantics.Lexical.Noun.Relational.Barker2011.NominalInterpType.canTakePossessor : NominalInterpType → Bool

Can this interpretation type take a possessor?

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.NominalInterpType.pred1.canTakePossessor = false
• Semantics.Lexical.Noun.Relational.Barker2011.NominalInterpType.pred2.canTakePossessor = true

def Semantics.Lexical.Noun.Relational.Barker2011.NominalInterpType.canBridge : NominalInterpType → Bool

Can this interpretation type accommodate bridging?

Equations

• Semantics.Lexical.Noun.Relational.Barker2011.NominalInterpType.pred1.canBridge = false
• Semantics.Lexical.Noun.Relational.Barker2011.NominalInterpType.pred2.canBridge = true

theorem Semantics.Lexical.Noun.Relational.Barker2011.unification_principle (t : NominalInterpType) : t.hasRelatumSlot = t.canTakePossessor ∧ t.canTakePossessor = t.canBridge

hasRelatumSlot ⟺ canTakePossessor ⟺ canBridge.

theorem Semantics.Lexical.Noun.Relational.Barker2011.bridging_is_possession (t : NominalInterpType) : t.canBridge = t.canTakePossessor

Bridging asymmetry = possessive asymmetry.

theorem Semantics.Lexical.Noun.Relational.Barker2011.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.Lexical.Noun.Relational.Barker2011.structural_explanation (t : NominalInterpType) : t.canBridge = true ↔ t.hasRelatumSlot = true

Bridging ↔ having a relatum slot.

noncomputable def Semantics.Lexical.Noun.Relational.Barker2011.possessiveAsNPQ {E : Type} [Fintype E] [DecidableEq E] (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.Lexical.Noun.Relational.Barker2011.possessiveAsNPQ possessor R P = Fintype.elems.toList.any fun (y : E) => R possessor y && P y

theorem Semantics.Lexical.Noun.Relational.Barker2011.possessive_individual_eval {E : Type} (b : E) (P : E → Bool) : 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.