Modal Typological Types

Theory-neutral vocabulary for cross-linguistic modal typology: ModalForce, ModalFlavor, ForceFlavor, ModalItem, ConcordType, ModalDecomposition.

These types classify modal meanings along two independent dimensions — force (quantificational strength) and flavor (contextual source) — following @cite{kratzer-1981} and @cite{imel-guo-steinert-threlkeld-2026}.

Separated from Core.Logic.Intensional because Kripke frames and frame correspondence are pure mathematical logic, while force/flavor classification is linguistic typology. The two are connected (Kripke semantics interprets force-flavor pairs) but conceptually independent.

What belongs here vs. Core.Logic.Intensional

• Here (Core.Modality): ModalForce, ModalFlavor, ForceFlavor, ModalItem, ConcordType, ModalDecomposition — linguistic classification of modal meanings.
• There (Core.Logic.Intensional): AccessRel, kripkeEval, frame conditions (IsReflexive, IsSerial, IsTransitive, IsSymmetric, IsEuclidean), correspondence theorems, the lattice of normal modal logics — mathematical semantics.

inductive Core.Modality.ModalForce : Type

Modal force: necessity (□), weak necessity (□w), or possibility (◇). @cite{von-fintel-iatridou-2008}, @cite{agha-jeretic-2026}.

Weak necessity ("ought", "should") sits between □ and ◇ in strength: □φ → □wφ → ◇φ. The nature of this intermediate force is debated:

• @cite{von-fintel-iatridou-2008}: same ∀ quantifier as strong necessity but over a refined (smaller) set of best worlds (domain restriction).
• Rubinstein (2014): fundamentally comparative meaning.
• @cite{agha-jeretic-2022}: non-quantificational (plural predication).

Weak necessity has no clean dual in this 3-point space: domain refinement weakens ∀ but strengthens ∃ (@cite{agha-jeretic-2026}; UNVERIFIED §2.4).

• necessity : ModalForce
• weakNecessity : ModalForce
• possibility : ModalForce

@[implicit_reducible]

instance Core.Modality.instDecidableEqModalForce : DecidableEq ModalForce

Equations

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

def Core.Modality.instReprModalForce.repr : ModalForce → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Modality.instReprModalForce : Repr ModalForce

Equations

• Core.Modality.instReprModalForce = { reprPrec := Core.Modality.instReprModalForce.repr }

def Core.Modality.instInhabitedModalForce.default : ModalForce

Equations

• Core.Modality.instInhabitedModalForce.default = Core.Modality.ModalForce.necessity

@[implicit_reducible]

instance Core.Modality.instInhabitedModalForce : Inhabited ModalForce

Equations

• Core.Modality.instInhabitedModalForce = { default := Core.Modality.instInhabitedModalForce.default }

instance Core.Modality.instLawfulBEqModalForce : LawfulBEq ModalForce

@[implicit_reducible]

instance Core.Modality.instToStringModalForce : ToString ModalForce

Equations

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

def Core.Modality.ModalForce.dual : ModalForce → ModalForce

Classical dual: □ ↔ ◇. Weak necessity maps to possibility as a stipulated default. The literature is unsettled: Yalcin 2016, Lassiter 2017, Carr 2024, and arguably von Fintel & Iatridou 2008 themselves discuss candidate weak-necessity duals ("might-as-easily-not", "could", priority might). The "no clean dual" claim attributed to @cite{agha-jeretic-2026} (UNVERIFIED §2.4 quote) should be read as "no consensus dual", not as a structural impossibility.

Equations

• Core.Modality.ModalForce.necessity.dual = Core.Modality.ModalForce.possibility
• Core.Modality.ModalForce.weakNecessity.dual = Core.Modality.ModalForce.possibility
• Core.Modality.ModalForce.possibility.dual = Core.Modality.ModalForce.necessity

@[simp]

theorem Core.Modality.ModalForce.dual_dual_necessity : necessity.dual.dual = necessity

@[simp]

theorem Core.Modality.ModalForce.dual_dual_possibility : possibility.dual.dual = possibility

def Core.Modality.ModalForce.all : List ModalForce

All modal forces.

Equations

• Core.Modality.ModalForce.all = [Core.Modality.ModalForce.necessity, Core.Modality.ModalForce.weakNecessity, Core.Modality.ModalForce.possibility]

