Modal Base Kind

[Kle16]

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 is referenced by both theory-layer modules (Modality.TemporalConstraint, Tense.ModalTense) and by study files. It depends only on the Finset Ordering tense vocabulary (Core.Order, via Tense).

inductive Semantics.Modality.ModalBaseKind : Type

Classification of modal base temporal character. [Kle16] (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 Semantics.Modality.instDecidableEqModalBaseKind : DecidableEq ModalBaseKind

Equations

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

@[implicit_reducible]

instance Semantics.Modality.instReprModalBaseKind : Repr ModalBaseKind

Equations

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

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

Equations

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

def Semantics.Modality.ModalBaseKind.permitsOrientation : ModalBaseKind → Finset Ordering → Bool

The temporal orientation permitted by a modal base kind ([Kle16] Table 1, §1.2).

Derived, not stipulated. A doxastic base returns histories ending at the eval time, so it permits an orientation iff its comparison cell admits a non-future reference time (lt or eq ∈ the cell); a circumstantial base returns future-departing histories, so it permits an orientation iff the cell admits a future reference time (gt ∈ the cell). On the four named tenses this reproduces Klecha's table — including why DOX permits nonpast (it contains eq) and CIR permits its future part (it contains gt).

Equations

• Semantics.Modality.ModalBaseKind.doxastic.permitsOrientation x✝ = decide (Ordering.lt ∈ x✝ ∨ Ordering.eq ∈ x✝)
• Semantics.Modality.ModalBaseKind.circumstantial.permitsOrientation x✝ = decide (Ordering.gt ∈ x✝)

theorem Semantics.Modality.ModalBaseKind.dox_blocks_future : doxastic.permitsOrientation Tense.future = false

Doxastic modal bases block future orientation (the ULC).

theorem Semantics.Modality.ModalBaseKind.cir_permits_future : circumstantial.permitsOrientation Tense.future = true

Circumstantial modal bases permit future orientation.

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

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