Documentation

Linglib.Theories.Semantics.Dynamic.Systems.IntensionalCDRT.Basic

source
def Semantics.Dynamic.IntensionalCDRT.ICDRTAssignment.«term_⟦_⟧ᵢ» :
Lean.TrailingParserDescr

Notation for individual variable lookup

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Semantics.Dynamic.IntensionalCDRT.ICDRTAssignment.«term_⟦_⟧ₚ» :
    Lean.TrailingParserDescr

    Notation for propositional variable lookup

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Semantics.Dynamic.IntensionalCDRT.IContext (W : Type u_1) (E : Type u_2) :
      Type (max u_2 u_1)

      Set of assignment-world pairs (information state in flat update).

      Equations
      Instances For
        source
        instance Semantics.Dynamic.IntensionalCDRT.instMembershipProdICDRTAssignmentIContext {W : Type u_1} {E : Type u_2} :
        Membership (Core.ICDRTAssignment W E × W) (IContext W E)
        Equations
        source
        instance Semantics.Dynamic.IntensionalCDRT.instEmptyCollectionIContext {W : Type u_1} {E : Type u_2} :
        EmptyCollection (IContext W E)
        Equations
        source
        instance Semantics.Dynamic.IntensionalCDRT.instHasSubsetIContext {W : Type u_1} {E : Type u_2} :
        HasSubset (IContext W E)
        Equations
        source
        instance Semantics.Dynamic.IntensionalCDRT.instUnionIContext {W : Type u_1} {E : Type u_2} :
        Union (IContext W E)
        Equations
        source
        instance Semantics.Dynamic.IntensionalCDRT.instInterIContext {W : Type u_1} {E : Type u_2} :
        Inter (IContext W E)
        Equations
        source
        def Semantics.Dynamic.IntensionalCDRT.IContext.univ {W : Type u_1} {E : Type u_2} :
        IContext W E

        The trivial context (all possibilities)

        Equations
        Instances For
          source
          def Semantics.Dynamic.IntensionalCDRT.IContext.empty {W : Type u_1} {E : Type u_2} :
          IContext W E

          The absurd context (no possibilities)

          Equations
          Instances For
            source
            def Semantics.Dynamic.IntensionalCDRT.IContext.consistent {W : Type u_1} {E : Type u_2} (c : IContext W E) :
            Prop

            Context is consistent (non-empty)

            Equations
            Instances For
              source
              def Semantics.Dynamic.IntensionalCDRT.IContext.worlds {W : Type u_1} {E : Type u_2} (c : IContext W E) :
              Set W

              Worlds in the context (projection)

              Equations
              Instances For
                source
                def Semantics.Dynamic.IntensionalCDRT.IContext.update {W : Type u_1} {E : Type u_2} (c : IContext W E) (p : W → Prop) :
                IContext W E

                Update with a world-predicate

                Equations
                Instances For
                  source
                  def Semantics.Dynamic.IntensionalCDRT.IContext.updateFull {W : Type u_1} {E : Type u_2} (c : IContext W E) (p : Core.ICDRTAssignment W E → W → Prop) :
                  IContext W E

                  Update with an assignment-world predicate

                  Equations
                  Instances For
                    source
                    def Semantics.Dynamic.IntensionalCDRT.IContext.«term_⟦_⟧» :
                    Lean.TrailingParserDescr
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Semantics.Dynamic.IntensionalCDRT.DynProp (W : Type u_1) (E : Type u_2) :
                      Type (max u_2 u_1)

                      Context-to-context transformer (sentence denotation).

                      Equations
                      Instances For
                        source
                        def Semantics.Dynamic.IntensionalCDRT.DynProp.id {W : Type u_1} {E : Type u_2} :
                        DynProp W E

                        Identity (says nothing)

                        Equations
                        Instances For
                          source
                          def Semantics.Dynamic.IntensionalCDRT.DynProp.absurd {W : Type u_1} {E : Type u_2} :
                          DynProp W E

                          Absurd (contradiction)

                          Equations
                          Instances For
                            source
                            def Semantics.Dynamic.IntensionalCDRT.DynProp.taut {W : Type u_1} {E : Type u_2} :
                            DynProp W E

                            Tautology (accepts all)

                            Equations
                            Instances For
                              source
                              def Semantics.Dynamic.IntensionalCDRT.DynProp.ofProp {W : Type u_1} {E : Type u_2} (p : W → Prop) :
                              DynProp W E

                              Lift a classical proposition

                              Equations
                              Instances For
                                source
                                structure Semantics.Dynamic.IntensionalCDRT.CommitmentSet (W : Type u_1) (E : Type u_2) :
                                Type (max u_1 u_2)

                                Speaker's public commitments (discourse consistency requires non-empty).

                                Instances For
                                  source
                                  def Semantics.Dynamic.IntensionalCDRT.CommitmentSet.initial {W : Type u_1} {E : Type u_2} [Nonempty W] :
                                  CommitmentSet W E

                                  Initial commitment set (all worlds)

                                  Equations
                                  Instances For