Modal indefinites and semantic variation: lessons from Chuj

[AOR24]'s account of Chuj yalnhej: the modal component is at-issue, event-relative (Semantics/Modality/EventRelativity, after [Hac06]), and its flavor is derived from structural position and predicate volitionality rather than stipulated lexically. The lexical entries live in the ModalIndefinites fragments (Chuj, Spanish, German, French, Italian); this file holds the paper's denotation, the cross-linguistic typology over the pooled entries, the position × volitionality derivation, and finite-model witnesses for non-maximality, upper-boundedness, and harmonic anchoring.

One departure from [Hac06] (§4.1, fn. 17): yalnhej's anchor can be left free — bound by the speech-act event rather than the closest event binder — which is how external arguments above AspP still access the speech event.

Main declarations

• modalIndefiniteSat, upperBoundedSat — the paper's denotation (59).
• allEntries — the pooled fragment paradigms.
• predictedMIFlavors, flavor_pattern_derived — the position × volitionality pattern, derived from accessibleBinders and rcAvailable.

The modal indefinite denotation ((59))

def AlonsoOvalleRoyer2024.modalIndefiniteSat {Event : Type u_1} {W : Type u_2} {Entity : Type u_3} (f : Modality.AnchoringFn Event W) (e : Event) (domain : List Entity) (P Q : Entity → W → Prop) (w : W) : Prop

The modal indefinite denotation (59):

`⟦MI⟧^{f,e₁} = λP.λQ.λw. ∃x[P(x)(w) ∧ Q(x)(w)] ∧ ∀y[P(y)(w) → ◇_{f(e₁)}(Q(y)(w'))]`

Some domain member satisfies restrictor and scope, and every restrictor member is a possible scope-satisfier — the modal-variation effect.

Equations

• AlonsoOvalleRoyer2024.modalIndefiniteSat f e domain P Q w = ((∃ x ∈ domain, P x w ∧ Q x w) ∧ ∀ y ∈ domain, P y w → Modality.Kratzer.simplePossibility (f e) (Q y) w)

def AlonsoOvalleRoyer2024.upperBoundedSat {Event : Type u_1} {W : Type u_2} {Entity : Type u_3} (f : Modality.AnchoringFn Event W) (e : Event) (domain : List Entity) (P Q : Entity → W → Prop) (w : W) : Prop

The upper-bounded denotation: additionally, not every P is Q in the actual world — algún's witness upper bound (§4.2; distinct from the anti-singleton domain constraint of [AOMB10]).

Equations

• AlonsoOvalleRoyer2024.upperBoundedSat f e domain P Q w = (AlonsoOvalleRoyer2024.modalIndefiniteSat f e domain P Q w ∧ ¬∀ x ∈ domain, P x w → Q x w)

theorem AlonsoOvalleRoyer2024.upperBounded_entails_plain {Event : Type u_1} {W : Type u_2} {Entity : Type u_3} (f : Modality.AnchoringFn Event W) (e : Event) (domain : List Entity) (P Q : Entity → W → Prop) (w : W) (h : upperBoundedSat f e domain P Q w) : modalIndefiniteSat f e domain P Q w

Upper-boundedness strengthens the plain denotation.

The pooled sample

def AlonsoOvalleRoyer2024.allEntries : List Features.ModalIndefinite.ModalIndefiniteEntry

The pooled cross-linguistic sample: the five fragment paradigms.

Equations

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

Typological Generalizations (§6)

theorem AlonsoOvalleRoyer2024.yalnhej_irgendein_minimal_pair : Chuj.ModalIndefinites.yalnhejEntry.flavors = German.ModalIndefinites.irgendeinEntry.flavors ∧ Chuj.ModalIndefinites.yalnhejEntry.status ≠ German.ModalIndefinites.irgendeinEntry.status

Status and content are independent: yalnhej and irgendein share the same flavor inventory but differ in status (§6.1).

theorem AlonsoOvalleRoyer2024.yalnhej_unique_profile : (List.filter (fun (e : Features.ModalIndefinite.ModalIndefiniteEntry) => e.status == Features.ModalIndefinite.ModalComponentStatus.atIssue && e.hasFlavor Modality.ModalFlavor.epistemic && e.hasFlavor Modality.ModalFlavor.circumstantial) allEntries).length = 1

