Modal Indefinites: Cross-Linguistic Typology & Kratzer 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

Three Dimensions of Variation (§6)

1. Status: Is the modal component at-issue or not-at-issue?
2. Content: Which modal flavors does the component support?
3. Upper-boundedness: Does the indefinite impose an anti-singleton inference (¬∀x[P(x) → Q(x)])?

Key Bridge Theorems

1. Position → Anchor: The syntactic position of the yalnhej DP determines which anchoring functions are semantically productive.
2. Anchor → Flavor: Speech event → epistemic; described event → RC.
3. Volitionality: RC requires a volitional verb (decision subevent).
4. Voice → Position: Chuj voice system determines external/internal.
5. Cross-linguistic predictions: Three-dimensional typology instantiated.

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.allEntries : List Core.ModalIndefinite.ModalIndefiniteEntry

Equations

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

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.allEntries_count : allEntries.length = 7

theorem Phenomena.ModalIndefinites.Studies.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 Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.yalnhej_irgendein_differ_in_status : Fragments.Chuj.ModalIndefinites.yalnhejEntry.status ≠ Fragments.German.ModalIndefinites.irgendeinEntry.status

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

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

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

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.upper_bounded_items : (List.filter (fun (x : Core.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 Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.yalnhej_unique_profile : (List.filter (fun (e : Core.ModalIndefinite.ModalIndefiniteEntry) => e.status == Core.ModalIndefinite.ModalComponentStatus.atIssue && e.hasEpistemic && e.hasCircumstantial) 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 Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.at_issue_and_ub_exists : (allEntries.any fun (e : Core.ModalIndefinite.ModalIndefiniteEntry) => e.status == Core.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 Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.at_issue_and_not_ub_exists : (allEntries.any fun (e : Core.ModalIndefinite.ModalIndefiniteEntry) => e.status == Core.ModalIndefinite.ModalComponentStatus.atIssue && !e.upperBounded) = true

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

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

inductive Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.ChujDPPosition : Type

Syntactic positions for a DP in Chuj, cross-classified with verb volitionality (§3–4, Table 5).

The paper shows that RC availability depends on TWO factors: (1) structural position (external vs internal/adjunct), and (2) whether the verb describes a volitional event (one containing a decision subevent that can anchor RC modality).

• externalArg : ChujDPPosition

  External argument (subject of transitive)

• internalArgVolitional : ChujDPPosition

  Internal argument of a volitional verb (e.g., "buy")

• internalArgNonVolitional : ChujDPPosition

  Internal argument of a non-volitional verb (e.g., "like")

• adjunctVolitional : ChujDPPosition

  Adjunct of a volitional verb (e.g., "Malin ate where")

• adjunctNonVolitional : ChujDPPosition

  Adjunct of a non-volitional verb (e.g., "it rained where")

instance Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instDecidableEqChujDPPosition : DecidableEq ChujDPPosition

Equations

• Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instDecidableEqChujDPPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instBEqChujDPPosition : BEq ChujDPPosition

Equations

• Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instBEqChujDPPosition = { beq := Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instBEqChujDPPosition.beq }

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instBEqChujDPPosition.beq : ChujDPPosition → ChujDPPosition → Bool

Equations

• Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instBEqChujDPPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprChujDPPosition : Repr ChujDPPosition

Equations

• Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprChujDPPosition = { reprPrec := Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprChujDPPosition.repr }

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprChujDPPosition.repr : ChujDPPosition → ℕ → Std.Format

Equations

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

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.yalnhejFlavorsAt : ChujDPPosition → List Core.Modality.ModalFlavor

Which modal flavors are available to yalnhej in each position (Table 5, §3.2–4.2).

Equations

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

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.ext_arg_epistemic_only : yalnhejFlavorsAt ChujDPPosition.externalArg = [Core.Modality.ModalFlavor.epistemic]

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.int_arg_vol_both_flavors : yalnhejFlavorsAt ChujDPPosition.internalArgVolitional = [Core.Modality.ModalFlavor.epistemic, Core.Modality.ModalFlavor.circumstantial]

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.int_arg_nonvol_epistemic_only : yalnhejFlavorsAt ChujDPPosition.internalArgNonVolitional = [Core.Modality.ModalFlavor.epistemic]

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.position_matters : yalnhejFlavorsAt ChujDPPosition.externalArg ≠ yalnhejFlavorsAt ChujDPPosition.internalArgVolitional

Position sensitivity: external ≠ volitional internal flavor sets.

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.volitionality_matters : yalnhejFlavorsAt ChujDPPosition.internalArgVolitional ≠ yalnhejFlavorsAt ChujDPPosition.internalArgNonVolitional

Volitionality sensitivity: volitional ≠ non-volitional internal flavor sets (§4.1).

structure Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.YalnhejExample : Type

A Chuj yalnhej example sentence with empirical judgments.

• chuj : String
• gloss : String
• position : ChujDPPosition
• availableFlavors : List Core.Modality.ModalFlavor
• exampleNumber : String

  Example number in @cite{alonso-ovalle-royer-2024}

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprYalnhejExample.repr : YalnhejExample → ℕ → Std.Format

Equations

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

instance Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprYalnhejExample : Repr YalnhejExample

Equations

• Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprYalnhejExample = { reprPrec := Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprYalnhejExample.repr }

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.ex22_extArg : YalnhejExample

Equations

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

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.ex31_intArgRC : YalnhejExample

Equations

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

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.ex34_intArgNonVol : YalnhejExample

Equations

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

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.ex41_adjunctRC : YalnhejExample

Equations

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

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.ex39_adjunctNonVol : YalnhejExample

Equations

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

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.allExamples : List YalnhejExample

Equations

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

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.examples_match_position_prediction : (allExamples.all fun (ex : YalnhejExample) => ex.availableFlavors == yalnhejFlavorsAt ex.position) = true

Consistency: each example's available flavors match the position-based prediction from yalnhejFlavorsAt.

Yalnhej is compatible with partial-domain scenarios, unlike maximal free relatives (English whatever).

structure Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.MaximalityDatum : Type

• context : String
• chuj : String
• gloss : String
• yalnhejFelicitous : Bool
• exampleNumber : String

  Example number in @cite{alonso-ovalle-royer-2024}

instance Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprMaximalityDatum : Repr MaximalityDatum

Equations

• Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprMaximalityDatum = { reprPrec := Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprMaximalityDatum.repr }

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprMaximalityDatum.repr : MaximalityDatum → ℕ → Std.Format

Equations

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

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.ex43_partialRC : MaximalityDatum

Equations

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

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.ex46_partialEpi : MaximalityDatum

Equations

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

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.all_partial_domain_felicitous : ([ex43_partialRC, ex46_partialEpi].all fun (x : MaximalityDatum) => x.yalnhejFelicitous) = true

Some modal indefinites have "unremarkable" (plain existential) readings in addition to their modal readings. @cite{alonso-ovalle-royer-2024} (§5) correlate this with predicativity.

structure Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.UnremarkableReadingDatum : Type

• language : String
• form : String
• hasUnremarkable : Bool
• predicative : Bool
• exampleNumber : String

  Example number(s) in @cite{alonso-ovalle-royer-2024}

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprUnremarkableReadingDatum.repr : UnremarkableReadingDatum → ℕ → Std.Format

Equations

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

instance Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprUnremarkableReadingDatum : Repr UnremarkableReadingDatum

Equations

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

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.unoCualquiera_unremarkable : UnremarkableReadingDatum

Equations

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

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.irgendein_unremarkable : UnremarkableReadingDatum

Equations

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

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.komon_unremarkable : UnremarkableReadingDatum

Equations

• Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.komon_unremarkable = { language := "Chuj (Mayan)", form := "komon", hasUnremarkable := true, predicative := true, exampleNumber := "§5" }

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.yalnhej_unremarkable : UnremarkableReadingDatum

Equations

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

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.allUnremarkableData : List UnremarkableReadingDatum

Equations

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

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.predicativity_unremarkable_correlation : (allUnremarkableData.all fun (d : UnremarkableReadingDatum) => d.predicative == d.hasUnremarkable) = true

Predicativity correlates with unremarkable readings across all data.

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.yalnhej_entry_unremarkable_agrees : Fragments.Chuj.ModalIndefinites.yalnhejEntry.hasUnremarkableReading = yalnhej_unremarkable.hasUnremarkable

Cross-check: fragment entry fields agree with independent empirical data.

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.komon_entry_unremarkable_agrees : Fragments.Chuj.ModalIndefinites.komonEntry.hasUnremarkableReading = komon_unremarkable.hasUnremarkable

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.unoCualquiera_entry_unremarkable_agrees : Fragments.Spanish.ModalIndefinites.unoCualquieraEntry.hasUnremarkableReading = unoCualquiera_unremarkable.hasUnremarkable

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.predicativity_correlates_unremarkable : (allEntries.all fun (e : Core.ModalIndefinite.ModalIndefiniteEntry) => e.canBePredicate == e.hasUnremarkableReading) = true

Predicativity correlates with unremarkable readings across all entries.

Under an external modal (imperative, deontic, attitude verb), the MI's anchor can be co-indexed with the modal's event, giving "any X is fine" readings.

inductive Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.EmbeddingModal : Type

• imperative : EmbeddingModal
• deontic : EmbeddingModal
• attitudeVerb : EmbeddingModal

instance Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instDecidableEqEmbeddingModal : DecidableEq EmbeddingModal

Equations

• Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instDecidableEqEmbeddingModal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instBEqEmbeddingModal : BEq EmbeddingModal

Equations

• Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instBEqEmbeddingModal = { beq := Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instBEqEmbeddingModal.beq }

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instBEqEmbeddingModal.beq : EmbeddingModal → EmbeddingModal → Bool

Equations

• Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instBEqEmbeddingModal.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprEmbeddingModal : Repr EmbeddingModal

Equations

• Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprEmbeddingModal = { reprPrec := Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprEmbeddingModal.repr }

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprEmbeddingModal.repr : EmbeddingModal → ℕ → Std.Format

Equations

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

structure Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.HarmonicDatum : Type

• chuj : String
• gloss : String
• embedding : EmbeddingModal
• isHarmonic : Bool
• reading : String
• exampleNumber : String

  Example number in @cite{alonso-ovalle-royer-2024}

instance Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprHarmonicDatum : Repr HarmonicDatum

Equations

• Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprHarmonicDatum = { reprPrec := Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprHarmonicDatum.repr }

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.instReprHarmonicDatum.repr : HarmonicDatum → ℕ → Std.Format

Equations

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

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.ex82_imperativeNonharmonic : HarmonicDatum

Equations

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

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.ex85_imperativeHarmonic : HarmonicDatum

Equations

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

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.ex90_attitudeHarmonic : HarmonicDatum

Equations

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

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.imperative_ambiguity : ex82_imperativeNonharmonic.chuj = ex85_imperativeHarmonic.chuj ∧ ex82_imperativeNonharmonic.isHarmonic ≠ ex85_imperativeHarmonic.isHarmonic

Same surface string, two readings: (82) non-harmonic and (85) harmonic share the same Chuj form but differ in anchor co-indexing.

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.availableAnchors : ChujDPPosition → List Semantics.Modality.EventRelativity.AnchorType

Which anchor types are semantically productive given a syntactic position (cross-classified with verb volitionality).

This is A-O&R's core structural explanation for the position-sensitivity of yalnhej's modal flavor.

Equations

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

def Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.predictedFlavors (pos : ChujDPPosition) : List Core.Modality.ModalFlavor

The predicted flavors for a position = the flavors of its available anchor types.

Equations

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

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.speech_anchor_epistemic : Semantics.Modality.EventRelativity.AnchorType.speechEvent.toFlavor = Core.Modality.ModalFlavor.epistemic

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.described_anchor_circumstantial : Semantics.Modality.EventRelativity.AnchorType.describedEvent.toFlavor = Core.Modality.ModalFlavor.circumstantial

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.predictions_match_data (pos : ChujDPPosition) : predictedFlavors pos = yalnhejFlavorsAt pos

The anchoring theory predicts exactly the observed flavor distribution for ALL five position types in Table 5.

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.active_agent_is_external : Causation.Studies.Coon2019.vØ.hasD = true ∧ predictedFlavors ChujDPPosition.externalArg = [Core.Modality.ModalFlavor.epistemic]

Active transitive voice (vØ): agent = external → epistemic only.

theorem Phenomena.ModalIndefinites.Studies.AlonsoOvalleRoyer2024.passive_theme_is_internal : Causation.Studies.Coon2019.v_ch.hasD = false ∧ predictedFlavors ChujDPPosition.internalArgVolitional = [Core.Modality.ModalFlavor.epistemic, Core.Modality.ModalFlavor.circumstantial]

Passive voice (-ch): theme promoted, agent implicit → both flavors.

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

Upper-bounded modal indefinites impose an anti-singleton inference (§5).

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

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

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

Yalnhej is not upper-bounded: compatible with partial-domain scenarios. The EventRelativity worked example demonstrates this concretely with yalnhej_nonmaximal_ab.