Deictic Features: Demonstrative Distance and Person Orientation

[Mor21]

Framework-agnostic enumeration of deictic features carried by demonstratives. Promoted from Fragments/Shan/Definiteness.SpatialRelation (which carried just proximal | distal) for cross-fragment reuse.

Coverage

The four constructors cover the WALS Ch. 41 distance-system typology:

• Two-way systems (~54% of attested languages): use proximal | distal. English (this/that), Mandarin (zhe/na), French (ce N-ci/ce N-la), Shan (nâj/nân), Magahi (i/ũ), and most Indo-European languages.

• Three-way distance-oriented systems: use proximal | medial | distal. Latin (hic/iste/ille), Spanish (este/ese/aquel), Hunzib.

• Distance-neutral demonstratives (Modern German dieser, Hawaiian no-contrast forms): use unspecified.

Out of scope at this enum

Adding more granularity (person-orientation, visibility, elevation, posture) should follow the concrete-then-abstract discipline: add a constructor when a fragment actually needs it, not in anticipation. Specifically:

• Person-oriented three-way systems (Japanese ko/so/a, Korean i/ku/ce): add nearSpeaker | nearHearer | awayFromBoth constructors when the first fragment needs them.
• Visibility contrasts (Quechua, Kwakwaka'wakw, ASL): add visible | invisible constructors when a fragment needs them.
• Elevation contrasts (Dyirbal, Nepali): add when needed.

This is the centralized type referenced by Semantics.Definiteness.Description.deictic (forthcoming) and by demonstrative entries in Fragments/.

inductive Features.Deixis.Feature : Type

Deictic features carried by demonstratives. Minimal enum sufficient for two-way and three-way distance systems plus distance-neutral demonstratives; extend when a fragment requires finer granularity (person orientation, visibility, elevation).

• proximal : Feature

  Close to speaker (e.g. English this, Mandarin zhe, Shan nâj).

• medial : Feature

  Intermediate distance (e.g. Latin iste, Spanish ese). For three-way distance-oriented systems only — person-oriented three-way systems (Japanese, Korean) need separate constructors.

• distal : Feature

  Far from speaker (e.g. English that, Mandarin na, Shan nân).

• unspecified : Feature

  Distance-neutral demonstrative (e.g. Modern German dieser). Used when a demonstrative is morphologically present but does not encode a distance contrast.

@[implicit_reducible]

instance Features.Deixis.instDecidableEqFeature : DecidableEq Feature

Equations

• Features.Deixis.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.Deixis.instReprFeature.repr : Feature → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Deixis.instReprFeature : Repr Feature

Equations

• Features.Deixis.instReprFeature = { reprPrec := Features.Deixis.instReprFeature.repr }

def Features.Deixis.Feature.EncodesDistance (f : Feature) : Prop

A demonstrative encodes a distance contrast iff its feature is one of proximal/medial/distal (not unspecified).

Equations

• f.EncodesDistance = (f ≠ Features.Deixis.Feature.unspecified)

@[implicit_reducible]

instance Features.Deixis.instDecidablePredFeatureEncodesDistance : DecidablePred Feature.EncodesDistance

Equations

• Features.Deixis.instDecidablePredFeatureEncodesDistance x✝ = Features.Deixis.instDecidablePredFeatureEncodesDistance._aux_1 x✝

theorem Features.Deixis.encodesDistance_iff (f : Feature) : f.EncodesDistance ↔ f ≠ Feature.unspecified

Distance-encoding features are exactly the non-unspecified ones.

The demonstrative capability

[Demonstrative α] is the spatial-deixis property itself — the genuinely demonstrative axis, word-class-neutral (a demonstrative pronoun this, determiner this book, or adverb here all instance it). This is the lesson of [PGG17]: the morphological "demonstrative pronoun" label is not the property. They show German der/die/das — long called demonstrative pronouns — are strong-article personal pronouns with no spatial deixis (footnote 1: "it is far from clear that there is anything truly 'demonstrative' about" them); the genuine German demonstrative is dieser. So a carrier counts as a demonstrative iff it carries a Features.Deixis.Feature, not by morphological label — dieser and this instance Demonstrative, der does not (it is a PersonalPronoun). Mirrors the word-class-neutral Indefinite capability.

class Demonstrative (α : Type u_1) : Type u_1

A carrier that encodes a deictic (demonstrative) contrast: it exposes a Features.Deixis.Feature (proximal/medial/distal, or unspecified for a distance-neutral demonstrative like German dieser). The deictic feature varies per element (this proximal vs that distal), so this is a genuine per-element accessor.

• deixis : α → Features.Deixis.Feature

  The deictic feature the carrier encodes.