def Core.Modality.ModalForce.atLeastAsStrong : ModalForce → ModalForce → Bool

Strength ordering on modal force: □ ≥ □w ≥ ◇. f₁.atLeastAsStrong f₂ iff an f₁-claim is at least as strong as an f₂-claim. @cite{von-fintel-iatridou-2008}: must φ → ought φ → can φ.

Equations

• Core.Modality.ModalForce.necessity.atLeastAsStrong x✝ = true
• Core.Modality.ModalForce.weakNecessity.atLeastAsStrong Core.Modality.ModalForce.weakNecessity = true
• Core.Modality.ModalForce.weakNecessity.atLeastAsStrong Core.Modality.ModalForce.possibility = true
• Core.Modality.ModalForce.possibility.atLeastAsStrong Core.Modality.ModalForce.possibility = true
• x✝¹.atLeastAsStrong x✝ = false

theorem Core.Modality.ModalForce.atLeastAsStrong_refl (f : ModalForce) : f.atLeastAsStrong f = true

theorem Core.Modality.ModalForce.atLeastAsStrong_trans (f₁ f₂ f₃ : ModalForce) (h₁ : f₁.atLeastAsStrong f₂ = true) (h₂ : f₂.atLeastAsStrong f₃ = true) : f₁.atLeastAsStrong f₃ = true

theorem Core.Modality.ModalForce.necessity_strongest (f : ModalForce) : necessity.atLeastAsStrong f = true

theorem Core.Modality.ModalForce.possibility_weakest (f : ModalForce) : f.atLeastAsStrong possibility = true

inductive Core.Modality.ModalFlavor : Type

Modal flavor: the contextual source of modality. Theory-neutral: avoids commitment to how flavor is semantically encoded. Teleological is subsumed under circumstantial (both concern facts/abilities). Bouletic (desires/wishes) is distinguished from deontic (norms/rules), following @cite{kratzer-1981}'s four-way classification.

• epistemic : ModalFlavor
• deontic : ModalFlavor
• bouletic : ModalFlavor
• circumstantial : ModalFlavor

@[implicit_reducible]

instance Core.Modality.instDecidableEqModalFlavor : DecidableEq ModalFlavor

Equations

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

def Core.Modality.instReprModalFlavor.repr : ModalFlavor → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Modality.instReprModalFlavor : Repr ModalFlavor

Equations

• Core.Modality.instReprModalFlavor = { reprPrec := Core.Modality.instReprModalFlavor.repr }

@[implicit_reducible]

instance Core.Modality.instInhabitedModalFlavor : Inhabited ModalFlavor

Equations

• Core.Modality.instInhabitedModalFlavor = { default := Core.Modality.instInhabitedModalFlavor.default }

def Core.Modality.instInhabitedModalFlavor.default : ModalFlavor

Equations

• Core.Modality.instInhabitedModalFlavor.default = Core.Modality.ModalFlavor.epistemic

instance Core.Modality.instLawfulBEqModalFlavor : LawfulBEq ModalFlavor

@[implicit_reducible]

instance Core.Modality.instToStringModalFlavor : ToString ModalFlavor

Equations

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

def Core.Modality.ModalFlavor.all : List ModalFlavor

All modal flavors.

Equations

• Core.Modality.ModalFlavor.all = [Core.Modality.ModalFlavor.epistemic, Core.Modality.ModalFlavor.deontic, Core.Modality.ModalFlavor.bouletic, Core.Modality.ModalFlavor.circumstantial]

structure Core.Modality.ForceFlavor : Type

A force-flavor pair: one point in the modal semantic space P. |P| = |Force| × |Flavor| = 3 × 4 = 12.

Imel, Guo, & @cite{imel-guo-steinert-threlkeld-2026}: modal meanings are subsets of P. Their original database uses a 2×3 space (necessity/possibility × 3 flavors); we extend to 3×4 by adding weak necessity as a distinct force value (following @cite{agha-jeretic-2026}) and bouletic as a distinct flavor (following @cite{kratzer-1981}).

• force : ModalForce
• flavor : ModalFlavor

def Core.Modality.instDecidableEqForceFlavor.decEq (x✝ x✝¹ : ForceFlavor) : Decidable (x✝ = x✝¹)

