Shan Definiteness Fragment

@cite{moroney-2021}

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 @cite{schwarz-2009} 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

@cite{moroney-2021} §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 Fragments.Shan.Definiteness.blocking : Semantics.Kinds.NMP.BlockingPrinciple

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

Equations

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

def Fragments.Shan.Definiteness.articleInventory : Core.Nominal.ArticleInventory

Shan @cite{moroney-2021}: no overt definite or indefinite article. Demonstratives nâj/nân are optional in anaphoric contexts; bare nouns can express both unique and anaphoric definiteness. articleInventory is the canonical upstream object from which both DefMarkingStrategy (Moroney cell) and ArticleType (Schwarz cell) are derived — see toMarkingStrategy / toArticleType.

Equations

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

theorem Fragments.Shan.Definiteness.articleInventory_marking : articleInventory.toMarkingStrategy = Features.Definiteness.DefMarkingStrategy.unmarked

Shan's inventory projects to the .unmarked Moroney cell.

def Fragments.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 Fragments.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 Fragments.Shan.Definiteness.neutral_nonkind_is_iota : Semantics.Kinds.MeaningPreservation.selectShift neutralNonKindCtx = some Semantics.Kinds.MeaningPreservation.TypeShift.iota

Non-kind context yields definite (ι) reading.

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

Kind context yields kind (∩) reading.

theorem Fragments.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 Fragments.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 Core.Deixis.Feature (promoted from the former local SpatialRelation enum, 0.229.890).

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

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

Equations

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

@[implicit_reducible]

instance Fragments.Shan.Definiteness.instReprShanDemonstrative : Repr ShanDemonstrative

Equations

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

def Fragments.Shan.Definiteness.naj : ShanDemonstrative

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

Equations

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

def Fragments.Shan.Definiteness.nan : ShanDemonstrative

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

Equations

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

def Fragments.Shan.Definiteness.demDenotation {E : Type} (domain : List E) (dem : ShanDemonstrative) (restrictor : E → Bool) (spatialPred : Core.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 Core.Nominal.russellIotaList returning none when no unique satisfier exists.

Equations

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

def Fragments.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

• Fragments.Shan.Definiteness.bareDefinite domain restrictor = Core.Nominal.russellIotaList domain restrictor

theorem Fragments.Shan.Definiteness.dem_refines_bare {E : Type} (domain : List E) (restrictor : E → Bool) (spatialPred : Core.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 Fragments.Shan.Definiteness.liftToPrProp {E : Type} (selector : Option E) (scope : E → Bool) : Core.Presupposition.PrProp Unit

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

Equations

• Fragments.Shan.Definiteness.liftToPrProp selector scope = Core.Presupposition.PrProp.presupOfReferent (fun (x : Unit) => selector) fun (e : E) (x : Unit) => scope e