def Semantics.Modality.groundWet : Proposition

Proposition: the ground is wet. True at w0, w1, w3; false at w2.

Equations

• Semantics.Modality.groundWet Core.Proposition.World4.w0 = true
• Semantics.Modality.groundWet Core.Proposition.World4.w1 = true
• Semantics.Modality.groundWet Core.Proposition.World4.w2 = false
• Semantics.Modality.groundWet Core.Proposition.World4.w3 = true

def Semantics.Modality.concreteEpistemicBase : Kratzer.ModalBase

Equations

• Semantics.Modality.concreteEpistemicBase x✝ = [Semantics.Modality.groundWet]

def Semantics.Modality.concreteEpistemicParams : Kratzer.KratzerParams

Equations

• Semantics.Modality.concreteEpistemicParams = { base := Semantics.Modality.concreteEpistemicBase, ordering := Semantics.Modality.Kratzer.emptyBackground }

def Semantics.Modality.KratzerEpistemic : ModalTheory

Equations

• Semantics.Modality.KratzerEpistemic = Semantics.Modality.Kratzer.KratzerTheory Semantics.Modality.concreteEpistemicParams

def Semantics.Modality.concreteCircumstantialBase : Kratzer.ModalBase

Equations

• Semantics.Modality.concreteCircumstantialBase x✝ = []

def Semantics.Modality.concreteDeonticOrdering : Kratzer.OrderingSource

Equations

• Semantics.Modality.concreteDeonticOrdering x✝ = [Semantics.Modality.johnHome]

def Semantics.Modality.concreteDeonticParams : Kratzer.KratzerParams

Equations

• Semantics.Modality.concreteDeonticParams = { base := Semantics.Modality.concreteCircumstantialBase, ordering := Semantics.Modality.concreteDeonticOrdering }

def Semantics.Modality.KratzerDeontic : ModalTheory

Equations

• Semantics.Modality.KratzerDeontic = Semantics.Modality.Kratzer.KratzerTheory Semantics.Modality.concreteDeonticParams

def Semantics.Modality.theoriesAgreeAt (T₁ T₂ : ModalTheory) (f : ModalForce) (p : Proposition) (w : Attitudes.Intensional.World) : Bool

Do two theories agree on modal force f for proposition p at world w?

Equations

• Semantics.Modality.theoriesAgreeAt T₁ T₂ f p w = (T₁.eval f p w == T₂.eval f p w)

def Semantics.Modality.theoriesAgreeOn (T₁ T₂ : ModalTheory) (f : ModalForce) (p : Proposition) : Bool

Do two theories agree on modal force f for proposition p across all worlds?

Equations

• Semantics.Modality.theoriesAgreeOn T₁ T₂ f p = Semantics.Modality.allWorlds'.all fun (w : Semantics.Attitudes.Intensional.World) => Semantics.Modality.theoriesAgreeAt T₁ T₂ f p w

def Semantics.Modality.divergingWorlds (T₁ T₂ : ModalTheory) (f : ModalForce) (p : Proposition) : List Attitudes.Intensional.World

Find worlds where two theories diverge.

Equations

• Semantics.Modality.divergingWorlds T₁ T₂ f p = List.filter (fun (w : Semantics.Attitudes.Intensional.World) => !Semantics.Modality.theoriesAgreeAt T₁ T₂ f p w) Semantics.Modality.allWorlds'

def Semantics.Modality.theoriesAgreeOnProposition (T₁ T₂ : ModalTheory) (p : Proposition) : Bool

Do two theories agree on all modal forces for proposition p?

Equations

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

theorem Semantics.Modality.minimal_kratzer_equals_universal_simple_necessity (w : Attitudes.Intensional.World) : Kratzer.KratzerMinimal.eval Core.Modality.ModalForce.necessity raining w = SimpleUniversal.eval Core.Modality.ModalForce.necessity raining w

Minimal Kratzer = Universal Simple for necessity on raining.

theorem Semantics.Modality.minimal_kratzer_equals_universal_simple_possibility (w : Attitudes.Intensional.World) : Kratzer.KratzerMinimal.eval Core.Modality.ModalForce.possibility raining w = SimpleUniversal.eval Core.Modality.ModalForce.possibility raining w

theorem Semantics.Modality.agree_on_trivially_true : theoriesAgreeOnProposition Kratzer.KratzerMinimal SimpleUniversal triviallyTrue = true

Agreement on trivially true.

theorem Semantics.Modality.agree_on_trivially_false : theoriesAgreeOnProposition Kratzer.KratzerMinimal SimpleUniversal triviallyFalse = true

Agreement on trivially false.

theorem Semantics.Modality.epistemic_vs_minimal_differ : ∃ (p : Proposition) (w : Attitudes.Intensional.World), KratzerEpistemic.eval Core.Modality.ModalForce.necessity p w ≠ Kratzer.KratzerMinimal.eval Core.Modality.ModalForce.necessity p w

Epistemic and minimal Kratzer differ on some proposition and world.

theorem Semantics.Modality.kratzer_context_dependence : KratzerEpistemic.eval Core.Modality.ModalForce.necessity groundWet Core.Proposition.World4.w0 = true ∧ Kratzer.KratzerMinimal.eval Core.Modality.ModalForce.necessity groundWet Core.Proposition.World4.w0 = false

Different conversational backgrounds yield different truth values.

theorem Semantics.Modality.both_satisfy_duality (params : Kratzer.KratzerParams) (R : Attitudes.Intensional.World → Attitudes.Intensional.World → Bool) (p : Proposition) (w : Attitudes.Intensional.World) : (Kratzer.KratzerTheory params).dualityHolds p w = true ∧ (Simple R).dualityHolds p w = true

Both Kratzer and Simple satisfy duality.

theorem Semantics.Modality.agree_on_trivially_true_necessity : theoriesAgreeOn Kratzer.KratzerMinimal SimpleUniversal Core.Modality.ModalForce.necessity triviallyTrue = true

Agreement: Minimal Kratzer and Universal Simple agree on necessity for trivially true.

theorem Semantics.Modality.agree_on_trivially_true_possibility : theoriesAgreeOn Kratzer.KratzerMinimal SimpleUniversal Core.Modality.ModalForce.possibility triviallyTrue = true

Agreement: Both agree on possibility for trivially true.

theorem Semantics.Modality.agree_on_trivially_false_necessity : theoriesAgreeOn Kratzer.KratzerMinimal SimpleUniversal Core.Modality.ModalForce.necessity triviallyFalse = true

Agreement: Both agree on necessity for trivially false.