@cite{ahn-kocab-davidson-2026}

Pragmatics of spatial descriptions: Sign language loci. Language (2026), 1–40.

Core Analysis

Sign language loci (spatial locations in signing space) are spatial modifiers, not agreement markers. The indexical point IX directed toward a location A (written IX_A) is a predicate R(x, a) that relates an entity to a location. IX_A composes with a nominal restriction via predicate modification to form a demonstrative-like expression.

This analysis unifies the use of loci in both the verbal domain (verb "agreement" = incorporation of IX into the verb) and the nominal domain (IX_A = spatial modifier on a null demonstrative), and derives their optionality from pragmatic principles: loci are licensed when disambiguation is needed (Be Brief), paralleling demonstratives in spoken languages and differential object marking.

Key Formalizations

• ixLoc — the core IX_LOC denotation: λo. λx. R(x, o) (eq. 22a)
• ixA — IX pointing at locus A, applied: λx. R(x, a) (eq. 22b)
• ixModified — IX_A composes with nominal restriction via predMod (eq. 23–27)
• LocusRelationType — the deictic-to-abstract continuum for R (eqs. 38–40)
• VerbLocusType — selectional properties replacing Padden's trichotomy
• incorporateSubj/Obj/Both — verbal incorporation as predMod on argument positions
• Bridge theorems to TwoDimProp (@cite{potts-2005}), SemClass, Ariel accessibility, Gricean maxims

Theoretical Contributions

1. Reduces Padden's three-way verb classification (agreeing, spatial, plain) to selectional properties of the verb — what type of nominal (personal, locational) can be incorporated
2. Derives optionality of loci from Be Brief (M3): loci are costlier referential forms, dispreferred when a simpler form suffices
3. Parallels DOM (@cite{aissen-2003}): both involve overt marking conditioned by disambiguation need along prominence scales

inductive AhnKocabDavidson2026.SemClass : Type

Basic semantic classes for NP entities (inlined from substrate; @cite{resnik-1996} / @cite{erk-2007} style selectional classes). Used by this paper specifically for VerbLocusType → SemClass mapping (personal → animate, locational → location).

• animate : SemClass
• inanimate : SemClass
• human : SemClass
• animal : SemClass
• plant : SemClass
• artifact : SemClass
• abstract_ : SemClass
• event : SemClass
• location : SemClass
• time : SemClass

def AhnKocabDavidson2026.instReprSemClass.repr : SemClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AhnKocabDavidson2026.instReprSemClass : Repr SemClass

Equations

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

@[implicit_reducible]

instance AhnKocabDavidson2026.instDecidableEqSemClass : DecidableEq SemClass

Equations

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

inductive AhnKocabDavidson2026.Locus : Type

Abstract locus: a location in signing space used to track discourse referents. Two loci are distinguished if they occupy different spatial positions. The type is kept abstract — concrete spatial geometry is orthogonal to the pragmatic analysis.

• a : Locus
• b : Locus
• c : Locus

@[implicit_reducible]

instance AhnKocabDavidson2026.instDecidableEqLocus : DecidableEq Locus

Equations

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

@[implicit_reducible]

instance AhnKocabDavidson2026.instReprLocus : Repr Locus

Equations

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

def AhnKocabDavidson2026.instReprLocus.repr : Locus → ℕ → Std.Format

Equations

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

inductive AhnKocabDavidson2026.LocusRelationType : Type

The relation R between an entity and a locus. The paper's key insight is that R is not fixed — it ranges from transparent physical co-location to arbitrary discourse association (eqs. 38–40).

See deicticR (eq. 38) and abstractR (eq. 40) for concrete examples at the extremes of this continuum.

• deictic : LocusRelationType

  Deictic: R(x, o) iff x is physically located at o in the signing context. The referent is present and the signer points at them. This is the most transparent R (eq. 38).

• metonymic : LocusRelationType

  Metonymic: R(x, o) iff x is the regular occupant of location o. E.g., pointing at an office to refer to its occupant (eq. 39).

• abstract : LocusRelationType

  Abstract: R(x, o) iff x has been associated with o by prior discourse introduction. No physical or conventional link required. This is the most opaque R (eq. 40).

@[implicit_reducible]

instance AhnKocabDavidson2026.instDecidableEqLocusRelationType : DecidableEq LocusRelationType

Equations

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

@[implicit_reducible]

instance AhnKocabDavidson2026.instReprLocusRelationType : Repr LocusRelationType

Equations

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

