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).

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 Core.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}).

instance Core.ModalIndefinite.instDecidableEqModalComponentStatus : DecidableEq ModalComponentStatus

Equations

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

instance Core.ModalIndefinite.instBEqModalComponentStatus : BEq ModalComponentStatus

Equations

• Core.ModalIndefinite.instBEqModalComponentStatus = { beq := Core.ModalIndefinite.instBEqModalComponentStatus.beq }

def Core.ModalIndefinite.instBEqModalComponentStatus.beq : ModalComponentStatus → ModalComponentStatus → Bool

Equations

• Core.ModalIndefinite.instBEqModalComponentStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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

Equations

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

instance Core.ModalIndefinite.instReprModalComponentStatus : Repr ModalComponentStatus

Equations

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

structure Core.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 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}.

• source : String

  Source citation

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

Equations

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

instance Core.ModalIndefinite.instReprModalIndefiniteEntry : Repr ModalIndefiniteEntry

Equations

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

def Core.ModalIndefinite.ModalIndefiniteEntry.hasEpistemic (e : ModalIndefiniteEntry) : Bool

Equations

• e.hasEpistemic = e.flavors.any fun (x : Core.Modality.ModalFlavor) => x == Core.Modality.ModalFlavor.epistemic

def Core.ModalIndefinite.ModalIndefiniteEntry.hasCircumstantial (e : ModalIndefiniteEntry) : Bool

Equations

• e.hasCircumstantial = e.flavors.any fun (x : Core.Modality.ModalFlavor) => x == Core.Modality.ModalFlavor.circumstantial