Ahn, Kocab & Davidson 2026: sign language loci as spatial modifiers

Sign language loci — areas of signing space that nominals are pointed to and that verbs start or end at — are analysed as one spatial modifier IX_LOC = λo λx. R(x, o), an intersective restriction relating an entity to a location. Nominal uses compose it with a covert demonstrative (the unique entity associated with the location); verbal uses incorporate the restricted argument into the verb, replacing agreement. Being a modifier, a locus is subject to the same Be brief competition as any other restriction, so it is licensed only when reference must be disambiguated.

This file defines ixLoc, the demonstrative that over Modifier.intersective, the two-dimensional introducing and anaphoric uses, incorporate, and a verb's Padden class read off its selection. that_isSome_iff is the uniqueness presupposition; scenario_help derives the interpretation of AHELPB from the incorporated points; paddenClass_of_selection recovers the agreeing/spatial/plain trichotomy; the row theorems state the pragmatic hypothesis over the consultants' judgments.

TODO

The experiment's ratings in the number, animacy and narrative conditions are results for Data/Experiments; the hypothesis over them, including that the narrative manipulation did not disambiguate, is not yet stated. The stimuli of Appendix A1 are printed unmarked.

References

• [AKD26]
• [Pot05]
• [Kap89]
• [Ari01]
• [Gri75]
• [Ais03]

The spatial modifier

def AhnKocabDavidson2026.ixLoc {E : Type u_1} {L : Type u_2} (R : E → L → Prop) (o : L) : E → Prop

⟦IX_LOC⟧ = λo λx. R(x, o): pointing at o predicates of x that it is associated with o, for whatever relation R the context supplies.

Equations

• AhnKocabDavidson2026.ixLoc R o x = R x o

noncomputable def AhnKocabDavidson2026.that {E : Type u_1} (R P : E → Prop) : Option E

The demonstrative ⟦that⟧ = λR λP. ιx. P(x) ∧ R(x): the unique entity meeting the spatial and the nominal restriction.

Equations

• AhnKocabDavidson2026.that R P = Reference.iota (Modifier.intersective R P)

theorem AhnKocabDavidson2026.that_isSome_iff {E : Type u_1} (R P : E → Prop) : (that R P).isSome = true ↔ ∃! x : E, P x ∧ R x

that refers exactly when there is a unique entity meeting both restrictions.

theorem AhnKocabDavidson2026.that_top {E : Type u_1} (R : E → Prop) : that R ⊤ = Reference.iota R

With a trivial nominal restriction (the ASL null pronoun), that is ιx. R(x).

The continuum of relations

Deictic, metonymic, and abstract uses differ only in R: the location of the referent, a location associated with it, or a location arbitrarily assigned to it by introduction.

def AhnKocabDavidson2026.locatedAt {E : Type u_1} {L : Type u_2} (at_ : E → L) : E → L → Prop

Direct deixis: x is currently located at o.

Equations

• AhnKocabDavidson2026.locatedAt at_ x o = (at_ x = o)

def AhnKocabDavidson2026.assigned {E : Type u_1} {L : Type u_2} (assoc : E → Option L) : E → L → Prop

Arbitrary association by introduction: x has been assigned locus o.

Equations

• AhnKocabDavidson2026.assigned assoc x o = (assoc x = some o)

theorem AhnKocabDavidson2026.that_assigned_isSome {E : Type u_1} {L : Type u_2} (assoc : E → Option L) (h : ∀ (x y : E) (o : L), assoc x = some o → assoc y = some o → x = y) (o : L) : (that (ixLoc (assigned assoc) o) ⊤).isSome = true ↔ ∃ (x : E), assoc x = some o

Under an injective assignment, the null demonstrative with IX_a refers whenever some entity was introduced at a.

Introducing and anaphoric uses

def AhnKocabDavidson2026.introducing {E : Type u_1} {L : Type u_2} {W : Type u_3} (p : W → Prop) (R : W → E → L → Prop) (x : E) (o : L) : ConventionalImplicature.TwoDim W (W → Prop)

The introducing use SOL IX_a …: the association is use-conditional, supplementing the at-issue clause p.

Equations

• AhnKocabDavidson2026.introducing p R x o = { atIssue := p, notAtIssue := fun (w : W) => R w x o }

def AhnKocabDavidson2026.anaphoric {E : Type u_1} {L : Type u_2} {W : Type u_3} (P : W → E → Prop) (R : W → E → L → Prop) (o : L) : ConventionalImplicature.TwoDim W (W → Prop)

