Documentation

Linglib.Semantics.Intensional.Conjunction

Generalized Conjunction #

[PR83]

Conjunction and disjunction defined recursively over the IL type structure:

source
def Intensional.Conjunction.genConj (τ : Ty) (E W : Type) :
Denot E W τ → Denot E W τ → Denot E W τ

Generalized conjunction ([PR83] Definition 5). At intension types, conjunction is pointwise over indices.

Equations
Instances For
    source
    def Intensional.Conjunction.genDisj (τ : Ty) (E W : Type) :
    Denot E W τ → Denot E W τ → Denot E W τ

    Generalized disjunction.

    Equations
    Instances For
      source
      def Intensional.Conjunction.genNeg (τ : Ty) (E W : Type) :
      Denot E W τ → Denot E W τ

      Generalized negation (pointwise complement) — the recursion form of ·ᶜ, needed for negative coordination (nor = ¬(A ∨ B)). Junk at .e.

      Equations
      Instances For
        source
        theorem Intensional.Conjunction.genConj_at_t (E W : Type) (p q : Prop) :
        genConj Ty.t E W p q = (p ∧ q)
        source
        theorem Intensional.Conjunction.genConj_at_et (E W : Type) (f g : E → Prop) :
        genConj (Ty.e ⇒ Ty.t) E W f g = fun (x : E) => f x ∧ g x
        source
        theorem Intensional.Conjunction.genConj_at_eet (E W : Type) (f g : E → E → Prop) :
        genConj (Ty.e ⇒ Ty.e ⇒ Ty.t) E W f g = fun (x y : E) => f x y ∧ g x y
        source
        theorem Intensional.Conjunction.genConj_at_intens (E W : Type) {a : Ty} (f g : Denot E W a.intens) :
        genConj a.intens E W f g = fun (i : W) => genConj a E W (f i) (g i)

        At intension types, conjunction is pointwise over indices.

        source
        theorem Intensional.Conjunction.genConj_comm_t (E W : Type) (p q : Prop) :
        genConj Ty.t E W p q = genConj Ty.t E W q p
        source
        theorem Intensional.Conjunction.genConj_assoc_t (E W : Type) (p q r : Prop) :
        genConj Ty.t E W (genConj Ty.t E W p q) r = genConj Ty.t E W p (genConj Ty.t E W q r)
        source
        theorem Intensional.Conjunction.genDisj_comm_t (E W : Type) (p q : Prop) :
        genDisj Ty.t E W p q = genDisj Ty.t E W q p

        [PR83] Key Facts #

        source
        theorem Intensional.Conjunction.genConj_pointwise {E W : Type} {σ τ : Ty} (f g : Denot E W (σ ⇒ τ)) :
        genConj (σ ⇒ τ) E W f g = fun (x : Denot E W σ) => genConj τ E W (f x) (g x)

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

        source
        theorem Intensional.Conjunction.genConj_distributes_over_app {E W : Type} {σ τ : Ty} (f g : Denot E W (σ ⇒ τ)) (x : Denot E W σ) :
        genConj (σ ⇒ τ) E W f g x = genConj τ E W (f x) (g x)

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

        source
        theorem Intensional.Conjunction.genConj_lambda_distribution {E W : Type} {σ τ : Ty} (f g : Denot E W σ → Denot E W τ) :
        genConj (σ ⇒ τ) E W f g = fun (v : Denot E W σ) => genConj τ E W (f v) (g v)

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

        source
        theorem Intensional.Conjunction.genDisj_distributes_over_app {E W : Type} {σ τ : Ty} (f g : Denot E W (σ ⇒ τ)) (x : Denot E W σ) :
        genDisj (σ ⇒ τ) E W f g x = genDisj τ E W (f x) (g x)
        source
        theorem Intensional.Conjunction.genDisj_lambda_distribution {E W : Type} {σ τ : Ty} (f g : Denot E W σ → Denot E W τ) :
        genDisj (σ ⇒ τ) E W f g = fun (v : Denot E W σ) => genDisj τ E W (f v) (g v)
        source
        def Intensional.Conjunction.coordEntities {E W : Type} (e1 e2 : Denot E W Ty.e) :
        Denot E W ((Ty.e ⇒ Ty.t) ⇒ Ty.t)

        Coordinated entities: λP. P(e₁) ∧ P(e₂) — type-raise each entity via Quantification.individual and conjoin the quantifiers.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem Intensional.Conjunction.coordEntities_both_satisfy {E W : Type} (e1 e2 : Denot E W Ty.e) (p : Denot E W (Ty.e ⇒ Ty.t)) :
          coordEntities e1 e2 p = (p e1 ∧ p e2)

          [MS14] [MS16] Decomposition #

          DP conjunction decomposes into three operations:

          source
          def Intensional.Conjunction.msShift {E W : Type} (x : Denot E W Ty.e) :
          Denot E W (Ty.e ⇒ Ty.t)

          ☉: M&S type-shifter. Individual → singleton property.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev Intensional.Conjunction.inclFunc {E W : Type} (x : Denot E W Ty.e) :
            Denot E W ((Ty.e ⇒ Ty.t) ⇒ Ty.t)

            MU particle semantics = Quantification.individual.

            Equations
            Instances For
              source
              theorem Intensional.Conjunction.ms_full_derivation {E W : Type} (e1 e2 : Denot E W Ty.e) :
              genConj ((Ty.e ⇒ Ty.t) ⇒ Ty.t) E W (Quantification.individual e1) (Quantification.individual e2) = coordEntities e1 e2

              Full M&S derivation: J(MU(e₁), MU(e₂)) = coordEntities e₁ e₂.