def AhnKocabDavidson2026.instReprLocusRelationType.repr : LocusRelationType → ℕ → Std.Format

Equations

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

def AhnKocabDavidson2026.LocusRelationType.transparency : LocusRelationType → Fin 3

Transparency of the R relation: how much the spatial location correlates with the physical world. Higher = more transparent. This orders the deictic-to-abstract continuum (eqs. 38–40).

Equations

• AhnKocabDavidson2026.LocusRelationType.deictic.transparency = 2
• AhnKocabDavidson2026.LocusRelationType.metonymic.transparency = 1
• AhnKocabDavidson2026.LocusRelationType.abstract.transparency = 0

theorem AhnKocabDavidson2026.deictic_most_transparent : LocusRelationType.deictic.transparency > LocusRelationType.abstract.transparency ∧ LocusRelationType.deictic.transparency > LocusRelationType.metonymic.transparency

The deictic–abstract continuum is ordered: deictic > metonymic > abstract.

inductive AhnKocabDavidson2026.Entity : Type

Entity type for ASL discourse scenarios.

• jin : Entity
• sol : Entity
• linda : Entity
• mike : Entity
• bob : Entity
• will : Entity
• girl : Entity
• boy : Entity
• tv : Entity
• tree : Entity
• ball : Entity

@[implicit_reducible]

instance AhnKocabDavidson2026.instDecidableEqEntity : DecidableEq Entity

Equations

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

@[implicit_reducible]

instance AhnKocabDavidson2026.instReprEntity : Repr Entity

Equations

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

def AhnKocabDavidson2026.instReprEntity.repr : Entity → ℕ → Std.Format

Equations

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

def AhnKocabDavidson2026.ixLoc (R : Entity → Locus → Bool) : Locus → Entity → Bool

⟦IX_LOC⟧ = λo. λx. R(x, o) — the core denotation of the indexical point. Takes a location variable o and returns a predicate over entities. This is the spatial predicate that all uses of loci share.

Eq. 22a of @cite{ahn-kocab-davidson-2026}.

Equations

• AhnKocabDavidson2026.ixLoc R o x = R x o

def AhnKocabDavidson2026.ixA (R : Entity → Locus → Bool) (loc : Locus) : Entity → Bool

⟦IX_A⟧ = λx. R(x, a) — IX pointing at a specific locus A. This is ixLoc R partially applied to a concrete locus.

Analogous to a Kaplan demonstration (@cite{kaplan-1989}): IX_A requires a contextual element (the R relation) to determine reference, and when R is functional, picks out a unique entity — like a pointing gesture that presents an individual in context (see ixA_unique_when_functional).

Eq. 22b of @cite{ahn-kocab-davidson-2026}.

Equations

• AhnKocabDavidson2026.ixA R loc = AhnKocabDavidson2026.ixLoc R loc

def AhnKocabDavidson2026.ixModified (R : Entity → Locus → Bool) (loc : Locus) (P : Entity → Bool) : Entity → Bool

IX_A composes with a nominal restriction P via predicate modification: ⟦P + IX_A⟧ = λx. P(x) ∧ R(x, a).

This covers:

• ⟦[that+IX_A] girl⟧ = ιx. girl(x) ∧ R(x, a) (English, eq. 23)
• ⟦[she+IX_A]⟧ = ιx. fem(x) ∧ R(x, a) (English, eq. 25)
• ⟦[ta+IX_A]⟧ = ιx. entity(x) ∧ R(x, a) (Mandarin, eq. 26)
• ⟦[∅+IX_A]⟧ = ιx. R(x, a) (ASL, eq. 27)

Equations

• AhnKocabDavidson2026.ixModified R loc P = Semantics.Composition.Modification.predMod P (AhnKocabDavidson2026.ixA R loc)

def AhnKocabDavidson2026.ixNull (R : Entity → Locus → Bool) (loc : Locus) : Entity → Bool

ASL null-pronoun case: ∅ + IX_A. The nominal restriction is vacuous (truePred), so the result is just R(x, a). Eq. 27.

Equations

• AhnKocabDavidson2026.ixNull R loc = AhnKocabDavidson2026.ixModified R loc Semantics.Composition.Modification.truePred

theorem AhnKocabDavidson2026.ixNull_eq_ixA (R : Entity → Locus → Bool) (loc : Locus) : ixNull R loc = ixA R loc

The null-pronoun case reduces to the bare spatial predicate.

