Deictic Features: Demonstrative Distance and Person Orientation

@cite{moroney-2021}

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 Core.Nominal.NominalKind.deictic (forthcoming) and by demonstrative entries in Fragments/.

inductive Core.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 Core.Deixis.instDecidableEqFeature : DecidableEq Feature

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Core.Deixis.instReprFeature.repr Core.Deixis.Feature.medial prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Deixis.Feature.medial")).group prec✝
• Core.Deixis.instReprFeature.repr Core.Deixis.Feature.distal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Deixis.Feature.distal")).group prec✝

@[implicit_reducible]

instance Core.Deixis.instReprFeature : Repr Feature

Equations

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

def Core.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 ≠ Core.Deixis.Feature.unspecified)

@[implicit_reducible]

instance Core.Deixis.instDecidablePredFeatureEncodesDistance : DecidablePred Feature.EncodesDistance

Equations

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

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

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