Moroney (2021): Definiteness and Quantification — Evidence from Shan

@cite{moroney-2021}

Shan (Southwestern Tai, Kra-Dai) bare nouns can be interpreted as indefinite, definite, generic, or kind-denoting. The key finding is that bare nouns in Shan express BOTH unique and anaphoric definiteness — contra @cite{jenks-2018}'s prediction that languages without overt definite articles mark at most one type of definiteness.

Core contributions formalized here

1. Revised definiteness marking typology (Table 4.1/4.4): adds an "unmarked" category where bare nouns express both unique and anaphoric definiteness. Languages: Shan, Serbian, Kannada.

2. Bare noun interpretation distribution (Table 2.3): Shan and English bare nouns agree on low ∃, kind, and generic readings. They differ ONLY on definite readings — Shan bare nouns can be definite, English cannot.

3. Type-shifting analysis: all bare nouns are base type ⟨s,⟨e,t⟩⟩. Definite readings arise via unblocked ι type-shift (no overt "the" to block it). Kind readings via ∩. Existential via DPP (Derived Predicate Predication, NMP.DPP), which yields obligatory low scope.

4. Cross-linguistic definiteness data (Table 4.4): Shan uses bare nouns in ALL @cite{schwarz-2009} definite use types. Demonstrative-noun phrases (N Clf Dem) are optional in anaphoric/relational-bridging/donkey contexts where German requires the strong article and Mandarin/Thai require demonstratives.

inductive Moroney2021.DefForm : Type

What form a language uses to express definiteness in a given context.

• weakArticle : DefForm
• strongArticle : DefForm
• bare : DefForm
• dem : DefForm
• bareOrDem : DefForm

@[implicit_reducible]

instance Moroney2021.instDecidableEqDefForm : DecidableEq DefForm

Equations

• Moroney2021.instDecidableEqDefForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Moroney2021.instReprDefForm : Repr DefForm

Equations

• Moroney2021.instReprDefForm = { reprPrec := Moroney2021.instReprDefForm.repr }

def Moroney2021.instReprDefForm.repr : DefForm → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Moroney2021.instReprDefForm.repr Moroney2021.DefForm.bare prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Moroney2021.DefForm.bare")).group prec✝
• Moroney2021.instReprDefForm.repr Moroney2021.DefForm.dem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Moroney2021.DefForm.dem")).group prec✝

structure Moroney2021.DefExpressionDatum : Type

Cross-linguistic datum: what form does language L use for definite use type U? Connects @cite{hawkins-1978}'s use types (already in Features.Definiteness.DefiniteUseType) to actual morphological expression.

• language : String
• useType : Features.Definiteness.DefiniteUseType
• bridgingSubtype : Option Features.Definiteness.BridgingSubtype
• form : DefForm

@[implicit_reducible]

instance Moroney2021.instReprDefExpressionDatum : Repr DefExpressionDatum

Equations

• Moroney2021.instReprDefExpressionDatum = { reprPrec := Moroney2021.instReprDefExpressionDatum.repr }

def Moroney2021.instReprDefExpressionDatum.repr : DefExpressionDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Moroney2021.instDecidableEqDefExpressionDatum : DecidableEq DefExpressionDatum

Equations

• Moroney2021.instDecidableEqDefExpressionDatum = Moroney2021.instDecidableEqDefExpressionDatum.decEq

def Moroney2021.instDecidableEqDefExpressionDatum.decEq (x✝ x✝¹ : DefExpressionDatum) : Decidable (x✝ = x✝¹)

Equations

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

def Moroney2021.germanData : List DefExpressionDatum

German data (@cite{schwarz-2009}): weak article for situational uniqueness and part-whole bridging; strong article for anaphora, producer-product bridging, and donkey anaphora.

Equations

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

def Moroney2021.thaiData : List DefExpressionDatum

Thai data (@cite{jenks-2015}): bare nouns for uniqueness contexts, demonstrative-noun phrases for anaphoric/relational contexts.

Equations

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

def Moroney2021.mandarinData : List DefExpressionDatum

Mandarin data (@cite{jenks-2018}): bare nouns for uniqueness contexts, demonstrative-noun phrases for anaphoric/relational/donkey contexts. Same pattern as Thai — Mandarin is classified as .markedAnaphoric in @cite{jenks-2018}'s typology.

Equations

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

