Documentation

Linglib.Semantics.Modality.ModalTypes

Theory-neutral vocabulary for cross-linguistic modal typology: ModalForce, ModalFlavor, ForceFlavor, ModalItem, ConcordType, ModalDecomposition, and the modal-temporal axes TemporalPerspective / TemporalOrientation.

These types classify modal meanings along two independent dimensions — force (quantificational strength) and flavor (contextual source) — following [Kra81] and [IGST26].

Separated from 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. `Intensional` #

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

inductive Modality.ModalForce :

Modal force: necessity (□), weak necessity (□w), or possibility (◇). [vFI08], [AJ26].

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

[vFI08]: same ∀ quantifier as strong necessity but over a refined (smaller) set of best worlds (domain restriction).
Rubinstein (2014): fundamentally comparative meaning.
[AJ22]: non-quantificational (plural predication).

Weak necessity has no clean dual in this 3-point space: domain refinement weakens ∀ but strengthens ∃ ([AJ26]; UNVERIFIED §2.4).

necessity : ModalForce
weakNecessity : ModalForce
possibility : ModalForce

Instances For

@[instance_reducible]

instance Modality.instDecidableEqModalForce :

DecidableEq ModalForce

Equations

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

@[instance_reducible]

instance Modality.instReprModalForce :

Repr ModalForce

Equations

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

def Modality.instReprModalForce.repr :

ModalForce → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Modality.instInhabitedModalForce :

Inhabited ModalForce

Equations

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

instance Modality.instLawfulBEqModalForce :

LawfulBEq ModalForce

@[instance_reducible]

instance Modality.instToStringModalForce :

ToString ModalForce

Equations

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

def 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 [AJ26] (UNVERIFIED §2.4 quote) should be read as "no consensus dual", not as a structural impossibility.

Equations

Instances For

@[simp]

theorem Modality.ModalForce.dual_dual_necessity :

necessity.dual.dual = necessity

@[simp]

theorem Modality.ModalForce.dual_dual_possibility :

possibility.dual.dual = possibility

def Modality.ModalForce.all :

List ModalForce

All modal forces.

Equations

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

Instances For

def 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. [vFI08]: must φ → ought φ → can φ.

Equations

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

Instances For

theorem Modality.ModalForce.atLeastAsStrong_refl (f : ModalForce) :

f.atLeastAsStrong f = true

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

f₁.atLeastAsStrong f₃ = true

theorem Modality.ModalForce.necessity_strongest (f : ModalForce) :

necessity.atLeastAsStrong f = true

theorem Modality.ModalForce.possibility_weakest (f : ModalForce) :

f.atLeastAsStrong possibility = true

inductive Modality.ModalFlavor :

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 [Kra81]'s four-way classification.

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

Instances For

@[instance_reducible]

instance Modality.instDecidableEqModalFlavor :

DecidableEq ModalFlavor

Equations

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

@[instance_reducible]

instance Modality.instReprModalFlavor :

Repr ModalFlavor

Equations

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

def Modality.instReprModalFlavor.repr :

ModalFlavor → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Modality.instInhabitedModalFlavor :

Inhabited ModalFlavor

Equations

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

instance Modality.instLawfulBEqModalFlavor :

LawfulBEq ModalFlavor

@[instance_reducible]

instance Modality.instToStringModalFlavor :

ToString ModalFlavor

Equations

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

def Modality.ModalFlavor.all :

List ModalFlavor

All modal flavors.

Equations

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

Instances For

structure Modality.ForceFlavor :

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

Imel, Guo, & [IGST26]: 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 [AJ26]) and bouletic as a distinct flavor (following [Kra81]).

force : ModalForce
flavor : ModalFlavor

Instances For

@[instance_reducible]

instance Modality.instDecidableEqForceFlavor :

DecidableEq ForceFlavor

Equations

Modality.instDecidableEqForceFlavor = Modality.instDecidableEqForceFlavor.decEq

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

Decidable (x✝ = x✝¹)

Equations

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 ⋯

Instances For

@[instance_reducible]

instance Modality.instReprForceFlavor :

Repr ForceFlavor

Equations

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

def Modality.instReprForceFlavor.repr :

ForceFlavor → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Modality.instInhabitedForceFlavor :

Inhabited ForceFlavor

Equations

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

instance Modality.instLawfulBEqForceFlavor :

LawfulBEq ForceFlavor

@[instance_reducible]

