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

[Mor21] shows that Shan (Southwestern Tai, Kra-Dai) bare nouns express both unique and anaphoric definiteness, instantiating an unmarked cell that [Jen18]'s definiteness typology had no slot for. Because Shan has no articles, no covert type-shift is blocked — ι, ι^x, and ∩ are all available to bare nouns — while the optional demonstratives nâj/nân merely add spatial content. The cell is derived from Shan.Determiners.inventory, the bare-noun reading distribution from MeaningPreservation.selectShift over Shan.Nouns.blocking, and the refutation is stated against Jenks2018.jenksAttestedStrategies.

References

• [Mor21]

Bare-noun readings (Table 2.3)

inductive Moroney2021.BareNounInterp : Type

The five candidate readings of a bare noun.

• lowExistential : BareNounInterp

  Low-scope ∃, introduced by Derived Predicate Predication at vP ([Mor21] (85)), hence below negation.

• highExistential : BareNounInterp

  Wide-scope ∃ above negation — unavailable to bare nouns, since DPP applies no higher than vP.

• definite : BareNounInterp

  Definite, via the ι type-shift.

• kind : BareNounInterp

  Kind, via the ∩ type-shift.

• generic : BareNounInterp

  Generic, via GEN over situations.

@[instance_reducible]

instance Moroney2021.instDecidableEqBareNounInterp : DecidableEq BareNounInterp

Equations

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

@[instance_reducible]

instance Moroney2021.instReprBareNounInterp : Repr BareNounInterp

Equations

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

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

Equations

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

structure Moroney2021.InterpAvailability : Type

One Table 2.3 row: whether a reading is available to Shan and English count and mass bare nouns.

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

@[instance_reducible]

instance Moroney2021.instReprInterpAvailability : Repr InterpAvailability

Equations

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

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

Equations

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

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

Equations

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

@[instance_reducible]

instance Moroney2021.instDecidableEqInterpAvailability : DecidableEq InterpAvailability

Equations

• Moroney2021.instDecidableEqInterpAvailability = Moroney2021.instDecidableEqInterpAvailability.decEq

def Moroney2021.interpretationTable : List InterpAvailability

Table 2.3: Shan and English bare nouns share the low-∃, kind, and generic readings, both lack the high-∃ reading, and part ways only on the definite reading.

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 reading is the sole point where Shan and English bare nouns differ.

Type-shift selection

def Moroney2021.shanCtx (downDefined : Bool) : Semantics.Kinds.MeaningPreservation.TypeShiftContext

The type-shift context of a Shan number-neutral bare noun: nothing is blocked (Shan.Nouns.blocking), and only the predicate's kind-compatibility varies.

Equations

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

theorem Moroney2021.shan_iota_english_none : Semantics.Kinds.MeaningPreservation.selectShift (shanCtx false) = 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

With a non-kind predicate a Shan bare noun type-shifts by ι — the definite reading — while an English bare singular gets no shift at all, since the and a block ι and ∃.

theorem Moroney2021.shan_kind_ambiguity : Semantics.Kinds.MeaningPreservation.selectShift (shanCtx true) = some Semantics.Kinds.MeaningPreservation.TypeShift.down ∧ Semantics.Kinds.MeaningPreservation.TypeShift.iota ∈ Semantics.Kinds.MeaningPreservation.availableShifts (shanCtx true) ∧ Semantics.Kinds.MeaningPreservation.TypeShift.iotaAnaphoric ∈ Semantics.Kinds.MeaningPreservation.availableShifts (shanCtx true)

With a kind-compatible predicate ∩ is selected while ι and ι^x remain available — the definite/kind ambiguity of Shan bare nouns.

theorem Moroney2021.shan_thai_anaphoric_contrast : Semantics.Kinds.MeaningPreservation.TypeShift.iotaAnaphoric ∈ Semantics.Kinds.MeaningPreservation.availableShifts (shanCtx false) ∧ Semantics.Kinds.MeaningPreservation.TypeShift.iotaAnaphoric ∉ Semantics.Kinds.MeaningPreservation.availableShifts (have __src := shanCtx false; { number := __src.number, downDefined := __src.downDefined, iotaBlocked := __src.iotaBlocked, iotaAnaphoricBlocked := true, existsBlocked := __src.existsBlocked, instantiationAccessible := __src.instantiationAccessible })

Shan's ι^x is unblocked, so bare nouns reach anaphoric definiteness; blocking ι^x — Thai's demonstrative — removes exactly that reading.

theorem Moroney2021.shan_exists_is_last_resort : (Semantics.Kinds.MeaningPreservation.availableShifts (shanCtx false)).head? = some Semantics.Kinds.MeaningPreservation.TypeShift.iota ∧ Semantics.Kinds.MeaningPreservation.TypeShift.exists ∈ Semantics.Kinds.MeaningPreservation.availableShifts (shanCtx false)

ι outranks ∃ under Meaning Preservation: ∃ is available but never selected when ι is, so Shan bare nouns default to definite or kind readings, and the existential reading arises only through DPP at vP — whence the missing high-∃ row of Table 2.3.

The typology, derived per language (Tables 4.1 and 4.4)

theorem Moroney2021.derive_all_languages : English.Determiners.inventory.markingStrategy = Semantics.Definiteness.DefMarkingStrategy.generallyMarked ∧ German.Determiners.inventory.markingStrategy = Semantics.Definiteness.DefMarkingStrategy.bipartite ∧ Thai.Determiners.inventory.markingStrategy = Semantics.Definiteness.DefMarkingStrategy.markedAnaphoric ∧ Shan.Determiners.inventory.markingStrategy = Semantics.Definiteness.DefMarkingStrategy.unmarked