theorem AhnKocabDavidson2026.ixModified_entails_base (R : Entity → Locus → Bool) (loc : Locus) (P : Entity → Bool) (x : Entity) (h : ixModified R loc P x = true) : P x = true

IX_A + P entails P: the modified expression is strictly more restrictive than the bare nominal. Any entity satisfying P ∧ R(·, a) also satisfies P.

theorem AhnKocabDavidson2026.ixModified_entails_spatial (R : Entity → Locus → Bool) (loc : Locus) (P : Entity → Bool) (x : Entity) (h : ixModified R loc P x = true) : ixA R loc x = true

IX_A + P entails R(·, a): the modified expression entails the spatial predicate.

theorem AhnKocabDavidson2026.ixModified_order (R : Entity → Locus → Bool) (loc : Locus) (P : Entity → Bool) : ixModified R loc P = Semantics.Composition.Modification.predMod (ixA R loc) P

The order of composition does not matter: P ∧ R(·, a) = R(·, a) ∧ P. This follows from commutativity of predicate modification.

theorem AhnKocabDavidson2026.ixA_unique_when_functional (R : Entity → Locus → Bool) (hfun : ∀ (x y : Entity) (loc : Locus), R x loc = true → R y loc = true → x = y) (loc : Locus) (x y : Entity) (hx : ixA R loc x = true) (hy : ixA R loc y = true) : x = y

When R is functional (each locus maps to at most one entity), IX_A determines a unique referent — at most one entity satisfies R(·, a). This is the demonstrative-like property of IX_A: like a Kaplan demonstration, it picks out a unique individual in context.

inductive AhnKocabDavidson2026.VerbLocusType : Type

The type of nominal that a verb selects for in its argument slots. This replaces Padden (1983)'s three-way classification:

• personal → "agreeing" verbs (HELP, GIVE, TELL, ASK)
• locational → "spatial" verbs (MOVE, PUT, CARRY)
• unspecified → "plain" verbs (MEMORIZE, LOVE, THINK, WONDER)

The key insight of @cite{ahn-kocab-davidson-2026} §3.5 is that all three classes can incorporate IX_LOC; they differ only in what entity type the spatial predicate selects for.

• personal : VerbLocusType

  Verb selects for personal entities (agent/patient). Locus incorporation marks person information.

• locational : VerbLocusType

  Verb selects for locational entities (source/goal). Locus incorporation marks spatial information.

• unspecified : VerbLocusType

  Verb does not lexically specify; incorporation is possible but not triggered by the verb's own selectional requirements.

@[implicit_reducible]

instance AhnKocabDavidson2026.instDecidableEqVerbLocusType : DecidableEq VerbLocusType

Equations

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

@[implicit_reducible]

instance AhnKocabDavidson2026.instReprVerbLocusType : Repr VerbLocusType

Equations

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

def AhnKocabDavidson2026.instReprVerbLocusType.repr : VerbLocusType → ℕ → Std.Format

Equations

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

def AhnKocabDavidson2026.VerbLocusType.toSemClass : VerbLocusType → Option SemClass

Bridge to selectional preference classes: verb locus types correspond to semantic classes from the cross-linguistic selectional preference framework. personal maps to SemClass.animate (person arguments), locational maps to SemClass.location, and unspecified has no selectional restriction.

Equations

• AhnKocabDavidson2026.VerbLocusType.personal.toSemClass = some AhnKocabDavidson2026.SemClass.animate
• AhnKocabDavidson2026.VerbLocusType.locational.toSemClass = some AhnKocabDavidson2026.SemClass.location
• AhnKocabDavidson2026.VerbLocusType.unspecified.toSemClass = none

structure AhnKocabDavidson2026.ASLVerbEntry : Type

An ASL verb entry with locus selectional properties.

• gloss : String

  Verb gloss

• subjectType : VerbLocusType

  What the subject slot selects for

• objectType : VerbLocusType

  What the object slot selects for

• hasPath : Bool

  Whether the verb has a directional movement component

@[implicit_reducible]

instance AhnKocabDavidson2026.instReprASLVerbEntry : Repr ASLVerbEntry

Equations

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

def AhnKocabDavidson2026.instReprASLVerbEntry.repr : ASLVerbEntry → ℕ → Std.Format

Equations

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

def AhnKocabDavidson2026.help : ASLVerbEntry

HELP: agreeing verb. Subject = agent (personal), object = recipient (personal). Has path movement from source to goal.

Equations

