Documentation

Linglib.Theories.Semantics.Montague.Conjunction

source
def Semantics.Montague.Ty.isConjoinable :
Ty → Bool

A type is conjoinable if it "ends in t" (Definition 4).

Equations
Instances For
    source
    def Semantics.Montague.Conjunction.genConj (τ : Ty) (m : Model) :
    m.interpTy τ → m.interpTy τ → m.interpTy τ

    Generalized conjunction (Definition 5).

    Equations
    Instances For
      source
      def Semantics.Montague.Conjunction.genDisj (τ : Ty) (m : Model) :
      m.interpTy τ → m.interpTy τ → m.interpTy τ

      Generalized disjunction.

      Equations
      Instances For
        source
        theorem Semantics.Montague.Conjunction.genConj_at_t (m : Model) (p q : Bool) :
        genConj Ty.t m p q = (p && q)
        source
        theorem Semantics.Montague.Conjunction.genConj_at_et (m : Model) (f g : m.Entity → Bool) :
        genConj (Ty.e ⇒ Ty.t) m f g = fun (x : m.Entity) => f x && g x
        source
        theorem Semantics.Montague.Conjunction.genConj_at_eet (m : Model) (f g : m.Entity → m.Entity → Bool) :
        genConj (Ty.e ⇒ Ty.e ⇒ Ty.t) m f g = fun (x y : m.Entity) => f x y && g x y
        source
        theorem Semantics.Montague.Conjunction.genConj_comm_t (m : Model) (p q : Bool) :
        genConj Ty.t m p q = genConj Ty.t m q p
        source
        theorem Semantics.Montague.Conjunction.genConj_assoc_t (m : Model) (p q r : Bool) :
        genConj Ty.t m (genConj Ty.t m p q) r = genConj Ty.t m p (genConj Ty.t m q r)
        source
        theorem Semantics.Montague.Conjunction.genDisj_comm_t (m : Model) (p q : Bool) :
        genDisj Ty.t m p q = genDisj Ty.t m q p

        @cite{partee-rooth-1983} Key Facts #

        @cite{partee-rooth-1983}

        source
        theorem Semantics.Montague.Conjunction.genConj_pointwise {m : Model} {σ τ : Ty} (f g : m.interpTy (σ ⇒ τ)) :
        genConj (σ ⇒ τ) m f g = fun (x : m.interpTy σ) => genConj τ m (f x) (g x)

        Fact 6a: φ ∩ ψ = λz[φ(z) ∩ ψ(z)]

        source
        theorem Semantics.Montague.Conjunction.genConj_distributes_over_app {m : Model} {σ τ : Ty} (f g : m.interpTy (σ ⇒ τ)) (x : m.interpTy σ) :
        genConj (σ ⇒ τ) m f g x = genConj τ m (f x) (g x)

        Fact 6b: [φ ∩ ψ](α) = φ(α) ∩ ψ(α)

        source
        theorem Semantics.Montague.Conjunction.genConj_lambda_distribution {m : Model} {σ τ : Ty} (f g : m.interpTy σ → m.interpTy τ) :
        genConj (σ ⇒ τ) m f g = fun (v : m.interpTy σ) => genConj τ m (f v) (g v)

        Fact 6c: λv.φ ∩ λv.ψ = λv[φ ∩ ψ]

        source
        theorem Semantics.Montague.Conjunction.genDisj_distributes_over_app {m : Model} {σ τ : Ty} (f g : m.interpTy (σ ⇒ τ)) (x : m.interpTy σ) :
        genDisj (σ ⇒ τ) m f g x = genDisj τ m (f x) (g x)
        source
        theorem Semantics.Montague.Conjunction.genDisj_lambda_distribution {m : Model} {σ τ : Ty} (f g : m.interpTy σ → m.interpTy τ) :
        genDisj (σ ⇒ τ) m f g = fun (v : m.interpTy σ) => genDisj τ m (f v) (g v)
        source
        def Semantics.Montague.Conjunction.typeRaise {m : Model} (e : m.interpTy Ty.e) :
        m.interpTy ((Ty.e ⇒ Ty.t) ⇒ Ty.t)

        Type-raise an entity to a GQ: e ↦ λP.P(e)

        Equations
        Instances For
          source
          def Semantics.Montague.Conjunction.coordEntities {m : Model} (e1 e2 : m.interpTy Ty.e) :
          m.interpTy ((Ty.e ⇒ Ty.t) ⇒ Ty.t)

          Coordinated entities: λP. P(e₁) ∧ P(e₂)

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem Semantics.Montague.Conjunction.typeRaise_preserves {m : Model} (e : m.interpTy Ty.e) (p : m.interpTy (Ty.e ⇒ Ty.t)) :
            typeRaise e p = p e
            source
            theorem Semantics.Montague.Conjunction.coordEntities_both_satisfy {m : Model} (e1 e2 : m.interpTy Ty.e) (p : m.interpTy (Ty.e ⇒ Ty.t)) :
            coordEntities e1 e2 p = (p e1 && p e2)
            source
            def Semantics.Montague.Conjunction.tall_sem :
            toyModel.interpTy (Ty.e ⇒ Ty.t)
            Equations
            Instances For
              source
              def Semantics.Montague.Conjunction.happy_sem :
              toyModel.interpTy (Ty.e ⇒ Ty.t)
              Equations
              Instances For
                source
                def Semantics.Montague.Conjunction.tall_and_happy :
                toyModel.interpTy (Ty.e ⇒ Ty.t)
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem Semantics.Montague.Conjunction.tall_and_happy_is_pointwise :
                  tall_and_happy = fun (x : toyModel.interpTy Ty.e) => tall_sem x && happy_sem x