Yalnhej is the sample's only at-issue item with both epistemic and random-choice flavors.

Independence of Dimensions

theorem AlonsoOvalleRoyer2024.status_ub_independent : ((((allEntries.any fun (e : Features.ModalIndefinite.ModalIndefiniteEntry) => e.status == Features.ModalIndefinite.ModalComponentStatus.atIssue && e.upperBounded) && allEntries.any fun (e : Features.ModalIndefinite.ModalIndefiniteEntry) => e.status == Features.ModalIndefinite.ModalComponentStatus.atIssue && !e.upperBounded) && allEntries.any fun (e : Features.ModalIndefinite.ModalIndefiniteEntry) => e.status == Features.ModalIndefinite.ModalComponentStatus.notAtIssue && e.upperBounded) && allEntries.any fun (e : Features.ModalIndefinite.ModalIndefiniteEntry) => e.status == Features.ModalIndefinite.ModalComponentStatus.notAtIssue && !e.upperBounded) = true

Status and upper-boundedness are independent: all four cells of the 2×2 matrix are attested (uno cualquiera, yalnhej, algún, irgendein).

AnchorConstraint Bridge

theorem AlonsoOvalleRoyer2024.anchored_entries_at_issue : (allEntries.all fun (e : Features.ModalIndefinite.ModalIndefiniteEntry) => !e.anchorConstraint.isSome || e.status == Features.ModalIndefinite.ModalComponentStatus.atIssue) = true

Anchored entries are at-issue: event-relative anchoring is the paper's mechanism for at-issue modal components. The converse fails — komon is at-issue yet fits neither anchor constructor (§6.2). True by construction of the entries.

theorem AlonsoOvalleRoyer2024.anchor_constraint_underdetermines_flavor : Spanish.ModalIndefinites.unoCualquieraEntry.anchorConstraint = some Features.ModalIndefinite.AnchorConstraint.volitionalOnly ∧ Spanish.ModalIndefinites.unoCualquieraEntry.hasFlavor Modality.ModalFlavor.epistemic = false ∧ Chuj.ModalIndefinites.yalnhejEntry.anchorConstraint = some Features.ModalIndefinite.AnchorConstraint.unrestricted ∧ Chuj.ModalIndefinites.yalnhejEntry.hasFlavor Modality.ModalFlavor.epistemic = true ∧ French.ModalIndefinites.nimporteQuelEntry.anchorConstraint = some Features.ModalIndefinite.AnchorConstraint.unrestricted ∧ French.ModalIndefinites.nimporteQuelEntry.hasFlavor Modality.ModalFlavor.epistemic = false

The anchor constraint underdetermines flavor (§6.2): uno cualquiera's volitional-only f blocks epistemic readings, while the unrestricted constraint admits both an epistemic item (yalnhej) and a random-choice-only one (n'importe quel).

Position and accessible binders

inductive AlonsoOvalleRoyer2024.ChujArgPosition : Type

Structural position of a DP in the Chuj clause. Factored from verb volitionality (an orthogonal property of the predicate, not of the structural position).

• external : ChujArgPosition

  External argument (above vP): subject of transitive

• internal : ChujArgPosition

  Internal argument (within vP): object, complement

• adjunct : ChujArgPosition

  Adjunct (adjoined to vP): locative, manner, etc.

@[instance_reducible]

instance AlonsoOvalleRoyer2024.instDecidableEqChujArgPosition : DecidableEq ChujArgPosition

Equations

• AlonsoOvalleRoyer2024.instDecidableEqChujArgPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AlonsoOvalleRoyer2024.instReprChujArgPosition.repr : ChujArgPosition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AlonsoOvalleRoyer2024.instReprChujArgPosition : Repr ChujArgPosition

Equations

• AlonsoOvalleRoyer2024.instReprChujArgPosition = { reprPrec := AlonsoOvalleRoyer2024.instReprChujArgPosition.repr }

def AlonsoOvalleRoyer2024.accessibleBinders : ChujArgPosition → List Modality.EventBinder

The event binders accessible from a position: external arguments sit above the aspectual projection that binds the VP event, so only the speech-act event is accessible; internal arguments and adjuncts access both.

Equations