• AhnKocabDavidson2026.help = { gloss := "HELP", subjectType := AhnKocabDavidson2026.VerbLocusType.personal, objectType := AhnKocabDavidson2026.VerbLocusType.personal, hasPath := true }

def AhnKocabDavidson2026.give : ASLVerbEntry

GIVE: agreeing verb with transfer semantics.

Equations

• AhnKocabDavidson2026.give = { gloss := "GIVE", subjectType := AhnKocabDavidson2026.VerbLocusType.personal, objectType := AhnKocabDavidson2026.VerbLocusType.personal, hasPath := true }

def AhnKocabDavidson2026.ask : ASLVerbEntry

ASK: agreeing verb.

Equations

• AhnKocabDavidson2026.ask = { gloss := "ASK", subjectType := AhnKocabDavidson2026.VerbLocusType.personal, objectType := AhnKocabDavidson2026.VerbLocusType.personal, hasPath := true }

def AhnKocabDavidson2026.push : ASLVerbEntry

PUSH: agreeing verb.

Equations

• AhnKocabDavidson2026.push = { gloss := "PUSH", subjectType := AhnKocabDavidson2026.VerbLocusType.personal, objectType := AhnKocabDavidson2026.VerbLocusType.personal, hasPath := true }

def AhnKocabDavidson2026.move : ASLVerbEntry

MOVE: spatial verb. Source and goal are locations, not persons.

Equations

• AhnKocabDavidson2026.move = { gloss := "MOVE", subjectType := AhnKocabDavidson2026.VerbLocusType.locational, objectType := AhnKocabDavidson2026.VerbLocusType.locational, hasPath := true }

def AhnKocabDavidson2026.put : ASLVerbEntry

PUT: spatial verb.

Equations

• AhnKocabDavidson2026.put = { gloss := "PUT", subjectType := AhnKocabDavidson2026.VerbLocusType.personal, objectType := AhnKocabDavidson2026.VerbLocusType.locational, hasPath := true }

def AhnKocabDavidson2026.dance : ASLVerbEntry

DANCE: plain verb. No lexical locus selection, but CAN incorporate a locus via co-location when pragmatically needed.

Equations

• AhnKocabDavidson2026.dance = { gloss := "DANCE", subjectType := AhnKocabDavidson2026.VerbLocusType.unspecified, objectType := AhnKocabDavidson2026.VerbLocusType.unspecified, hasPath := false }

def AhnKocabDavidson2026.fall : ASLVerbEntry

FALL: plain verb. Intransitive, no path.

Equations

• AhnKocabDavidson2026.fall = { gloss := "FALL", subjectType := AhnKocabDavidson2026.VerbLocusType.unspecified, objectType := AhnKocabDavidson2026.VerbLocusType.unspecified, hasPath := false }

def AhnKocabDavidson2026.run : ASLVerbEntry

RUN: plain verb.

Equations

• AhnKocabDavidson2026.run = { gloss := "RUN", subjectType := AhnKocabDavidson2026.VerbLocusType.unspecified, objectType := AhnKocabDavidson2026.VerbLocusType.unspecified, hasPath := false }

theorem AhnKocabDavidson2026.all_types_can_incorporate : dance.subjectType = VerbLocusType.unspecified ∧ help.subjectType = VerbLocusType.personal ∧ move.subjectType = VerbLocusType.locational

All three verb types can incorporate IX_LOC. The traditional claim that only "agreeing" and "spatial" verbs show locus modification is empirically wrong — plain verbs like DANCE can be locationally modified when disambiguation requires it (§2.2, exx. 9–11).

theorem AhnKocabDavidson2026.agreeing_vs_plain_is_selectional : help.objectType = VerbLocusType.personal ∧ dance.objectType = VerbLocusType.unspecified

The difference between "agreeing" and "plain" verbs is selectional, not categorical: both can incorporate, but agreeing verbs lexically select for personal nominals while plain verbs do not.

theorem AhnKocabDavidson2026.selectional_bridge : help.subjectType.toSemClass = some SemClass.animate ∧ help.objectType.toSemClass = some SemClass.animate ∧ move.subjectType.toSemClass = some SemClass.location ∧ move.objectType.toSemClass = some SemClass.location ∧ dance.subjectType.toSemClass = none

Agreeing verbs select for animate entities; spatial verbs select for locations. This connects the ASL-specific typology to the cross-linguistic selectional preference framework.

def AhnKocabDavidson2026.incorporateSubj (verbMeaning : Entity → Entity → Bool) (R : Entity → Locus → Bool) (loc : Locus) : Entity → Entity → Bool

