Modal Indefinites: Cross-Linguistic Data

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

Theory-neutral empirical data on modal indefinites, following @cite{alonso-ovalle-royer-2024} "Modal indefinites: Lessons from Chuj."

Definition

A modal indefinite is an indefinite determiner / DP that conventionally encodes a modal component: beyond existential quantification, it conveys that any domain member could have been the witness (modal variation / free choice), or that the speaker doesn't know which individual satisfies the predicate (epistemic ignorance), or that any choice is permitted (random choice).

Three Dimensions of Variation (§6)

1. Status: Is the modal component at-issue (part of assertive content) or not-at-issue (presupposed / conventionally implicated)?
2. Content: Which modal flavors does the component support? (Epistemic, random choice / circumstantial, or both.)
3. Upper-boundedness: Does the indefinite impose an anti-singleton inference (¬∀x[P(x) → Q(x)])?

def Phenomena.ModalIndefinites.Data.yalnhej : Core.ModalIndefinite.ModalIndefiniteEntry

Chuj yalnhej: at-issue, epistemic + random choice, not upper-bounded, position-sensitive (§6).

External argument → epistemic only. Internal argument / adjunct (volitional) → epistemic or random choice. Internal argument / adjunct (non-volitional) → epistemic only.

Equations

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

def Phenomena.ModalIndefinites.Data.komon : Core.ModalIndefinite.ModalIndefiniteEntry

Chuj komon: at-issue random-choice modifier for mass/plural (@cite{alonso-ovalle-royer-2021}; cited in @cite{alonso-ovalle-royer-2024}, §5).

Equations

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

def Phenomena.ModalIndefinites.Data.algún : Core.ModalIndefinite.ModalIndefiniteEntry

Spanish algún: not-at-issue, epistemic only, upper-bounded (§6; @cite{alonso-ovalle-menendez-benito-2010}).

Equations

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

def Phenomena.ModalIndefinites.Data.irgendein : Core.ModalIndefinite.ModalIndefiniteEntry

German irgendein: not-at-issue, epistemic + random choice, not upper-bounded (§6). Epistemic in episodic assertions; random choice under deontic modals.

Equations

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

def Phenomena.ModalIndefinites.Data.unoCualquiera : Core.ModalIndefinite.ModalIndefiniteEntry

Spanish uno cualquiera: at-issue, random choice only, upper-bounded (§5–6; @cite{alonso-ovalle-menendez-benito-2010}).

Equations

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

def Phenomena.ModalIndefinites.Data.nimporteQuel : Core.ModalIndefinite.ModalIndefiniteEntry

French n'importe quel: at-issue, random choice only, not upper-bounded (§6; @cite{jayez-tovena-2006}).

Note: at-issue status and non-upper-boundedness are inferred from the cited source; @cite{alonso-ovalle-royer-2024} discusses content only.

Equations

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

def Phenomena.ModalIndefinites.Data.unQualsiasi : Core.ModalIndefinite.ModalIndefiniteEntry

Italian un qualsiasi: at-issue, random choice, not upper-bounded (§6; @cite{chierchia-2013}, §5.3.2).

Note: at-issue status and non-upper-boundedness are inferred from the cited source; @cite{alonso-ovalle-royer-2024} discusses content only.

Equations

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

def Phenomena.ModalIndefinites.Data.allEntries : List Core.ModalIndefinite.ModalIndefiniteEntry

Equations

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

theorem Phenomena.ModalIndefinites.Data.allEntries_count : allEntries.length = 7

theorem Phenomena.ModalIndefinites.Data.yalnhej_at_issue : yalnhej.status = Core.ModalIndefinite.ModalComponentStatus.atIssue

theorem Phenomena.ModalIndefinites.Data.algún_not_at_issue : algún.status = Core.ModalIndefinite.ModalComponentStatus.notAtIssue

theorem Phenomena.ModalIndefinites.Data.irgendein_not_at_issue : irgendein.status = Core.ModalIndefinite.ModalComponentStatus.notAtIssue

theorem Phenomena.ModalIndefinites.Data.unoCualquiera_at_issue : unoCualquiera.status = Core.ModalIndefinite.ModalComponentStatus.atIssue

theorem Phenomena.ModalIndefinites.Data.nimporteQuel_at_issue : nimporteQuel.status = Core.ModalIndefinite.ModalComponentStatus.atIssue

theorem Phenomena.ModalIndefinites.Data.yalnhej_not_upper_bounded : yalnhej.upperBounded = false

theorem Phenomena.ModalIndefinites.Data.algún_upper_bounded : algún.upperBounded = true

