Ahn & Zhu (2025): A bridge to definiteness

[AZ25c]

Mandarin lacks a definite article; it marks definiteness with bare nouns and with demonstrative descriptions (na-CL-N). [AZ25c] use bridging — the licensing of a definite whose referent was not introduced in the context — to probe which mechanism underlies each form, and propose that the demonstrative na is a relationalizing definite.

The analysis (eq. 48, eq. 44a)

The paper's denotations are built on [Sch09b]'s situation-semantic definite article and [Jen18]'s ι type-shifter; [Bar11]'s relationalizer π and detransitivizer Ex (and [VJ02]'s Prag) supply the relational sub-component. Writing sᵣ for the resource situation:

• bare definite (eq. 44a): ⟦bare P⟧ = λsᵣ. ιx[P(x)(sᵣ)] — the unique P in sᵣ (situational uniqueness; Schwarz-weak).
• na definite (eq. 48): ⟦na P⟧ = λsᵣ. λz. ιx[π(P)(z)(x)(sᵣ)] = ιx[P(x)(sᵣ) ∧ R(z,x)(sᵣ)] — the unique x that is P and bears the contextual relation R to the index z. Here ι (uniqueness) is the definiteness; π (relationalization) is what na adds.

Layered grounding

This file is a thin consumer of Semantics/Possessive/Relational.lean (Barker's π, Ex, iotaPresupposition, naSemantics, bareSemantics, CanFillRelatum). It does not re-implement them. ι is modelled by the substrate's iotaPresupposition (the existence-and-uniqueness presupposition a definite carries); the felicity of a definite is the holding of that presupposition.

Main results

• na_restores_uniqueness — the keystone. When a sortal noun P is not situationally unique (≥ 2 satisfiers), the bare definite's uniqueness presupposition fails, but adding R(z, ·) via π (= na) narrows the extension to a singleton, so the na definite is felicitous. The bridging asymmetry is a consequence of π restoring uniqueness, not a stipulation.
• relational_bare_felicitous — a lexically relational noun supplies its own relatum (eq. 57–58: covert possessor / Mandarin argument-drop), so bare bridging is licensed without na.
• bridge_licensed_iff — the Study-4 2×2 as a derived fact over the substrate's CanFillRelatum: relational bridging is licensed iff na applies or the noun is lexically relational (i.e. fails exactly at bare + non-relational).
• diverges_from_jenks_on_bare_relational — [AZ25c] vs [Jen18]: Ahn & Zhu license bare relational bridging, whereas Jenks's Index! (Maximize Presupposition) strictly prefers the indexed na form whenever an antecedent is available. The two accounts assign opposite status to the bare relational cell.

The two definite-forming routes (eq. 44a, eq. 48)

def AhnZhu2025.bareDefiniteFelicitous {E : Type u_1} {S : Type u_2} (P : ArgumentStructure.Relational.Pred1 E S) (s : S) : Prop

Felicity of a bare definite (eq. 44a): the uniqueness presupposition of the noun alone. bare P denotes the unique x with P x in s — situational uniqueness (Schwarz-weak / [Jen18]'s ι).

Equations

• AhnZhu2025.bareDefiniteFelicitous P s = ArgumentStructure.Relational.iotaPresupposition (ArgumentStructure.Relational.bareSemantics P) s

def AhnZhu2025.naDefiniteFelicitous {E : Type u_1} {S : Type u_2} (P : ArgumentStructure.Relational.Pred1 E S) (R : ArgumentStructure.Relational.Pred2 E S) (z : E) (s : S) : Prop

Felicity of a na definite (eq. 48): the uniqueness presupposition of the relationalized predicate π P R. na P (with index z) denotes the unique x with P x ∧ R z x in s. The ι is the definiteness; the π is what na adds.

Equations

• AhnZhu2025.naDefiniteFelicitous P R z s = ArgumentStructure.Relational.iotaPresupposition (ArgumentStructure.Relational.naSemantics P R z) s

The relationalizer restores uniqueness

theorem AhnZhu2025.na_restores_uniqueness {E : Type u_1} {S : Type u_2} (P : ArgumentStructure.Relational.Pred1 E S) (R : ArgumentStructure.Relational.Pred2 E S) (z : E) (s : S) (hAmbiguous : ∃ (a : E) (b : E), a ≠ b ∧ P a s ∧ P b s) (hDisambiguated : ∃! x : E, P x s ∧ R z x s) : ¬bareDefiniteFelicitous P s ∧ naDefiniteFelicitous P R z s

Keystone. A sortal noun P that is not situationally unique (two distinct satisfiers) cannot head a bare definite — its uniqueness presupposition fails. But na conjoins the contextual relation R(z, ·) via π, and if that narrows the extension to a singleton, the na definite is felicitous.

This is [AZ25c]'s bridging asymmetry derived from the denotations: the gap between bare and na is π restoring the ι presupposition, not a stipulation.

theorem AhnZhu2025.relational_bare_felicitous {E : Type u_1} {S : Type u_2} (Rel : ArgumentStructure.Relational.Pred2 E S) (z : E) (s : S) (hUnique : ∃! x : E, Rel z x s) : bareDefiniteFelicitous (fun (x : E) => Rel z x) s

A lexically relational noun (a Pred2) supplies its own relatum: with the antecedent z filling the internal argument (eq. 57–58: covert possessor / Mandarin argument-drop), the bare definite's uniqueness presupposition can be met without na. This is why bare relational bridging is licensed.

The bridging asymmetry as InterpretationSource (Study 4)

def AhnZhu2025.bridgeSource (lexicallyRelational naApplies : Bool) : ArgumentStructure.Relational.InterpretationSource

The interpretation source of a bridged definite, computed from whether the noun is lexically relational and whether na (π) applies. The source is derived, not stipulated: it is the substrate's InterpretationSource.

Equations

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

theorem AhnZhu2025.bridge_licensed_iff (lexRel naApp : Bool) : ArgumentStructure.Relational.CanFillRelatum (bridgeSource lexRel naApp) ↔ naApp = true ∨ lexRel = true

Study 4, derived. Relational bridging is licensed (CanFillRelatum) exactly when na applies or the noun is lexically relational — i.e. it fails only in the bare + non-relational cell. This is the 2×2 that [AZ25c]'s Study 4 confirms, read off the computed InterpretationSource.

theorem AhnZhu2025.bare_nonrelational_cannot_bridge : ¬ArgumentStructure.Relational.CanFillRelatum (bridgeSource false false)

The decisive Study-4 cell: a bare, non-relational noun cannot relationally bridge — no na, no lexical relation, so no relatum slot.

Shared bridging split ([Sch09b] / [Jen18])

theorem AhnZhu2025.inherits_schwarz_bridging_split : Features.Definiteness.bridgingPresupType Features.Definiteness.BridgingSubtype.partWhole = Features.Definiteness.DefPresupType.uniqueness ∧ Features.Definiteness.bridgingPresupType Features.Definiteness.BridgingSubtype.relational = Features.Definiteness.DefPresupType.familiarity

[AZ25c] inherit Schwarz's bridging split, shared with [Jen18] via the common Features.Definiteness.bridgingPresupType: part-whole bridging is the uniqueness route (bare ι; bare nouns suffice), relational bridging the familiarity route (the relatum index; na or a lexical relation).

Divergence from [Jen18]

theorem AhnZhu2025.diverges_from_jenks_on_bare_relational {E : Type u_1} {S : Type u_2} (Rel : ArgumentStructure.Relational.Pred2 E S) (z : E) (s : S) (hUnique : ∃! x : E, Rel z x s) : bareDefiniteFelicitous (fun (x : E) => Rel z x) s ∧ Jenks2018.indexConstraint { isIndexed := true, indexAvailable := true } < Jenks2018.indexConstraint { isIndexed := false, indexAvailable := true }

Divergence from [Jen18] (the comparison [AZ25c] §4 draws).

Ahn & Zhu license a bare relational definite: a lexically relational noun supplies its own relatum, so the uniqueness presupposition is met without na (relational_bare_felicitous).

[Jen18]'s Index! (a Maximize-Presupposition instance) instead requires the indexed na form whenever an antecedent is available — so it strictly disprefers the bare form in exactly this cell (Jenks2018.index_prefers_indexed_when_available).

The two accounts thus assign opposite status to the bare relational-bridging form: Ahn & Zhu predict it licensed; Jenks predicts it blocked. Both halves below are derived from each account's own machinery.

Data: the bridging felicity rows (Data/Examples/AhnZhu2025.json)

theorem AhnZhu2025.naCL_rows_acceptable (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.feature? "definite_form" = some "naCL" → row.judgment = Features.Judgment.acceptable

na-CL is acceptable in every condition (both bridging types, both noun types) — na itself is the relationalizer, so it always supplies the relatum slot (bridge_licensed_iff, naApp = true).

theorem AhnZhu2025.bare_relational_noun_bridges (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.feature? "definite_form" = some "bare" → row.feature? "bridging_type" = some "relational" → row.feature? "noun_arity" = some "relational" → row.judgment = Features.Judgment.acceptable

Bare + relational noun bridges (Study 4): the lexically 2-place noun supplies its own relatum (relational_bare_felicitous).

theorem AhnZhu2025.bare_nonrelational_noun_degraded (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.feature? "definite_form" = some "bare" → row.feature? "bridging_type" = some "relational" → row.feature? "noun_arity" = some "sortal" → row.judgment = Features.Judgment.marginal

The decisive Study-4 cell. Bare + non-relational noun in relational bridging is degraded — a bare noun licenses relational bridging only if the noun is lexically relational (bare_nonrelational_cannot_bridge). Marginal, not out: the cell is rated below its rivals but not at floor.

theorem AhnZhu2025.english_that_degraded (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.feature? "definite_form" = some "that" → row.judgment = Features.Judgment.marginal

English demonstrative that is degraded but not ungrammatical in bridging (Study 2): economy-blocked because the definite competes, not a hard constraint. Modelled as .marginal (the paper's gradient ~4.3–5.0/7 finding), in contrast to English the, which is acceptable.

theorem AhnZhu2025.english_the_acceptable (row : Data.Examples.LinguisticExample) : row ∈ Examples.all → row.feature? "definite_form" = some "the" → row.judgment = Features.Judgment.acceptable

English definite the bridges freely (Study 2 baseline).