Incorporation of IX_A for the subject argument: the verb's meaning is conjoined with the spatial predicate via predicate modification on the subject position. For each fixed object y, the subject predicate λx. V(x, y) is modified by ixA R loc.

This is the semantic content of what is traditionally called "verb agreement" in sign languages — it is predicate modification, not agreement in the syntactic sense.

Equations

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

def AhnKocabDavidson2026.incorporateObj (verbMeaning : Entity → Entity → Bool) (R : Entity → Locus → Bool) (loc : Locus) : Entity → Entity → Bool

Incorporation of IX_A for the object argument: the verb's meaning is conjoined with the spatial predicate via predicate modification on the object position.

Equations

• AhnKocabDavidson2026.incorporateObj verbMeaning R loc x y = Semantics.Composition.Modification.predMod (verbMeaning x) (AhnKocabDavidson2026.ixA R loc) y

def AhnKocabDavidson2026.incorporateBoth (verbMeaning : Entity → Entity → Bool) (R : Entity → Locus → Bool) (locSubj locObj : Locus) : Entity → Entity → Bool

Full incorporation (both arguments): sequential application of object incorporation then subject incorporation.

For ₍ₐ₎VERB₍ᵦ₎, this yields λx y. V(x,y) ∧ R(y,b) ∧ R(x,a).

Equations

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

theorem AhnKocabDavidson2026.incorporate_both_eq_sequential (V : Entity → Entity → Bool) (R : Entity → Locus → Bool) (locSubj locObj : Locus) : incorporateBoth V R locSubj locObj = incorporateSubj (incorporateObj V R locObj) R locSubj

Full incorporation is equivalent to sequential incorporation: incorporate the object, then the subject.

theorem AhnKocabDavidson2026.incorporate_order_independent (V : Entity → Entity → Bool) (R : Entity → Locus → Bool) (locSubj locObj : Locus) (x y : Entity) : incorporateSubj (incorporateObj V R locObj) R locSubj x y = incorporateObj (incorporateSubj V R locSubj) R locObj x y

The order of incorporation does not matter: incorporating subject then object yields the same result as object then subject.

structure AhnKocabDavidson2026.PragmaticContext : Type

Disambiguation context: the discourse factors that determine whether locus marking is pragmatically needed. These correspond to the three experimental conditions in §4 of @cite{ahn-kocab-davidson-2026}.

• numReferents : Fin 3

  Number of potential referents for the target predicate.

• narrativeSupport : Bool

  Whether narrative context provides disambiguating information.

• competitorAnimate : Bool

  Whether the competing referent (if any) is animate. When the competitor is inanimate, animacy alone disambiguates.

@[implicit_reducible]

instance AhnKocabDavidson2026.instDecidableEqPragmaticContext : DecidableEq PragmaticContext

Equations

• AhnKocabDavidson2026.instDecidableEqPragmaticContext = AhnKocabDavidson2026.instDecidableEqPragmaticContext.decEq

def AhnKocabDavidson2026.instDecidableEqPragmaticContext.decEq (x✝ x✝¹ : PragmaticContext) : Decidable (x✝ = x✝¹)

Equations

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

def AhnKocabDavidson2026.instReprPragmaticContext.repr : PragmaticContext → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AhnKocabDavidson2026.instReprPragmaticContext : Repr PragmaticContext

Equations

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

def AhnKocabDavidson2026.PragmaticContext.hasContextSupport (ctx : PragmaticContext) : Bool

Contextual support: whether the discourse context alone provides sufficient information to resolve the intended referent.

Equations

• ctx.hasContextSupport = (decide (↑ctx.numReferents ≤ 1) || ctx.narrativeSupport || !ctx.competitorAnimate)

def AhnKocabDavidson2026.locusNeeded (ctx : PragmaticContext) : Bool

Whether locus marking is pragmatically needed: loci are licensed for disambiguation when contextual support is insufficient.

The main hypothesis (eq. 53): "Locus use (IX_LOC and its incorporated forms, e.g. locationally modified verbs) is pragmatically licensed to disambiguate between potential antecedents."

Equations

• AhnKocabDavidson2026.locusNeeded ctx = !ctx.hasContextSupport

inductive AhnKocabDavidson2026.LocusUtterance : Type

Utterance type: bare (no locus marking) vs. marked (with loci on nouns and/or verbs). These are the alternatives the speaker chooses between.

