Hanink (2021): DP Structure and Internally Headed Relatives in Wášiw

[Han21]

The architectural claim of [Han21] (developing the framework of Hanink 2018) is that the resource situation evaluating a definite description's restrictor is a bound variable in the syntactic structure — a "situation pronoun" — rather than a free contextual parameter handed to the interpretation function. The resource situation is selected by an index inside DP, not by the matrix context, and that index can be bound by higher operators.

What this file tests

The IL substrate operationalizes this in two parallel pieces:

• SitAssignment W := Nat → W in Intensional.Variables is the situation-pronoun assignment, parallel to the entity assignment.
• Description.unique R sIdx in Semantics.Definiteness.Description carries a situationIdx : Nat recording which situation pronoun the description is bound to.

The empirical payoff is that the same description can pick out different referents under different situation assignments. We test this with a two-room frame where "the table" picks out different tables depending on which resource situation the structure is bound to.

We additionally verify:

1. Restrictor sensitivity to the situation assignment — a restrictor that consults interpSitPronoun returns different extensions under different gs.
2. Index-record discipline — the surface interpretation function ignores the index (it just records which pronoun is bound, the gs does the work), but the usesSituationPronoun classifier correctly flags unique and demonstrative as the binders.
3. Anaphoric vs. unique split — anaphoric definites consult the entity assignment (the antecedent index), so the situation assignment is irrelevant for them. This contrasts with unique, matching the Schwarz weak/strong split.

inductive Hanink2021.Item : Type

Two tables, one in each room. The "the table" diagnostic in [Han21]'s style: shifting the bound resource situation flips the referent.

• tableKitchen : Item
• tableLiving : Item

@[implicit_reducible]

instance Hanink2021.instDecidableEqItem : DecidableEq Item

Equations

• Hanink2021.instDecidableEqItem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Hanink2021.instReprItem : Repr Item

Equations

• Hanink2021.instReprItem = { reprPrec := Hanink2021.instReprItem.repr }

def Hanink2021.instReprItem.repr : Item → ℕ → Std.Format

Equations

• Hanink2021.instReprItem.repr Hanink2021.Item.tableKitchen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hanink2021.Item.tableKitchen")).group prec✝
• Hanink2021.instReprItem.repr Hanink2021.Item.tableLiving prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hanink2021.Item.tableLiving")).group prec✝

inductive Hanink2021.Room : Type

Two rooms, each its own situation.

• kitchen : Room
• living : Room

@[implicit_reducible]

instance Hanink2021.instDecidableEqRoom : DecidableEq Room

Equations

• Hanink2021.instDecidableEqRoom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hanink2021.instReprRoom.repr : Room → ℕ → Std.Format

Equations

• Hanink2021.instReprRoom.repr Hanink2021.Room.kitchen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hanink2021.Room.kitchen")).group prec✝
• Hanink2021.instReprRoom.repr Hanink2021.Room.living prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hanink2021.Room.living")).group prec✝

@[implicit_reducible]

instance Hanink2021.instReprRoom : Repr Room

Equations

• Hanink2021.instReprRoom = { reprPrec := Hanink2021.instReprRoom.repr }

def Hanink2021.tableIn : Room → Item → Prop

"Table-in-room": the predicate is true at exactly one item per room. Encodes the [Han21] resource-situation idea — what counts as "the table" depends on the situation we evaluate at.

Equations

• Hanink2021.tableIn Hanink2021.Room.kitchen Hanink2021.Item.tableKitchen = True
• Hanink2021.tableIn Hanink2021.Room.kitchen x✝ = False
• Hanink2021.tableIn Hanink2021.Room.living Hanink2021.Item.tableLiving = True
• Hanink2021.tableIn Hanink2021.Room.living x✝ = False

def Hanink2021.tableAtSit0 : Intensional.Variables.DenotGS Item Room Intensional.Ty.et

The restrictor the table at the situation pointed to by pronoun 0: a DenotGS that consults interpSitPronoun 0 to fetch the resource situation, then evaluates tableIn at that situation.