theorem Phenomena.ModalIndefinites.Data.irgendein_not_upper_bounded : irgendein.upperBounded = false

theorem Phenomena.ModalIndefinites.Data.unoCualquiera_upper_bounded : unoCualquiera.upperBounded = true

theorem Phenomena.ModalIndefinites.Data.nimporteQuel_not_upper_bounded : nimporteQuel.upperBounded = false

theorem Phenomena.ModalIndefinites.Data.yalnhej_has_epistemic : yalnhej.hasEpistemic = true

theorem Phenomena.ModalIndefinites.Data.yalnhej_has_rc : yalnhej.hasCircumstantial = true

theorem Phenomena.ModalIndefinites.Data.algún_epistemic_only : algún.hasEpistemic = true ∧ algún.hasCircumstantial = false

theorem Phenomena.ModalIndefinites.Data.irgendein_both_flavors : irgendein.hasEpistemic = true ∧ irgendein.hasCircumstantial = true

theorem Phenomena.ModalIndefinites.Data.unoCualquiera_rc_only : unoCualquiera.hasEpistemic = false ∧ unoCualquiera.hasCircumstantial = true

theorem Phenomena.ModalIndefinites.Data.yalnhej_position_sensitive : yalnhej.positionSensitive = true

theorem Phenomena.ModalIndefinites.Data.algún_not_position_sensitive : algún.positionSensitive = false

theorem Phenomena.ModalIndefinites.Data.yalnhej_irgendein_same_flavors : yalnhej.flavors = irgendein.flavors

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

theorem Phenomena.ModalIndefinites.Data.yalnhej_irgendein_differ_in_status : yalnhej.status ≠ irgendein.status

theorem Phenomena.ModalIndefinites.Data.at_issue_items : ([yalnhej, unoCualquiera, nimporteQuel, unQualsiasi].all fun (x : Core.ModalIndefinite.ModalIndefiniteEntry) => x.status == Core.ModalIndefinite.ModalComponentStatus.atIssue) = true

The at-issue / not-at-issue split (§6.1): yalnhej, uno cualquiera are at-issue; algún, irgendein are not-at-issue. (n'importe quel and un qualsiasi classified as at-issue per their respective cited sources.)

theorem Phenomena.ModalIndefinites.Data.not_at_issue_items : ([algún, irgendein].all fun (x : Core.ModalIndefinite.ModalIndefiniteEntry) => x.status == Core.ModalIndefinite.ModalComponentStatus.notAtIssue) = true

theorem Phenomena.ModalIndefinites.Data.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.Data.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}.

inductive Phenomena.ModalIndefinites.Data.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.Data.instDecidableEqChujDPPosition : DecidableEq ChujDPPosition

Equations

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

instance Phenomena.ModalIndefinites.Data.instBEqChujDPPosition : BEq ChujDPPosition

Equations

• Phenomena.ModalIndefinites.Data.instBEqChujDPPosition = { beq := Phenomena.ModalIndefinites.Data.instBEqChujDPPosition.beq }

def Phenomena.ModalIndefinites.Data.instBEqChujDPPosition.beq : ChujDPPosition → ChujDPPosition → Bool

Equations

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

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

Equations

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

instance Phenomena.ModalIndefinites.Data.instReprChujDPPosition : Repr ChujDPPosition

Equations

• Phenomena.ModalIndefinites.Data.instReprChujDPPosition = { reprPrec := Phenomena.ModalIndefinites.Data.instReprChujDPPosition.repr }

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

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

External argument: epistemic only — too high to co-bind with the VP event, so the anchor must project from the assertion (speech event). Internal/adjunct + volitional: both epistemic and RC — the described event has a decision subevent that can anchor normative modality. Internal/adjunct + non-volitional: epistemic only — the described event has no decision subevent, so f(e) cannot yield RC (§4.1, ex.34).

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.ModalIndefinites.Data.yalnhejFlavorsAt Phenomena.ModalIndefinites.Data.ChujDPPosition.externalArg = [Core.Modality.ModalFlavor.epistemic]
• Phenomena.ModalIndefinites.Data.yalnhejFlavorsAt Phenomena.ModalIndefinites.Data.ChujDPPosition.internalArgNonVolitional = [Core.Modality.ModalFlavor.epistemic]
• Phenomena.ModalIndefinites.Data.yalnhejFlavorsAt Phenomena.ModalIndefinites.Data.ChujDPPosition.adjunctVolitional = [Core.Modality.ModalFlavor.epistemic, Core.Modality.ModalFlavor.circumstantial]
• Phenomena.ModalIndefinites.Data.yalnhejFlavorsAt Phenomena.ModalIndefinites.Data.ChujDPPosition.adjunctNonVolitional = [Core.Modality.ModalFlavor.epistemic]

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