• bare : LocusUtterance

  No locus marking: bare nouns, citation-form verbs.

• marked : LocusUtterance

  Locus-marked: IX on nouns, locationally modified verbs.

@[implicit_reducible]

instance AhnKocabDavidson2026.instDecidableEqLocusUtterance : DecidableEq LocusUtterance

Equations

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

def AhnKocabDavidson2026.instReprLocusUtterance.repr : LocusUtterance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AhnKocabDavidson2026.instReprLocusUtterance : Repr LocusUtterance

Equations

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

def AhnKocabDavidson2026.LocusUtterance.cost : LocusUtterance → ℕ

Cost: locus-marked utterances are more costly (more phonological material, more articulatory effort). This is the Be Brief (M3) pressure against unnecessary locus use.

Equations

• AhnKocabDavidson2026.LocusUtterance.bare.cost = 0
• AhnKocabDavidson2026.LocusUtterance.marked.cost = 1

theorem AhnKocabDavidson2026.marked_costlier : LocusUtterance.marked.cost > LocusUtterance.bare.cost

Marked utterances are costlier than bare ones.

def AhnKocabDavidson2026.LocusUtterance.resolvesIn (u : LocusUtterance) (ctx : PragmaticContext) : Bool

Informativity: whether the utterance resolves ambiguity in context.

Equations

• AhnKocabDavidson2026.LocusUtterance.bare.resolvesIn ctx = ctx.hasContextSupport
• AhnKocabDavidson2026.LocusUtterance.marked.resolvesIn ctx = true

def AhnKocabDavidson2026.oneRef_plusCtx : PragmaticContext

One referent, with contextual support.

Equations

• AhnKocabDavidson2026.oneRef_plusCtx = { numReferents := 1, narrativeSupport := true, competitorAnimate := true }

def AhnKocabDavidson2026.twoRef_minusCtx : PragmaticContext

Two referents, no contextual support (both animate, no narrative).

Equations

• AhnKocabDavidson2026.twoRef_minusCtx = { numReferents := 2, narrativeSupport := false, competitorAnimate := true }

def AhnKocabDavidson2026.twoRef_plusCtx : PragmaticContext

Two referents, with contextual support (narrative present).

Equations

• AhnKocabDavidson2026.twoRef_plusCtx = { numReferents := 2, narrativeSupport := true, competitorAnimate := true }

def AhnKocabDavidson2026.twoRef_inanimate : PragmaticContext

Two referents, inanimate competitor (animacy disambiguates).

Equations

• AhnKocabDavidson2026.twoRef_inanimate = { numReferents := 2, narrativeSupport := false, competitorAnimate := false }

theorem AhnKocabDavidson2026.oneRef_has_support : oneRef_plusCtx.hasContextSupport = true

One referent: context suffices, locus not needed.

theorem AhnKocabDavidson2026.twoRef_animate_locus_needed : locusNeeded twoRef_minusCtx = true

Two animate referents without narrative: locus needed.

theorem AhnKocabDavidson2026.twoRef_narrative_has_support : twoRef_plusCtx.hasContextSupport = true

Two referents with narrative support: context suffices.

theorem AhnKocabDavidson2026.inanimate_has_support : twoRef_inanimate.hasContextSupport = true

Two referents, inanimate competitor: context suffices (animacy disambiguates — only the animate referent can be the agent).

theorem AhnKocabDavidson2026.marked_always_resolves (ctx : PragmaticContext) : LocusUtterance.marked.resolvesIn ctx = true

Locus-marked utterances always resolve, regardless of context.

theorem AhnKocabDavidson2026.bare_fails_iff_no_support (ctx : PragmaticContext) : LocusUtterance.bare.resolvesIn ctx = ctx.hasContextSupport

Bare utterances fail to resolve exactly when context is insufficient.

def AhnKocabDavidson2026.locusTension : Pragmatics.GriceanMaxims.MannerSubmaxim × Pragmatics.GriceanMaxims.MannerSubmaxim

The pragmatic tension in locus use is between M2 (avoid ambiguity) and M3 (be brief). Loci resolve ambiguity (satisfying M2) but add phonological material (violating M3). The speaker should use loci iff the M2 gain outweighs the M3 cost — i.e., iff disambiguation is actually needed.

This is structurally identical to the Be Brief / Avoid Ambiguity tradeoff that governs modifier use in spoken languages (e.g., "the tall one" vs. "it" in a reference game).

Equations

