Documentation

Linglib.Phenomena.FreeChoice.Worlds

Power-set-of-atoms world models for free-choice scenarios #

The standard small modal-logic models used to demonstrate free-choice inference. A PowerSet2World enumerates the 2² = 4 truth assignments to two atoms — Aloni 2022 Figure 1 (w_∅, w_a, w_b, w_ab).

This pattern is independently reinvented in Aloni2022.lean (as PermissionWorld over coffee/tea), Heim1992.lean (line 51, "4-world model with two binary dimensions"), Boylan2023.lean (line 570), Roberts2023.lean (line 301). Hoisting it here lets all of those consume one definition.

The holds helper takes a typed FCAtom rather than a String, so typos are caught by the compiler rather than silently producing false.

source
inductive Phenomena.FreeChoice.PowerSet2World :
Type

Power-set-of-{a,b}: the 4 truth assignments to two propositional atoms.

Names follow Aloni 2022 Figure 1 (w_∅, w_a, w_b, w_ab):

Instances For
    source
    @[implicit_reducible]
    instance Phenomena.FreeChoice.instDecidableEqPowerSet2World :
    DecidableEq PowerSet2World
    Equations
    source
    def Phenomena.FreeChoice.instReprPowerSet2World.repr :
    PowerSet2World → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Phenomena.FreeChoice.instReprPowerSet2World :
      Repr PowerSet2World
      Equations
      source
      @[implicit_reducible]
      instance Phenomena.FreeChoice.instFintypePowerSet2World :
      Fintype PowerSet2World
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Phenomena.FreeChoice.PowerSet2World.holds :
      PowerSet2World → FCAtom → Bool

      Truth-table for the two-atom power set. The third atom (c) is unsatisfiable in this baseline 4-world model — embedded scenarios needing c should use a larger world type.

      Equations
      Instances For
        source
        @[reducible, inline]
        abbrev Phenomena.FreeChoice.PowerSet2World.satisfies :
        PowerSet2World → FCAtom → Bool

        Synonym used by Studies that prefer the predicate spelling.

        Equations
        Instances For