theorem Moroney2021.mandarin_thai_same_pattern : List.map (fun (x : DefExpressionDatum) => x.form) mandarinData = List.map (fun (x : DefExpressionDatum) => x.form) thaiData

Mandarin and Thai have the same definiteness expression pattern: bare for uniqueness, demonstrative for anaphoric/relational/donkey.

def Moroney2021.shanData : List DefExpressionDatum

Shan data (@cite{moroney-2021} Table 4.4): bare nouns in ALL contexts. Demonstratives optional in anaphoric and relational-bridging contexts. This is the key empirical finding — Shan bare nouns cover ALL of Schwarz's definite use types, unlike Mandarin/Thai (anaphoric requires dem) or German (weak/strong articles).

Equations

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

theorem Moroney2021.shan_bare_in_all_contexts : (shanData.all fun (d : DefExpressionDatum) => d.form == DefForm.bare || d.form == DefForm.bareOrDem) = true

Shan bare nouns are acceptable in every definite use type.

theorem Moroney2021.german_no_bare : (germanData.all fun (d : DefExpressionDatum) => d.form == DefForm.weakArticle || d.form == DefForm.strongArticle) = true

German requires a distinct article form for every context — no bare nouns.

inductive Moroney2021.BareNounInterp : Type

The five possible interpretations of bare nouns.

• lowExistential : BareNounInterp
• highExistential : BareNounInterp
• definite : BareNounInterp
• kind : BareNounInterp
• generic : BareNounInterp

@[implicit_reducible]

instance Moroney2021.instDecidableEqBareNounInterp : DecidableEq BareNounInterp

Equations

• Moroney2021.instDecidableEqBareNounInterp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Moroney2021.instReprBareNounInterp.repr : BareNounInterp → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Moroney2021.instReprBareNounInterp : Repr BareNounInterp

Equations

• Moroney2021.instReprBareNounInterp = { reprPrec := Moroney2021.instReprBareNounInterp.repr }

structure Moroney2021.InterpAvailability : Type

Availability of a bare noun interpretation in Shan vs English.

• interp : BareNounInterp
• shanCount : Bool
• shanMass : Bool
• englishCount : Bool
• englishMass : Bool

def Moroney2021.instReprInterpAvailability.repr : InterpAvailability → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Moroney2021.instReprInterpAvailability : Repr InterpAvailability

Equations

• Moroney2021.instReprInterpAvailability = { reprPrec := Moroney2021.instReprInterpAvailability.repr }

def Moroney2021.instDecidableEqInterpAvailability.decEq (x✝ x✝¹ : InterpAvailability) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Moroney2021.instDecidableEqInterpAvailability : DecidableEq InterpAvailability

Equations

• Moroney2021.instDecidableEqInterpAvailability = Moroney2021.instDecidableEqInterpAvailability.decEq

def Moroney2021.interpretationTable : List InterpAvailability

Table 2.3: bare noun interpretation distribution in Shan and English.

Shan and English agree on four of five readings. The sole difference is the definite reading: Shan ✓ (via unblocked ι), English ✗ (ι blocked by overt the).

Equations

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

theorem Moroney2021.definite_is_sole_difference : List.map (fun (x : InterpAvailability) => x.interp) (List.filter (fun (d : InterpAvailability) => d.shanCount != d.englishCount || d.shanMass != d.englishMass) interpretationTable) = [BareNounInterp.definite]

The definite interpretation is the ONLY point where Shan and English bare nouns differ (Table 2.3).

theorem Moroney2021.high_existential_universally_blocked : ((List.filter (fun (x : InterpAvailability) => x.interp == BareNounInterp.highExistential) interpretationTable).all fun (d : InterpAvailability) => !d.shanCount && !d.shanMass && !d.englishCount && !d.englishMass) = true

High scope existential is universally unavailable for bare nouns — a consequence of DPP/DKP locality (@cite{chierchia-1998}). The existential introduced by DPP applies at the point of composition (vP level), so it cannot scope above negation.

def Moroney2021.shanBlocking : Semantics.Kinds.NMP.BlockingPrinciple

Shan has no overt determiners: all type-shifts are unblocked.

Contrast with English (MeaningPreservation.englishBlocking): the presence of the blocks covert ι, and a/some block covert ∃. In Shan, the absence of articles means the blocking principle imposes no constraints on covert type-shifting. Crucially, both ι AND ι^x are unblocked — this is what allows Shan bare nouns to express both unique and anaphoric definiteness (@cite{moroney-2021} §4.3).

