Docs / Semantics / Modality / DomainSemantics

Domain semantics

import Linglib.Semantics.Modality.DomainSemantics · namespace DomainSemantics

Domain semantics evaluates a sentence at an index pairing a world with an information state, a set of worlds over which epistemic modals quantify: might φ is true when φ holds at some world of the state and must φ when it holds at every one, whatever the world of evaluation. A state accepts a sentence when the sentence is true, relative to the state, at each of its worlds. A nonepistemic sentence is accepted by the states that entail it, must φ by the states that accept φ, and might φ by the states with a world verifying φ and by the absurd state.

Consequence preserves truth at every index (standard), truth at the diagonal indices, those whose world lies in the state (diagonal), or acceptance (informational).

Main definitions

DomainSemantics.Sentence W: sentences, a Boolean algebra pointwise.
Sentence.ofProp, Sentence.might, Sentence.must: nonepistemic sentences and the modals.
Sentence.AcceptedIn: acceptance in an information state.
StandardConsequence, DiagonalConsequence, InformationalConsequence.

Main statements

Sentence.acceptedIn_must_iff: must φ is accepted exactly where φ is.
Sentence.acceptedIn_might_iff: might φ is accepted by the absurd state and by the states with a world verifying φ.
informationalConsequence_singleton_iff: informational consequence from one premise is inclusion of the accepting states.

Implementation notes

The context of an index is fixed, so a sentence is a function of the information state and the world.

References

Yalcin 2007, Epistemic Modals formalized

Declarations

A sentence, its context fixed, is true or false at an information state and a world.

@[reducible, inline] abbrev Sentence L50–51

(W : Type u_2) :

Type u_2

Sentence W = (Set W → W → Prop)

Used by Sentence.ofProp, Sentence.might, Sentence.must, Sentence.AcceptedIn, Sentence.might_might, Sentence.must_eq_compl_might_compl, Sentence.acceptedIn_empty, Sentence.acceptedIn_must_iff, Sentence.acceptedIn_might_iff, StandardConsequence, DiagonalConsequence, InformationalConsequence, StandardConsequence.diagonalConsequence, informationalConsequence_singleton_iff

Used in AnandHacquard2013, EgreRossiSprenger2026b, KlinedinstRothschild2012, Rudin2025a, Yalcin2007

A nonepistemic sentence places a condition on the world alone.

def Sentence.ofProp L57–58

{W : Type u_1} (p : Set W) :

Sentence.ofProp p x✝ w = (w ∈ p)

Built from

Used by Sentence.ofProp_empty, Sentence.acceptedIn_ofProp_iff

Used in AnandHacquard2013, EgreRossiSprenger2026b, KlinedinstRothschild2012, Rudin2025a, Yalcin2007

might φ is true when φ holds at some world of the state.

def Sentence.might L60–61

{W : Type u_1} (φ : Sentence W) :

φ.might s x✝ = ∃ (w' : W), w' ∈ s ∧ φ s w'

Built from

Used by Sentence.might_might, Sentence.must_eq_compl_might_compl, Sentence.acceptedIn_might_iff

Used in AnandHacquard2013, EgreRossiSprenger2026b, KlinedinstRothschild2012, Rudin2025a, Yalcin2007

must φ is true when φ holds at every world of the state.

def Sentence.must L63–64

{W : Type u_1} (φ : Sentence W) :

φ.must s x✝ = ∀ (w' : W), w' ∈ s → φ s w'

Built from

Used by Sentence.must_eq_compl_might_compl, Sentence.acceptedIn_must_iff

Used in AnandHacquard2013, EgreRossiSprenger2026b, KlinedinstRothschild2012, Rudin2025a, Yalcin2007

A state accepts a sentence when the sentence is true, relative to the state, at each of its worlds.

def Sentence.AcceptedIn L66–68

{W : Type u_1} (φ : Sentence W) (s : Set W) :

φ.AcceptedIn s = ∀ (w : W), w ∈ s → φ s w

Built from

Used by Sentence.acceptedIn_empty, Sentence.acceptedIn_ofProp_iff, Sentence.acceptedIn_must_iff, Sentence.acceptedIn_might_iff, InformationalConsequence, informationalConsequence_singleton_iff

Used in AnandHacquard2013, EgreRossiSprenger2026b, Rudin2025a, Yalcin2007

theorem Sentence.acceptedIn_must_iff L83–84

{W : Type u_1} (φ : Sentence W) {s : Set W} :

φ.must.AcceptedIn s ↔ φ.AcceptedIn s

Built from , ,

theorem Sentence.acceptedIn_might_iff L86–89

{W : Type u_1} (φ : Sentence W) {s : Set W} :

φ.might.AcceptedIn s ↔ s = ∅ ∨ ∃ (w : W), w ∈ s ∧ φ s w

Built from , ,

Standard consequence preserves truth at every index.

def StandardConsequence L93–95

{W : Type u_1} (Γ : List (Sentence W)) (φ : Sentence W) :

StandardConsequence Γ φ = ∀ (s : Set W) (w : W), (∀ (γ : Sentence W), γ ∈ Γ → γ s w) → φ s w

Built from

Used by StandardConsequence.diagonalConsequence

Used in KlinedinstRothschild2012

Diagonal consequence preserves truth at the diagonal indices, those whose world lies in the information state.

def DiagonalConsequence L97–100

{W : Type u_1} (Γ : List (Sentence W)) (φ : Sentence W) :

DiagonalConsequence Γ φ = ∀ (s : Set W) (w : W), w ∈ s → (∀ (γ : Sentence W), γ ∈ Γ → γ s w) → φ s w

Built from

Used by StandardConsequence.diagonalConsequence

Used in Yalcin2007

Informational consequence preserves acceptance.

def InformationalConsequence L102–104

{W : Type u_1} (Γ : List (Sentence W)) (φ : Sentence W) :

InformationalConsequence Γ φ = ∀ (s : Set W), (∀ (γ : Sentence W), γ ∈ Γ → γ.AcceptedIn s) → φ.AcceptedIn s

Built from ,

Used by informationalConsequence_singleton_iff

Used in Rudin2025a, Yalcin2007

theorem informationalConsequence_singleton_iff L112–114

{W : Type u_1} {φ ψ : Sentence W} :

InformationalConsequence [φ] ψ ↔ ∀ (s : Set W), φ.AcceptedIn s → ψ.AcceptedIn s

Built from , ,