Each Table 4.4 language's marking strategy, computed by Determiner.Inventory.markingStrategy from its declared inventory: the four languages fill all four cells of the revised typology.

theorem Moroney2021.derive_article_types : English.Determiners.inventory.articleType = Semantics.Definiteness.ArticleType.weakOnly ∧ German.Determiners.inventory.articleType = Semantics.Definiteness.ArticleType.weakAndStrong ∧ Thai.Determiners.inventory.articleType = Semantics.Definiteness.ArticleType.weakOnly ∧ Shan.Determiners.inventory.articleType = Semantics.Definiteness.ArticleType.none_

The [Sch13]-style article-type projection of the same inventories.

theorem Moroney2021.articleType_lossy : English.Determiners.inventory.markingStrategy ≠ Mandarin.Determiners.inventory.markingStrategy ∧ English.Determiners.inventory.articleType = Mandarin.Determiners.inventory.articleType

ArticleType is lossy where DefMarkingStrategy is not: English and Mandarin differ in strategy yet collapse to the same article type.

Shan count nouns are fake-mass nouns (§2.3.1)

inductive Moroney2021.FakeMassEntity : Type

A four-element mereology: dogs a, b, their sum ab, and a leg c below the sum that is not a dog.

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

@[instance_reducible]

instance Moroney2021.instDecidableEqFakeMassEntity : DecidableEq FakeMassEntity

Equations

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

@[instance_reducible]

instance Moroney2021.instFintypeFakeMassEntity : Fintype FakeMassEntity

Equations

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

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

Equations

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

@[instance_reducible]

instance Moroney2021.instReprFakeMassEntity : Repr FakeMassEntity

Equations

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

@[instance_reducible]

instance Moroney2021.instSemilatticeSupFakeMassEntity : SemilatticeSup FakeMassEntity

Equations

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

def Moroney2021.isDog : FakeMassEntity → Prop

Dogs: the atoms a, b and their sum ab; the leg c is not a dog.

Equations

• Moroney2021.isDog Moroney2021.FakeMassEntity.c = False
• Moroney2021.isDog x✝ = True

@[instance_reducible]

instance Moroney2021.instDecidablePredFakeMassEntityIsDog : DecidablePred isDog

Equations

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

theorem Moroney2021.isDog_fakeMass : Mereology.FakeMass isDog

Shan bare count nouns pattern with English furniture-type nouns ([Mor21] §2.3.1): cumulative — the sum of dogs is dogs — but not g-homogeneous, since the leg below the sum has no dog part.

Demonstratives add spatial content (§2.4.3)

def Moroney2021.demDenotation {E : Type} (domain : List E) (d : DemonstrativeDeterminer) (restrictor : E → Bool) (spatialPred : Features.Deixis.Feature → E → Bool) : Option E

The demonstrative denotation of [Mor21] (147)–(148), a referent selector with the demonstrative's spatial content added to the restrictor: ⟦DEM⟧(P) = ιx[P(x) ∧ SPATIAL(x)], where russellIotaList carries the uniqueness presupposition.

Equations

• Moroney2021.demDenotation domain d restrictor spatialPred = Semantics.Definiteness.russellIotaList domain fun (e : E) => restrictor e && spatialPred d.deictic e

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

The bare definite description is the unfiltered referent selector, the uniqueness-based reading available to Shan bare nouns.

Equations

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

theorem Moroney2021.dem_refines_bare {E : Type} (domain : List E) (restrictor : E → Bool) (spatialPred : Features.Deixis.Feature → E → Bool) (d : DemonstrativeDeterminer) (e : E) (hBare : bareDefinite domain restrictor = some e) (hSpatial : spatialPred d.deictic e = true) : demDenotation domain d restrictor spatialPred = some e

When the bare description selects a referent that satisfies the demonstrative's spatial predicate, the demonstrative selects the same referent, so nâj/nân are optional in such contexts — the bare noun already provides the definite reading via unblocked ι.

Realization: anaphoric definiteness without an anaphoric article

theorem Moroney2021.shan_anaphoric_not_realized_via_article : ¬Shan.Determiners.inventory.Realizes Semantics.Definiteness.DescriptionKind.anaphoric

Shan has no determiner realizing anaphoric definiteness, yet expresses it — through bare nouns (unblocked ι^x) and the optional demonstratives.

theorem Moroney2021.shan_demonstrative_realized : Shan.Determiners.inventory.Realizes Semantics.Definiteness.DescriptionKind.demonstrative

Shan does realize the demonstrative kind — the nâj/nân paradigm.

theorem Moroney2021.english_german_anaphoric_realized : English.Determiners.inventory.Realizes Semantics.Definiteness.DescriptionKind.anaphoric ∧ German.Determiners.inventory.Realizes Semantics.Definiteness.DescriptionKind.anaphoric

English realizes anaphoric definiteness through syncretic the and German through its dedicated strong article, while Shan has no realizing form at all.

Refuting Jenks's attested-cell prediction

theorem Moroney2021.shan_refutes_jenks_typology : Shan.Determiners.inventory.markingStrategy ∉ Jenks2018.jenksAttestedStrategies

Shan's derived strategy falls outside [Jen18]'s attested set — the discovery of the fourth, unmarked cell.