Modal Base Kind

@cite{klecha-2016}

Classification of modal bases by their temporal character. This is the foundational type underlying the distinction between doxastic (DOX) and circumstantial (CIR) modal base pronouns.

DOX returns actual histories (ending at eval time) → past/present orientation. CIR returns future histories (departing from eval time) → future orientation.

This type lives in Core because it is referenced by both theory-layer modules (Modality.TemporalConstraint, Tense.ModalTense) and by phenomena-layer study files. It depends only on GramTense from Core.

inductive Core.Modality.ModalBaseKind : Type

Classification of modal base temporal character. @cite{klecha-2016} (35): DOX returns actual histories 𝒜_t, CIR returns future histories ℱ_t.

• doxastic : ModalBaseKind

  Doxastic: accessible histories are actual (end at eval time). Yields past/present temporal orientation.

• circumstantial : ModalBaseKind

  Circumstantial: accessible histories are future (depart from eval time). Yields future temporal orientation.

@[implicit_reducible]

instance Core.Modality.instDecidableEqModalBaseKind : DecidableEq ModalBaseKind

Equations

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

def Core.Modality.instReprModalBaseKind.repr : ModalBaseKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Modality.instReprModalBaseKind : Repr ModalBaseKind

Equations

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

def Core.Modality.ModalBaseKind.permitsOrientation : ModalBaseKind → Time.Tense.GramTense → Bool

The temporal orientation permitted by a modal base kind. @cite{klecha-2016} Table 1 and §1.2.

Equations

• Core.Modality.ModalBaseKind.doxastic.permitsOrientation Core.Time.Tense.GramTense.past = true
• Core.Modality.ModalBaseKind.doxastic.permitsOrientation Core.Time.Tense.GramTense.present = true
• Core.Modality.ModalBaseKind.doxastic.permitsOrientation Core.Time.Tense.GramTense.nonpast = true
• Core.Modality.ModalBaseKind.doxastic.permitsOrientation Core.Time.Tense.GramTense.future = false
• Core.Modality.ModalBaseKind.circumstantial.permitsOrientation Core.Time.Tense.GramTense.future = true
• Core.Modality.ModalBaseKind.circumstantial.permitsOrientation Core.Time.Tense.GramTense.nonpast = true
• Core.Modality.ModalBaseKind.circumstantial.permitsOrientation Core.Time.Tense.GramTense.past = false
• Core.Modality.ModalBaseKind.circumstantial.permitsOrientation Core.Time.Tense.GramTense.present = false

theorem Core.Modality.ModalBaseKind.dox_blocks_future : doxastic.permitsOrientation Time.Tense.GramTense.future = false

Doxastic modal bases block future orientation (the ULC).

theorem Core.Modality.ModalBaseKind.cir_permits_future : circumstantial.permitsOrientation Time.Tense.GramTense.future = true

Circumstantial modal bases permit future orientation.

theorem Core.Modality.ModalBaseKind.upper_limit_from_dox : doxastic.permitsOrientation Time.Tense.GramTense.past = true ∧ doxastic.permitsOrientation Time.Tense.GramTense.present = true ∧ doxastic.permitsOrientation Time.Tense.GramTense.future = false

The upper limit is derived from doxastic temporal character: DOX blocks future, permits past and present.