Shan Definiteness Fragment

[Mor21]

Language-specific parameters for definiteness in Shan (Southwestern Tai, Kra-Dai). Shan has no overt definite or indefinite articles — bare nouns express both unique and anaphoric definiteness via unblocked covert type-shifting.

Key Properties

1. No articles: hasUniqueForm = false, hasAnaphoricForm = false
2. Unmarked strategy: DefMarkingStrategy.unmarked — bare nouns cover all [Sch09b] use types
3. Unblocked type-shifts: ι, ι^x, ∩, and ∃ are all available
4. Demonstratives: nâj (proximal) and nân (distal) are optional in anaphoric contexts, required in no context

Demonstrative Semantics

[Mor21] §2.1.3:

• ⟦nâj⟧ = λP : |P_s| = 1. ιx[P_s(x) ∧ CLOSE.TO.SPEAKER(x)]
• ⟦nân⟧ = λP : |P_s| = 1. ιx[P_s(x) ∧ FAR.FROM.SPEAKER(x)]

Both carry a cardinality presupposition (unique satisfier in the situation) and add spatial content to the presupposition filter.

def Shan.Definiteness.blocking : Semantics.Kinds.NMP.BlockingPrinciple

Shan blocking principle: no overt determiners block any type-shift.

Equations

• Shan.Definiteness.blocking = { determiners := [], iotaBlocked := false, existsBlocked := false, downBlocked := false }

def Shan.Definiteness.determiners : List Determiner.Entry

Shan [Mor21]: no overt definite or indefinite article — no .article entries. Demonstratives nâj/nân are optional in anaphoric contexts (their definiteUses are empty: they obligatorily expone nothing), so bare nouns can express both unique and anaphoric definiteness. The declared determiner set is the canonical upstream object from which both DefMarkingStrategy (Moroney cell) and ArticleType (Schwarz cell) are derived — see Determiner.markingStrategy / Determiner.articleType.

Equations

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

theorem Shan.Definiteness.marking : Determiner.markingStrategy determiners = Features.Definiteness.DefMarkingStrategy.unmarked

Shan's determiner set projects to the .unmarked Moroney cell.

def Shan.Definiteness.neutralNonKindCtx : Semantics.Kinds.MeaningPreservation.TypeShiftContext

Type-shift context for Shan number-neutral bare nouns with a non-kind-compatible predicate (e.g., mǎa 'dog' in episodic context). ι is selected: definite reading.

Equations

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

def Shan.Definiteness.neutralKindCtx : Semantics.Kinds.MeaningPreservation.TypeShiftContext

Type-shift context for Shan number-neutral bare nouns with a kind-compatible predicate (e.g., mǎa 'dog' in generic context). ∩ is selected: kind reading.

Equations

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

theorem Shan.Definiteness.neutral_nonkind_is_iota : Semantics.Kinds.MeaningPreservation.selectShift neutralNonKindCtx = some Semantics.Kinds.MeaningPreservation.TypeShift.iota

Non-kind context yields definite (ι) reading.

theorem Shan.Definiteness.neutral_kind_is_down : Semantics.Kinds.MeaningPreservation.selectShift neutralKindCtx = some Semantics.Kinds.MeaningPreservation.TypeShift.down

Kind context yields kind (∩) reading.

theorem Shan.Definiteness.all_shifts_available : Semantics.Kinds.MeaningPreservation.TypeShift.down ∈ Semantics.Kinds.MeaningPreservation.availableShifts neutralKindCtx ∧ Semantics.Kinds.MeaningPreservation.TypeShift.iota ∈ Semantics.Kinds.MeaningPreservation.availableShifts neutralKindCtx ∧ Semantics.Kinds.MeaningPreservation.TypeShift.iotaAnaphoric ∈ Semantics.Kinds.MeaningPreservation.availableShifts neutralKindCtx ∧ Semantics.Kinds.MeaningPreservation.TypeShift.exists ∈ Semantics.Kinds.MeaningPreservation.availableShifts neutralKindCtx

All three high-ranked shifts (∩, ι, ι^x) are available in kind context.

structure Shan.Definiteness.ShanDemonstrative : Type