Derived from Fragments.Shan.Definiteness.blocking — the single source of truth for Shan's article inventory.

Equations

• Moroney2021.shanBlocking = Fragments.Shan.Definiteness.blocking

theorem Moroney2021.shan_neutral_prefers_iota : have ctx := { number := Semantics.Kinds.MeaningPreservation.NumberFeature.neutral, downDefined := false, iotaBlocked := false, iotaAnaphoricBlocked := false, existsBlocked := false, instantiationAccessible := true }; Semantics.Kinds.MeaningPreservation.selectShift ctx = some Semantics.Kinds.MeaningPreservation.TypeShift.iota

When a Shan bare noun is used in a context requiring unique definiteness, the preferred type-shift is ι (definite), by Meaning Preservation ({∩, ι, ι^x} > ∃). Number-neutral nouns allow both ι and ∩, but ∩ requires a kind-compatible predicate (downDefined).

Compare: English singular nouns get none (MeaningPreservation.dayal_consistent_english_bare_singular_out).

theorem Moroney2021.shan_neutral_kind_prefers_down : have ctx := { number := Semantics.Kinds.MeaningPreservation.NumberFeature.neutral, downDefined := true, iotaBlocked := false, iotaAnaphoricBlocked := false, existsBlocked := false, instantiationAccessible := true }; Semantics.Kinds.MeaningPreservation.selectShift ctx = some Semantics.Kinds.MeaningPreservation.TypeShift.down

When a Shan bare noun is used with a kind-compatible predicate, ∩ is selected (it appears first in availableShifts for number-neutral nouns with downDefined).

theorem Moroney2021.shan_neutral_both_available : have ctx := { number := Semantics.Kinds.MeaningPreservation.NumberFeature.neutral, downDefined := true, iotaBlocked := false, iotaAnaphoricBlocked := false, existsBlocked := false, instantiationAccessible := true }; Semantics.Kinds.MeaningPreservation.TypeShift.down ∈ Semantics.Kinds.MeaningPreservation.availableShifts ctx ∧ Semantics.Kinds.MeaningPreservation.TypeShift.iota ∈ Semantics.Kinds.MeaningPreservation.availableShifts ctx ∧ Semantics.Kinds.MeaningPreservation.TypeShift.iotaAnaphoric ∈ Semantics.Kinds.MeaningPreservation.availableShifts ctx

Number-neutral nouns in Shan make BOTH ∩ and ι available simultaneously when the predicate is kind-compatible. This correctly predicts the ambiguity between definite and kind readings for Shan bare nouns.

theorem Moroney2021.shan_english_definiteness_contrast : Semantics.Kinds.MeaningPreservation.selectShift { number := Semantics.Kinds.MeaningPreservation.NumberFeature.neutral, downDefined := false, iotaBlocked := false, iotaAnaphoricBlocked := false, existsBlocked := false, instantiationAccessible := true } = some Semantics.Kinds.MeaningPreservation.TypeShift.iota ∧ Semantics.Kinds.MeaningPreservation.selectShift { number := Semantics.Kinds.MeaningPreservation.NumberFeature.sg, downDefined := false, iotaBlocked := true, iotaAnaphoricBlocked := true, existsBlocked := true, instantiationAccessible := true } = none

The Shan–English definiteness contrast derived from blocking.

Same base noun type (⟨s,⟨e,t⟩⟩), same type-shifting operations, different article inventories. Shan has no "the" → ι unblocked → bare nouns can be definite. English has "the" → ι blocked → bare nouns cannot be definite (must use overt determiner).

theorem Moroney2021.shan_thai_anaphoric_contrast : Semantics.Kinds.MeaningPreservation.TypeShift.iotaAnaphoric ∈ Semantics.Kinds.MeaningPreservation.availableShifts { number := Semantics.Kinds.MeaningPreservation.NumberFeature.neutral, downDefined := false, iotaBlocked := false, iotaAnaphoricBlocked := false, existsBlocked := false, instantiationAccessible := true } ∧ Semantics.Kinds.MeaningPreservation.TypeShift.iotaAnaphoric ∉ Semantics.Kinds.MeaningPreservation.availableShifts { number := Semantics.Kinds.MeaningPreservation.NumberFeature.neutral, downDefined := false, iotaBlocked := false, iotaAnaphoricBlocked := true, existsBlocked := false, instantiationAccessible := true }

The Shan–Thai anaphoric definiteness contrast derived from blocking.