The anaphoric use ∅ IX_a DANCE: asserts of an entity associated with o that it satisfies P and presupposes, use-conditionally, that exactly one entity is.

Equations

• AhnKocabDavidson2026.anaphoric P R o = { atIssue := fun (w : W) => ∃ (x : E), R w x o ∧ P w x, notAtIssue := fun (w : W) => ∃! x : E, R w x o }

theorem AhnKocabDavidson2026.introducing_neg_notAtIssue {E : Type u_1} {L : Type u_2} {W : Type u_3} (p : W → Prop) (R : W → E → L → Prop) (x : E) (o : L) : (introducing p R x o).neg.notAtIssue = fun (w : W) => R w x o

The association introduced by IX_a survives negation of the clause.

theorem AhnKocabDavidson2026.anaphoric_atIssue {E : Type u_1} {L : Type u_2} {W : Type u_3} (P : W → E → Prop) (R : W → E → L → Prop) (o : L) (w : W) (h : (anaphoric P R o).notAtIssue w) : (anaphoric P R o).atIssue w ↔ ∀ (x : E), R w x o → P w x

Given its presupposition, the anaphoric use predicates P of the entity at o.

Incorporation into verbs

def AhnKocabDavidson2026.incorporate {E : Type u_1} (V : E → E → Prop) (subj obj : E → Prop) : E → E → Prop

Locational modification AVB: the points restrict the verb's subject and object slots.

Equations

• AhnKocabDavidson2026.incorporate V subj obj x y = (Modifier.intersective subj (fun (x : E) => V x y) x ∧ obj y)

def AhnKocabDavidson2026.incorporate₁ {E : Type u_1} (V subj : E → Prop) : E → Prop

Locational modification of an intransitive, V_a: the point restricts the sole slot.

Equations

• AhnKocabDavidson2026.incorporate₁ V subj = Modifier.intersective subj V

inductive AhnKocabDavidson2026.Entity : Type

The scenario Jin at locus A, Sol at locus B.

• jin : Entity
• sol : Entity

@[instance_reducible]

instance AhnKocabDavidson2026.instDecidableEqEntity : DecidableEq Entity

Equations

• AhnKocabDavidson2026.instDecidableEqEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive AhnKocabDavidson2026.Locus : Type

Loci.

• a : Locus
• b : Locus

@[instance_reducible]

instance AhnKocabDavidson2026.instDecidableEqLocus : DecidableEq Locus

Equations

• AhnKocabDavidson2026.instDecidableEqLocus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AhnKocabDavidson2026.scenario : Entity → Locus → Prop

Jin was introduced at A and Sol at B.

Equations

• AhnKocabDavidson2026.scenario AhnKocabDavidson2026.Entity.jin AhnKocabDavidson2026.Locus.a = True
• AhnKocabDavidson2026.scenario AhnKocabDavidson2026.Entity.sol AhnKocabDavidson2026.Locus.b = True
• AhnKocabDavidson2026.scenario x✝¹ x✝ = False

@[instance_reducible]

instance AhnKocabDavidson2026.instDecidableRelEntityLocusScenario : DecidableRel scenario

Equations

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

theorem AhnKocabDavidson2026.scenario_help (help : Entity → Entity → Prop) [DecidableRel help] (h : help Entity.jin Entity.sol) : incorporate help (ixLoc scenario Locus.a) (ixLoc scenario Locus.b) Entity.jin Entity.sol ∧ ¬incorporate help (ixLoc scenario Locus.a) (ixLoc scenario Locus.b) Entity.sol Entity.jin

AHELPB reads as Jin helped Sol and not as Sol helped Jin, from the points alone.

Selection and Padden's classes

inductive AhnKocabDavidson2026.Selection : Type

What a verb's argument slot selects: a person locus, a location locus, or nothing.

• personal : Selection
• locational : Selection
• unspecified : Selection

@[instance_reducible]

instance AhnKocabDavidson2026.instDecidableEqSelection : DecidableEq Selection

Equations

• AhnKocabDavidson2026.instDecidableEqSelection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AhnKocabDavidson2026.instReprSelection : Repr Selection

Equations

• AhnKocabDavidson2026.instReprSelection = { reprPrec := AhnKocabDavidson2026.instReprSelection.repr }

def AhnKocabDavidson2026.instReprSelection.repr : Selection → ℕ → Std.Format

Equations

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

structure AhnKocabDavidson2026.Verb : Type