This is the [Han21] situation-pronoun pattern: the structural index 0 selects which situation in gs to use.

Equations

• Hanink2021.tableAtSit0 _g gs x = Hanink2021.tableIn (Intensional.Variables.interpSitPronoun 0 gs) x

def Hanink2021.g₀ : Core.Assignment Item

A trivial entity assignment. Entity binding is not exercised here.

Equations

• Hanink2021.g₀ x✝ = Hanink2021.Item.tableKitchen

def Hanink2021.gsKitchen : Intensional.Variables.SitAssignment Room

Situation assignment with pronoun 0 ↦ kitchen.

Equations

• Hanink2021.gsKitchen x✝ = Hanink2021.Room.kitchen

def Hanink2021.gsLiving : Intensional.Variables.SitAssignment Room

Situation assignment with pronoun 0 ↦ living.

Equations

• Hanink2021.gsLiving x✝ = Hanink2021.Room.living

theorem Hanink2021.tableAtSit0_existsUnique_kitchen : ∃! x : Item, tableAtSit0 g₀ gsKitchen x

Restrictor uniqueness in the kitchen situation: only tableKitchen satisfies tableAtSit0.

theorem Hanink2021.tableAtSit0_existsUnique_living : ∃! x : Item, tableAtSit0 g₀ gsLiving x

Restrictor uniqueness in the living-room situation: only tableLiving satisfies tableAtSit0.

theorem Hanink2021.theTable_kitchen : Semantics.Definiteness.interpret (Semantics.Definiteness.Description.unique tableAtSit0 0) g₀ gsKitchen = some Item.tableKitchen

Witness extraction for the kitchen case: the unique satisfier is tableKitchen.

theorem Hanink2021.theTable_living : Semantics.Definiteness.interpret (Semantics.Definiteness.Description.unique tableAtSit0 0) g₀ gsLiving = some Item.tableLiving

Witness extraction for the living-room case: the unique satisfier is tableLiving.

theorem Hanink2021.same_description_different_referents : Semantics.Definiteness.interpret (Semantics.Definiteness.Description.unique tableAtSit0 0) g₀ gsKitchen ≠ Semantics.Definiteness.interpret (Semantics.Definiteness.Description.unique tableAtSit0 0) g₀ gsLiving

The Hanink payoff: the same .unique description picks out different referents under different situation assignments. The description is one syntactic object; the resource situation is a bound variable, not a free parameter.

theorem Hanink2021.unique_index_does_not_alter_referent_directly : Semantics.Definiteness.interpret (Semantics.Definiteness.Description.unique tableAtSit0 0) g₀ gsKitchen = Semantics.Definiteness.interpret (Semantics.Definiteness.Description.unique tableAtSit0 7) g₀ gsKitchen

The index argument to .unique does not select among situations at the interpretation layer — the restrictor R already takes the full situation assignment, and the index records which pronoun is bound. (Semantics.Definiteness.interpret_unique_index_irrelevant makes this explicit.) The Hanink claim is recovered via the restrictor calling interpSitPronoun sIdx, not via the interpreter inspecting sIdx.

theorem Hanink2021.situation_binders_classified (R : Intensional.Variables.DenotGS Item Room Intensional.Ty.et) (deictic : Features.Deixis.Feature) (sIdx d : ℕ) : (Semantics.Definiteness.Description.unique R sIdx).usesSituationPronoun = true ∧ (Semantics.Definiteness.Description.demonstrative R deictic sIdx d).usesSituationPronoun = true ∧ (Semantics.Definiteness.Description.anaphoric R d).usesSituationPronoun = false ∧ (Semantics.Definiteness.Description.bare R).usesSituationPronoun = false ∧ (Semantics.Definiteness.Description.indefinite R).usesSituationPronoun = false

Among Description constructors, exactly unique and demonstrative are flagged as binding a structural situation pronoun. Anaphoric definites do not — they consult the entity assignment for an antecedent, not the situation assignment.