Shan: ι^x is unblocked → bare nouns can be anaphorically definite. Thai: ι^x is blocked by demonstrative → demonstrative required for anaphoric definiteness. Both languages have unblocked ι (unique definiteness via bare nouns).

theorem Moroney2021.shan_exists_is_last_resort : (Semantics.Kinds.MeaningPreservation.availableShifts { number := Semantics.Kinds.MeaningPreservation.NumberFeature.neutral, downDefined := false, iotaBlocked := false, iotaAnaphoricBlocked := false, existsBlocked := false, instantiationAccessible := true }).head? = some Semantics.Kinds.MeaningPreservation.TypeShift.iota ∧ Semantics.Kinds.MeaningPreservation.TypeShift.exists ∈ Semantics.Kinds.MeaningPreservation.availableShifts { number := Semantics.Kinds.MeaningPreservation.NumberFeature.neutral, downDefined := false, iotaBlocked := false, iotaAnaphoricBlocked := false, existsBlocked := false, instantiationAccessible := true }

∃ is available as a last resort in Shan (when ∩ and ι are inapplicable), but by Meaning Preservation it is always dispreferred. This means bare nouns default to definite/kind, not existential — the existential reading arises only via DPP at vP.

theorem Moroney2021.shan_article_type : Features.Definiteness.strategyToArticleType Features.Definiteness.DefMarkingStrategy.unmarked = Features.Definiteness.ArticleType.none_

Shan's unmarked strategy correctly maps to ArticleType.none_.

theorem Moroney2021.shan_no_morphological_distinction : (Features.Definiteness.articleTypeToDistinguishedPresup Features.Definiteness.ArticleType.none_).length = 0

Features.Definiteness.articleTypeToDistinguishedPresup correctly returns zero morphologically distinguished presupposition types for Shan.

theorem Moroney2021.marking_ne_availability : (Features.Definiteness.articleTypeToDistinguishedPresup Features.Definiteness.ArticleType.none_).length = 0 ∧ shanBlocking.iotaBlocked = false ∧ shanBlocking.downBlocked = false ∧ shanBlocking.existsBlocked = false

The central Moroney insight: morphological marking ≠ semantic availability.

Shan morphologically distinguishes zero presupposition types (no articles) but semantically expresses both unique and anaphoric definiteness (via covert type-shifting). The bridge between article inventory and semantic availability is the blocking principle: no articles → no blocking → all type-shifts (ι, ι^x, ∩) available.

theorem Moroney2021.unmarked_distinct_from_existing : Features.Definiteness.DefMarkingStrategy.unmarked ≠ Features.Definiteness.DefMarkingStrategy.generallyMarked ∧ Features.Definiteness.DefMarkingStrategy.unmarked ≠ Features.Definiteness.DefMarkingStrategy.bipartite ∧ Features.Definiteness.DefMarkingStrategy.unmarked ≠ Features.Definiteness.DefMarkingStrategy.markedAnaphoric

Moroney's new category is genuinely distinct from the three existing ones.

theorem Moroney2021.derive_all_languages : Fragments.English.Definiteness.articleInventory.toMarkingStrategy = Features.Definiteness.DefMarkingStrategy.generallyMarked ∧ Fragments.German.Definiteness.articleInventory.toMarkingStrategy = Features.Definiteness.DefMarkingStrategy.bipartite ∧ Fragments.Thai.Definiteness.articleInventory.toMarkingStrategy = Features.Definiteness.DefMarkingStrategy.markedAnaphoric ∧ Fragments.Shan.Definiteness.articleInventory.toMarkingStrategy = Features.Definiteness.DefMarkingStrategy.unmarked

The four Table 4.4 languages classify into the four strategy cells when the strategy is computed from each language's Fragments.{Lang}.Definiteness.articleInventory. The classification is not stipulated — it is derived by ArticleInventory.toMarkingStrategy from the morphological inventory bools.

theorem Moroney2021.derive_consistent_with_stipulated : Fragments.English.Definiteness.articleInventory.toArticleType = Features.Definiteness.ArticleType.weakOnly ∧ Fragments.German.Definiteness.articleInventory.toArticleType = Features.Definiteness.ArticleType.weakAndStrong ∧ Fragments.Thai.Definiteness.articleInventory.toArticleType = Features.Definiteness.ArticleType.weakOnly ∧ Fragments.Shan.Definiteness.articleInventory.toArticleType = Features.Definiteness.ArticleType.none_