External argument restricts to epistemic only (§3.2.1).

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

Volitional internal argument allows both flavors (§3.2.2).

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

Non-volitional internal argument restricts to epistemic only (§3.2.2, ex.28/34).

theorem Phenomena.ModalIndefinites.Data.position_matters : yalnhejFlavorsAt ChujDPPosition.externalArg ≠ yalnhejFlavorsAt ChujDPPosition.internalArgVolitional

Position sensitivity: external ≠ volitional internal flavor sets.

theorem Phenomena.ModalIndefinites.Data.volitionality_matters : yalnhejFlavorsAt ChujDPPosition.internalArgVolitional ≠ yalnhejFlavorsAt ChujDPPosition.internalArgNonVolitional

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

structure Phenomena.ModalIndefinites.Data.YalnhejExample : Type

A Chuj yalnhej example sentence with empirical judgments.

• chuj : String

  Chuj sentence

• gloss : String

  English gloss

• position : ChujDPPosition

  Syntactic position of the yalnhej DP

• availableFlavors : List Core.Modality.ModalFlavor

  Available modal reading(s)

• exampleNumber : String

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

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

Equations

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

instance Phenomena.ModalIndefinites.Data.instReprYalnhejExample : Repr YalnhejExample

Equations

• Phenomena.ModalIndefinites.Data.instReprYalnhejExample = { reprPrec := Phenomena.ModalIndefinites.Data.instReprYalnhejExample.repr }

def Phenomena.ModalIndefinites.Data.ex22_extArg : YalnhejExample

(22)/(3): External argument, epistemic only. "A person or group of people danced at the party, I don't know who (maybe all did)." RC unavailable.

Equations

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

def Phenomena.ModalIndefinites.Data.ex31_intArgRC : YalnhejExample

(31): Internal argument, volitional verb, random choice available. "Xun bought a random book / some random books."

Equations

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

def Phenomena.ModalIndefinites.Data.ex34_intArgNonVol : YalnhejExample

(34)/(28): Internal argument, non-volitional verb, epistemic only. "Xun liked some dish(es) or other, I don't know which (maybe all)." RC unavailable with non-volitional 'like'.

Equations

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

def Phenomena.ModalIndefinites.Data.ex41_adjunctRC : YalnhejExample

(41): Adjunct, volitional verb, random choice available. "Malin ate yalnhej where" = Malin ate at a random place.

Equations

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

def Phenomena.ModalIndefinites.Data.ex39_adjunctNonVol : YalnhejExample

(39): Adjunct, non-volitional verb, epistemic only. "There was rain yalnhej where yesterday" = It rained somewhere, I don't know where. RC unavailable.

Equations

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

def Phenomena.ModalIndefinites.Data.allExamples : List YalnhejExample

Equations

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

theorem Phenomena.ModalIndefinites.Data.ex22_epistemic_only : ex22_extArg.availableFlavors = [Core.Modality.ModalFlavor.epistemic]

Per-example flavor verification.

theorem Phenomena.ModalIndefinites.Data.ex31_allows_rc : ex31_intArgRC.availableFlavors = [Core.Modality.ModalFlavor.epistemic, Core.Modality.ModalFlavor.circumstantial]

theorem Phenomena.ModalIndefinites.Data.ex34_nonvol_epistemic_only : ex34_intArgNonVol.availableFlavors = [Core.Modality.ModalFlavor.epistemic]

theorem Phenomena.ModalIndefinites.Data.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). A whatever-FR requires every domain member to satisfy the scope; yalnhej does not. This is distinct from upper-boundedness: UB blocks ∀P→Q (anti-singleton), whereas non-maximality merely allows ¬∀P→Q without requiring it.

structure Phenomena.ModalIndefinites.Data.MaximalityDatum : Type

A maximality datum: a context + Chuj sentence + felicity judgment.

• context : String

  Context description

• chuj : String

  Chuj sentence

• gloss : String

  English gloss

• yalnhejFelicitous : Bool

  Whether yalnhej is felicitous in this context

• exampleNumber : String

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

instance Phenomena.ModalIndefinites.Data.instReprMaximalityDatum : Repr MaximalityDatum

Equations

• Phenomena.ModalIndefinites.Data.instReprMaximalityDatum = { reprPrec := Phenomena.ModalIndefinites.Data.instReprMaximalityDatum.repr }

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

