Documentation

Linglib.Phenomena.Modality.Studies.Aloni2022

@cite{aloni-2022}: BSML Applied to Permission Disjunction #

@cite{aloni-2022}

Phenomena-level instantiation of BSML for the classic free choice example: "You may have coffee or tea" → "You may have coffee AND you may have tea."

The core BSML theory (formulas, support, enrichment, FC theorems) lives in Theories/Semantics/Dynamic/Systems/BSML/. This file provides the concrete deontic model and verifies the FC predictions computationally.

source
inductive Phenomena.Modality.Studies.Aloni2022.PermissionWorld :
Type

Example world type for "You may have coffee or tea"

Instances For
    source
    instance Phenomena.Modality.Studies.Aloni2022.instDecidableEqPermissionWorld :
    DecidableEq PermissionWorld
    Equations
    source
    def Phenomena.Modality.Studies.Aloni2022.instReprPermissionWorld.repr :
    PermissionWorld → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance Phenomena.Modality.Studies.Aloni2022.instReprPermissionWorld :
      Repr PermissionWorld
      Equations
      source
      def Phenomena.Modality.Studies.Aloni2022.coffeePermitted :
      PermissionWorld → Bool

      The proposition "coffee is permitted"

      Equations
      Instances For
        source
        def Phenomena.Modality.Studies.Aloni2022.teaPermitted :
        PermissionWorld → Bool

        The proposition "tea is permitted"

        Equations
        Instances For
          source
          def Phenomena.Modality.Studies.Aloni2022.permissionWorlds :
          List PermissionWorld

          All permission worlds

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Phenomena.Modality.Studies.Aloni2022.deonticModel :
            Semantics.Dynamic.BSML.BSMLModel PermissionWorld

            Deontic model: universal accessibility

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Phenomena.Modality.Studies.Aloni2022.restrictiveModel :
              Semantics.Dynamic.BSML.BSMLModel PermissionWorld

              Restrictive deontic model: from 'neither', only 'neither' is accessible

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                def Phenomena.Modality.Studies.Aloni2022.mayHaveCoffeeOrTea :
                Semantics.Dynamic.BSML.BSMLFormula

                The formula ◇(coffee ∨ tea)

                Equations
                Instances For
                  source
                  def Phenomena.Modality.Studies.Aloni2022.freeChoiceTeam :
                  Semantics.Dynamic.TeamSemantics.Team PermissionWorld

                  Team representing "free choice holds" (both options available)

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Phenomena.Modality.Studies.Aloni2022.mayCoffee :
                    Semantics.Dynamic.BSML.BSMLFormula
                    Equations
                    Instances For
                      source
                      def Phenomena.Modality.Studies.Aloni2022.mayTea :
                      Semantics.Dynamic.BSML.BSMLFormula
                      Equations
                      Instances For
                        source
                        def Phenomena.Modality.Studies.Aloni2022.prohibition :
                        Semantics.Dynamic.BSML.BSMLFormula
                        Equations
                        Instances For
                          source
                          def Phenomena.Modality.Studies.Aloni2022.notMayCoffee :
                          Semantics.Dynamic.BSML.BSMLFormula
                          Equations
                          Instances For
                            source
                            def Phenomena.Modality.Studies.Aloni2022.notMayTea :
                            Semantics.Dynamic.BSML.BSMLFormula
                            Equations
                            Instances For
                              source
                              def Phenomena.Modality.Studies.Aloni2022.prohibitionTeam :
                              Semantics.Dynamic.TeamSemantics.Team PermissionWorld

                              Team where neither is permitted (with restricted accessibility)

                              Equations
                              Instances For
                                source
                                def Phenomena.Modality.Studies.Aloni2022.wideScopeDisj :
                                Semantics.Dynamic.BSML.BSMLFormula
                                Equations
                                Instances For