Equations

• Core.Modality.instDecidableEqForceFlavor.decEq { force := a, flavor := a_1 } { force := b, flavor := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Modality.instDecidableEqForceFlavor : DecidableEq ForceFlavor

Equations

• Core.Modality.instDecidableEqForceFlavor = Core.Modality.instDecidableEqForceFlavor.decEq

def Core.Modality.instReprForceFlavor.repr : ForceFlavor → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Modality.instReprForceFlavor : Repr ForceFlavor

Equations

• Core.Modality.instReprForceFlavor = { reprPrec := Core.Modality.instReprForceFlavor.repr }

@[implicit_reducible]

instance Core.Modality.instInhabitedForceFlavor : Inhabited ForceFlavor

Equations

• Core.Modality.instInhabitedForceFlavor = { default := Core.Modality.instInhabitedForceFlavor.default }

def Core.Modality.instInhabitedForceFlavor.default : ForceFlavor

Equations

• Core.Modality.instInhabitedForceFlavor.default = { force := default, flavor := default }

instance Core.Modality.instLawfulBEqForceFlavor : LawfulBEq ForceFlavor

@[implicit_reducible]

instance Core.Modality.instToStringForceFlavor : ToString ForceFlavor

Equations

• Core.Modality.instToStringForceFlavor = { toString := fun (ff : Core.Modality.ForceFlavor) => toString "(" ++ toString ff.force ++ toString "," ++ toString ff.flavor ++ toString ")" }

def Core.Modality.ForceFlavor.universe : List ForceFlavor

All twelve points in the modal semantic space (|ModalForce| × |ModalFlavor| = 3 × 4).

Equations

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

theorem Core.Modality.ForceFlavor.universe_length : «universe».length = 12

def Core.Modality.ForceFlavor.cartesianProduct (fos : List ModalForce) (fls : List ModalFlavor) : List ForceFlavor

The Cartesian product of forces and flavors. Infrastructure for constructing modal meanings; no theoretical commitment (just list operations).

Equations

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

structure Core.Modality.ModalItem : Type

A modal item: the shared core of any expression carrying modal meaning.

Unifies AuxEntry.{form, modalMeaning, register}, ModalAdvEntry.{form, modalMeaning, register}, and ModalExpression.{form, meaning} under a common type.

• form : String
• meaning : List ForceFlavor
• register : Features.Register.Level

def Core.Modality.instReprModalItem.repr : ModalItem → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Modality.instReprModalItem : Repr ModalItem

Equations

• Core.Modality.instReprModalItem = { reprPrec := Core.Modality.instReprModalItem.repr }

def Core.Modality.instBEqModalItem.beq : ModalItem → ModalItem → Bool

Equations

• Core.Modality.instBEqModalItem.beq { form := a, meaning := a_1, register := a_2 } { form := b, meaning := b_1, register := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Core.Modality.instBEqModalItem.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Core.Modality.instBEqModalItem : BEq ModalItem

Equations

• Core.Modality.instBEqModalItem = { beq := Core.Modality.instBEqModalItem.beq }

def Core.Modality.ModalItem.areRegisterVariants (a b : ModalItem) : Prop

Two modal items are register variants if they differ in register.

Equations

• a.areRegisterVariants b = Features.Register.areVariants a.register b.register

@[implicit_reducible]

instance Core.Modality.instDecidableAreRegisterVariants (a b : ModalItem) : Decidable (a.areRegisterVariants b)

Equations

• Core.Modality.instDecidableAreRegisterVariants a b = Core.Modality.instDecidableAreRegisterVariants._aux_1 a b

inductive Core.Modality.ConcordType : Type

Classification of concord phenomena by what logical type is doubled.

• negation : ConcordType
• modalNecessity : ConcordType
• modalPossibility : ConcordType

@[implicit_reducible]

instance Core.Modality.instDecidableEqConcordType : DecidableEq ConcordType

Equations

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

@[implicit_reducible]

instance Core.Modality.instReprConcordType : Repr ConcordType

Equations

• Core.Modality.instReprConcordType = { reprPrec := Core.Modality.instReprConcordType.repr }

def Core.Modality.instReprConcordType.repr : ConcordType → ℕ → Std.Format

Equations

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

def Core.Modality.ConcordType.fromModalForce : ModalForce → ConcordType

Map modal force to the corresponding concord type. Weak necessity patterns with necessity for concord purposes (both are ∀ quantifiers).

Equations

• Core.Modality.ConcordType.fromModalForce Core.Modality.ModalForce.necessity = Core.Modality.ConcordType.modalNecessity
• Core.Modality.ConcordType.fromModalForce Core.Modality.ModalForce.weakNecessity = Core.Modality.ConcordType.modalNecessity
• Core.Modality.ConcordType.fromModalForce Core.Modality.ModalForce.possibility = Core.Modality.ConcordType.modalPossibility

def Core.Modality.ModalItem.sharesConcordForce (a b : ModalItem) : Bool

Two modal items share concord-compatible force: both necessity and weak necessity map to the same concord class (necessity-type). This is the structural precondition for modal concord.

Equations

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

inductive Core.Modality.ModalInterpretability : Type

Interpretability of a modal feature (@cite{zeijlstra-2007}).

Modal elements carry features specifying modal force (∃/∀). Features are either interpretable (semantically active — the element contributes a modal operator at LF) or uninterpretable (semantically vacuous — the element is checked by a c-commanding interpretable feature and does not contribute its own operator).

@cite{ciardelli-guerrini-2026} use this distinction to derive narrow-scope readings for "MOD A COORD MOD B" sentences: when both auxiliaries carry uninterpretable features, a single silent interpretable operator scopes over the coordination, yielding Δ(A ∘ B) rather than ΔA ∘ ΔB.

• interpretable : ModalInterpretability
• uninterpretable : ModalInterpretability

@[implicit_reducible]

instance Core.Modality.instDecidableEqModalInterpretability : DecidableEq ModalInterpretability

Equations

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

def Core.Modality.instReprModalInterpretability.repr : ModalInterpretability → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Modality.instReprModalInterpretability : Repr ModalInterpretability

Equations

• Core.Modality.instReprModalInterpretability = { reprPrec := Core.Modality.instReprModalInterpretability.repr }

def Core.Modality.instBEqModalInterpretability.beq : ModalInterpretability → ModalInterpretability → Bool

Equations

• Core.Modality.instBEqModalInterpretability.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Core.Modality.instBEqModalInterpretability : BEq ModalInterpretability

Equations

• Core.Modality.instBEqModalInterpretability = { beq := Core.Modality.instBEqModalInterpretability.beq }

@[implicit_reducible]

instance Core.Modality.instInhabitedModalInterpretability : Inhabited ModalInterpretability

Equations

• Core.Modality.instInhabitedModalInterpretability = { default := Core.Modality.instInhabitedModalInterpretability.default }

def Core.Modality.instInhabitedModalInterpretability.default : ModalInterpretability

Equations

• Core.Modality.instInhabitedModalInterpretability.default = Core.Modality.ModalInterpretability.interpretable

structure Core.Modality.ModalFeature : Type

A modal feature: force (∃/∀) paired with interpretability (i/u).

@cite{zeijlstra-2007}: every modal element carries a feature from this four-cell space: [i∃-MOD], [u∃-MOD], [i∀-MOD], [u∀-MOD].

• force : ModalForce
• interp : ModalInterpretability

def Core.Modality.instDecidableEqModalFeature.decEq (x✝ x✝¹ : ModalFeature) : Decidable (x✝ = x✝¹)

Equations

• Core.Modality.instDecidableEqModalFeature.decEq { force := a, interp := a_1 } { force := b, interp := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Modality.instDecidableEqModalFeature : DecidableEq ModalFeature

Equations

• Core.Modality.instDecidableEqModalFeature = Core.Modality.instDecidableEqModalFeature.decEq

def Core.Modality.instReprModalFeature.repr : ModalFeature → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Modality.instReprModalFeature : Repr ModalFeature

Equations

• Core.Modality.instReprModalFeature = { reprPrec := Core.Modality.instReprModalFeature.repr }

@[implicit_reducible]

instance Core.Modality.instBEqModalFeature : BEq ModalFeature

Equations

• Core.Modality.instBEqModalFeature = { beq := Core.Modality.instBEqModalFeature.beq }

def Core.Modality.instBEqModalFeature.beq : ModalFeature → ModalFeature → Bool

Equations

• Core.Modality.instBEqModalFeature.beq { force := a, interp := a_1 } { force := b, interp := b_1 } = (a == b && a_1 == b_1)
• Core.Modality.instBEqModalFeature.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Core.Modality.instInhabitedModalFeature : Inhabited ModalFeature

Equations

• Core.Modality.instInhabitedModalFeature = { default := Core.Modality.instInhabitedModalFeature.default }

def Core.Modality.instInhabitedModalFeature.default : ModalFeature

Equations

• Core.Modality.instInhabitedModalFeature.default = { force := default, interp := default }

def Core.Modality.ModalFeature.checks (checker checked : ModalFeature) : Bool

Feature checking: an interpretable feature checks a c-commanded uninterpretable feature of matching concord class.

@cite{zeijlstra-2007}: u-features must be c-commanded by a matching i-feature to be licensed. The match is by concord class (necessity and weak necessity both count as ∀-type).

Equations

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

@[reducible, inline]

abbrev Core.Modality.ModalForce.negatedConcordForce : ModalForce → ModalForce

Negation flips the relevant modal force for concord purposes.

@cite{ciardelli-guerrini-2026} (UNVERIFIED §4.2): modal concord across negation requires opposite forces — ALLOWi∃ is well-formed because ¬∀ = ∃, but *DEMANDi∀ is ill-formed (same force).

Derived from ModalForce.dual — negation over a modal operator yields its dual force (¬□ = ◇, ¬◇ = □).

Equations

• Core.Modality.ModalForce.negatedConcordForce = Core.Modality.ModalForce.dual

def Core.Modality.ModalFeature.checksAcrossNegation (checker checked : ModalFeature) : Bool

Feature checking across negation: an interpretable feature checks a negated uninterpretable feature when their forces are duals.

ALLOWi∃: ∃ checks negated ∀ (= ∃) ✓ *DEMANDi∀: ∀ checks negated ∀ (= ∃) ✗

Equations

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

inductive Core.Modality.ModalDecomposition : Type

Whether a modal meaning decomposes into independent force and flavor dimensions or is a unitary, non-decomposable operator.

@cite{werner-2006}, @cite{condoravdi-2002}: some modals resist the standard force × flavor decomposition. "Will" and other temporal-modal elements do not factor cleanly into a modal force and a conversational background flavor.

• decomposable : ModalDecomposition
• unitary : ModalDecomposition

@[implicit_reducible]

instance Core.Modality.instDecidableEqModalDecomposition : DecidableEq ModalDecomposition

Equations

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

def Core.Modality.instReprModalDecomposition.repr : ModalDecomposition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Modality.instReprModalDecomposition : Repr ModalDecomposition

Equations

• Core.Modality.instReprModalDecomposition = { reprPrec := Core.Modality.instReprModalDecomposition.repr }

def Core.Modality.ModalItem.decomposition (m : ModalItem) : ModalDecomposition

Classify a modal item by whether its meaning set equals the Cartesian product of its force and flavor projections. A modal is decomposable iff every combination of its attested forces and flavors is also attested — the two dimensions are independent.

Equations

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

def Core.Modality.ModalItem.isUnitary (m : ModalItem) : Bool

A modal item is unitary (non-decomposable into force × flavor).

Equations

• m.isUnitary = (m.decomposition == Core.Modality.ModalDecomposition.unitary)

theorem Core.Modality.singleton_decomposable (ff : ForceFlavor) : { form := "m", meaning := [ff] }.isUnitary = false

Singleton meanings are trivially decomposable: a modal with exactly one force-flavor pair always satisfies IFF.

theorem Core.Modality.cross_cutting_is_unitary : { form := "m", meaning := [{ force := ModalForce.necessity, flavor := ModalFlavor.epistemic }, { force := ModalForce.possibility, flavor := ModalFlavor.deontic }] }.isUnitary = true

A non-IFF meaning is unitary: necessity-epistemic + possibility-deontic without the cross-product pairs.

inductive Core.Modality.ProjectionMode : Type

Mode of projecting conversational backgrounds. @cite{kratzer-2012} replaces the traditional epistemic/circumstantial dichotomy with a distinction between factual and content modes:

• Factual: the modal quantifies over worlds containing a counterpart of some actual-world situation or body of evidence. The actual world is always among the accessible worlds (w ∈ ∩f(w)).
• Content: the modal quantifies over worlds compatible with the propositional content of some information source (rumour, report, sensory evidence). The actual world need not be accessible — the speaker can disbelieve the content.

@cite{matthewson-2016} (UNVERIFIED Table 18.2 reference).

The old circumstantial class is entirely factual. The old epistemic class splits: factual epistemics (inferential, based on situation counterparts) vs. content epistemics (reportative, based on propositional content).

• factual : ProjectionMode
• content : ProjectionMode

@[implicit_reducible]

instance Core.Modality.instDecidableEqProjectionMode : DecidableEq ProjectionMode

Equations

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

@[implicit_reducible]

instance Core.Modality.instReprProjectionMode : Repr ProjectionMode

Equations

• Core.Modality.instReprProjectionMode = { reprPrec := Core.Modality.instReprProjectionMode.repr }

def Core.Modality.instReprProjectionMode.repr : ProjectionMode → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Modality.instBEqProjectionMode : BEq ProjectionMode

Equations

• Core.Modality.instBEqProjectionMode = { beq := Core.Modality.instBEqProjectionMode.beq }

def Core.Modality.instBEqProjectionMode.beq : ProjectionMode → ProjectionMode → Bool

Equations

• Core.Modality.instBEqProjectionMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Core.Modality.instInhabitedProjectionMode : Inhabited ProjectionMode

Equations

• Core.Modality.instInhabitedProjectionMode = { default := Core.Modality.instInhabitedProjectionMode.default }

def Core.Modality.instInhabitedProjectionMode.default : ProjectionMode

Equations

• Core.Modality.instInhabitedProjectionMode.default = Core.Modality.ProjectionMode.factual

@[implicit_reducible]

instance Core.Modality.instToStringProjectionMode : ToString ProjectionMode

Equations

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

inductive Core.Modality.BackgroundClass : Type

Three-way classification of conversational backgrounds. @cite{matthewson-2016} (UNVERIFIED Table 18.3 reference). Refines the traditional epistemic/circumstantial binary into a three-way split based on projection mode and whether information source is encoded.

• factualCircumstantial: factual mode, no information source encoded. Covers deontic, bouletic, teleological, ability, pure circumstantial. English: can (circumstantial), German: können.
• factualEvidential: factual mode, information source encoded. The speaker cannot disbelieve the prejacent. St'át'imcets: k'a (inferential), English: must (indirect evidence).
• contentEvidential: content mode, information source encoded. The speaker can disbelieve the prejacent. St'át'imcets: lákw7a (sensory non-visual), German: sollen.

• factualCircumstantial : BackgroundClass
• factualEvidential : BackgroundClass
• contentEvidential : BackgroundClass

@[implicit_reducible]

instance Core.Modality.instDecidableEqBackgroundClass : DecidableEq BackgroundClass

Equations

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

@[implicit_reducible]

instance Core.Modality.instReprBackgroundClass : Repr BackgroundClass

Equations

• Core.Modality.instReprBackgroundClass = { reprPrec := Core.Modality.instReprBackgroundClass.repr }

def Core.Modality.instReprBackgroundClass.repr : BackgroundClass → ℕ → Std.Format

Equations

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

def Core.Modality.instBEqBackgroundClass.beq : BackgroundClass → BackgroundClass → Bool

Equations

• Core.Modality.instBEqBackgroundClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Core.Modality.instBEqBackgroundClass : BEq BackgroundClass

Equations

• Core.Modality.instBEqBackgroundClass = { beq := Core.Modality.instBEqBackgroundClass.beq }

def Core.Modality.instInhabitedBackgroundClass.default : BackgroundClass

Equations

• Core.Modality.instInhabitedBackgroundClass.default = Core.Modality.BackgroundClass.factualCircumstantial

@[implicit_reducible]

instance Core.Modality.instInhabitedBackgroundClass : Inhabited BackgroundClass

Equations

• Core.Modality.instInhabitedBackgroundClass = { default := Core.Modality.instInhabitedBackgroundClass.default }

@[implicit_reducible]

instance Core.Modality.instToStringBackgroundClass : ToString BackgroundClass

Equations

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

def Core.Modality.BackgroundClass.projectionMode : BackgroundClass → ProjectionMode

The projection mode of each background class.

Equations

• Core.Modality.BackgroundClass.factualCircumstantial.projectionMode = Core.Modality.ProjectionMode.factual
• Core.Modality.BackgroundClass.factualEvidential.projectionMode = Core.Modality.ProjectionMode.factual
• Core.Modality.BackgroundClass.contentEvidential.projectionMode = Core.Modality.ProjectionMode.content

def Core.Modality.BackgroundClass.EncodesInfoSource (b : BackgroundClass) : Prop

Whether the background class encodes an information source.

Equations

• b.EncodesInfoSource = (b = Core.Modality.BackgroundClass.factualEvidential ∨ b = Core.Modality.BackgroundClass.contentEvidential)

@[implicit_reducible]

instance Core.Modality.instDecidablePredBackgroundClassEncodesInfoSource : DecidablePred BackgroundClass.EncodesInfoSource

Equations

• Core.Modality.instDecidablePredBackgroundClassEncodesInfoSource x✝ = Core.Modality.instDecidablePredBackgroundClassEncodesInfoSource._aux_1 x✝

def Core.Modality.BackgroundClass.AllowsSpeakerDisbelief (b : BackgroundClass) : Prop

Whether the speaker can disbelieve the prejacent under this class. Only content-mode backgrounds allow speaker disbelief — factual modes commit the speaker to the prejacent being compatible with reality.

Equations

• b.AllowsSpeakerDisbelief = (b = Core.Modality.BackgroundClass.contentEvidential)

@[implicit_reducible]

instance Core.Modality.instDecidablePredBackgroundClassAllowsSpeakerDisbelief : DecidablePred BackgroundClass.AllowsSpeakerDisbelief

Equations

• Core.Modality.instDecidablePredBackgroundClassAllowsSpeakerDisbelief x✝ = Core.Modality.instDecidablePredBackgroundClassAllowsSpeakerDisbelief._aux_1 x✝

def Core.Modality.BackgroundClass.traditionalFlavor : BackgroundClass → ModalFlavor

The traditional epistemic/circumstantial classification that the three-way split refines.

Equations

• Core.Modality.BackgroundClass.factualCircumstantial.traditionalFlavor = Core.Modality.ModalFlavor.circumstantial
• Core.Modality.BackgroundClass.factualEvidential.traditionalFlavor = Core.Modality.ModalFlavor.epistemic
• Core.Modality.BackgroundClass.contentEvidential.traditionalFlavor = Core.Modality.ModalFlavor.epistemic

theorem Core.Modality.circumstantial_always_factual : BackgroundClass.factualCircumstantial.projectionMode = ProjectionMode.factual

Traditional circumstantial modals are always factual.

theorem Core.Modality.content_encodes_info : BackgroundClass.contentEvidential.EncodesInfoSource

Content-mode backgrounds always encode an information source.

theorem Core.Modality.factual_epistemic_no_disbelief : ¬BackgroundClass.factualEvidential.AllowsSpeakerDisbelief

Speaker disbelief distinguishes the two epistemic subtypes.

theorem Core.Modality.content_epistemic_allows_disbelief : BackgroundClass.contentEvidential.AllowsSpeakerDisbelief

inductive Core.Modality.ForceAnalysis : Type

How a modal's quantificational force is determined. Distinguishes three mechanisms that the List ForceFlavor encoding conflates:

• fixed: The modal lexically specifies a single force value. English must (necessity), can (possibility).
• variableForce: The modal is semantically compatible with both necessity and possibility contexts without being ambiguous. Gitksan ima('a), gat (@cite{matthewson-2013}).
• strengthened: The modal has a fixed base force (typically possibility) but can receive strengthened readings in the absence of a contrasting dual. Nez Perce o'qa (@cite{deal-2011}): a possibility modal acceptable in necessity contexts because no contrasting necessity modal triggers scalar implicature.

• fixed : ModalForce → ForceAnalysis
• variableForce : ForceAnalysis
• strengthened : ModalForce → ForceAnalysis

@[implicit_reducible]

instance Core.Modality.instDecidableEqForceAnalysis : DecidableEq ForceAnalysis

Equations

• Core.Modality.instDecidableEqForceAnalysis = Core.Modality.instDecidableEqForceAnalysis.decEq

def Core.Modality.instDecidableEqForceAnalysis.decEq (x✝ x✝¹ : ForceAnalysis) : Decidable (x✝ = x✝¹)

Equations

• Core.Modality.instDecidableEqForceAnalysis.decEq (Core.Modality.ForceAnalysis.fixed a) (Core.Modality.ForceAnalysis.fixed b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Core.Modality.instDecidableEqForceAnalysis.decEq (Core.Modality.ForceAnalysis.fixed a) Core.Modality.ForceAnalysis.variableForce = isFalse ⋯
• Core.Modality.instDecidableEqForceAnalysis.decEq (Core.Modality.ForceAnalysis.fixed a) (Core.Modality.ForceAnalysis.strengthened a_1) = isFalse ⋯
• Core.Modality.instDecidableEqForceAnalysis.decEq Core.Modality.ForceAnalysis.variableForce (Core.Modality.ForceAnalysis.fixed a) = isFalse ⋯
• Core.Modality.instDecidableEqForceAnalysis.decEq Core.Modality.ForceAnalysis.variableForce Core.Modality.ForceAnalysis.variableForce = isTrue ⋯
• Core.Modality.instDecidableEqForceAnalysis.decEq Core.Modality.ForceAnalysis.variableForce (Core.Modality.ForceAnalysis.strengthened a) = isFalse ⋯
• Core.Modality.instDecidableEqForceAnalysis.decEq (Core.Modality.ForceAnalysis.strengthened a) (Core.Modality.ForceAnalysis.fixed a_1) = isFalse ⋯
• Core.Modality.instDecidableEqForceAnalysis.decEq (Core.Modality.ForceAnalysis.strengthened a) Core.Modality.ForceAnalysis.variableForce = isFalse ⋯
• Core.Modality.instDecidableEqForceAnalysis.decEq (Core.Modality.ForceAnalysis.strengthened a) (Core.Modality.ForceAnalysis.strengthened b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Core.Modality.instReprForceAnalysis.repr : ForceAnalysis → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Modality.instReprForceAnalysis : Repr ForceAnalysis

Equations

• Core.Modality.instReprForceAnalysis = { reprPrec := Core.Modality.instReprForceAnalysis.repr }

def Core.Modality.ForceAnalysis.AdmitsNecessity (a : ForceAnalysis) : Prop

Whether the modal has a necessity reading (semantically or pragmatically).

Equations

• a.AdmitsNecessity = (a ≠ Core.Modality.ForceAnalysis.fixed Core.Modality.ModalForce.possibility)

@[implicit_reducible]

instance Core.Modality.instDecidablePredForceAnalysisAdmitsNecessity : DecidablePred ForceAnalysis.AdmitsNecessity

Equations

• Core.Modality.instDecidablePredForceAnalysisAdmitsNecessity x✝ = Core.Modality.instDecidablePredForceAnalysisAdmitsNecessity._aux_1 x✝

def Core.Modality.ForceAnalysis.AdmitsPossibility (a : ForceAnalysis) : Prop

Whether the modal has a possibility reading.

Equations

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

@[implicit_reducible]

instance Core.Modality.instDecidablePredForceAnalysisAdmitsPossibility : DecidablePred ForceAnalysis.AdmitsPossibility

Equations

• Core.Modality.instDecidablePredForceAnalysisAdmitsPossibility x✝ = Core.Modality.instDecidablePredForceAnalysisAdmitsPossibility._aux_1 x✝

def Core.Modality.ForceAnalysis.HasDual : ForceAnalysis → Prop

Whether the modal has a lexical dual (contrasting force partner). @cite{matthewson-2016} (UNVERIFIED §18.3.2): modals without duals do not come in necessity–possibility pairs.

Equations

• (Core.Modality.ForceAnalysis.fixed a).HasDual = True
• Core.Modality.ForceAnalysis.variableForce.HasDual = False
• (Core.Modality.ForceAnalysis.strengthened a).HasDual = False

@[implicit_reducible]

instance Core.Modality.instDecidablePredForceAnalysisHasDual : DecidablePred ForceAnalysis.HasDual

Equations

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