The inventory-derived ArticleType agrees with Schwarz's stipulated typology for the four Table 4.4 languages. The classification is derived rather than assigned by fiat — toArticleType composes toMarkingStrategy with the strategy → articleType collapse.

theorem Moroney2021.type_shift_referent_agreement (E : Type) (domain : List E) (restrictor : E → Bool) : (Core.Nominal.russellIotaList domain fun (e : E) => restrictor e && true) = Core.Nominal.russellIotaList domain restrictor

The type-shift system and the canonical referent selector agree:

• ι (unique definiteness) corresponds to russellIotaList domain R — the Russellian iota over the bare restrictor
• ι^x (anaphoric definiteness) corresponds to russellIotaList domain (R ∧ Q) — the Russellian iota over the intersection of restrictor and anaphoric filter

When Q is vacuously true, the intersected predicate R ∧ true equals R, so ι^x reduces to ι at the referent-selector layer. The denotational counterpart (presupOfReferent of these selectors) inherits this collapse by congruence.

theorem Moroney2021.dpp_scope_below_neg (interp : InterpAvailability) : interp ∈ interpretationTable → interp.interp = BareNounInterp.highExistential → interp.shanCount = false ∧ interp.shanMass = false ∧ interp.englishCount = false ∧ interp.englishMass = false

DPP yields obligatory low scope existential: the existential introduced by DPP applies at the vP level, so it cannot scope above negation. This is why highExistential is universally unavailable for bare nouns (@cite{chierchia-1998}; @cite{moroney-2021} §2.3).

The theorem derives the universal blocking from the data table rather than stipulating it.

inductive Moroney2021.FakeMassEntity : Type

