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

@cite{hanink-2021}

The architectural claim of @cite{hanink-2021} (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 F := Nat → F.Index in Core.Logic.Intensional.Variables is the situation-pronoun assignment, parallel to the entity assignment.
• NominalKind.unique R sIdx in Core.Nominal.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 Phenomena.Definiteness.Studies.Hanink2021.Item : Type

Two tables, one in each room. The "the table" diagnostic in @cite{hanink-2021}'s style: shifting the bound resource situation flips the referent.

• tableKitchen : Item
• tableLiving : Item

@[implicit_reducible]

instance Phenomena.Definiteness.Studies.Hanink2021.instDecidableEqItem : DecidableEq Item

Equations

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

def Phenomena.Definiteness.Studies.Hanink2021.instReprItem.repr : Item → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Definiteness.Studies.Hanink2021.instReprItem : Repr Item

Equations

• Phenomena.Definiteness.Studies.Hanink2021.instReprItem = { reprPrec := Phenomena.Definiteness.Studies.Hanink2021.instReprItem.repr }

inductive Phenomena.Definiteness.Studies.Hanink2021.Room : Type

Two rooms, each its own situation.

• kitchen : Room
• living : Room

@[implicit_reducible]

instance Phenomena.Definiteness.Studies.Hanink2021.instDecidableEqRoom : DecidableEq Room

Equations

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

@[implicit_reducible]

instance Phenomena.Definiteness.Studies.Hanink2021.instReprRoom : Repr Room

Equations

• Phenomena.Definiteness.Studies.Hanink2021.instReprRoom = { reprPrec := Phenomena.Definiteness.Studies.Hanink2021.instReprRoom.repr }

def Phenomena.Definiteness.Studies.Hanink2021.instReprRoom.repr : Room → ℕ → Std.Format

Equations

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

def Phenomena.Definiteness.Studies.Hanink2021.F : Core.Logic.Intensional.Frame

Equations

• Phenomena.Definiteness.Studies.Hanink2021.F = { Entity := Phenomena.Definiteness.Studies.Hanink2021.Item, Index := Phenomena.Definiteness.Studies.Hanink2021.Room }

def Phenomena.Definiteness.Studies.Hanink2021.tableIn : Room → Item → Prop

"Table-in-room": the predicate is true at exactly one item per room. Encodes the @cite{hanink-2021} resource-situation idea — what counts as "the table" depends on the situation we evaluate at.

Equations

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

def Phenomena.Definiteness.Studies.Hanink2021.tableAtSit0 : Core.Logic.Intensional.Variables.DenotGS F Core.Logic.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 @cite{hanink-2021} situation-pronoun pattern: the structural index 0 selects which situation in gs to use.

Equations

• Phenomena.Definiteness.Studies.Hanink2021.tableAtSit0 _g gs x = Phenomena.Definiteness.Studies.Hanink2021.tableIn (Core.Logic.Intensional.Variables.interpSitPronoun 0 gs) x

def Phenomena.Definiteness.Studies.Hanink2021.g₀ : Core.Assignment F.Entity

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

Equations

• Phenomena.Definiteness.Studies.Hanink2021.g₀ x✝ = Phenomena.Definiteness.Studies.Hanink2021.Item.tableKitchen

def Phenomena.Definiteness.Studies.Hanink2021.gsKitchen : Core.Logic.Intensional.Variables.SitAssignment F

Situation assignment with pronoun 0 ↦ kitchen.

Equations

• Phenomena.Definiteness.Studies.Hanink2021.gsKitchen x✝ = Phenomena.Definiteness.Studies.Hanink2021.Room.kitchen

def Phenomena.Definiteness.Studies.Hanink2021.gsLiving : Core.Logic.Intensional.Variables.SitAssignment F

Situation assignment with pronoun 0 ↦ living.

Equations

• Phenomena.Definiteness.Studies.Hanink2021.gsLiving x✝ = Phenomena.Definiteness.Studies.Hanink2021.Room.living

theorem Phenomena.Definiteness.Studies.Hanink2021.tableAtSit0_existsUnique_kitchen : Core.Nominal.existsUnique fun (x : F.Denot Core.Logic.Intensional.Ty.e) => tableAtSit0 g₀ gsKitchen x

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

theorem Phenomena.Definiteness.Studies.Hanink2021.tableAtSit0_existsUnique_living : Core.Nominal.existsUnique fun (x : F.Denot Core.Logic.Intensional.Ty.e) => tableAtSit0 g₀ gsLiving x

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

theorem Phenomena.Definiteness.Studies.Hanink2021.theTable_kitchen : Core.Nominal.interpret (Core.Nominal.NominalKind.unique tableAtSit0 0) g₀ gsKitchen = some Item.tableKitchen

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

theorem Phenomena.Definiteness.Studies.Hanink2021.theTable_living : Core.Nominal.interpret (Core.Nominal.NominalKind.unique tableAtSit0 0) g₀ gsLiving = some Item.tableLiving

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

theorem Phenomena.Definiteness.Studies.Hanink2021.same_description_different_referents : Core.Nominal.interpret (Core.Nominal.NominalKind.unique tableAtSit0 0) g₀ gsKitchen ≠ Core.Nominal.interpret (Core.Nominal.NominalKind.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 Phenomena.Definiteness.Studies.Hanink2021.unique_index_does_not_alter_referent_directly : Core.Nominal.interpret (Core.Nominal.NominalKind.unique tableAtSit0 0) g₀ gsKitchen = Core.Nominal.interpret (Core.Nominal.NominalKind.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. (Core.Nominal.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 Phenomena.Definiteness.Studies.Hanink2021.situation_binders_classified (R : Core.Logic.Intensional.Variables.DenotGS F Core.Logic.Intensional.Ty.et) (deictic : Core.Deixis.Feature) (sIdx d : ℕ) : (Core.Nominal.NominalKind.unique R sIdx).usesSituationPronoun = true ∧ (Core.Nominal.NominalKind.demonstrative R deictic sIdx d).usesSituationPronoun = true ∧ (Core.Nominal.NominalKind.anaphoric R d).usesSituationPronoun = false ∧ (Core.Nominal.NominalKind.bare R).usesSituationPronoun = false ∧ (Core.Nominal.NominalKind.indefinite R).usesSituationPronoun = false

Among NominalKind 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 Phenomena.Definiteness.Studies.Hanink2021.anaphoric_independent_of_situation (R : Core.Logic.Intensional.Variables.DenotGS F Core.Logic.Intensional.Ty.et) (d : ℕ) (hgs : R g₀ gsKitchen = R g₀ gsLiving) : Core.Nominal.interpret (Core.Nominal.NominalKind.anaphoric R d) g₀ gsKitchen = Core.Nominal.interpret (Core.Nominal.NominalKind.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 @cite{hanink-2021}'s architecture: the anaphoric layer reads from g, the unique layer reads from gs.

theorem Phenomena.Definiteness.Studies.Hanink2021.anaphoric_const_restrictor_situation_insensitive (d : ℕ) : Core.Nominal.interpret (Core.Nominal.NominalKind.anaphoric (Core.Logic.Intensional.Variables.DenotGS.const fun (x : F.Denot Core.Logic.Intensional.Ty.e) => True) d) g₀ gsKitchen = Core.Nominal.interpret (Core.Nominal.NominalKind.anaphoric (Core.Logic.Intensional.Variables.DenotGS.const fun (x : F.Denot Core.Logic.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.