• AlonsoOvalleRoyer2024.accessibleBinders AlonsoOvalleRoyer2024.ChujArgPosition.external = [Modality.EventBinder.speechAct]
• AlonsoOvalleRoyer2024.accessibleBinders AlonsoOvalleRoyer2024.ChujArgPosition.internal = [Modality.EventBinder.speechAct, Modality.EventBinder.vpEvent]
• AlonsoOvalleRoyer2024.accessibleBinders AlonsoOvalleRoyer2024.ChujArgPosition.adjunct = [Modality.EventBinder.speechAct, Modality.EventBinder.vpEvent]

MI Flavor Derivation via EventBinder

def AlonsoOvalleRoyer2024.miAnchorFlavor (b : Modality.EventBinder) : Modality.ModalFlavor

The MI flavor projected by an event binder: speech-act events project epistemic, VP events circumstantial (via EventBinder.toAnchorType and AnchorType.toFlavor).

Equations

• AlonsoOvalleRoyer2024.miAnchorFlavor b = b.toAnchorType.toFlavor

def AlonsoOvalleRoyer2024.baseMIFlavors (pos : ChujArgPosition) : List Modality.ModalFlavor

One flavor per accessible binder.

Equations

• AlonsoOvalleRoyer2024.baseMIFlavors pos = List.map AlonsoOvalleRoyer2024.miAnchorFlavor (AlonsoOvalleRoyer2024.accessibleBinders pos)

def AlonsoOvalleRoyer2024.rcAvailable (pos : ChujArgPosition) (volitional : Bool) : Bool

Random choice requires VP-event access (internal or adjunct position) and a volitional predicate, whose decision subevent anchors the reading.

Equations

• AlonsoOvalleRoyer2024.rcAvailable pos volitional = (((AlonsoOvalleRoyer2024.accessibleBinders pos).any fun (x : Modality.EventBinder) => x == Modality.EventBinder.vpEvent) && volitional)

def AlonsoOvalleRoyer2024.predictedMIFlavors (pos : ChujArgPosition) (volitional : Bool) : List Modality.ModalFlavor

Predicted MI flavors: where random choice is unavailable, the circumstantial flavor is filtered out.

Equations

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

Flavor Pattern Verification

theorem AlonsoOvalleRoyer2024.flavor_pattern_derived : predictedMIFlavors ChujArgPosition.external true = [Modality.ModalFlavor.epistemic] ∧ predictedMIFlavors ChujArgPosition.external false = [Modality.ModalFlavor.epistemic] ∧ predictedMIFlavors ChujArgPosition.internal true = [Modality.ModalFlavor.epistemic, Modality.ModalFlavor.circumstantial] ∧ predictedMIFlavors ChujArgPosition.internal false = [Modality.ModalFlavor.epistemic] ∧ predictedMIFlavors ChujArgPosition.adjunct true = [Modality.ModalFlavor.epistemic, Modality.ModalFlavor.circumstantial] ∧ predictedMIFlavors ChujArgPosition.adjunct false = [Modality.ModalFlavor.epistemic]

The position × volitionality flavor pattern of §3.4, derived from accessible binders, flavor projection, and the volitionality constraint.

Voice heads to flavors

Voice heads with [D] introduce a specifier above AspP, whose event variable is bound by the speech-act event; without [D] the highest DP is the internal argument, accessible to both binders.

def AlonsoOvalleRoyer2024.argPositionOf (vh : Minimalist.Voice.Head) : ChujArgPosition

Argument position from the Voice head: [+D] heads project an external argument above AspP.

Equations

• AlonsoOvalleRoyer2024.argPositionOf vh = if vh.hasD = true then AlonsoOvalleRoyer2024.ChujArgPosition.external else AlonsoOvalleRoyer2024.ChujArgPosition.internal

def AlonsoOvalleRoyer2024.predictedMIFlavorsOf (vh : Minimalist.Voice.Head) (volitional : Bool) : List Modality.ModalFlavor

Flavor predictions for a Voice head and predicate volitionality.

Equations

• AlonsoOvalleRoyer2024.predictedMIFlavorsOf vh volitional = AlonsoOvalleRoyer2024.predictedMIFlavors (AlonsoOvalleRoyer2024.argPositionOf vh) volitional