Equations

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

def Phenomena.ModalIndefinites.Data.ex43_partialRC : MaximalityDatum

(43)/(44): Partial-domain, RC context. Context: 10 tools on a table; speaker grabbed 3 at random. Yalnhej is felicitous — no maximality requirement.

Equations

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

def Phenomena.ModalIndefinites.Data.ex46_partialEpi : MaximalityDatum

(46)/(47): Partial-domain, epistemic context. Context: 10 meals available; speaker ate 5 but doesn't remember which. Yalnhej is felicitous — compatible with not knowing, without requiring all meals to have been eaten.

Equations

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

def Phenomena.ModalIndefinites.Data.allMaximalityData : List MaximalityDatum

Equations

• Phenomena.ModalIndefinites.Data.allMaximalityData = [Phenomena.ModalIndefinites.Data.ex43_partialRC, Phenomena.ModalIndefinites.Data.ex46_partialEpi]

theorem Phenomena.ModalIndefinites.Data.ex43_felicitous : ex43_partialRC.yalnhejFelicitous = true

Per-datum: both partial-domain examples are felicitous with yalnhej.

theorem Phenomena.ModalIndefinites.Data.ex46_felicitous : ex46_partialEpi.yalnhejFelicitous = true

theorem Phenomena.ModalIndefinites.Data.all_partial_domain_felicitous : (allMaximalityData.all fun (x : MaximalityDatum) => x.yalnhejFelicitous) = true

All maximality data show yalnhej is felicitous in partial-domain contexts — confirming non-maximality.

Some modal indefinites have "unremarkable" (plain existential) readings in addition to their modal readings. Komon and uno cualquiera can mean just "some" without modal flavor; yalnhej cannot. @cite{alonso-ovalle-royer-2024} (§5) correlate this with predicativity: items that can appear in predicative position tend to have unremarkable readings; yalnhej cannot be predicative and correspondingly lacks unremarkable readings.

structure Phenomena.ModalIndefinites.Data.UnremarkableReadingDatum : Type

An unremarkable-reading datum: item + whether it has unremarkable readings.

• language : String

  Language

• form : String

  Surface form

• hasUnremarkable : Bool

  Does the item have unremarkable (non-modal) readings?

• predicative : Bool

  Can the item appear in predicative position?

• exampleNumber : String

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

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

Equations

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

instance Phenomena.ModalIndefinites.Data.instReprUnremarkableReadingDatum : Repr UnremarkableReadingDatum

Equations

• Phenomena.ModalIndefinites.Data.instReprUnremarkableReadingDatum = { reprPrec := Phenomena.ModalIndefinites.Data.instReprUnremarkableReadingDatum.repr }

def Phenomena.ModalIndefinites.Data.unoCualquiera_unremarkable : UnremarkableReadingDatum

(99)–(102): uno cualquiera has unremarkable readings; can be predicative.

Equations

• Phenomena.ModalIndefinites.Data.unoCualquiera_unremarkable = { language := "Spanish", form := "uno cualquiera", hasUnremarkable := true, predicative := true, exampleNumber := "(99)–(102)" }

def Phenomena.ModalIndefinites.Data.irgendein_unremarkable : UnremarkableReadingDatum

(94)/(95): irgendein has unremarkable readings; can be predicative.

Equations

• Phenomena.ModalIndefinites.Data.irgendein_unremarkable = { language := "German", form := "irgendein", hasUnremarkable := true, predicative := true, exampleNumber := "(94)/(95)" }

def Phenomena.ModalIndefinites.Data.komon_unremarkable : UnremarkableReadingDatum

komon has unremarkable readings; can be predicative (§5).

Equations

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

def Phenomena.ModalIndefinites.Data.yalnhej_unremarkable : UnremarkableReadingDatum

(104)/(105): yalnhej LACKS unremarkable readings; CANNOT be predicative.

Equations

• Phenomena.ModalIndefinites.Data.yalnhej_unremarkable = { language := "Chuj (Mayan)", form := "yalnhej", hasUnremarkable := false, predicative := false, exampleNumber := "(104)/(105)" }

def Phenomena.ModalIndefinites.Data.allUnremarkableData : List UnremarkableReadingDatum

Equations

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

theorem Phenomena.ModalIndefinites.Data.yalnhej_no_unremarkable : yalnhej_unremarkable.hasUnremarkable = false

theorem Phenomena.ModalIndefinites.Data.komon_has_unremarkable : komon_unremarkable.hasUnremarkable = true

theorem Phenomena.ModalIndefinites.Data.unoCualquiera_has_unremarkable : unoCualquiera_unremarkable.hasUnremarkable = true