• AhnKocabDavidson2026.locusTension = (Pragmatics.GriceanMaxims.MannerSubmaxim.avoidAmbiguity, Pragmatics.GriceanMaxims.MannerSubmaxim.beBrief)

theorem AhnKocabDavidson2026.tension_is_genuine : locusTension.1 ≠ locusTension.2

The two maxims in tension are distinct.

def AhnKocabDavidson2026.optimalLocusChoice (ctx : PragmaticContext) : LocusUtterance

Optimal locus use: use loci iff context alone is insufficient for disambiguation. This resolves the M2/M3 tension by making the M3 cost justified only when M2 would otherwise be violated.

Equations

• AhnKocabDavidson2026.optimalLocusChoice ctx = if AhnKocabDavidson2026.locusNeeded ctx = true then AhnKocabDavidson2026.LocusUtterance.marked else AhnKocabDavidson2026.LocusUtterance.bare

theorem AhnKocabDavidson2026.optimal_always_resolves (ctx : PragmaticContext) : (optimalLocusChoice ctx).resolvesIn ctx = true

The optimal choice always resolves the referent.

def AhnKocabDavidson2026.ixLocAccessibility : Features.AccessibilityLevel

Where IX_LOC falls on Ariel's accessibility marking scale.

IX_LOC is a stressed pronominal form with an accompanying gesture (pointing to a locus). This maps to stressedPronGesture — a stressed pronoun with a deictic gesture (rank 12).

Without the locus (bare noun), the form would be a definite description or a null argument (depending on language). The locus-marked form is thus less accessible (more informative, more rigid) than a bare pronoun, and more accessible than a full definite description.

Equations

• AhnKocabDavidson2026.ixLocAccessibility = Features.AccessibilityLevel.stressedPronGesture

def AhnKocabDavidson2026.bareNullAccessibility : Features.AccessibilityLevel

Bare pronominal reference (ASL null argument) maps to zero.

Equations

• AhnKocabDavidson2026.bareNullAccessibility = Features.AccessibilityLevel.zero

theorem AhnKocabDavidson2026.ixLoc_less_accessible_than_null : ixLocAccessibility.rank < bareNullAccessibility.rank

IX_LOC is less accessible (lower rank) than a bare null argument. This means it is more informative and should be used only when the more reduced form (null argument) is insufficient.

theorem AhnKocabDavidson2026.ixLoc_more_accessible_than_description : ixLocAccessibility.rank > Features.AccessibilityLevel.shortDefDescription.rank

IX_LOC is more accessible than a full definite description. It is not as heavy as "the boy who is sitting on the left."

theorem AhnKocabDavidson2026.accessibility_predicts_locus_use : ixLocAccessibility.informativity > bareNullAccessibility.informativity ∧ ixLocAccessibility.attenuation < bareNullAccessibility.attenuation

The accessibility prediction: speakers should use IX_LOC only when the more reduced form (null argument / bare noun) fails to uniquely identify the referent. This is Ariel's core principle applied to sign language loci.

Parallel to Differential Object Marking (@cite{aissen-2003})

Both locus marking in sign languages and DOM in spoken languages involve optional overt marking conditioned by disambiguation need:

• In DOM, objects are overtly case-marked when they are atypical (high animacy/definiteness, which makes them harder to distinguish from subjects).
• In sign language, loci are overtly used when context fails to disambiguate.

The shared principle: "Mark when disambiguation is needed; omit marking when the default interpretation suffices."

@cite{aissen-2003} formalizes DOM as harmonic alignment of prominence scales with grammatical relations. The locus parallel suggests the same mechanism extends to the visual-spatial modality.

See Phenomena/Case/Studies/Aissen2003.lean for the OT formalization.

def AhnKocabDavidson2026.deicticR (physicalLocation : Entity → Locus) : Entity → Locus → Bool

Deictic R: physical co-location. The signer points directly at a present referent. This is the most transparent relation type (LocusRelationType.deictic, eq. 38).

Equations

• AhnKocabDavidson2026.deicticR physicalLocation x o = (physicalLocation x == o)

def AhnKocabDavidson2026.abstractR (association : Entity → Option Locus) : Entity → Locus → Bool

Abstract R: discourse-introduced association. The signer has arbitrarily associated entities with loci earlier in the discourse. This is the most opaque relation type (LocusRelationType.abstract, eq. 40).

Equations

• AhnKocabDavidson2026.abstractR association x o = (association x == some o)

def AhnKocabDavidson2026.scenario1 : Entity → Locus → Bool

