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
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
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
Instances For
Extract the underlying function from a 1-place predicate
Instances For
Extract the underlying function from a 2-place predicate
Instances For
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
- Semantics.Lexical.Determiner.Demonstrative.AhnZhu2025.relationalizer P R = Semantics.Lexical.Determiner.Demonstrative.AhnZhu2025.Pred.pred2 fun (z x : E) (s : S) => P.toPred1 x s && R z x s
Instances For
Notation: π(P, R)
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 → Boolhas a slot for z)
The definition is just: does this arity equal two?
Equations
Instances For
For a specific predicate, can it accommodate a relatum? This just reads off the arity from the type.
Equations
Instances For
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 2: 1-place predicates cannot accommodate relata.
Again, NOT a stipulation — it FOLLOWS from the type. Pred1 has arity one, so canAccommodateRelatum = false.
Theorem 3: 2-place predicates can accommodate relata.
Follows from having arity two.
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)
The noun's denotation at its inherent arity
Instances For
The semantic contribution of a Mandarin definite expression.
We track:
- The resulting predicate (with its arity)
- Whether an external relatum was introduced (by na)
- arity : Arity
The arity of the resulting predicate
The predicate itself
- externalRelatumIntroduced : Bool
Was an external relatum introduced?
Instances For
Bare noun semantics: Just the noun's denotation.
No type change occurs — the arity is whatever the noun lexically has.
Equations
- Semantics.Lexical.Determiner.Demonstrative.AhnZhu2025.bareSemantics n = { arity := n.arity, pred := n.denotation, externalRelatumIntroduced := false }
Instances For
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.
Instances For
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
Instances For
The Ahn & Zhu Main Theorem (Derived Version):
For a SORTAL noun, bare definites cannot relationally bridge, but na definites can.
This is DERIVED from:
- Sortal nouns have arity 1
- Bare semantics preserves arity → arity 1 → no relatum slot
- Na semantics applies π → arity 2 → has relatum slot
The asymmetry emerges from the compositional structure.
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:
- STRUCTURAL FACT:
E → S → Boolhas 1 entity argument - STRUCTURAL FACT:
E → E → S → Boolhas 2 entity arguments - DEFINITION: π conjoins with R, producing a 2-place predicate from 1-place
- DEFINITION: Relatum accommodation requires a slot (= 2nd argument)
- THEOREM: π enables accommodation (because it produces arity 2)
- THEOREM: Bare sortals can't accommodate (because they stay at arity 1)
- 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)
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.
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.
Connection Theorem 1: Our local π matches Barker's π.
This shows the two formalizations are compatible.
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.
The Derivation Chain:
- @cite{barker-2011}: π : Pred1 → Pred2 (type-shifter adds argument)
- @cite{barker-2011}: Pred2 has a relatum slot (the extra argument)
- @cite{ahn-zhu-2025}: Mandarin na applies π
- THEREFORE: na creates a relatum slot
- 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 #
- Shared Foundation: Both modules use the same Pred1/Pred2 distinction
- Explicit Derivation: Ahn & Zhu's results cite Barker's
- No Redundancy: The core insight (π adds argument) is proved ONCE in Barker
- 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.