theorem AlonsoOvalleRoyer2024.voice_flavor_predictions : predictedMIFlavorsOf Coon2019.vØ true = [Modality.ModalFlavor.epistemic] ∧ predictedMIFlavorsOf Coon2019.v_w true = [Modality.ModalFlavor.epistemic] ∧ predictedMIFlavorsOf Coon2019.v_ch true = [Modality.ModalFlavor.epistemic, Modality.ModalFlavor.circumstantial] ∧ predictedMIFlavorsOf Coon2019.v_j true = [Modality.ModalFlavor.epistemic, Modality.ModalFlavor.circumstantial] ∧ predictedMIFlavorsOf Coon2019.v_ch false = [Modality.ModalFlavor.epistemic] ∧ predictedMIFlavorsOf Coon2019.v_j false = [Modality.ModalFlavor.epistemic]

Flavor predictions per voice head: the external-argument heads (Ø, -w) admit epistemic only; the internal-argument heads (-ch, -j) admit both with a volitional predicate and epistemic only without (§3.4).

Flavor selectivity (§6.2)

theorem AlonsoOvalleRoyer2024.komon_never_epistemic : Chuj.ModalIndefinites.komonEntry.hasFlavor Modality.ModalFlavor.epistemic = false ∧ Chuj.ModalIndefinites.yalnhejEntry.hasFlavor Modality.ModalFlavor.epistemic = true

Komon can never express speaker ignorance ([AOR21]); yalnhej can.

Unremarkable Readings and Predicativity (§5)

theorem AlonsoOvalleRoyer2024.predicativity_correlates_unremarkable : (allEntries.all fun (e : Features.ModalIndefinite.ModalIndefiniteEntry) => e.canBePredicate == e.hasUnremarkableReading) = true

Predicativity and unremarkable readings coincide across all seven entries (§5). True by construction of the entries — the two fields were filled from the same diagnostics — so this records the encoding, not an independent prediction.

theorem AlonsoOvalleRoyer2024.numberNeutral_implies_not_ub : ((List.filter (fun (x : Features.ModalIndefinite.ModalIndefiniteEntry) => x.numberNeutral) allEntries).all fun (x : Features.ModalIndefinite.ModalIndefiniteEntry) => !x.upperBounded) = true

Number-neutral items lack upper-boundedness. (Footnote 18 of [AOR24], p. 32, crediting Louise McNally (p.c.): the lack of an upper bound for yalnhej DPs may be tied to their being semantically number neutral.)

Worked examples

Finite-model witnesses instantiating the denotations above: non-maximality and the upper-bound contrast (book scenario, §3.2.4) and the harmonic vs non-harmonic anchoring distinction (card scenario, §4.3).

Book scenario

inductive AlonsoOvalleRoyer2024.Book : Type

Three books for testing the modal indefinite semantics.

• a : Book
• b : Book
• c : Book

@[instance_reducible]

instance AlonsoOvalleRoyer2024.instDecidableEqBook : DecidableEq Book

Equations

• AlonsoOvalleRoyer2024.instDecidableEqBook x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AlonsoOvalleRoyer2024.instReprBook.repr : Book → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AlonsoOvalleRoyer2024.instReprBook : Repr Book

Equations

• AlonsoOvalleRoyer2024.instReprBook = { reprPrec := AlonsoOvalleRoyer2024.instReprBook.repr }

inductive AlonsoOvalleRoyer2024.SpeechOrDescribed : Type

A speech event and a described event.

• speech : SpeechOrDescribed
• described : SpeechOrDescribed

@[instance_reducible]

instance AlonsoOvalleRoyer2024.instDecidableEqSpeechOrDescribed : DecidableEq SpeechOrDescribed

Equations

• AlonsoOvalleRoyer2024.instDecidableEqSpeechOrDescribed x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AlonsoOvalleRoyer2024.instReprSpeechOrDescribed.repr : SpeechOrDescribed → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AlonsoOvalleRoyer2024.instReprSpeechOrDescribed : Repr SpeechOrDescribed

Equations

• AlonsoOvalleRoyer2024.instReprSpeechOrDescribed = { reprPrec := AlonsoOvalleRoyer2024.instReprSpeechOrDescribed.repr }