Concrete witness of FakeMass behavior: Shan bare count nouns like mǎa 'dog' are CUM (the sum of two dogs is dogs) but not g-homogeneous (a dog's leg is part of a dog but is not itself a dog).

We construct a three-element partial order: two atoms a, b and their join ab = a ⊔ b. The predicate isDog holds of a, b, and ab (CUM), but fails g-homogeneity at ab because its proper parts a and b could have sub-parts (in a richer model) that are not dogs. Here we use the atoms directly: ab has proper parts a and b which ARE dogs, so g-homogeneity holds vacuously on this small model. The genuine failure requires non-atomic non-P parts, which we model by adding a non-dog atom c with c ≤ ab (representing a dog-leg).

• a : FakeMassEntity
• b : FakeMassEntity
• c : FakeMassEntity
• ab : FakeMassEntity

@[implicit_reducible]

instance Moroney2021.instDecidableEqFakeMassEntity : DecidableEq FakeMassEntity

Equations

• Moroney2021.instDecidableEqFakeMassEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Moroney2021.instReprFakeMassEntity.repr : FakeMassEntity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Moroney2021.instReprFakeMassEntity : Repr FakeMassEntity

Equations

• Moroney2021.instReprFakeMassEntity = { reprPrec := Moroney2021.instReprFakeMassEntity.repr }

@[implicit_reducible]

instance Moroney2021.instPartialOrderFakeMassEntity : PartialOrder FakeMassEntity

Equations

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

def Moroney2021.isDog : FakeMassEntity → Prop

Dog-predicate: a, b, and ab are dogs; c (the leg) is not.

Equations

• Moroney2021.isDog Moroney2021.FakeMassEntity.a = True
• Moroney2021.isDog Moroney2021.FakeMassEntity.b = True
• Moroney2021.isDog Moroney2021.FakeMassEntity.c = False
• Moroney2021.isDog Moroney2021.FakeMassEntity.ab = True

theorem Moroney2021.isDog_not_gHomogeneous : ¬Mereology.gHomogeneous isDog

isDog is not g-homogeneous: ab is a dog, c < ab, but no dog z ≤ c exists (since c is an atom and isDog c = False).

theorem Moroney2021.blocking_strategy_correspondence : have englishInv := Fragments.English.Definiteness.articleInventory; have germanInv := Fragments.German.Definiteness.articleInventory; have thaiInv := Fragments.Thai.Definiteness.articleInventory; have shanInv := Fragments.Shan.Definiteness.articleInventory; (englishInv.toMarkingStrategy = Features.Definiteness.DefMarkingStrategy.generallyMarked ∧ englishInv.hasUniqueArticle ∧ englishInv.hasAnaphoricArticle ∧ englishInv.uniqueAnaphoricSyncretism) ∧ (germanInv.toMarkingStrategy = Features.Definiteness.DefMarkingStrategy.bipartite ∧ germanInv.hasUniqueArticle ∧ germanInv.hasAnaphoricArticle ∧ ¬germanInv.uniqueAnaphoricSyncretism) ∧ (thaiInv.toMarkingStrategy = Features.Definiteness.DefMarkingStrategy.markedAnaphoric ∧ ¬thaiInv.hasUniqueArticle ∧ thaiInv.hasAnaphoricArticle) ∧ shanInv.toMarkingStrategy = Features.Definiteness.DefMarkingStrategy.unmarked ∧ ¬shanInv.hasUniqueArticle ∧ ¬shanInv.hasAnaphoricArticle ∧ shanBlocking.iotaBlocked = false ∧ shanBlocking.existsBlocked = false ∧ shanBlocking.downBlocked = false

The blocking principle connects article inventory to available type-shifts, and ArticleInventory.toMarkingStrategy connects inventory to marking strategy. This theorem shows the full correspondence for the four Table 4.4 languages: the same inventory bools that determine the marking strategy also determine which type-shifts are blocked.

This is the structural core of Moroney's analysis: article inventory is the single parameter from which both the typological classification AND the available interpretations of bare nouns are derived.

theorem Moroney2021.demonstrative_adds_spatial_info {E : Type} (domain : List E) (restrictor : E → Bool) (spatialPred : Core.Deixis.Feature → E → Bool) : (Fragments.Shan.Definiteness.demDenotation domain Fragments.Shan.Definiteness.naj restrictor spatialPred = Core.Nominal.russellIotaList domain fun (e : E) => restrictor e && spatialPred Core.Deixis.Feature.proximal e) ∧ (Fragments.Shan.Definiteness.demDenotation domain Fragments.Shan.Definiteness.nan restrictor spatialPred = Core.Nominal.russellIotaList domain fun (e : E) => restrictor e && spatialPred Core.Deixis.Feature.distal e) ∧ Fragments.Shan.Definiteness.bareDefinite domain restrictor = Core.Nominal.russellIotaList domain restrictor

Shan demonstratives refine the bare definite by adding a spatial filter to the referent selector:

• Bare noun: russellIotaList domain restrictor — any unique satisfier
• nâj: russellIotaList domain (restrictor && spatialPred .proximal)
• nân: russellIotaList domain (restrictor && spatialPred .distal)

The demonstrative is always optional in Shan because the bare noun already provides a definite reading via unblocked ι. The demonstrative adds information (spatial restriction) but never replaces an unavailable reading (unlike Thai/Mandarin where demonstratives are required for anaphoric definiteness).

When the bare definite already selects a referent that satisfies the demonstrative's spatial predicate, the demonstrative agrees with the bare form (handled by Fragments.Shan.Definiteness.dem_refines_bare).

theorem Moroney2021.shan_clf_is_atomization {α : Type u_1} [PartialOrder α] (P : α → Prop) : Semantics.Classifier.classifierDenot Typology.ClassifierStrategy.forNoun P (fun (x : α) => 0) 0 = Semantics.Classifier.clfForNoun P

Shan is a CLF-for-N language: the classifier atomizes the noun denotation (@cite{little-moroney-royer-2022}; @cite{moroney-2021} Ch. 3).

The classifier semantics module provides clfForNoun as a thin wrapper around Mereology.atomize. This bridge confirms that Shan classifiers use the atomization strategy (CLF-for-N), connecting the Shan fragment's ClassifierStrategy.forNoun to the denotation function.

The §1–§7 derivation works at the level of DefMarkingParams (three booleans). Core.Nominal.ArticleInventory is the upstream object — it records the morphological inventory directly (indefinite article, unique article, anaphoric article, syncretism flag, demonstrative paradigm, possessive paradigm) and derives the DefMarkingParams reading.

This section verifies that the inventory-derived classifications agree with the parameters used in §7 for all four languages, and connects the licensing predicate ArticleInventory.licensesKind to Moroney's central empirical finding: Shan licenses anaphoric definiteness without any anaphoric article.

@[reducible, inline]

abbrev Moroney2021.englishInv : Core.Nominal.ArticleInventory

Shorthand handles for the four Table 4.4 inventories, each defined in its language fragment (Fragments.{Lang}.Definiteness.articleInventory). Centralizing the names here keeps the §14 theorems readable without duplicating fragment-level data.

Equations

• Moroney2021.englishInv = Fragments.English.Definiteness.articleInventory

@[reducible, inline]

abbrev Moroney2021.germanInv : Core.Nominal.ArticleInventory

Equations

• Moroney2021.germanInv = Fragments.German.Definiteness.articleInventory

@[reducible, inline]

abbrev Moroney2021.mandarinInv : Core.Nominal.ArticleInventory

Equations

• Moroney2021.mandarinInv = Fragments.Mandarin.Definiteness.articleInventory

@[reducible, inline]

abbrev Moroney2021.thaiInv : Core.Nominal.ArticleInventory

Equations

• Moroney2021.thaiInv = Fragments.Thai.Definiteness.articleInventory

@[reducible, inline]

abbrev Moroney2021.shanInv : Core.Nominal.ArticleInventory

Equations

• Moroney2021.shanInv = Fragments.Shan.Definiteness.articleInventory

theorem Moroney2021.inventory_derives_all_languages : englishInv.toMarkingStrategy = Features.Definiteness.DefMarkingStrategy.generallyMarked ∧ germanInv.toMarkingStrategy = Features.Definiteness.DefMarkingStrategy.bipartite ∧ thaiInv.toMarkingStrategy = Features.Definiteness.DefMarkingStrategy.markedAnaphoric ∧ shanInv.toMarkingStrategy = Features.Definiteness.DefMarkingStrategy.unmarked

Inventory-derived strategies match §7's derive_all_languages for the four Table 4.4 languages. The inventory subsumes the params layer (the §7 *Params defs are now inv.toMarkingParams projections, so the agreement theorem that previously lived here is rfl-tautological and has been removed).

theorem Moroney2021.mandarin_in_markedAnaphoric : mandarinInv.toMarkingStrategy = Features.Definiteness.DefMarkingStrategy.markedAnaphoric

Mandarin is in .markedAnaphoric — same cell as Thai. (Not part of Moroney's Table 4.4 but anchors the Jenks 2018 typological backdrop.)

theorem Moroney2021.shan_anaphoric_not_licensed_via_article {F : Core.Logic.Intensional.Frame} (R : Core.Logic.Intensional.Variables.DenotGS F Core.Logic.Intensional.Ty.et) (d : ℕ) : ¬shanInv.licensesKind (Core.Nominal.NominalKind.anaphoric R d)

Moroney's central observation, stated against the article inventory: Shan has no article that licenses an .anaphoric NominalKind, yet expresses anaphoric definiteness through bare nouns and optional demonstratives. The licensing predicate makes this morphologically visible — .anaphoric is not licensed by Shan's inventory.

theorem Moroney2021.shan_bare_licensed {F : Core.Logic.Intensional.Frame} (R : Core.Logic.Intensional.Variables.DenotGS F Core.Logic.Intensional.Ty.et) : shanInv.licensesKind (Core.Nominal.NominalKind.bare R)

Bare nominals are licensed for Shan (and every language) — this is the morphological substrate for Moroney's analysis: Shan's anaphoric definites surface as bare nouns.

theorem Moroney2021.shan_demonstrative_licensed {F : Core.Logic.Intensional.Frame} (R : Core.Logic.Intensional.Variables.DenotGS F Core.Logic.Intensional.Ty.et) (deictic : Core.Deixis.Feature) (sIdx d : ℕ) : shanInv.licensesKind (Core.Nominal.NominalKind.demonstrative R deictic sIdx d)

Demonstratives are licensed in Shan (the nâj/nân paradigm). Combined with shan_bare_licensed, this gives the morphological inventory of strategies Shan deploys for definite reference.

theorem Moroney2021.english_anaphoric_licensed_via_syncretism {F : Core.Logic.Intensional.Frame} (R : Core.Logic.Intensional.Variables.DenotGS F Core.Logic.Intensional.Ty.et) (d : ℕ) : englishInv.licensesKind (Core.Nominal.NominalKind.anaphoric R d)

English licenses .anaphoric via the syncretic the (uniqueArticle ∧ syncretism), without an independent strong article. Contrasts with Shan (no licensing form at all) and German (independent strong form).

theorem Moroney2021.german_anaphoric_licensed_via_strong_article {F : Core.Logic.Intensional.Frame} (R : Core.Logic.Intensional.Variables.DenotGS F Core.Logic.Intensional.Ty.et) (d : ℕ) : germanInv.licensesKind (Core.Nominal.NominalKind.anaphoric R d)

German licenses .anaphoric via its independent strong article (no syncretism). The unique vs anaphoric distinction is morphologically marked.

theorem Moroney2021.english_mandarin_articleType_collapse : englishInv.toArticleType = mandarinInv.toArticleType

The English and Mandarin inventories both collapse to ArticleType.weakOnly, witnessing the lossiness of ArticleType relative to DefMarkingStrategy: the inventories differ (English has a unique article, Mandarin does not), and the strategies differ (.generallyMarked vs .markedAnaphoric), yet toArticleType collapses both to .weakOnly.

theorem Moroney2021.english_mandarin_inventory_distinct : englishInv ≠ mandarinInv

The English and Mandarin inventories themselves are distinct, even though their ArticleType classifications collide. They differ on hasUniqueArticle (English True, Mandarin False).

theorem Moroney2021.shan_bare_unique_agreement {F : Core.Logic.Intensional.Frame} (R : Core.Logic.Intensional.Variables.DenotGS F Core.Logic.Intensional.Ty.et) (sIdx : ℕ) (g : Core.Assignment F.Entity) (gs : Core.Logic.Intensional.Variables.SitAssignment F) : Core.Nominal.interpret (Core.Nominal.NominalKind.bare R) g gs = Core.Nominal.interpret (Core.Nominal.NominalKind.unique R sIdx) g gs

Shan-specific consequence of Core.Nominal.interpret_bare_eq_unique: a bare definite description and a uniqueness definite over the same restrictor select the same referent. This is the Core-API analogue of Moroney's claim that bare nouns in Shan express weak/uniqueness definiteness via unblocked ι.

theorem Moroney2021.shan_demonstrative_anaphoric_agreement {F : Core.Logic.Intensional.Frame} (R : Core.Logic.Intensional.Variables.DenotGS F Core.Logic.Intensional.Ty.et) (deictic : Core.Deixis.Feature) (sIdx d : ℕ) (g : Core.Assignment F.Entity) (gs : Core.Logic.Intensional.Variables.SitAssignment F) : Core.Nominal.interpret (Core.Nominal.NominalKind.demonstrative R deictic sIdx d) g gs = Core.Nominal.interpret (Core.Nominal.NominalKind.anaphoric R d) g gs

Shan-specific consequence of Core.Nominal.interpret_demonstrative_eq_anaphoric: the demonstrative's deictic feature is a presupposition filter, not a referent selector. Demonstrative- and anaphoric-marked descriptions over the same restrictor and discourse index pick the same entity. This is the type-theoretic correlate of Moroney's claim that nâj/nân add spatial content rather than substituting a different selector.

@cite{jenks-2018} §7 proposed a typology of definiteness marking with three attested cells (.generallyMarked, .bipartite, .markedAnaphoric) and one unattested cell (a language overtly marking only unique definites). The empirical core of @cite{moroney-2021} is the discovery that Shan instantiates a fourth attested cell — .unmarked — that Jenks's three-cell space had no slot for: bare nouns express both unique and anaphoric definiteness without any obligatory morphological marking.

The theorems below state the refutation against the substrate. Shan derives .unmarked (already proved in §7 / §14); .unmarked is distinct from each of Jenks's three cells (already proved in §6); the new content is the joint statement that Shan instantiates a strategy not in the Jenks-attested set.

theorem Moroney2021.shan_strategy_not_jenks_attested : Fragments.Shan.Definiteness.articleInventory.toMarkingStrategy ∉ Phenomena.Definiteness.Studies.Jenks2018.jenksAttestedStrategies

Shan's morphologically-derived strategy is not in the @cite{jenks-2018}-attested set (imported from Phenomena.Definiteness.Studies.Jenks2018.jenksAttestedStrategies).

theorem Moroney2021.moroney_shan_refutes_jenks_typology : Fragments.Shan.Definiteness.articleInventory.toMarkingStrategy = Features.Definiteness.DefMarkingStrategy.unmarked ∧ Features.Definiteness.DefMarkingStrategy.unmarked ∉ Phenomena.Definiteness.Studies.Jenks2018.jenksAttestedStrategies

The Moroney refutation in one statement: Shan instantiates a marking strategy that @cite{jenks-2018}'s typology predicted to be unattested. This is the formal content of the prose claim "contra @cite{jenks-2018}'s prediction" in this file's module docstring.