Modal Indefinite Types

@cite{alonso-ovalle-menendez-benito-2010} @cite{alonso-ovalle-royer-2024}

Framework-agnostic types for recording cross-linguistic properties of modal indefinites — indefinite determiners/DPs that conventionally encode a modal component (e.g., Chuj yalnhej, Spanish algún, German irgendein).

Sibling of Features/IndefiniteType.lean: that file classifies indefinites by Degano & Aloni's variation/constancy types (Haspelmath's NS/SU/SK map); this file classifies modal indefinites by Alonso-Ovalle & Royer's three dimensions (status × content × upper-boundedness).

Three Dimensions of Variation

Following @cite{alonso-ovalle-royer-2024}:

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 it impose an anti-singleton inference?

inductive Features.ModalIndefinite.ModalComponentStatus : Type

Whether the modal component of a modal indefinite is at-issue or not-at-issue.

Diagnostics:

• At-issue: targetable by direct denial ("No, that's not true — you know exactly which book you bought")
• Not-at-issue: targetable by "Hey, wait a minute!" but not by direct denial; projects under negation, questions, modals

• atIssue : ModalComponentStatus

  Modal component is part of assertive content (challengeable by direct denial). Ex: Chuj yalnhej, Sp. uno cualquiera.

• notAtIssue : ModalComponentStatus

  Modal component is not part of assertive content: presupposed, conventionally implicated, or conversationally implicated. Projects or persists under embedding operators. Ex: Sp. algún (conv. implicature per @cite{alonso-ovalle-menendez-benito-2010}), Ger. irgendein (domain widening per @cite{kratzer-shimoyama-2002}).

@[implicit_reducible]

instance Features.ModalIndefinite.instDecidableEqModalComponentStatus : DecidableEq ModalComponentStatus

Equations

• Features.ModalIndefinite.instDecidableEqModalComponentStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.ModalIndefinite.instReprModalComponentStatus.repr : ModalComponentStatus → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.ModalIndefinite.instReprModalComponentStatus : Repr ModalComponentStatus

Equations

• Features.ModalIndefinite.instReprModalComponentStatus = { reprPrec := Features.ModalIndefinite.instReprModalComponentStatus.repr }

inductive Features.ModalIndefinite.AnchorConstraint : Type

Whether the anchoring function f has a definedness condition. @cite{alonso-ovalle-royer-2024} §4.1–4.2.

Modal indefinites whose modal component is at-issue project their modal domain from an event argument via an anchoring function f. The key lexical distinction is whether f has no definedness condition (accepting any event) or presupposes normative content. Note that f's definedness controls which events CAN anchor the MI; content licensing (whether the event has propositional content) independently determines the resulting modal flavor.

• unrestricted : AnchorConstraint

  f has no definedness condition: defined for any event regardless of content. The anchor constraint does not restrict WHERE f can anchor. Whether the resulting background is epistemic, however, depends on the specific projection function f — not just on anchor definedness or content licensing. For yalnhej, f yields an epistemic background from contentful events; for n'importe quel and un qualsiasi, f always yields a circumstantial/ indiscriminacy background regardless of the event's content (@cite{alonso-ovalle-royer-2024}, §6.2: "different functions projecting modal domains from those anchors"). Ex: Chuj yalnhej, French n'importe quel, Italian un qualsiasi.

• volitionalOnly : AnchorConstraint

  f presupposes that its event argument has normative content (a decision subevent of a volitional event). Speech acts lack normative content, so f(speech event) is undefined → no epistemic. Only yields RC readings (from volitional VP events). Ex: Spanish uno cualquiera.

@[implicit_reducible]

instance Features.ModalIndefinite.instDecidableEqAnchorConstraint : DecidableEq AnchorConstraint

Equations

• Features.ModalIndefinite.instDecidableEqAnchorConstraint x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.ModalIndefinite.instReprAnchorConstraint.repr : AnchorConstraint → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.ModalIndefinite.instReprAnchorConstraint : Repr AnchorConstraint

Equations

• Features.ModalIndefinite.instReprAnchorConstraint = { reprPrec := Features.ModalIndefinite.instReprAnchorConstraint.repr }

structure Features.ModalIndefinite.ModalIndefiniteEntry : Type

A cross-linguistic modal indefinite entry parameterized along @cite{alonso-ovalle-royer-2024} three dimensions of variation.

• language : String

  Language name

• form : String

  Surface form

• gloss : String

  Gloss or translation

• status : ModalComponentStatus

  Dimension 1: Is the modal component at-issue?

• flavors : List Core.Modality.ModalFlavor

  Dimension 2: Which modal flavors are available?

• upperBounded : Bool

  Dimension 3: Does it impose an upper bound (anti-singleton)?

• positionSensitive : Bool

  Is the available flavor sensitive to syntactic position?

• hasUnremarkableReading : Bool

  Does the item have a plain/unremarkable (non-modal) reading in addition to its modal reading? (A-@cite{alonso-ovalle-royer-2024}, §5)

• canBePredicate : Bool

  Can the item appear in predicative position? Correlates with unremarkable readings per A-@cite{alonso-ovalle-royer-2024}.

• anchorConstraint : Option AnchorConstraint

  Anchor constraint on the anchoring function f. Only applicable to at-issue modal indefinites analyzed via event-relative anchoring (@cite{alonso-ovalle-royer-2024}). none for items with non-at-issue modal components (e.g., algún, irgendein) where the mechanism is conversational implicature or domain widening.

• numberNeutral : Bool

  Whether the item is number-neutral (compatible with singular and plural reference). Chuj yalnhej is number-neutral (wh-phrase origin); Spanish algún is singular-only.

• source : String

  Source citation

def Features.ModalIndefinite.instReprModalIndefiniteEntry.repr : ModalIndefiniteEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.ModalIndefinite.instReprModalIndefiniteEntry : Repr ModalIndefiniteEntry

Equations

• Features.ModalIndefinite.instReprModalIndefiniteEntry = { reprPrec := Features.ModalIndefinite.instReprModalIndefiniteEntry.repr }

def Features.ModalIndefinite.ModalIndefiniteEntry.hasFlavor (e : ModalIndefiniteEntry) (f : Core.Modality.ModalFlavor) : Prop

Whether the entry's modal component supports a given flavor. Generic over ModalFlavor rather than cherry-picking named projections.

Equations

• e.hasFlavor f = (f ∈ e.flavors)

@[implicit_reducible]

instance Features.ModalIndefinite.instDecidableHasFlavor (e : ModalIndefiniteEntry) (f : Core.Modality.ModalFlavor) : Decidable (e.hasFlavor f)

Equations

• Features.ModalIndefinite.instDecidableHasFlavor e f = Features.ModalIndefinite.instDecidableHasFlavor._aux_1 e f