Documentation

Linglib.Phenomena.FreeChoice.Studies.Fox2007

Fox 2007: Free Choice via Recursive Exhaustification @cite{fox-2007} #

The original grammatical account of free-choice permission. Recursive application of the covert exhaustivity operator exh (Innocent Exclusion) over the Sauerland alternatives {◇(p∨q), ◇p, ◇q, ◇(p∧q)} derives the FC inference without Innocent Inclusion.

The five-world model below (ModalW) makes each ◇-formula correspond to which propositional situations are accessible from the evaluation world, so that the four Sauerland alternatives have non-trivial truth values and the IE algorithm has something to compute over.

source
inductive Phenomena.FreeChoice.Studies.Fox2007.ModalW :
Type

Modal worlds named by which ◇-propositions they make true.

Instances For
    source
    @[implicit_reducible]
    instance Phenomena.FreeChoice.Studies.Fox2007.instReprModalW :
    Repr ModalW
    Equations
    source
    def Phenomena.FreeChoice.Studies.Fox2007.instReprModalW.repr :
    ModalW → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Phenomena.FreeChoice.Studies.Fox2007.instDecidableEqModalW :
      DecidableEq ModalW
      Equations
      source
      @[implicit_reducible]
      instance Phenomena.FreeChoice.Studies.Fox2007.instFintypeModalW :
      Fintype ModalW
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Phenomena.FreeChoice.Studies.Fox2007.diamP :
      ModalW → Bool
      Equations
      Instances For
        source
        def Phenomena.FreeChoice.Studies.Fox2007.diamQ :
        ModalW → Bool
        Equations
        Instances For
          source
          def Phenomena.FreeChoice.Studies.Fox2007.diamPorQ :
          ModalW → Bool
          Equations
          Instances For
            source
            def Phenomena.FreeChoice.Studies.Fox2007.diamPandQ :
            ModalW → Bool
            Equations
            Instances For
              source
              @[reducible, inline]
              abbrev Phenomena.FreeChoice.Studies.Fox2007.modalAltsF :
              Finset (Finset ModalW)

              Sauerland alternatives under ◇: {◇(p∨q), ◇p, ◇q, ◇(p∧q)}.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[reducible, inline]
                abbrev Phenomena.FreeChoice.Studies.Fox2007.diamPorQF :
                Finset ModalW
                Equations
                Instances For
                  source
                  @[reducible, inline]
                  abbrev Phenomena.FreeChoice.Studies.Fox2007.diamPF :
                  Finset ModalW
                  Equations
                  Instances For
                    source
                    @[reducible, inline]
                    abbrev Phenomena.FreeChoice.Studies.Fox2007.diamQF :
                    Finset ModalW
                    Equations
                    Instances For
                      source
                      @[reducible, inline]
                      abbrev Phenomena.FreeChoice.Studies.Fox2007.diamPandQF :
                      Finset ModalW
                      Equations
                      Instances For
                        source
                        theorem Phenomena.FreeChoice.Studies.Fox2007.exhDiamPorQ_eq :
                        Exhaustification.innocent.exh modalAltsF diamPorQF = Exhaustification.predToFinset fun (w : ModalW) => diamPorQ w && !diamPandQ w

                        Layer 1: Exh(◇(p∨q)) = ◇(p∨q) ∧ ¬◇(p∧q). Only ◇(p∧q) is innocently excludable; ◇p and ◇q cannot be IE-excluded because excluding ◇p while keeping ◇(p∨q) forces ◇q, and conversely.

                        source
                        theorem Phenomena.FreeChoice.Studies.Fox2007.exhDiamP_eq :
                        Exhaustification.innocent.exh modalAltsF diamPF = Exhaustification.predToFinset fun (w : ModalW) => diamP w && !diamQ w

                        Exhaustifying ◇p (relative to the same alternatives) excludes ◇q.

                        source
                        theorem Phenomena.FreeChoice.Studies.Fox2007.exhDiamQ_eq :
                        Exhaustification.innocent.exh modalAltsF diamQF = Exhaustification.predToFinset fun (w : ModalW) => diamQ w && !diamP w

                        Exhaustifying ◇q excludes ◇p (symmetric).

                        source
                        theorem Phenomena.FreeChoice.Studies.Fox2007.exhDiamPandQ_eq :
                        Exhaustification.innocent.exh modalAltsF diamPandQF = diamPandQF

                        Exhaustifying ◇(p∧q) is vacuous: it entails every other alternative, so nothing is non-weaker.

                        source
                        @[reducible, inline]
                        abbrev Phenomena.FreeChoice.Studies.Fox2007.layer2AltsF :
                        Finset (Finset ModalW)

                        Layer-2 alternatives: {Exh(φ) : φ ∈ C} — the exhaustified versions of the original Sauerland alternatives.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          @[reducible, inline]
                          abbrev Phenomena.FreeChoice.Studies.Fox2007.layer1ResultF :
                          Finset ModalW

                          Layer-1 result, used as the prejacent for layer 2.

                          Equations
                          Instances For
                            source
                            theorem Phenomena.FreeChoice.Studies.Fox2007.free_choice :
                            Exhaustification.innocent.exh layer2AltsF layer1ResultF = Exhaustification.predToFinset fun (w : ModalW) => diamP w && diamQ w && !diamPandQ w

                            Free Choice: double exhaustification yields ◇p ∧ ◇q ∧ ¬◇(p∧q).

                            Exh(C')[Exh(C)(◇(p∨q))] excludes the layer-2 alternatives Exh(◇p) = ◇p ∧ ¬◇q and Exh(◇q) = ◇q ∧ ¬◇p. Negating both (given the layer-1 prejacent ◇(p∨q) ∧ ¬◇(p∧q)) forces both ◇p and ◇q to hold.

                            source
                            theorem Phenomena.FreeChoice.Studies.Fox2007.fc_entails_both_disjuncts (w : ModalW) (h : w ∈ Exhaustification.innocent.exh layer2AltsF layer1ResultF) :
                            diamP w = true ∧ diamQ w = true

                            FC entails both disjuncts hold: the speaker has permission for each disjunct individually.