Docs / Semantics / Modality / ComparativePossibility

Comparative possibility

import Linglib.Semantics.Modality.ComparativePossibility · namespace ComparativePossibility

Source

This file defines comparative possibility, the lifting of a relation on worlds to a relation on propositions. In Lewis's sense A is at least as possible as B when every B-world is dominated by some A-world. Kratzer's revised notion compares only the worlds in exactly one of the two propositions: A is at least as good a possibility as B unless some world of B \ A strictly dominates every world of A \ B. Over a total relation the revised notion is Lewis's notion applied to the two difference sets, and the strict part of Lewis's notion asks for a single A-world strictly dominating every B-world.

Main definitions

Main statements

References

Declarations

Lewis r A B says that A is at least as possible as B: every world of B is r-dominated by some world of A, that is B lies in the image of A under r.

def LewisL43–46
{α : Type u_1} (r : α → α → Prop) (A B : Set α) :
Prop
  • Lewis r A B = (B ⊆ SetRel.image {p : α × α | r p.1 p.2} A)

Instances ComparativeProbability.instIsLikelihoodMonoSetLewisOfRefl, ComparativeProbability.instIsNontrivialSetLewisOfNonempty

Used by lewis_iff, not_lewis_iff, lewis_empty, lewis_empty_left_iff, lewis_singleton_iff, lewis_of_subset, instReflSetLewis, Lewis.mono_left, Lewis.anti_right, Lewis.union, Lewis.trans, instIsTransSetLewis, instTotalSetLewis, asymmRel_lewis_iff, kratzer_iff_lewis_sdiff

Used in Logic/ComparativeProbability/WorldOrdering, Semantics/Modality/Necessity, Semantics/Modality/OrderingSemantics, AnandHacquard2013, HollidayIcard2013 and 4 more

Kratzer r A B says that A is at least as good a possibility as B in Kratzer's revised sense: no world of B \ A strictly dominates every world of A \ B (Kratzer 2012, p. 41).

def KratzerL48–51
{α : Type u_1} (r : α → α → Prop) (A B : Set α) :
Prop
  • Kratzer r A B = ¬∃ (b : α), b ∈ B \ A ∧ ∀ (a : α), a ∈ A \ B → AsymmRel r b a

Instances ComparativeProbability.instIsLikelihoodMonoSetKratzer, ComparativeProbability.instIsNontrivialSetKratzerOfNonempty, ComparativeProbability.instIsQualitativeAdditiveSetKratzer

Used by kratzer_iff, kratzer_sdiff_sdiff_iff, kratzer_of_subset, instReflSetKratzer, kratzer_univ_iff, kratzer_iff_lewis_sdiff, kratzer_union_of_disjoint

Used in Logic/ComparativeProbability/WorldOrdering, Kratzer2012, Lassiter2015

Lewis's comparative possibility

L57
L59–60
L62
L64–65
L67–68
L70–71
L73
L75–76
L78–79
L81–82
L84–88
L90
L92–96

Over a total relation, A is more possible than B exactly when some world of A strictly dominates every world of B.

theorem asymmRel_lewis_iffL98–106
{α : Type u_1} {r : α → α → Prop} {A B : Set α} [Std.Total r] :
AsymmRel (Lewis r) A B ↔ ∃ (a : α), a ∈ A ∧ ∀ (b : α), b ∈ B → AsymmRel r a b

Built from

Kratzer's revised comparative possibility

L110–111
L117
L119
L121–124

Over a total relation, A is at least as good a possibility as B exactly when A \ B is at least as possible as B \ A in Lewis's sense.

theorem kratzer_iff_lewis_sdiffL126–130
{α : Type u_1} {r : α → α → Prop} {A B : Set α} [Std.Total r] :
Kratzer r A B ↔ Lewis r (A \ B) (B \ A)

Built from ,

L132–140