A verb's selectional specification for its subject and object slots.

• gloss : String
• subject : Selection
• object : Selection

@[instance_reducible]

instance AhnKocabDavidson2026.instReprVerb : Repr Verb

Equations

• AhnKocabDavidson2026.instReprVerb = { reprPrec := AhnKocabDavidson2026.instReprVerb.repr }

def AhnKocabDavidson2026.instReprVerb.repr : Verb → ℕ → Std.Format

Equations

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

inductive AhnKocabDavidson2026.PaddenClass : Type

Padden's trichotomy of sign language verbs.

• agreeing : PaddenClass
• spatial : PaddenClass
• plain : PaddenClass

@[instance_reducible]

instance AhnKocabDavidson2026.instDecidableEqPaddenClass : DecidableEq PaddenClass

Equations

• AhnKocabDavidson2026.instDecidableEqPaddenClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AhnKocabDavidson2026.instReprPaddenClass : Repr PaddenClass

Equations

• AhnKocabDavidson2026.instReprPaddenClass = { reprPrec := AhnKocabDavidson2026.instReprPaddenClass.repr }

def AhnKocabDavidson2026.instReprPaddenClass.repr : PaddenClass → ℕ → Std.Format

Equations

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

def AhnKocabDavidson2026.Verb.paddenClass (v : Verb) : PaddenClass

Padden's class, read off selection: a verb selecting a location is spatial, one selecting persons only is agreeing, one selecting nothing is plain.

Equations

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

def AhnKocabDavidson2026.help : Verb

HELP, WALK-TO, PUT, MOVE, and DANCE.

Equations

• AhnKocabDavidson2026.help = { gloss := "HELP", subject := AhnKocabDavidson2026.Selection.personal, object := AhnKocabDavidson2026.Selection.personal }

def AhnKocabDavidson2026.walkTo : Verb

Equations

• AhnKocabDavidson2026.walkTo = { gloss := "WALK-TO", subject := AhnKocabDavidson2026.Selection.personal, object := AhnKocabDavidson2026.Selection.locational }

def AhnKocabDavidson2026.put : Verb

Equations

• AhnKocabDavidson2026.put = { gloss := "PUT", subject := AhnKocabDavidson2026.Selection.personal, object := AhnKocabDavidson2026.Selection.locational }

def AhnKocabDavidson2026.move : Verb

Equations

• AhnKocabDavidson2026.move = { gloss := "MOVE", subject := AhnKocabDavidson2026.Selection.locational, object := AhnKocabDavidson2026.Selection.locational }

def AhnKocabDavidson2026.dance : Verb

Equations

• AhnKocabDavidson2026.dance = { gloss := "DANCE", subject := AhnKocabDavidson2026.Selection.unspecified, object := AhnKocabDavidson2026.Selection.unspecified }

theorem AhnKocabDavidson2026.paddenClass_of_selection : help.paddenClass = PaddenClass.agreeing ∧ put.paddenClass = PaddenClass.spatial ∧ move.paddenClass = PaddenClass.spatial ∧ dance.paddenClass = PaddenClass.plain

Selection recovers the trichotomy: HELP agreeing, PUT and MOVE spatial, DANCE plain.

The pragmatic hypothesis

Locus use is licensed to disambiguate between potential antecedents. Rows carry locus (whether nouns and verbs are locus-marked), resolved (whether context or an overt nominal already resolves reference), and condition (consultant for the elicited contrasts, else the experiment's manipulation). The consultants' judgments are counts of the three signers who accept a sentence.

theorem AhnKocabDavidson2026.unresolved_without_locus_degraded (row : Datum) : row ∈ Examples.all → row.feature? "condition" = some "consultant" → row.feature? "locus" = some "false" → row.feature? "resolved" = some "false" → row.judgment ≠ Judgment.acceptable

Without loci and without resolution, discourses are degraded.

theorem AhnKocabDavidson2026.resolved_without_locus_acceptable (row : Datum) : row ∈ Examples.all → row.feature? "condition" = some "consultant" → row.feature? "locus" = some "false" → row.feature? "resolved" = some "true" → row.judgment = Judgment.acceptable

Without loci, resolved discourses are fully acceptable.

theorem AhnKocabDavidson2026.locus_acceptable (row : Datum) : row ∈ Examples.all → row.feature? "condition" = some "consultant" → row.feature? "locus" = some "true" → row.judgment = Judgment.acceptable

Locus-marked discourses are acceptable whether or not reference was already resolved.