Documentation

Linglib.Phenomena.Complementation.Attitudes.IntensionalExamples

source
inductive Phenomena.Complementation.Attitudes.IntensionalExamples.ToyIEntity :
Type

A small domain for examples

Instances For
    source
    instance Phenomena.Complementation.Attitudes.IntensionalExamples.instReprToyIEntity :
    Repr ToyIEntity
    Equations
    source
    def Phenomena.Complementation.Attitudes.IntensionalExamples.instReprToyIEntity.repr :
    ToyIEntity → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance Phenomena.Complementation.Attitudes.IntensionalExamples.instDecidableEqToyIEntity :
      DecidableEq ToyIEntity
      Equations
      source
      def Phenomena.Complementation.Attitudes.IntensionalExamples.toyIModel :
      Semantics.Attitudes.Intensional.IModel
      Equations
      Instances For
        source
        def Phenomena.Complementation.Attitudes.IntensionalExamples.sleeps :
        toyIModel.interpTy (Semantics.Attitudes.Intensional.Ty.intens (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t))

        "sleeps" as a world-dependent property.

        Equations
        Instances For
          source
          def Phenomena.Complementation.Attitudes.IntensionalExamples.happy :
          toyIModel.interpTy (Semantics.Attitudes.Intensional.Ty.intens (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t))

          "is happy" as a world-dependent property.

          Equations
          Instances For
            source
            def Phenomena.Complementation.Attitudes.IntensionalExamples.morningStar :
            toyIModel.interpTy Semantics.Attitudes.Intensional.Ty.indConcept

            "the morning star" - an individual concept that picks out potentially different individuals in different worlds.

            Equations
            Instances For
              source
              def Phenomena.Complementation.Attitudes.IntensionalExamples.eveningStar :
              toyIModel.interpTy Semantics.Attitudes.Intensional.Ty.indConcept

              "the evening star" - another individual concept

              Equations
              Instances For
                source
                theorem Phenomena.Complementation.Attitudes.IntensionalExamples.extensions_equal_at_w0 :
                Semantics.Attitudes.Intensional.down morningStar Core.Proposition.World4.w0 = Semantics.Attitudes.Intensional.down eveningStar Core.Proposition.World4.w0

                In the actual world (w0), morning star = evening star. But their INTENSIONS differ (they pick out different things in other worlds).

                source
                theorem Phenomena.Complementation.Attitudes.IntensionalExamples.intensions_differ :
                morningStar ≠ eveningStar
                source
                def Phenomena.Complementation.Attitudes.IntensionalExamples.believes_access :
                ToyIEntity → Semantics.Attitudes.Intensional.World → Semantics.Attitudes.Intensional.World → Bool

                Doxastic accessibility relation: which worlds are compatible with what an agent believes. R(a, w, w') means w' is compatible with what a believes in w.

                Equations
                Instances For
                  source
                  def Phenomena.Complementation.Attitudes.IntensionalExamples.believe :
                  toyIModel.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Attitudes.Intensional.Ty.prop ⇒ Semantics.Montague.Ty.t)

                  "believe" as an attitude verb. ⟦believe⟧(a)(p)(w) = ∀w'. R(a,w,w') → p(w')

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Phenomena.Complementation.Attitudes.IntensionalExamples.believeAt :
                    Semantics.Attitudes.Intensional.World → toyIModel.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Attitudes.Intensional.Ty.prop ⇒ Semantics.Montague.Ty.t)

                    Extended believe that's world-dependent.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Phenomena.Complementation.Attitudes.IntensionalExamples.johnBelievesMary_deDicto :
                      toyIModel.interpTy Semantics.Montague.Ty.t

                      "John believes Mary sleeps" (de dicto)

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Phenomena.Complementation.Attitudes.IntensionalExamples.johnBelievesJohnSleeps :
                        toyIModel.interpTy Semantics.Montague.Ty.t

                        "John believes John sleeps" (de dicto)

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def Phenomena.Complementation.Attitudes.IntensionalExamples.someCookies :
                          toyIModel.interpTy Semantics.Attitudes.Intensional.Ty.prop

                          Proposition: "John ate some cookies" (simplified)

                          Equations
                          Instances For
                            source
                            def Phenomena.Complementation.Attitudes.IntensionalExamples.allCookies :
                            toyIModel.interpTy Semantics.Attitudes.Intensional.Ty.prop

                            Proposition: "John ate all cookies" (simplified)

                            Equations
                            Instances For
                              source
                              def Phenomena.Complementation.Attitudes.IntensionalExamples.maryBelievesSome :
                              toyIModel.interpTy Semantics.Montague.Ty.t

                              "Mary believes John ate some cookies"

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                def Phenomena.Complementation.Attitudes.IntensionalExamples.maryBelievesAll :
                                toyIModel.interpTy Semantics.Montague.Ty.t

                                "Mary believes John ate all cookies"

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  theorem Phenomena.Complementation.Attitudes.IntensionalExamples.belief_intensional :
                                  Semantics.Attitudes.Intensional.down morningStar Core.Proposition.World4.w0 = Semantics.Attitudes.Intensional.down eveningStar Core.Proposition.World4.w0 ∧ morningStar ≠ eveningStar

                                  Belief is intensional: co-extensional expressions can differ under belief.

                                  source
                                  theorem Phenomena.Complementation.Attitudes.IntensionalExamples.up_down_identity {m : Semantics.Attitudes.Intensional.IModel} {τ : Semantics.Montague.Ty} (x : m.interpTy τ) (w : Semantics.Attitudes.Intensional.World) :
                                  Semantics.Attitudes.Intensional.down (Semantics.Attitudes.Intensional.up x) w = x

                                  Up-down identity: applying down after up returns the original value.

                                  Bridge to Direct Reference Theory #

                                  The morningStar/eveningStar individual concepts defined above are Fregean concepts (world-dependent). In contrast, proper names in Semantics.Reference.Basic are Kripkean rigid designators.

                                  This section makes the distinction explicit, connecting the existing Hesperus/Phosphorus examples to the direct reference framework.

                                  source
                                  def Phenomena.Complementation.Attitudes.IntensionalExamples.hesperus_rigid :
                                  Core.Intension Semantics.Attitudes.Intensional.World ToyIEntity

                                  "Hesperus" as a Kripkean proper name: rigid designator.

                                  Contrast with morningStar above, which is a Fregean individual concept that varies across worlds. The proper name always returns .hesperus.

                                  Equations
                                  Instances For
                                    source
                                    theorem Phenomena.Complementation.Attitudes.IntensionalExamples.morningStar_not_rigid :
                                    ¬Core.Intension.IsRigid morningStar

                                    morningStar is NOT rigid: it picks out different entities at different worlds. This contrasts with hesperus_rigid which IS rigid.

                                    source
                                    theorem Phenomena.Complementation.Attitudes.IntensionalExamples.hesperus_rigid_isRigid :
                                    hesperus_rigid.IsRigid

                                    hesperus_rigid IS rigid (a proper name in the Kripkean sense).

                                    source
                                    theorem Phenomena.Complementation.Attitudes.IntensionalExamples.name_vs_concept_independence :
                                    hesperus_rigid.CoRefer morningStar Core.Proposition.World4.w0 ∧ ¬hesperus_rigid.CoExtensional morningStar

                                    Independence of names vs concepts: a Fregean individual concept (morningStar) can agree with a Kripkean name (hesperus_rigid) at one world while diverging at others.