theorem Hanink2021.anaphoric_independent_of_situation (R : Intensional.Variables.DenotGS Item Room Intensional.Ty.et) (d : ℕ) (hgs : R g₀ gsKitchen = R g₀ gsLiving) : Semantics.Definiteness.interpret (Semantics.Definiteness.Description.anaphoric R d) g₀ gsKitchen = Semantics.Definiteness.interpret (Semantics.Definiteness.Description.anaphoric R d) g₀ gsLiving

Anaphoric definites consult the entity assignment for the antecedent. When the restrictor itself is situation-insensitive (R g₀ gsKitchen = R g₀ gsLiving), the anaphoric reading is invariant under the resource-situation assignment — its referent is determined by the entity slot g₀ d. This is the orthogonality of entity-assignment binding and situation-assignment binding in [Han21]'s architecture: the anaphoric layer reads from g, the unique layer reads from gs.

theorem Hanink2021.anaphoric_const_restrictor_situation_insensitive (d : ℕ) : Semantics.Definiteness.interpret (Semantics.Definiteness.Description.anaphoric (Intensional.Variables.DenotGS.const fun (x : Intensional.Denot Item Room Intensional.Ty.e) => True) d) g₀ gsKitchen = Semantics.Definiteness.interpret (Semantics.Definiteness.Description.anaphoric (Intensional.Variables.DenotGS.const fun (x : Intensional.Denot Item Room Intensional.Ty.e) => True) d) g₀ gsLiving

Concrete instance: with a constant restrictor (the antecedent is self-identifying, no situation needed), anaphoric definites are insensitive to the resource-situation assignment.

[Han21] is the theory hub for the demonstrative pronoun (Syntax/Pronoun/Demonstrative): a demonstrative is the bare anaphoric idx (Hanink's Washo gí; [Elb05] pronouns-as-definites) plus a deictic feature realized as a presupposition on D. The lexical DemonstrativePronoun supplies its proximal/distal deixis via the Demonstrative capability; the restrictor and indices come from context.

def Hanink2021.demDescription {E W : Type} (p : DemonstrativePronoun) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx d : ℕ) : Semantics.Definiteness.Description E W

The denotation of a demonstrative pronoun: Description.demonstrative over a context restrictor, with the pronoun's deictic feature as the presupposition on D ([Han21] (34)/(35)).

Equations

• Hanink2021.demDescription p R sIdx d = Semantics.Definiteness.Description.demonstrative R p.deixis sIdx d

theorem Hanink2021.demDescription_eq_anaphoric {E W : Type} (p : DemonstrativePronoun) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx d : ℕ) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : Semantics.Definiteness.interpret (demDescription p R sIdx d) g gs = Semantics.Definiteness.interpret (Semantics.Definiteness.Description.anaphoric R d) g gs

A demonstrative pronoun picks the same referent as a plain anaphoric definite: its deixis is a presupposition filter, not a referent selector ([Han21]). The Pronoun-API capability Demonstrative.deixis is exactly the presupposition that drops out of referent selection.

theorem Hanink2021.der_strong_vs_demonstrative {E W : Type} (p : DemonstrativePronoun) (hdist : (Demonstrative.deixis p).EncodesDistance) (R : Intensional.Variables.DenotGS E W Intensional.Ty.et) (sIdx d : ℕ) (g : Core.Assignment E) (gs : Intensional.Variables.SitAssignment W) : Semantics.Definiteness.interpret (demDescription p R sIdx d) g gs = Semantics.Definiteness.interpret (Semantics.Definiteness.Description.anaphoric R d) g gs ∧ (Demonstrative.deixis p).EncodesDistance

[PGG17]'s orthogonality, now grounded in meaning (and stated in the later study, per chronology): German der — the strong-article personal pronoun, an anaphoric definite with no deixis — and a demonstrative pronoun pick the same referent (both anaphoric over d), yet only the demonstrative carries a deictic feature. Article-strength ⊥ demonstrativehood: PG&G's "der is not a Demonstrative" is a semantic fact, not just typing.