theorem AlonsoOvalleRoyer2024.yalnhej_three_way_contrast : modalIndefiniteSat AlonsoOvalleRoyer2024.fEPI✝ SpeechOrDescribed.speech AlonsoOvalleRoyer2024.allBooks✝ AlonsoOvalleRoyer2024.isBook✝ (fun (x1 : Book) (x2 : AlonsoOvalleRoyer2024.BookWorld✝) => x1 ∈ x2) {Book.a, Book.b, Book.c} ∧ modalIndefiniteSat AlonsoOvalleRoyer2024.fEPI✝ SpeechOrDescribed.speech AlonsoOvalleRoyer2024.allBooks✝ AlonsoOvalleRoyer2024.isBook✝ (fun (x1 : Book) (x2 : AlonsoOvalleRoyer2024.BookWorld✝) => x1 ∈ x2) {Book.a, Book.b} ∧ ¬upperBoundedSat AlonsoOvalleRoyer2024.fEPI✝ SpeechOrDescribed.speech AlonsoOvalleRoyer2024.allBooks✝ AlonsoOvalleRoyer2024.isBook✝ (fun (x1 : Book) (x2 : AlonsoOvalleRoyer2024.BookWorld✝) => x1 ∈ x2) {Book.a, Book.b, Book.c}

Yalnhej on the book model: it holds both when every book is available (abc) and when not all are (ab) — non-maximal and not upper-bounded — while the upper-bounded denotation fails in abc. A maximal item would fail in ab; an upper-bounded item (algún) fails in abc.

Card scenario

Under an external modal the MI's anchor can be co-indexed with the modal's event ("any X is fine" — harmonic) or bound to the described event ("a random X" — non-harmonic). Three cards, worlds varying in which cards are grabbable, and two anchoring events.

inductive AlonsoOvalleRoyer2024.Card : Type

Three cards for testing harmonic readings.

• c1 : Card
• c2 : Card
• c3 : Card

@[instance_reducible]

instance AlonsoOvalleRoyer2024.instDecidableEqCard : DecidableEq Card

Equations

• AlonsoOvalleRoyer2024.instDecidableEqCard x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance AlonsoOvalleRoyer2024.instReprCard : Repr Card

Equations

• AlonsoOvalleRoyer2024.instReprCard = { reprPrec := AlonsoOvalleRoyer2024.instReprCard.repr }

def AlonsoOvalleRoyer2024.instReprCard.repr : Card → ℕ → Std.Format

Equations

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

inductive AlonsoOvalleRoyer2024.GrabEvent : Type

The described (local) event and the imperative event.

• local : GrabEvent
• imperative : GrabEvent

@[instance_reducible]

instance AlonsoOvalleRoyer2024.instDecidableEqGrabEvent : DecidableEq GrabEvent

Equations

• AlonsoOvalleRoyer2024.instDecidableEqGrabEvent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AlonsoOvalleRoyer2024.instReprGrabEvent.repr : GrabEvent → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance AlonsoOvalleRoyer2024.instReprGrabEvent : Repr GrabEvent

Equations

• AlonsoOvalleRoyer2024.instReprGrabEvent = { reprPrec := AlonsoOvalleRoyer2024.instReprGrabEvent.repr }

theorem AlonsoOvalleRoyer2024.harmonic_nonharmonic_contrast : ¬modalIndefiniteSat AlonsoOvalleRoyer2024.fGrab✝ GrabEvent.local AlonsoOvalleRoyer2024.allCards✝ AlonsoOvalleRoyer2024.isCard✝ (fun (x1 : Card) (x2 : AlonsoOvalleRoyer2024.CardWorld✝) => x1 ∈ x2) {Card.c1} ∧ modalIndefiniteSat AlonsoOvalleRoyer2024.fGrab✝ GrabEvent.imperative AlonsoOvalleRoyer2024.allCards✝ AlonsoOvalleRoyer2024.isCard✝ (fun (x1 : Card) (x2 : AlonsoOvalleRoyer2024.CardWorld✝) => x1 ∈ x2) {Card.c1}

The two readings are formally distinct on the card model: anchored to the local event, only c1 is grabbable and the modal component fails; co-indexed with the imperative event, every card is grabbable in some accessible world — "any card is fine". Same world, domain, and predicates; only the anchoring event differs.