instance Modality.instToStringForceFlavor :

ToString ForceFlavor

Equations

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

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

Instances For

theorem Modality.ForceFlavor.universe_length :

«universe».length = 12

def 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

Modality.ForceFlavor.cartesianProduct fos fls = List.flatMap (fun (fo : Modality.ModalForce) => List.map (fun (fl : Modality.ModalFlavor) => { force := fo, flavor := fl }) fls) fos

Instances For

structure Modality.ModalItem :

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

Instances For

def Modality.instReprModalItem.repr :

ModalItem → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Modality.instReprModalItem :

Equations

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

def Modality.instBEqModalItem.beq :

ModalItem → ModalItem → Bool

Equations

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))
Modality.instBEqModalItem.beq x✝¹ x✝ = false

Instances For

@[instance_reducible]

instance Modality.instBEqModalItem :

Equations

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

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

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

Equations

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

Instances For

@[instance_reducible]

instance Modality.instDecidableAreRegisterVariants (a b : ModalItem) :

Decidable (a.areRegisterVariants b)

Equations

Modality.instDecidableAreRegisterVariants a b = Modality.instDecidableAreRegisterVariants._aux_1 a b

inductive Modality.ConcordType :

Classification of concord phenomena by what logical type is doubled.

negation : ConcordType
modalNecessity : ConcordType
modalPossibility : ConcordType

Instances For

@[instance_reducible]

instance Modality.instDecidableEqConcordType :

DecidableEq ConcordType

Equations

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

@[instance_reducible]

instance Modality.instReprConcordType :

Repr ConcordType

Equations

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

def Modality.instReprConcordType.repr :

ConcordType → ℕ → Std.Format

Equations

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

Instances For

def 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

Instances For

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

Instances For

inductive Modality.ModalInterpretability :

Interpretability of a modal feature ([Zei07]).

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

[CG26] 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

Instances For

@[instance_reducible]

instance Modality.instDecidableEqModalInterpretability :

DecidableEq ModalInterpretability

Equations

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

def Modality.instReprModalInterpretability.repr :

ModalInterpretability → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Modality.instReprModalInterpretability :

Repr ModalInterpretability

Equations

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

def Modality.instBEqModalInterpretability.beq :

ModalInterpretability → ModalInterpretability → Bool

Equations

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

Instances For

@[instance_reducible]

instance Modality.instBEqModalInterpretability :

BEq ModalInterpretability

Equations

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

@[instance_reducible]

instance Modality.instInhabitedModalInterpretability :

Inhabited ModalInterpretability

Equations

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

structure Modality.ModalFeature :

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

[Zei07]: every modal element carries a feature from this four-cell space: [i∃-MOD], [u∃-MOD], [i∀-MOD], [u∀-MOD].

force : ModalForce
interp : ModalInterpretability

Instances For

@[instance_reducible]

instance Modality.instDecidableEqModalFeature :

DecidableEq ModalFeature

Equations

Modality.instDecidableEqModalFeature = Modality.instDecidableEqModalFeature.decEq

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

Decidable (x✝ = x✝¹)

Equations

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 ⋯

Instances For

@[instance_reducible]

instance Modality.instReprModalFeature :

Repr ModalFeature

Equations

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

def Modality.instReprModalFeature.repr :

ModalFeature → ℕ → Std.Format

Equations

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

Instances For

def Modality.instBEqModalFeature.beq :

ModalFeature → ModalFeature → Bool

Equations

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

Instances For

@[instance_reducible]

instance Modality.instBEqModalFeature :

BEq ModalFeature

Equations

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

@[instance_reducible]

instance Modality.instInhabitedModalFeature :

Inhabited ModalFeature

Equations

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

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

Bool

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

[Zei07]: 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.

Instances For

@[reducible, inline]

abbrev Modality.ModalForce.negatedConcordForce :

ModalForce → ModalForce

Negation flips the relevant modal force for concord purposes.

