Modal Indefinite Types

Framework-agnostic types for recording cross-linguistic properties of modal indefinites — indefinites that conventionally encode a modal component (Chuj yalnhej, Spanish algún, German irgendein) — along [AOR24]'s dimensions of variation: status (§6.1), content (§6.2), and upper-boundedness (within §6.2). Random-choice readings are carried by the .circumstantial flavor.

Sibling of Features/IndefiniteType.lean, which classifies indefinites by Degano & Aloni's variation/constancy types.

Main declarations

• ModalIndefiniteEntry — a lexical entry over the three dimensions.
• ModalComponentStatus, AnchorConstraint — the status dimension and the definedness condition on the anchoring function f.

Modal component status

inductive Features.ModalIndefinite.ModalComponentStatus : Type

Whether the modal component of a modal indefinite is at-issue (challengeable by direct denial) or not-at-issue (projects under negation, questions, and modals).

• atIssue : ModalComponentStatus

  Part of assertive content. Ex: Chuj yalnhej, Sp. uno cualquiera.

• notAtIssue : ModalComponentStatus

  Presupposed or implicated rather than asserted. Ex: Sp. algún (conversational implicature per [AOMB10]), Ger. irgendein (domain widening per [KS17]).

@[instance_reducible]

instance Features.ModalIndefinite.instDecidableEqModalComponentStatus : DecidableEq ModalComponentStatus

Equations

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

@[instance_reducible]

instance Features.ModalIndefinite.instReprModalComponentStatus : Repr ModalComponentStatus

Equations

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

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

Equations

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

Anchor constraint

inductive Features.ModalIndefinite.AnchorConstraint : Type

Whether the anchoring function f of an at-issue modal indefinite has a definedness condition ([AOR24] §4).

• unrestricted : AnchorConstraint

  f is defined for any event. For yalnhej, f yields an epistemic background from contentful events. French n'importe quel and Italian un qualsiasi express random choice only; [AOR24] (§6.2) leaves open whether that follows from an anchor constraint or from a different projection function, so their listing here picks no horn.

• volitionalOnly : AnchorConstraint

  f presupposes normative content (a decision subevent of a volitional event), so only random-choice readings arise; on this analysis a speech event supplies no normative content, blocking epistemic readings. Ex: Spanish uno cualquiera.

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

@[instance_reducible]

instance Features.ModalIndefinite.instReprAnchorConstraint : Repr AnchorConstraint

Equations

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

Modal indefinite entry

structure Features.ModalIndefinite.ModalIndefiniteEntry : Type

A modal indefinite entry over [AOR24]'s dimensions of variation.

• form : String

  Surface form

• 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 on witnesses in the described situation? (Distinct from [AOMB10]'s anti-singleton domain constraint.)

• hasUnremarkableReading : Bool

  Does the item have a plain, non-modal reading in addition to its modal reading? ([AOR24], §5)

• canBePredicate : Bool

  Can the item appear in predicative position?

• anchorConstraint : Option AnchorConstraint

  Anchor constraint on the anchoring function f. none for not-at-issue items (conversational implicature, domain widening) and for at-issue items fitting neither constructor (Chuj komon: never epistemic, yet fine with non-volitional predicates).

• numberNeutral : Bool

  Is the item number-neutral? Chuj yalnhej is; Spanish algún is singular-only.

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

Equations

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

@[instance_reducible]

instance Features.ModalIndefinite.instReprModalIndefiniteEntry : Repr ModalIndefiniteEntry

Equations

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

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

Whether the entry's modal component supports a given flavor.

Equations

• e.hasFlavor f = e.flavors.contains f