inductive Phenomena.Reference.Studies.AhnZhu2025.Arity : Type

The arity of a predicate — how many entity arguments it takes.

This is linguistically meaningful:

• Arity 1: Sortal nouns (dog, book, seat)
• Arity 2: Relational nouns (author, mother) or relationalized predicates

• one : Arity
• two : Arity

@[implicit_reducible]

instance Phenomena.Reference.Studies.AhnZhu2025.instDecidableEqArity : DecidableEq Arity

Equations

• Phenomena.Reference.Studies.AhnZhu2025.instDecidableEqArity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Reference.Studies.AhnZhu2025.instReprArity : Repr Arity

Equations

• Phenomena.Reference.Studies.AhnZhu2025.instReprArity = { reprPrec := Phenomena.Reference.Studies.AhnZhu2025.instReprArity.repr }

def Phenomena.Reference.Studies.AhnZhu2025.instReprArity.repr : Arity → ℕ → Std.Format

Equations

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

inductive Phenomena.Reference.Studies.AhnZhu2025.Pred (E S : Type) : Arity → Type

A predicate with its arity tracked in the type.

This is the key to making the formalization explanatory: we can see from the TYPE whether a predicate has a relatum slot.

• pred1 {E S : Type} : (E → S → Bool) → Pred E S Arity.one

  1-place predicate: λx.λs. P(x)(s)

• pred2 {E S : Type} : (E → E → S → Bool) → Pred E S Arity.two

  2-place predicate: λz.λx.λs. P(z,x)(s) where z is the relatum

def Phenomena.Reference.Studies.AhnZhu2025.Pred.toPred1 {E S : Type} : Pred E S Arity.one → E → S → Bool

Extract the underlying function from a 1-place predicate

Equations

• (Phenomena.Reference.Studies.AhnZhu2025.Pred.pred1 f).toPred1 = f

def Phenomena.Reference.Studies.AhnZhu2025.Pred.toPred2 {E S : Type} : Pred E S Arity.two → E → E → S → Bool

Extract the underlying function from a 2-place predicate

Equations

• (Phenomena.Reference.Studies.AhnZhu2025.Pred.pred2 f).toPred2 = f

def Phenomena.Reference.Studies.AhnZhu2025.relationalizer {E S : Type} (P : Pred E S Arity.one) (R : E → E → S → Bool) : Pred E S Arity.two

Barker's Relationalizer π

π : Pred1 → Pred2

This is the KEY operation. It takes a 1-place predicate and returns a 2-place predicate by conjoining with a contextual relation R.

π(P) = λz.λx.λs. P(x)(s) ∧ R(z,x)(s)

Crucially, π CHANGES THE TYPE: it takes Arity.one and produces Arity.two. This type change is what creates the relatum slot.

Equations

• Phenomena.Reference.Studies.AhnZhu2025.relationalizer P R = Phenomena.Reference.Studies.AhnZhu2025.Pred.pred2 fun (z x : E) (s : S) => P.toPred1 x s && R z x s

def Phenomena.Reference.Studies.AhnZhu2025.«termπ(_,_)» : Lean.ParserDescr

Notation: π(P, R)

Equations

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

def Phenomena.Reference.Studies.AhnZhu2025.Arity.canAccommodateRelatum : Arity → Bool

Relatum Accommodation: Can this arity accommodate a relatum argument?

This is defined STRUCTURALLY by the arity, not stipulated:

• Arity 1 → NO (there's no slot in the type E → S → Bool)
• Arity 2 → YES (the type E → E → S → Bool has a slot for z)

The definition is just: does this arity equal two?

Equations

• Phenomena.Reference.Studies.AhnZhu2025.Arity.one.canAccommodateRelatum = false
• Phenomena.Reference.Studies.AhnZhu2025.Arity.two.canAccommodateRelatum = true

def Phenomena.Reference.Studies.AhnZhu2025.Pred.canAccommodateRelatum {E S : Type} {a : Arity} : Pred E S a → Bool

For a specific predicate, can it accommodate a relatum? This just reads off the arity from the type.

Equations

• x✝.canAccommodateRelatum = a.canAccommodateRelatum

theorem Phenomena.Reference.Studies.AhnZhu2025.pi_enables_relatum_accommodation {E S : Type} (P : Pred E S Arity.one) (R : E → E → S → Bool) : (relationalizer P R).canAccommodateRelatum = true

Theorem 1: π enables relatum accommodation.

This is NOT a stipulation — it FOLLOWS from π's type signature. π produces a Pred2, and Pred2 has arity two, so canAccommodateRelatum = true.

The proof is rfl because it's a consequence of the compositional structure.

theorem Phenomena.Reference.Studies.AhnZhu2025.pred1_cannot_accommodate_relatum {E S : Type} (P : Pred E S Arity.one) : P.canAccommodateRelatum = false

Theorem 2: 1-place predicates cannot accommodate relata.

Again, NOT a stipulation — it FOLLOWS from the type. Pred1 has arity one, so canAccommodateRelatum = false.

theorem Phenomena.Reference.Studies.AhnZhu2025.pred2_can_accommodate_relatum {E S : Type} (P : Pred E S Arity.two) : P.canAccommodateRelatum = true

Theorem 3: 2-place predicates can accommodate relata.

Follows from having arity two.

structure Phenomena.Reference.Studies.AhnZhu2025.Noun (E S : Type) : Type

A noun's lexical entry specifies its inherent arity.

• Sortal nouns (dog, seat, book): lexically 1-place
• Relational nouns (author, mother, part): lexically 2-place

This is a LEXICAL property, not derived from composition.

• form : String

  The noun form

• arity : Arity

  The noun's inherent arity (lexical property)

• denotation : Pred E S self.arity

  The noun's denotation at its inherent arity

def Phenomena.Reference.Studies.AhnZhu2025.Noun.sortal {E S : Type} (form : String) (P : E → S → Bool) : Noun E S

Convenient constructor for sortal nouns

Equations

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

def Phenomena.Reference.Studies.AhnZhu2025.Noun.relational {E S : Type} (form : String) (P : E → E → S → Bool) : Noun E S

Convenient constructor for relational nouns

Equations

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

structure Phenomena.Reference.Studies.AhnZhu2025.DefiniteSemantics (E S : Type) : Type

The semantic contribution of a Mandarin definite expression.

We track:

1. The resulting predicate (with its arity)
2. Whether an external relatum was introduced (by na)

• arity : Arity

  The arity of the resulting predicate

• pred : Pred E S self.arity

  The predicate itself

• externalRelatumIntroduced : Bool

  Was an external relatum introduced?

def Phenomena.Reference.Studies.AhnZhu2025.bareSemantics {E S : Type} (n : Noun E S) : DefiniteSemantics E S

Bare noun semantics: Just the noun's denotation.

No type change occurs — the arity is whatever the noun lexically has.

Equations

• Phenomena.Reference.Studies.AhnZhu2025.bareSemantics n = { arity := n.arity, pred := n.denotation, externalRelatumIntroduced := false }

def Phenomena.Reference.Studies.AhnZhu2025.naSemantics {E S : Type} (n : Noun E S) (R : E → E → S → Bool) : DefiniteSemantics E S

Na semantics: Apply π to the noun (if sortal), introducing external relatum.

This is where the type change happens:

• Sortal noun (arity 1) → π → arity 2
• Relational noun (arity 2) → already has slot, π adds another

For simplicity, we model na as always applying π to sortal nouns.

Equations

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

def Phenomena.Reference.Studies.AhnZhu2025.DefiniteSemantics.canRelationalBridge {E S : Type} (sem : DefiniteSemantics E S) : Bool

Relational bridging requires accommodating an antecedent as relatum.

This is possible iff the semantic representation has a relatum slot, which is iff the arity is 2.

Equations

• sem.canRelationalBridge = sem.arity.canAccommodateRelatum

theorem Phenomena.Reference.Studies.AhnZhu2025.ahn_zhu_derived {E S : Type} (n : Noun E S) (R : E → E → S → Bool) (hSortal : n.arity = Arity.one) : (bareSemantics n).canRelationalBridge = false ∧ (naSemantics n R).canRelationalBridge = true

The Ahn & Zhu Main Theorem (Derived Version):

For a SORTAL noun, bare definites cannot relationally bridge, but na definites can.

This is DERIVED from:

1. Sortal nouns have arity 1
2. Bare semantics preserves arity → arity 1 → no relatum slot
3. Na semantics applies π → arity 2 → has relatum slot

The asymmetry emerges from the compositional structure.

theorem Phenomena.Reference.Studies.AhnZhu2025.bridging_asymmetry_is_structural {E S : Type} (n : Noun E S) (R : E → E → S → Bool) (hSortal : n.arity = Arity.one) : (bareSemantics n).canRelationalBridge ≠ (naSemantics n R).canRelationalBridge

Corollary: The bridging asymmetry is a STRUCTURAL consequence.

The difference between bare and na is not stipulated — it follows from the fact that π changes the arity, creating a relatum slot where none existed.

The Explanatory Chain:

1. STRUCTURAL FACT: E → S → Bool has 1 entity argument
2. STRUCTURAL FACT: E → E → S → Bool has 2 entity arguments
3. DEFINITION: π conjoins with R, producing a 2-place predicate from 1-place
4. DEFINITION: Relatum accommodation requires a slot (= 2nd argument)
5. THEOREM: π enables accommodation (because it produces arity 2)
6. THEOREM: Bare sortals can't accommodate (because they stay at arity 1)
7. THEOREM: The asymmetry follows from π's type-changing nature

The bridging facts are not stipulated — they emerge from the interaction of:

• Lexical arity (sortal vs relational nouns)
• Compositional operations (π changes arity)
• Structural requirements (bridging needs a slot)

theorem Phenomena.Reference.Studies.AhnZhu2025.relatum_slot_is_second_argument {E S : Type} (P : Pred E S Arity.one) (R : E → E → S → Bool) (z x : E) (s : S) : (relationalizer P R).toPred2 z x s = (P.toPred1 x s && R z x s)

Key insight: The relatum slot is not a semantic primitive — it's the second argument position in a 2-place predicate.

"Having a relatum slot" = "having type E → E → S → Bool" "Lacking a relatum slot" = "having type E → S → Bool"

π creates the slot by changing the type.

This analysis explains the empirical patterns in Phenomena/Anaphora/Bridging.lean:

Noun Type	Form	Has Relatum Slot?	Relational Bridging?
Sortal	bare	No (arity 1)	No
Sortal	na	Yes (π → arity 2)	Yes
Relational	bare	Yes (arity 2)	Yes
Relational	na	Yes (arity 2)	Yes

The pattern falls out from composition, not stipulation.

theorem Phenomena.Reference.Studies.AhnZhu2025.relational_bare_can_bridge {E S : Type} (n : Noun E S) (hRelational : n.arity = Arity.two) : (bareSemantics n).canRelationalBridge = true

Relational nouns can bridge even when bare (they lexically have arity 2)

theorem Phenomena.Reference.Studies.AhnZhu2025.complete_bridging_pattern {E S : Type} (n : Noun E S) (R : E → E → S → Bool) : (n.arity = Arity.one → (bareSemantics n).canRelationalBridge = false) ∧ (n.arity = Arity.one → (naSemantics n R).canRelationalBridge = true) ∧ (n.arity = Arity.two → (bareSemantics n).canRelationalBridge = true) ∧ (n.arity = Arity.two → (naSemantics n R).canRelationalBridge = true)

The complete pattern: bridging licensing by form and noun type

What Makes This Explanatory

Previous Version (Stipulative)

def naCanBridge := true
def bareCanBridge (n) := n.isRelational
theorem na_can_bridge : naCanBridge = true := rfl

This Version (Derived)

-- Types encode structure
inductive Pred E S : Arity → Type where
  | pred1 : (E → S → Bool) → Pred E S.one
  | pred2 : (E → E → S → Bool) → Pred E S.two

-- π changes the type (adds argument)
def π(P, R) : Pred E S.two :=...

-- Accommodation is structural
def canAccommodate a := a ==.two

-- Theorems FOLLOW from type structure
theorem pi_enables : (π(P, R)).canAccommodate = true := rfl
theorem pred1_cannot : P.canAccommodate = false := rfl -- P : Pred E S.one

The Difference

In the derived version:

• The arity IS the relatum slot (not a separate property)
• π demonstrably changes the arity (visible in types)
• Bridging licensing follows from arity, which follows from composition
• Nothing is stipulated about bridging — it emerges from structure

This is Barker's insight formalized: the relationalizer creates structure that wasn't there before. The formalization makes this structural change visible and proves bridging licensing as a consequence.

Cumulative Integration with @cite{barker-2011}

This section shows how Ahn & Zhu's analysis DERIVES from Barker's framework. Rather than re-proving everything, we show the correspondence.

theorem Phenomena.Reference.Studies.AhnZhu2025.local_pi_matches_barker {E S : Type} (P : E → S → Bool) (R : E → E → S → Bool) (z x : E) (s : S) : (relationalizer (Pred.pred1 P) R).toPred2 z x s = Semantics.ArgumentStructure.Relational.π P R z x s

Connection Theorem 1: Our local π matches Barker's π.

This shows the two formalizations are compatible.

theorem Phenomena.Reference.Studies.AhnZhu2025.bridging_from_barker {E S : Type} (P : E → S → Bool) (R : E → E → S → Bool) : Semantics.ArgumentStructure.Relational.CanFillRelatum Semantics.ArgumentStructure.Relational.InterpretationSource.appliedPi

Connection Theorem 2: Bridging licensing derives from Barker's framework.

Ahn & Zhu's claim that na enables bridging for sortal nouns follows from Barker's claim that π creates a relatum slot.

theorem Phenomena.Reference.Studies.AhnZhu2025.derivation_chain {E S : Type} : Semantics.ArgumentStructure.Relational.CanFillRelatum Semantics.ArgumentStructure.Relational.InterpretationSource.appliedPi ∧ ¬Semantics.ArgumentStructure.Relational.CanFillRelatum Semantics.ArgumentStructure.Relational.InterpretationSource.noRelation

The Derivation Chain:

1. @cite{barker-2011}: π : Pred1 → Pred2 (type-shifter adds argument)
2. @cite{barker-2011}: Pred2 has a relatum slot (the extra argument)
3. @cite{ahn-zhu-2025}: Mandarin na applies π
4. THEREFORE: na creates a relatum slot
5. THEREFORE: na enables relational bridging

The Ahn & Zhu result is not stipulated — it follows from Barker's framework applied to Mandarin demonstratives.

What Makes This Cumulative

1. Shared Foundation: Both modules use the same Pred1/Pred2 distinction
2. Explicit Derivation: Ahn & Zhu's results cite Barker's
3. No Redundancy: The core insight (π adds argument) is proved ONCE in Barker
4. Extensibility: New papers can build on both, inheriting all results

This is how a library grows cumulatively: later work builds on earlier work, creating a web of interconnected results rather than isolated modules.