[CG26] (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

Modality.ModalForce.negatedConcordForce = Modality.ModalForce.dual

Instances For

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

Instances For

inductive Modality.ModalDecomposition :

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

[Wer06], [Con02]: 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

Instances For

@[instance_reducible]

instance Modality.instDecidableEqModalDecomposition :

DecidableEq ModalDecomposition

Equations

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

def Modality.instReprModalDecomposition.repr :

ModalDecomposition → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Modality.instReprModalDecomposition :

Repr ModalDecomposition

Equations

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

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

Instances For

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

Bool

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

Equations

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

Instances For

theorem 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 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 Modality.ProjectionMode :

Mode of projecting conversational backgrounds. [Kra12] 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.

[Mat16] (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

Instances For

@[instance_reducible]

instance Modality.instDecidableEqProjectionMode :

DecidableEq ProjectionMode

Equations

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

def Modality.instReprProjectionMode.repr :

ProjectionMode → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Modality.instReprProjectionMode :

Repr ProjectionMode

Equations

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

@[instance_reducible]

instance Modality.instBEqProjectionMode :

BEq ProjectionMode

Equations

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

def Modality.instBEqProjectionMode.beq :

ProjectionMode → ProjectionMode → Bool

Equations

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

Instances For

@[instance_reducible]

instance Modality.instInhabitedProjectionMode :

Inhabited ProjectionMode

Equations

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

@[instance_reducible]

instance Modality.instToStringProjectionMode :

ToString ProjectionMode

Equations

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

inductive Modality.BackgroundClass :

Three-way classification of conversational backgrounds. [Mat16] (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

Instances For

@[instance_reducible]

instance Modality.instDecidableEqBackgroundClass :

DecidableEq BackgroundClass

Equations

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

@[instance_reducible]

instance Modality.instReprBackgroundClass :

Repr BackgroundClass

Equations

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

def Modality.instReprBackgroundClass.repr :

BackgroundClass → ℕ → Std.Format

Equations

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

Instances For

def Modality.instBEqBackgroundClass.beq :

BackgroundClass → BackgroundClass → Bool

Equations

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

Instances For

@[instance_reducible]

instance Modality.instBEqBackgroundClass :

BEq BackgroundClass

Equations

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

@[instance_reducible]

instance Modality.instInhabitedBackgroundClass :

Inhabited BackgroundClass

Equations

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

@[instance_reducible]

instance Modality.instToStringBackgroundClass :

ToString BackgroundClass

Equations

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

def Modality.BackgroundClass.projectionMode :

BackgroundClass → ProjectionMode

The projection mode of each background class.

Equations

Instances For

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

Whether the background class encodes an information source.

Equations

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

Instances For

@[instance_reducible]

instance Modality.instDecidablePredBackgroundClassEncodesInfoSource :

DecidablePred BackgroundClass.EncodesInfoSource

Equations

Modality.instDecidablePredBackgroundClassEncodesInfoSource x✝ = Modality.instDecidablePredBackgroundClassEncodesInfoSource._aux_1 x✝

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

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 = Modality.BackgroundClass.contentEvidential)

Instances For

@[instance_reducible]

instance Modality.instDecidablePredBackgroundClassAllowsSpeakerDisbelief :

DecidablePred BackgroundClass.AllowsSpeakerDisbelief

Equations

Modality.instDecidablePredBackgroundClassAllowsSpeakerDisbelief x✝ = Modality.instDecidablePredBackgroundClassAllowsSpeakerDisbelief._aux_1 x✝

def Modality.BackgroundClass.traditionalFlavor :

BackgroundClass → ModalFlavor

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

Equations

Instances For

theorem Modality.circumstantial_always_factual :

BackgroundClass.factualCircumstantial.projectionMode = ProjectionMode.factual

Traditional circumstantial modals are always factual.

theorem Modality.content_encodes_info :

BackgroundClass.contentEvidential.EncodesInfoSource

Content-mode backgrounds always encode an information source.

theorem Modality.factual_epistemic_no_disbelief :

¬BackgroundClass.factualEvidential.AllowsSpeakerDisbelief

Speaker disbelief distinguishes the two epistemic subtypes.

theorem Modality.content_epistemic_allows_disbelief :

BackgroundClass.contentEvidential.AllowsSpeakerDisbelief

inductive Modality.ForceAnalysis :

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 ([Mat13]).
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 ([Dea11]): a possibility modal acceptable in necessity contexts because no contrasting necessity modal triggers scalar implicature.

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

Instances For

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

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[instance_reducible]

instance Modality.instDecidableEqForceAnalysis :

DecidableEq ForceAnalysis

Equations

Modality.instDecidableEqForceAnalysis = Modality.instDecidableEqForceAnalysis.decEq

@[instance_reducible]

instance Modality.instReprForceAnalysis :

Repr ForceAnalysis

Equations

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

def Modality.instReprForceAnalysis.repr :

ForceAnalysis → ℕ → Std.Format

Equations

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

Instances For

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

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

Equations

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

Instances For

@[instance_reducible]

instance Modality.instDecidablePredForceAnalysisAdmitsNecessity :

DecidablePred ForceAnalysis.AdmitsNecessity

Equations

Modality.instDecidablePredForceAnalysisAdmitsNecessity x✝ = Modality.instDecidablePredForceAnalysisAdmitsNecessity._aux_1 x✝

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

Whether the modal has a possibility reading.

Equations

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

Instances For

@[instance_reducible]

instance Modality.instDecidablePredForceAnalysisAdmitsPossibility :

DecidablePred ForceAnalysis.AdmitsPossibility

Equations

Modality.instDecidablePredForceAnalysisAdmitsPossibility x✝ = Modality.instDecidablePredForceAnalysisAdmitsPossibility._aux_1 x✝

def Modality.ForceAnalysis.HasDual :

ForceAnalysis → Prop

Whether the modal has a lexical dual (contrasting force partner). [Mat16] (UNVERIFIED §18.3.2): modals without duals do not come in necessity–possibility pairs.

Equations

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

Instances For

@[instance_reducible]

instance Modality.instDecidablePredForceAnalysisHasDual :

DecidablePred ForceAnalysis.HasDual

Equations

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

The two temporal axes of modal interpretation ([Con02] §2): the perspective is the time at which the modal base and ordering source are evaluated, the orientation the relation between the perspective time and the prejacent's time. [Con02] uses only the future/past orientations; the present cell goes unused there.

inductive Modality.TemporalPerspective :

Temporal perspective: the time at which a modal base / ordering source is evaluated.

present : TemporalPerspective
Modal base evaluated at the utterance time.
past : TemporalPerspective
Modal base evaluated at a prior time (e.g., via PERF > MODAL).

Instances For

@[instance_reducible]

instance Modality.instDecidableEqTemporalPerspective :

DecidableEq TemporalPerspective

Equations

Modality.instDecidableEqTemporalPerspective x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Modality.instReprTemporalPerspective.repr :

TemporalPerspective → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Modality.instReprTemporalPerspective :

Repr TemporalPerspective

Equations

Modality.instReprTemporalPerspective = { reprPrec := Modality.instReprTemporalPerspective.repr }

@[instance_reducible]

instance Modality.instBEqTemporalPerspective :

BEq TemporalPerspective

Equations

Modality.instBEqTemporalPerspective = { beq := Modality.instBEqTemporalPerspective.beq }

def Modality.instBEqTemporalPerspective.beq :

TemporalPerspective → TemporalPerspective → Bool

Equations

Modality.instBEqTemporalPerspective.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[instance_reducible]

instance Modality.instInhabitedTemporalPerspective :

Inhabited TemporalPerspective

Equations

Modality.instInhabitedTemporalPerspective = { default := Modality.instInhabitedTemporalPerspective.default }

inductive Modality.TemporalOrientation :

Temporal orientation: the temporal relation between the perspective time and the prejacent's instantiation time.

past : TemporalOrientation
Prejacent instantiated before the perspective time.
present : TemporalOrientation
Prejacent coincides with the perspective time.
future : TemporalOrientation
Prejacent instantiated at or after the perspective time.

Instances For

@[instance_reducible]

instance Modality.instDecidableEqTemporalOrientation :

DecidableEq TemporalOrientation

Equations

Modality.instDecidableEqTemporalOrientation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Modality.instReprTemporalOrientation.repr :

TemporalOrientation → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Modality.instReprTemporalOrientation :

Repr TemporalOrientation

Equations

Modality.instReprTemporalOrientation = { reprPrec := Modality.instReprTemporalOrientation.repr }

@[instance_reducible]

instance Modality.instBEqTemporalOrientation :

BEq TemporalOrientation

Equations

Modality.instBEqTemporalOrientation = { beq := Modality.instBEqTemporalOrientation.beq }

def Modality.instBEqTemporalOrientation.beq :

TemporalOrientation → TemporalOrientation → Bool

Equations

Modality.instBEqTemporalOrientation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[instance_reducible]

instance Modality.instInhabitedTemporalOrientation :

Inhabited TemporalOrientation

Equations

Modality.instInhabitedTemporalOrientation = { default := Modality.instInhabitedTemporalOrientation.default }