Shan demonstrative entry: form, gloss, and deictic content. Demonstratives in Shan appear in the structure [N Clf Dem]. The spatial field reuses the framework-agnostic Features.Deixis.Feature (promoted from the former local SpatialRelation enum, 0.229.890).

• form : String
• gloss : String
• spatial : Features.Deixis.Feature

@[implicit_reducible]

instance Shan.Definiteness.instReprShanDemonstrative : Repr ShanDemonstrative

Equations

• Shan.Definiteness.instReprShanDemonstrative = { reprPrec := Shan.Definiteness.instReprShanDemonstrative.repr }

def Shan.Definiteness.instReprShanDemonstrative.repr : ShanDemonstrative → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Shan.Definiteness.instDemonstrativeShanDemonstrative : Demonstrative ShanDemonstrative

A Shan demonstrative is a Demonstrative carrier — its spatial field is the deictic contrast the capability exposes.

Equations

• Shan.Definiteness.instDemonstrativeShanDemonstrative = { deixis := Shan.Definiteness.ShanDemonstrative.spatial }

def Shan.Definiteness.naj : ShanDemonstrative

nâj — proximal demonstrative ('this').

Equations

• Shan.Definiteness.naj = { form := "nâj", gloss := "this", spatial := Features.Deixis.Feature.proximal }

def Shan.Definiteness.nan : ShanDemonstrative

nân — distal demonstrative ('that').

Equations

• Shan.Definiteness.nan = { form := "nân", gloss := "that", spatial := Features.Deixis.Feature.distal }

theorem Shan.Definiteness.shan_demonstratives_encode_distance : (Demonstrative.deixis naj).EncodesDistance ∧ (Demonstrative.deixis nan).EncodesDistance

Both Shan demonstratives encode a distance contrast (nâj proximal, nân distal).

def Shan.Definiteness.demDenotation {E : Type} (domain : List E) (dem : ShanDemonstrative) (restrictor : E → Bool) (spatialPred : Features.Deixis.Feature → E → Bool) : Option E

Demonstrative denotation as a referent selector with spatial filter.

⟦DEM⟧(P) = ιx[P(x) ∧ SPATIAL(x)]

The demonstrative combines the restrictor P with a spatial filter encoding proximity to the speaker. The cardinality presupposition (|P_s| = 1) is handled by Semantics.Definiteness.russellIotaList returning none when no unique satisfier exists.

Equations

• Shan.Definiteness.demDenotation domain dem restrictor spatialPred = Semantics.Definiteness.russellIotaList domain fun (e : E) => restrictor e && spatialPred dem.spatial e

def Shan.Definiteness.bareDefinite {E : Type} (domain : List E) (restrictor : E → Bool) : Option E

A bare definite description (no demonstrative) uses no filter: any entity satisfying the restrictor is a candidate, regardless of spatial location. This is the uniqueness-based (weak) reading.

Equations

• Shan.Definiteness.bareDefinite domain restrictor = Semantics.Definiteness.russellIotaList domain restrictor

theorem Shan.Definiteness.dem_refines_bare {E : Type} (domain : List E) (restrictor : E → Bool) (spatialPred : Features.Deixis.Feature → E → Bool) (dem : ShanDemonstrative) (e : E) (hBare : bareDefinite domain restrictor = some e) (hSpatial : spatialPred dem.spatial e = true) : demDenotation domain dem restrictor spatialPred = some e

The demonstrative refines the bare definite: when the bare description selects a referent that also satisfies the spatial predicate, both selectors agree; the demonstrative can additionally select among multiple bare-restrictor satisfiers when the spatial filter narrows them to a singleton.

def Shan.Definiteness.liftToPartialProp {E : Type} (selector : Option E) (scope : E → Bool) : Semantics.Presupposition.PartialProp Unit

Lift a referent selector to a PartialProp Unit via the canonical presupOfReferent combinator. The presupposition is referent definedness; the assertion is the scope applied to the referent.

Equations

• Shan.Definiteness.liftToPartialProp selector scope = Semantics.Presupposition.PartialProp.presupOfReferent (fun (x : Unit) => selector) fun (e : E) (x : Unit) => scope e = true