Modal Indefinites: Cross-Linguistic Typology & Event-Relative Anchoring

@cite{alonso-ovalle-royer-2024} @cite{alonso-ovalle-menendez-benito-2010} @cite{alonso-ovalle-menendez-benito-2018} @cite{coon-2019} @cite{hacquard-2006} @cite{alonso-ovalle-royer-2021} @cite{chierchia-2013} @cite{jayez-tovena-2006} @cite{kratzer-shimoyama-2002}

Cross-linguistic typology of modal indefinites and bridge theorems connecting the event-relative modality theory (@cite{hacquard-2006}, formalized in Theories/Semantics/Modality/EventRelativity) to empirical observations.

Lexical entries are defined in Fragment files (single source of truth):

• Fragments/Chuj/ModalIndefinites.lean: yalnhej, komon
• Fragments/Spanish/ModalIndefinites.lean: algún, uno cualquiera
• Fragments/German/ModalIndefinites.lean: irgendein
• Fragments/French/ModalIndefinites.lean: n'importe quel
• Fragments/Italian/ModalIndefinites.lean: un qualsiasi

Architecture

The key contribution of @cite{alonso-ovalle-royer-2024} is DERIVING the position-sensitive flavor distribution of Chuj yalnhej from structural properties of event binding, rather than stipulating it lexically:

ChujArgPosition → accessibleBinders → miAnchorFlavor → predictedMIFlavors

1. Syntactic position determines which EventBinders are accessible
2. Each binder projects a specific MI flavor via AnchorType.toFlavor
3. RC (random choice) additionally requires verb volitionality

Three Dimensions of Variation (§6)

1. Status: at-issue vs not-at-issue
2. Content: which modal flavors
3. Upper-boundedness: anti-singleton inference

Anchor Constraint (§4)

At-issue modal indefinites are further distinguished by their AnchorConstraint: whether the anchoring function f has no definedness condition (unrestricted — defined for any event) or presupposes normative content (volitional-only). The anchor constraint controls where f CAN anchor; content licensing independently determines the resulting flavor.

Anchor Freedom (§4.1, footnote 17)

A-O&R depart from @cite{hacquard-2006} in one key respect: the event argument of yalnhej's anchoring function can be "left free" — bound by the existential closure of the speech act event rather than by the closest event binder. In Hacquard's system, modals are always bound by the closest c-commanding event binder; yalnhej allows non-local binding, which is how external arguments (above AspP) still access the speech event despite intervening projections.

def AlonsoOvalleRoyer2024.allEntries : List Features.ModalIndefinite.ModalIndefiniteEntry

Equations

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

theorem AlonsoOvalleRoyer2024.allEntries_count : allEntries.length = 7

theorem AlonsoOvalleRoyer2024.yalnhej_irgendein_same_flavors : Fragments.Chuj.ModalIndefinites.yalnhejEntry.flavors = Fragments.German.ModalIndefinites.irgendeinEntry.flavors

Chuj yalnhej and German irgendein share the same flavor inventory (epistemic + random choice) but differ in status.

theorem AlonsoOvalleRoyer2024.yalnhej_irgendein_differ_in_status : Fragments.Chuj.ModalIndefinites.yalnhejEntry.status ≠ Fragments.German.ModalIndefinites.irgendeinEntry.status

theorem AlonsoOvalleRoyer2024.at_issue_items : ([Fragments.Chuj.ModalIndefinites.yalnhejEntry, Fragments.Spanish.ModalIndefinites.unoCualquieraEntry, Fragments.French.ModalIndefinites.nimporteQuelEntry, Fragments.Italian.ModalIndefinites.unQualsiasiEntry].all fun (x : Features.ModalIndefinite.ModalIndefiniteEntry) => x.status == Features.ModalIndefinite.ModalComponentStatus.atIssue) = true

The at-issue / not-at-issue split (§6.1).

theorem AlonsoOvalleRoyer2024.not_at_issue_items : ([Fragments.Spanish.ModalIndefinites.algúnEntry, Fragments.German.ModalIndefinites.irgendeinEntry].all fun (x : Features.ModalIndefinite.ModalIndefiniteEntry) => x.status == Features.ModalIndefinite.ModalComponentStatus.notAtIssue) = true

theorem AlonsoOvalleRoyer2024.upper_bounded_items : (List.filter (fun (x : Features.ModalIndefinite.ModalIndefiniteEntry) => x.upperBounded) allEntries).length = 2

Upper-bounded items are a proper subset: only algún and uno cualquiera impose anti-singleton inferences.

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

