unicode_fol_kit.semantics.conditional

Counterfactual conditionals — Lewis / Stalnaker sphere semantics.

The material conditional gets counterfactuals wrong: “if kangaroos had no tails they would topple over” is not made true by kangaroos having tails. Counterfactuals A □→ B (“if A were the case, B would be”) are evaluated over a similarity ordering of worlds: from the actual world w you look at the closest worlds where A holds and check that B holds throughout them.

This module uses Lewis’s system of spheres: each world w carries a nested sequence of sets of worlds $_w$ (innermost first, w in the innermost), read as “increasingly distant neighbourhoods”. The truth condition (finite version):

w ⊨ A □→ B   iff   no sphere of w contains an A-world (vacuously true),
                   or, for the smallest sphere S that does, every A-world in S is a B-world.

The “might” counterfactual is the dual A ◇→ B ≡ ¬(A □→ ¬B). Antecedents and consequents are ordinary propositional formulas (atoms, ¬ ∧ ∨ → ↔). With a single innermost sphere {closest A-world} this is Stalnaker’s semantics; with ties it is Lewis’s.

Public API: CounterfactualModel, would(), might().

Functions

might(model, world, antecedent, consequent)

Return whether world ⊨ antecedent ◇→ consequent — the dual ¬(A □→ ¬B).

would(model, world, antecedent, consequent)

Return whether world ⊨ antecedent □→ consequent (Lewis "would" counterfactual).

Classes

CounterfactualModel(worlds, valuation, spheres)

A Lewis sphere model over a set of worlds.
class unicode_fol_kit.semantics.conditional.CounterfactualModel(worlds, valuation, spheres)[source]

Bases: object

A Lewis sphere model over a set of worlds.

valuation maps each world to the set of atom keys (atom.to_unicode_str()) true there. spheres maps each world w to its nested system of spheres — a list of frozensets ordered innermost (closest) first, each a superset of the previous, with w in the first. A world omitted from spheres is taken to have the single sphere {w}.

Parameters:
worlds: Tuple[Any, ...]
valuation: Dict[Any, FrozenSet[str]]
spheres: Dict[Any, List[FrozenSet[Any]]]
sphere_system(world)[source]

The nested spheres around world (default [{world}]).

Parameters:

world (Any)

Return type:

List[FrozenSet[Any]]

unicode_fol_kit.semantics.conditional.would(model, world, antecedent, consequent)[source]

Return whether world ⊨ antecedent □→ consequent (Lewis “would” counterfactual).

Vacuously true if no sphere of world holds an antecedent-world; otherwise the consequent must hold at every antecedent-world of the smallest antecedent-permitting sphere.

Parameters:
Return type:

bool

unicode_fol_kit.semantics.conditional.might(model, world, antecedent, consequent)[source]

Return whether world ⊨ antecedent ◇→ consequent — the dual ¬(A □→ ¬B).

Parameters:
Return type:

bool