theorem Phenomena.ModalIndefinites.Data.irgendein_has_unremarkable_datum : irgendein_unremarkable.hasUnremarkable = true

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

Predicativity correlates with unremarkable readings: every datum where canBePredicate = true also has unremarkable readings, and vice versa.

theorem Phenomena.ModalIndefinites.Data.yalnhej_entry_unremarkable_agrees : yalnhej.hasUnremarkableReading = yalnhej_unremarkable.hasUnremarkable

Cross-check: the entry-level fields agree with the datum-level fields for yalnhej, komon, and uno cualquiera.

theorem Phenomena.ModalIndefinites.Data.komon_entry_unremarkable_agrees : komon.hasUnremarkableReading = komon_unremarkable.hasUnremarkable

theorem Phenomena.ModalIndefinites.Data.unoCualquiera_entry_unremarkable_agrees : unoCualquiera.hasUnremarkableReading = unoCualquiera_unremarkable.hasUnremarkable

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. The non-harmonic reading anchors the MI to the described event independently; the harmonic reading aligns the MI's domain with the external modal's domain.

inductive Phenomena.ModalIndefinites.Data.EmbeddingModal : Type

The type of embedding modal for harmonic interpretation data.

• imperative : EmbeddingModal

  Imperative: "Grab yalnhej card!"

• deontic : EmbeddingModal

  Deontic: "You should grab yalnhej card."

• attitudeVerb : EmbeddingModal

  Attitude verb: "Xun thinks yalnhej person came."

instance Phenomena.ModalIndefinites.Data.instDecidableEqEmbeddingModal : DecidableEq EmbeddingModal

Equations

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

def Phenomena.ModalIndefinites.Data.instBEqEmbeddingModal.beq : EmbeddingModal → EmbeddingModal → Bool

Equations

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

instance Phenomena.ModalIndefinites.Data.instBEqEmbeddingModal : BEq EmbeddingModal

Equations

• Phenomena.ModalIndefinites.Data.instBEqEmbeddingModal = { beq := Phenomena.ModalIndefinites.Data.instBEqEmbeddingModal.beq }

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

Equations

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

instance Phenomena.ModalIndefinites.Data.instReprEmbeddingModal : Repr EmbeddingModal

Equations

• Phenomena.ModalIndefinites.Data.instReprEmbeddingModal = { reprPrec := Phenomena.ModalIndefinites.Data.instReprEmbeddingModal.repr }

structure Phenomena.ModalIndefinites.Data.HarmonicDatum : Type

A harmonic interpretation datum.

• chuj : String

  Chuj sentence

• gloss : String

  English gloss

• embedding : EmbeddingModal

  Which embedding modal

• isHarmonic : Bool

  Does the harmonic reading arise?

• reading : String

  Description of reading

• exampleNumber : String

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

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

Equations

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

instance Phenomena.ModalIndefinites.Data.instReprHarmonicDatum : Repr HarmonicDatum

Equations

• Phenomena.ModalIndefinites.Data.instReprHarmonicDatum = { reprPrec := Phenomena.ModalIndefinites.Data.instReprHarmonicDatum.repr }

def Phenomena.ModalIndefinites.Data.ex82_imperativeNonharmonic : HarmonicDatum

(82): Imperative, non-harmonic reading. "Grab a random card!" — MI anchors to the described (grabbing) event.

Equations

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

def Phenomena.ModalIndefinites.Data.ex85_imperativeHarmonic : HarmonicDatum

(85): Imperative, harmonic reading. "Grab yalnhej card!" — MI anchor co-indexed with imperative event, giving "any card is fine" / "it doesn't matter which."

Equations

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

def Phenomena.ModalIndefinites.Data.ex90_attitudeHarmonic : HarmonicDatum

(90)/(91): Attitude verb, harmonic reading. "Xun thinks yalnhej person came" — MI anchor co-indexed with doxastic modal of 'think', giving "whoever it was" reading.

Equations

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

def Phenomena.ModalIndefinites.Data.allHarmonicData : List HarmonicDatum

Equations

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

theorem Phenomena.ModalIndefinites.Data.ex82_nonharmonic : ex82_imperativeNonharmonic.isHarmonic = false

theorem Phenomena.ModalIndefinites.Data.ex85_harmonic : ex85_imperativeHarmonic.isHarmonic = true

theorem Phenomena.ModalIndefinites.Data.ex90_harmonic : ex90_attitudeHarmonic.isHarmonic = true

theorem Phenomena.ModalIndefinites.Data.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.