Yalnhej is the only item that is both at-issue AND has both epistemic and random choice flavors. This is the core empirical contribution of @cite{alonso-ovalle-royer-2024}.

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

The three dimensions are logically independent: we find items in multiple cells of the 2×2 (status × upper-bounded) matrix.

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

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

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

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

Consistency check: at-issue status aligns with anchor constraint across all entries. At-issue items use event-relative anchoring (anchorConstraint = some _); not-at-issue items use different mechanisms (conversational implicature for algún, domain widening for irgendein) and have anchorConstraint = none. This is true by construction of the entries — verifying we encoded the paper's §4 classification correctly.

theorem AlonsoOvalleRoyer2024.volitional_blocks_epistemic : Fragments.Spanish.ModalIndefinites.unoCualquieraEntry.anchorConstraint = some Features.ModalIndefinite.AnchorConstraint.volitionalOnly ∧ ¬Fragments.Spanish.ModalIndefinites.unoCualquieraEntry.hasFlavor Core.Modality.ModalFlavor.epistemic

Volitional-only anchor constraint correlates with lacking epistemic: uno cualquiera's f requires normative content, blocking speech event anchoring (speech acts lack normative content).

theorem AlonsoOvalleRoyer2024.unrestricted_with_epistemic : Fragments.Chuj.ModalIndefinites.yalnhejEntry.anchorConstraint = some Features.ModalIndefinite.AnchorConstraint.unrestricted ∧ Fragments.Chuj.ModalIndefinites.yalnhejEntry.hasFlavor Core.Modality.ModalFlavor.epistemic

Unrestricted anchor constraint is necessary but not sufficient for epistemic: yalnhej gets epistemic because f is defined for the speech event, but n'importe quel and un qualsiasi are unrestricted yet only have circumstantial (their lexical semantics restricts to indiscriminacy/FC readings).

theorem AlonsoOvalleRoyer2024.unrestricted_without_epistemic : Fragments.French.ModalIndefinites.nimporteQuelEntry.anchorConstraint = some Features.ModalIndefinite.AnchorConstraint.unrestricted ∧ ¬Fragments.French.ModalIndefinites.nimporteQuelEntry.hasFlavor Core.Modality.ModalFlavor.epistemic

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.

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instDecidableEqChujArgPosition : DecidableEq ChujArgPosition

Equations

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

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instReprChujArgPosition : Repr ChujArgPosition

Equations

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

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

Equations

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

def AlonsoOvalleRoyer2024.accessibleBinders : ChujArgPosition → List Semantics.Modality.EventRelativity.EventBinder

Map structural position to accessible event binders.

External args are above vP: the closest event binder is the speech act (or attitude) event. The VP event is inaccessible because the external argument is merged above the aspectual projection that binds the VP event variable.

Internal args and adjuncts are within/adjoined to vP: both the speech act event and the VP event are structurally accessible.

Equations

• One or more equations did not get rendered due to their size.
• AlonsoOvalleRoyer2024.accessibleBinders AlonsoOvalleRoyer2024.ChujArgPosition.external = [Semantics.Modality.EventRelativity.EventBinder.speechAct]

def AlonsoOvalleRoyer2024.miAnchorFlavor (b : Semantics.Modality.EventRelativity.EventBinder) : Core.Modality.ModalFlavor

The MI flavor projected by a given event binder. Speech act events project epistemic; VP events project circumstantial. DERIVED from EventBinder.toAnchorType + AnchorType.toFlavor (defined in EventRelativity.lean), not stipulated.

Equations

• AlonsoOvalleRoyer2024.miAnchorFlavor b = b.toAnchorType.toFlavor

theorem AlonsoOvalleRoyer2024.speechAct_projects_epistemic : miAnchorFlavor Semantics.Modality.EventRelativity.EventBinder.speechAct = Core.Modality.ModalFlavor.epistemic

theorem AlonsoOvalleRoyer2024.vpEvent_projects_circumstantial : miAnchorFlavor Semantics.Modality.EventRelativity.EventBinder.vpEvent = Core.Modality.ModalFlavor.circumstantial

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

Base MI flavors = one flavor per accessible binder, derived from the EventBinder infrastructure in EventRelativity. External: [epistemic]. Internal/adjunct: [epistemic, circumstantial].

Equations

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

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

Whether the random choice (RC) reading is available. RC requires TWO conditions: (a) VP event is structurally accessible (internal or adjunct position) (b) verb is volitional (decision subevent provides the anchoring point)

This captures @cite{alonso-ovalle-royer-2024}'s core structural explanation: the RC flavor comes from the VP event, but only volitional events contain a decision subevent that can serve as the anchor.