A concrete scenario: Jin is at locus A, Sol is at locus B.

Equations

• AhnKocabDavidson2026.scenario1 AhnKocabDavidson2026.Entity.jin AhnKocabDavidson2026.Locus.a = true
• AhnKocabDavidson2026.scenario1 AhnKocabDavidson2026.Entity.sol AhnKocabDavidson2026.Locus.b = true
• AhnKocabDavidson2026.scenario1 x✝¹ x✝ = false

theorem AhnKocabDavidson2026.scenario1_ixA_picks_jin : ixA scenario1 Locus.a Entity.jin = true ∧ ixA scenario1 Locus.a Entity.sol = false

In scenario1, IX_A picks out Jin.

theorem AhnKocabDavidson2026.scenario1_ixB_picks_sol : ixA scenario1 Locus.b Entity.sol = true ∧ ixA scenario1 Locus.b Entity.jin = false

In scenario1, IX_B picks out Sol.

theorem AhnKocabDavidson2026.scenario1_functional (x y : Entity) (loc : Locus) (hx : scenario1 x loc = true) (hy : scenario1 y loc = true) : x = y

scenario1 is functional: each locus maps to at most one entity. Therefore ixA_unique_when_functional applies, giving IX_A demonstrative-like uniqueness.

def AhnKocabDavidson2026.helpMeaning : Entity → Entity → Bool

Verbal incorporation in scenario1: "₍ₐ₎HELP₍ᵦ₎" (Jin helps Sol). A simple transitive verb meaning for testing incorporation.

Equations

• AhnKocabDavidson2026.helpMeaning AhnKocabDavidson2026.Entity.jin AhnKocabDavidson2026.Entity.sol = true
• AhnKocabDavidson2026.helpMeaning AhnKocabDavidson2026.Entity.sol AhnKocabDavidson2026.Entity.jin = true
• AhnKocabDavidson2026.helpMeaning AhnKocabDavidson2026.Entity.jin AhnKocabDavidson2026.Entity.jin = true
• AhnKocabDavidson2026.helpMeaning AhnKocabDavidson2026.Entity.sol AhnKocabDavidson2026.Entity.sol = true
• AhnKocabDavidson2026.helpMeaning x✝¹ x✝ = false

theorem AhnKocabDavidson2026.aHelpB_correct : incorporateBoth helpMeaning scenario1 Locus.a Locus.b Entity.jin Entity.sol = true ∧ incorporateBoth helpMeaning scenario1 Locus.a Locus.b Entity.sol Entity.jin = false

₍ₐ₎HELP₍ᵦ₎ with scenario1 R correctly restricts to "Jin helps Sol".

def AhnKocabDavidson2026.introducingUse (predicate : Entity → Bool) (R : Entity → Locus → Bool) (loc : Locus) : Pragmatics.Expressives.TwoDimProp Entity

Introducing use of IX_LOC: the locus association is use-conditional (CI) content, not at-issue. The sentence's truth conditions come from the predicate; the spatial association projects as a CI.

Uses TwoDimProp from @cite{potts-2005} directly — the introducing use of IX_LOC is structurally parallel to how expressives like "bastard" contribute CI content that projects through all operators.

Equations

• AhnKocabDavidson2026.introducingUse predicate R loc = { atIssue := fun (x : AhnKocabDavidson2026.Entity) => predicate x = true, ci := fun (x : AhnKocabDavidson2026.Entity) => R x loc = true }

def AhnKocabDavidson2026.anaphoricUse (R : Entity → Locus → Bool) (loc : Locus) (P : Entity → Bool) : Pragmatics.Expressives.TwoDimProp Entity

Anaphoric use: the spatial restriction IS at-issue (it picks out the unique entity associated with the locus). CI is trivial.

Equations

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

theorem AhnKocabDavidson2026.introducing_ci_projects (pred : Entity → Bool) (R : Entity → Locus → Bool) (loc : Locus) : (introducingUse pred R loc).neg.ci = (introducingUse pred R loc).ci

The introducing use's CI projects through negation: negating "JIN₍ₐ₎ DANCE" negates the dancing but preserves the locus association. Derived from TwoDimProp.ci_projects_through_neg.

theorem AhnKocabDavidson2026.anaphoric_ci_trivial (R : Entity → Locus → Bool) (loc : Locus) (P : Entity → Bool) (x : Entity) : (anaphoricUse R loc P).ci x

The anaphoric use has trivial CI: all use-conditional content was already introduced.