Equations

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

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

Predicted MI flavors for a given position and volitionality. When RC is not available, the circumstantial flavor (projected from the VP event) is blocked, leaving only epistemic.

Equations

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

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

Table 5 DERIVED from structural position + volitionality + EventBinder. The full five-cell pattern of @cite{alonso-ovalle-royer-2024} falls out from three orthogonal components: (1) accessibleBinders (structural position) (2) miAnchorFlavor (EventBinder → ModalFlavor, from EventRelativity) (3) rcAvailable (volitionality constraint)

theorem AlonsoOvalleRoyer2024.external_volitionality_irrelevant : predictedMIFlavors ChujArgPosition.external true = predictedMIFlavors ChujArgPosition.external false

External args: volitionality is irrelevant (no VP event access).

theorem AlonsoOvalleRoyer2024.position_matters : predictedMIFlavors ChujArgPosition.external true ≠ predictedMIFlavors ChujArgPosition.internal true

Position matters: external ≠ internal flavor sets (with volitional verb).

theorem AlonsoOvalleRoyer2024.volitionality_matters : predictedMIFlavors ChujArgPosition.internal true ≠ predictedMIFlavors ChujArgPosition.internal false

Volitionality matters: internal volitional ≠ internal non-volitional.

theorem AlonsoOvalleRoyer2024.internal_adjunct_same (v : Bool) : predictedMIFlavors ChujArgPosition.internal v = predictedMIFlavors ChujArgPosition.adjunct v

Internal and adjunct pattern alike (same accessible binders).

The full derivation chain connecting Chuj clause structure to MI flavor predictions:

VoiceHead.hasD → argPosition → accessibleBinders → predictedMIFlavors

hasD is the structural claim: Voice heads with [D] introduce a specifier in Spec,VoiceP (above vP, hence above AspP). This DP's event variable is bound by the speech act event (e₀), not by Asp's ∃e₂. Voice heads without [D] have no specifier — the highest DP is the internal argument (below AspP), accessible to both e₀ and e₂.

def AlonsoOvalleRoyer2024.argPositionOf (vh : Minimalist.VoiceHead) : ChujArgPosition

Derive argument position from Voice head: [+D] → external (above AspP), [-D] → internal (below AspP). This is the structural claim that replaces the stipulated position mapping.

Equations

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

def AlonsoOvalleRoyer2024.predictedMIFlavorsOf (vh : Minimalist.VoiceHead) (volitional : Bool) : List Core.Modality.ModalFlavor

End-to-end: Voice head determines MI flavor availability. Given a Voice head and verb volitionality, predict the MI flavors by composing the full derivation chain.

Equations

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

theorem AlonsoOvalleRoyer2024.voice_to_position : argPositionOf Coon2019.vØ = ChujArgPosition.external ∧ argPositionOf Coon2019.v_w = ChujArgPosition.external ∧ argPositionOf Coon2019.v_ch = ChujArgPosition.internal ∧ argPositionOf Coon2019.v_j = ChujArgPosition.internal

The four Chuj voice heads yield the correct argument positions.

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

End-to-end flavor predictions for each Chuj voice head. Active/antipassive (external arg): epistemic only. Passive/agentless (internal arg, volitional): epistemic + RC.

theorem AlonsoOvalleRoyer2024.voice_nonvolitional : predictedMIFlavorsOf Coon2019.v_ch false = [Core.Modality.ModalFlavor.epistemic] ∧ predictedMIFlavorsOf Coon2019.v_j false = [Core.Modality.ModalFlavor.epistemic]

Non-volitional verbs block RC even in passive: only epistemic.

theorem AlonsoOvalleRoyer2024.argPosition_parallels_modalPosition : Semantics.Modality.EventRelativity.ModalPosition.aboveAsp.defaultBinder = Semantics.Modality.EventRelativity.EventBinder.speechAct ∧ Semantics.Modality.EventRelativity.ModalPosition.belowAsp.defaultBinder = Semantics.Modality.EventRelativity.EventBinder.vpEvent ∧ accessibleBinders ChujArgPosition.external = [Semantics.Modality.EventRelativity.EventBinder.speechAct] ∧ accessibleBinders ChujArgPosition.internal = [Semantics.Modality.EventRelativity.EventBinder.speechAct, Semantics.Modality.EventRelativity.EventBinder.vpEvent]

Connection to EventRelativity's ModalPosition: the MI's position relative to AspP determines which binders are accessible, paralleling how ModalPosition determines which event binder a modal auxiliary is bound to. External = aboveAsp (speech act only), internal = belowAsp (VP event accessible).

theorem AlonsoOvalleRoyer2024.yalnhej_nonmaximal : Fragments.Chuj.ModalIndefinites.yalnhejEntry.upperBounded = false

Yalnhej is not upper-bounded: compatible with partial-domain scenarios where not all P are Q. This distinguishes it from maximal free relatives (whatever), which require all domain members to satisfy the scope. The EventRelativity worked example demonstrates this concretely with yalnhej_nonmaximal_ab (ModalIndefinites.lean).

theorem AlonsoOvalleRoyer2024.multi_flavor_items : (List.filter (fun (e : Features.ModalIndefinite.ModalIndefiniteEntry) => decide (e.hasFlavor Core.Modality.ModalFlavor.epistemic) && decide (e.hasFlavor Core.Modality.ModalFlavor.circumstantial)) allEntries).length = 2

Multi-flavor items: can express BOTH epistemic and RC. @cite{alonso-ovalle-royer-2024}, §6.2: yalnhej and irgendein tolerate more than one modal flavour.

theorem AlonsoOvalleRoyer2024.epistemic_only_items : (List.filter (fun (e : Features.ModalIndefinite.ModalIndefiniteEntry) => decide (e.hasFlavor Core.Modality.ModalFlavor.epistemic) && !decide (e.hasFlavor Core.Modality.ModalFlavor.circumstantial)) allEntries).length = 1

Epistemic-only items: algún conveys only speaker ignorance (§6.2, example 118).

theorem AlonsoOvalleRoyer2024.rc_only_items : (List.filter (fun (e : Features.ModalIndefinite.ModalIndefiniteEntry) => !decide (e.hasFlavor Core.Modality.ModalFlavor.epistemic) && decide (e.hasFlavor Core.Modality.ModalFlavor.circumstantial)) allEntries).length = 4

RC-only items: uno cualquiera, n'importe quel, un qualsiasi, komon convey only random choice / indiscriminacy (§6.2, examples 119–121).

theorem AlonsoOvalleRoyer2024.upper_bounded_group : ([Fragments.Spanish.ModalIndefinites.algúnEntry, Fragments.Spanish.ModalIndefinites.unoCualquieraEntry].all fun (x : Features.ModalIndefinite.ModalIndefiniteEntry) => x.upperBounded) = true

Upper-bounded modal indefinites impose an anti-singleton inference.

theorem AlonsoOvalleRoyer2024.not_upper_bounded_group : ([Fragments.Chuj.ModalIndefinites.yalnhejEntry, Fragments.German.ModalIndefinites.irgendeinEntry, Fragments.French.ModalIndefinites.nimporteQuelEntry, Fragments.Italian.ModalIndefinites.unQualsiasiEntry].all fun (x : Features.ModalIndefinite.ModalIndefiniteEntry) => x.upperBounded == false) = true

Non-upper-bounded modal indefinites: no anti-singleton.

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

Predicativity correlates with unremarkable readings across all entries. Items that can appear in predicative position also have non-modal ("unremarkable") readings. Derived directly from fragment entry fields — no intermediate data structures needed.

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 @cite{alonso-ovalle-royer-2024}, p.32, attributed to Louise McNally: wh-phrase origin → number neutrality → incompatible with anti-singleton inference, since anti-singleton presupposes a singleton alternative.)

theorem AlonsoOvalleRoyer2024.yalnhej_no_unremarkable : Fragments.Chuj.ModalIndefinites.yalnhejEntry.hasUnremarkableReading = false ∧ Fragments.Chuj.ModalIndefinites.yalnhejEntry.canBePredicate = false

Yalnhej lacks both predicative use and unremarkable readings.

theorem AlonsoOvalleRoyer2024.komon_has_unremarkable : Fragments.Chuj.ModalIndefinites.komonEntry.hasUnremarkableReading = true ∧ Fragments.Chuj.ModalIndefinites.komonEntry.canBePredicate = true

Komon has both (mass/plural modifier, can be predicative).

Under an external modal (imperative, deontic, attitude verb), the MI's anchor can be co-indexed with the modal's event binder, giving "any X is fine" readings (harmonic). When the anchor is independent (bound to the described event), the result is "a random X" (non-harmonic).

Same surface form, two readings:

• Non-harmonic: "Grab yalnhej card!" = grab a random card (MI anchored to described event → circumstantial/RC)
• Harmonic: "Grab yalnhej card!" = any card is fine (MI co-indexed with imperative event → permission domain)

The distinction maps directly to EventBinder:

• Non-harmonic anchor = vpEvent (aspect-bound)
• Harmonic anchor = speechAct or attitude (co-indexed with embedding modal)

theorem AlonsoOvalleRoyer2024.nonharmonic_is_vpEvent : Semantics.Modality.EventRelativity.EventBinder.vpEvent.canProjectEpistemic = false ∧ Semantics.Modality.EventRelativity.EventBinder.vpEvent.canProjectCircumstantial = true

Non-harmonic anchoring: MI bound to VP event → circumstantial only. VP events lack propositional content (content licensing).

theorem AlonsoOvalleRoyer2024.harmonic_is_speechAct : Semantics.Modality.EventRelativity.EventBinder.speechAct.canProjectEpistemic = true ∧ Semantics.Modality.EventRelativity.EventBinder.speechAct.canProjectCircumstantial = true

Harmonic anchoring: MI co-indexed with speech act → both flavors. Speech acts are contentful (epistemic available).

theorem AlonsoOvalleRoyer2024.harmonic_neq_nonharmonic : Semantics.Modality.EventRelativity.EventBinder.vpEvent.availableFlavors ≠ Semantics.Modality.EventRelativity.EventBinder.speechAct.availableFlavors

The two readings are formally distinct: non-harmonic and harmonic anchoring yield different available flavor profiles from the same MI, explaining the ambiguity of yalnhej under imperatives.

Concrete model-theoretic witnesses for the typological claims of Part I. These instantiate Theories/Semantics/Modality/ModalIndefinites.lean on small finite domains to demonstrate (a) non-maximality, (b) the upper-bounded vs. non-upper-bounded contrast, and (c) the harmonic vs. non-harmonic anchoring distinction. The toy domains live here in the study file (per CLAUDE.md: examples that name a paper's analyses belong with the paper, not in the abstract theory file).

inductive AlonsoOvalleRoyer2024.Book : Type

Three books for testing the modal indefinite semantics.

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

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instDecidableEqBook : DecidableEq Book

Equations

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

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instReprBook : Repr Book

Equations

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

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

Equations

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

def AlonsoOvalleRoyer2024.instInhabitedBook.default : Book

Equations

• AlonsoOvalleRoyer2024.instInhabitedBook.default = AlonsoOvalleRoyer2024.Book.a

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instInhabitedBook : Inhabited Book

Equations

• AlonsoOvalleRoyer2024.instInhabitedBook = { default := AlonsoOvalleRoyer2024.instInhabitedBook.default }

inductive AlonsoOvalleRoyer2024.BookWorld : Type

Three possible worlds varying in which books are available.

• abc : BookWorld
• ab : BookWorld
• ac : BookWorld

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instDecidableEqBookWorld : DecidableEq BookWorld

Equations

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

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instReprBookWorld : Repr BookWorld

Equations

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

def AlonsoOvalleRoyer2024.instReprBookWorld.repr : BookWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instInhabitedBookWorld : Inhabited BookWorld

Equations

• AlonsoOvalleRoyer2024.instInhabitedBookWorld = { default := AlonsoOvalleRoyer2024.instInhabitedBookWorld.default }

def AlonsoOvalleRoyer2024.instInhabitedBookWorld.default : BookWorld

Equations

• AlonsoOvalleRoyer2024.instInhabitedBookWorld.default = AlonsoOvalleRoyer2024.BookWorld.abc

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instFintypeBookWorld : Fintype BookWorld

Equations

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

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instDecidablePredBookWorldIsBook (book : Book) : DecidablePred (AlonsoOvalleRoyer2024.isBook✝ book)

Equations

• AlonsoOvalleRoyer2024.instDecidablePredBookWorldIsBook book x✝ = instDecidableTrue

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instDecidablePredBookWorldIsAvailable (book : Book) : DecidablePred (AlonsoOvalleRoyer2024.isAvailable✝ book)

Equations

• AlonsoOvalleRoyer2024.instDecidablePredBookWorldIsAvailable AlonsoOvalleRoyer2024.Book.a x✝ = instDecidableTrue
• AlonsoOvalleRoyer2024.instDecidablePredBookWorldIsAvailable AlonsoOvalleRoyer2024.Book.b AlonsoOvalleRoyer2024.BookWorld.abc = instDecidableTrue
• AlonsoOvalleRoyer2024.instDecidablePredBookWorldIsAvailable AlonsoOvalleRoyer2024.Book.b AlonsoOvalleRoyer2024.BookWorld.ab = instDecidableTrue
• AlonsoOvalleRoyer2024.instDecidablePredBookWorldIsAvailable AlonsoOvalleRoyer2024.Book.b AlonsoOvalleRoyer2024.BookWorld.ac = instDecidableFalse
• AlonsoOvalleRoyer2024.instDecidablePredBookWorldIsAvailable AlonsoOvalleRoyer2024.Book.c AlonsoOvalleRoyer2024.BookWorld.abc = instDecidableTrue
• AlonsoOvalleRoyer2024.instDecidablePredBookWorldIsAvailable AlonsoOvalleRoyer2024.Book.c AlonsoOvalleRoyer2024.BookWorld.ab = instDecidableFalse
• AlonsoOvalleRoyer2024.instDecidablePredBookWorldIsAvailable AlonsoOvalleRoyer2024.Book.c AlonsoOvalleRoyer2024.BookWorld.ac = instDecidableTrue

inductive AlonsoOvalleRoyer2024.SpeechOrDescribed : Type

A speech event and a described event.

• speech : SpeechOrDescribed
• described : SpeechOrDescribed

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instDecidableEqSpeechOrDescribed : DecidableEq SpeechOrDescribed

Equations

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

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instReprSpeechOrDescribed : Repr SpeechOrDescribed

Equations

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

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

Equations

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

theorem AlonsoOvalleRoyer2024.yalnhej_book_abc : Semantics.Modality.ModalIndefinites.modalIndefiniteSat AlonsoOvalleRoyer2024.fEPI✝ SpeechOrDescribed.speech AlonsoOvalleRoyer2024.allBW✝ AlonsoOvalleRoyer2024.allBooks✝ AlonsoOvalleRoyer2024.isBook✝ AlonsoOvalleRoyer2024.isAvailable✝ BookWorld.abc

"Yalnhej bought a book" in world abc: ∃x[book(x) ∧ avail(x)] ∧ ∀y[book(y) → ◇_{EPI}(avail(y))] Every book is available in some accessible world.

theorem AlonsoOvalleRoyer2024.yalnhej_not_upper_bounded_abc : Semantics.Modality.ModalIndefinites.modalIndefiniteSat AlonsoOvalleRoyer2024.fEPI✝ SpeechOrDescribed.speech AlonsoOvalleRoyer2024.allBW✝ AlonsoOvalleRoyer2024.allBooks✝ AlonsoOvalleRoyer2024.isBook✝ AlonsoOvalleRoyer2024.isAvailable✝ BookWorld.abc ∧ ¬Semantics.Modality.ModalIndefinites.upperBoundedSat AlonsoOvalleRoyer2024.fEPI✝ SpeechOrDescribed.speech AlonsoOvalleRoyer2024.allBW✝ AlonsoOvalleRoyer2024.allBooks✝ AlonsoOvalleRoyer2024.isBook✝ AlonsoOvalleRoyer2024.isAvailable✝ BookWorld.abc

Not upper-bounded: in world abc, all three books ARE available, yet the MI denotation holds. The anti-singleton condition fails (all books satisfy the scope), showing yalnhej is non-UB.

Yalnhej is compatible with partial-domain scenarios: the speaker can felicitously use yalnhej even when not all P are Q. This distinguishes it from maximal free relatives (whatever), which require every domain member to satisfy the scope. Unlike upper-boundedness (which blocks ∀P→Q), non-maximality is about COMPATIBILITY with ¬∀P→Q — a weaker property.

We demonstrate non-maximality using the 3-book model: in world ab (books a,b available but NOT c), the MI denotation still holds because every book is available in SOME accessible world, even though not every book is available in the actual world.

theorem AlonsoOvalleRoyer2024.yalnhej_nonmaximal_ab : Semantics.Modality.ModalIndefinites.modalIndefiniteSat AlonsoOvalleRoyer2024.fEPI✝ SpeechOrDescribed.speech AlonsoOvalleRoyer2024.allBW✝ AlonsoOvalleRoyer2024.allBooks✝ AlonsoOvalleRoyer2024.isBook✝ AlonsoOvalleRoyer2024.isAvailable✝ BookWorld.ab

MI holds in world ab where book c is NOT available. The existential component (∃x P∧Q) holds (book a is available). The modal component (∀y P→◇Q) holds (each book is available in some accessible world). Crucially, ¬∀y P→Q(y)(ab): book c is not available in ab. This shows yalnhej is compatible with not-all-P-being-Q — non-maximality.

theorem AlonsoOvalleRoyer2024.yalnhej_three_way_contrast : Semantics.Modality.ModalIndefinites.modalIndefiniteSat AlonsoOvalleRoyer2024.fEPI✝ SpeechOrDescribed.speech AlonsoOvalleRoyer2024.allBW✝ AlonsoOvalleRoyer2024.allBooks✝ AlonsoOvalleRoyer2024.isBook✝ AlonsoOvalleRoyer2024.isAvailable✝ BookWorld.abc ∧ Semantics.Modality.ModalIndefinites.modalIndefiniteSat AlonsoOvalleRoyer2024.fEPI✝ SpeechOrDescribed.speech AlonsoOvalleRoyer2024.allBW✝ AlonsoOvalleRoyer2024.allBooks✝ AlonsoOvalleRoyer2024.isBook✝ AlonsoOvalleRoyer2024.isAvailable✝ BookWorld.ab ∧ ¬Semantics.Modality.ModalIndefinites.upperBoundedSat AlonsoOvalleRoyer2024.fEPI✝ SpeechOrDescribed.speech AlonsoOvalleRoyer2024.allBW✝ AlonsoOvalleRoyer2024.allBooks✝ AlonsoOvalleRoyer2024.isBook✝ AlonsoOvalleRoyer2024.isAvailable✝ BookWorld.abc

Three-way contrast: maximality vs yalnhej vs algún. In world abc (all books available): MI holds + UB fails. In world ab (not all available): MI holds + UB holds. A maximal item (whatever) would require all books available (fail in ab). Algún (UB) would require not-all (fail in abc). Yalnhej (non-UB) succeeds in BOTH.

When a modal indefinite occurs under an external modal (imperative, deontic, attitude verb), the MI's anchoring event can be CO-INDEXED with the external modal's event. This "harmonic" configuration gives "any X is fine" readings — the MI's modal domain aligns with the embedding modal's domain.

Non-harmonic: the MI's anchor is independent of the external modal. "Grab yalnhej card" = grab a random card (MI anchors to described event). Harmonic: the MI's anchor is co-indexed with the imperative/deontic event. "Grab yalnhej card" = any card is fine (MI anchors to imperative event).

We model this with a card-grabbing scenario: three cards, worlds varying in which cards are grabbable, and two event types (local vs imperative).

inductive AlonsoOvalleRoyer2024.Card : Type

Three cards for testing harmonic readings.

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

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instDecidableEqCard : DecidableEq Card

Equations

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

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

Equations

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

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instReprCard : Repr Card

Equations

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

def AlonsoOvalleRoyer2024.instInhabitedCard.default : Card

Equations

• AlonsoOvalleRoyer2024.instInhabitedCard.default = AlonsoOvalleRoyer2024.Card.c1

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instInhabitedCard : Inhabited Card

Equations

• AlonsoOvalleRoyer2024.instInhabitedCard = { default := AlonsoOvalleRoyer2024.instInhabitedCard.default }

inductive AlonsoOvalleRoyer2024.CardWorld : Type

Three worlds varying in which cards are grabbable.

• all : CardWorld
• only1 : CardWorld
• only2 : CardWorld

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instDecidableEqCardWorld : DecidableEq CardWorld

Equations

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

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instReprCardWorld : Repr CardWorld

Equations

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

def AlonsoOvalleRoyer2024.instReprCardWorld.repr : CardWorld → ℕ → Std.Format

Equations

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

def AlonsoOvalleRoyer2024.instInhabitedCardWorld.default : CardWorld

Equations

• AlonsoOvalleRoyer2024.instInhabitedCardWorld.default = AlonsoOvalleRoyer2024.CardWorld.all

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instInhabitedCardWorld : Inhabited CardWorld

Equations

• AlonsoOvalleRoyer2024.instInhabitedCardWorld = { default := AlonsoOvalleRoyer2024.instInhabitedCardWorld.default }

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instDecidablePredCardWorldIsCard (c : Card) : DecidablePred (AlonsoOvalleRoyer2024.isCard✝ c)

Equations

• AlonsoOvalleRoyer2024.instDecidablePredCardWorldIsCard c x✝ = instDecidableTrue

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instDecidablePredCardWorldCanGrab (c : Card) : DecidablePred (AlonsoOvalleRoyer2024.canGrab✝ c)

Equations

• AlonsoOvalleRoyer2024.instDecidablePredCardWorldCanGrab AlonsoOvalleRoyer2024.Card.c1 AlonsoOvalleRoyer2024.CardWorld.all = instDecidableTrue
• AlonsoOvalleRoyer2024.instDecidablePredCardWorldCanGrab AlonsoOvalleRoyer2024.Card.c1 AlonsoOvalleRoyer2024.CardWorld.only1 = instDecidableTrue
• AlonsoOvalleRoyer2024.instDecidablePredCardWorldCanGrab AlonsoOvalleRoyer2024.Card.c1 AlonsoOvalleRoyer2024.CardWorld.only2 = instDecidableFalse
• AlonsoOvalleRoyer2024.instDecidablePredCardWorldCanGrab AlonsoOvalleRoyer2024.Card.c2 AlonsoOvalleRoyer2024.CardWorld.all = instDecidableTrue
• AlonsoOvalleRoyer2024.instDecidablePredCardWorldCanGrab AlonsoOvalleRoyer2024.Card.c2 AlonsoOvalleRoyer2024.CardWorld.only1 = instDecidableFalse
• AlonsoOvalleRoyer2024.instDecidablePredCardWorldCanGrab AlonsoOvalleRoyer2024.Card.c2 AlonsoOvalleRoyer2024.CardWorld.only2 = instDecidableTrue
• AlonsoOvalleRoyer2024.instDecidablePredCardWorldCanGrab AlonsoOvalleRoyer2024.Card.c3 AlonsoOvalleRoyer2024.CardWorld.all = instDecidableTrue
• AlonsoOvalleRoyer2024.instDecidablePredCardWorldCanGrab AlonsoOvalleRoyer2024.Card.c3 AlonsoOvalleRoyer2024.CardWorld.only1 = instDecidableFalse
• AlonsoOvalleRoyer2024.instDecidablePredCardWorldCanGrab AlonsoOvalleRoyer2024.Card.c3 AlonsoOvalleRoyer2024.CardWorld.only2 = instDecidableFalse

inductive AlonsoOvalleRoyer2024.GrabEvent : Type

Three event types: speech, local (described), imperative.

• speech : GrabEvent
• local : GrabEvent
• imperative : GrabEvent

@[implicit_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.

@[implicit_reducible]

instance AlonsoOvalleRoyer2024.instReprGrabEvent : Repr GrabEvent

Equations

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

theorem AlonsoOvalleRoyer2024.nonharmonic_fails : ¬Semantics.Modality.ModalIndefinites.modalIndefiniteSat AlonsoOvalleRoyer2024.fGrab✝ GrabEvent.local AlonsoOvalleRoyer2024.allCW✝ AlonsoOvalleRoyer2024.allCards✝ AlonsoOvalleRoyer2024.isCard✝ AlonsoOvalleRoyer2024.canGrab✝ CardWorld.only1

Non-harmonic MI fails: when the MI anchors to the local event, only world only1 is accessible. In only1, only c1 is grabbable. The modal component ∀y[card(y) → ◇_{local}(grab(y))] fails because c2 and c3 are not grabbable in any locally accessible world.

theorem AlonsoOvalleRoyer2024.harmonic_succeeds : Semantics.Modality.ModalIndefinites.modalIndefiniteSat AlonsoOvalleRoyer2024.fGrab✝ GrabEvent.imperative AlonsoOvalleRoyer2024.allCW✝ AlonsoOvalleRoyer2024.allCards✝ AlonsoOvalleRoyer2024.isCard✝ AlonsoOvalleRoyer2024.canGrab✝ CardWorld.only1

Harmonic MI succeeds: when the MI's anchor is co-indexed with the imperative event, all worlds are accessible. Every card is grabbable in some world (c1 in only1, c2 in only2, c3 in all). The modal component ∀y[card(y) → ◇_{imperative}(grab(y))] holds. This gives the "any card is fine" reading.

theorem AlonsoOvalleRoyer2024.harmonic_neq_nonharmonic_witness : ¬Semantics.Modality.ModalIndefinites.modalIndefiniteSat AlonsoOvalleRoyer2024.fGrab✝ GrabEvent.local AlonsoOvalleRoyer2024.allCW✝ AlonsoOvalleRoyer2024.allCards✝ AlonsoOvalleRoyer2024.isCard✝ AlonsoOvalleRoyer2024.canGrab✝ CardWorld.only1 ∧ Semantics.Modality.ModalIndefinites.modalIndefiniteSat AlonsoOvalleRoyer2024.fGrab✝ GrabEvent.imperative AlonsoOvalleRoyer2024.allCW✝ AlonsoOvalleRoyer2024.allCards✝ AlonsoOvalleRoyer2024.isCard✝ AlonsoOvalleRoyer2024.canGrab✝ CardWorld.only1

Harmonic ≠ non-harmonic: the two readings are formally distinct. Same world of evaluation (.only1), same domain, same predicates — only the anchoring event differs.