def Semantics.Composition.Modification.predMod {E : Type u_1} (p q : E → Bool) : E → Bool

Predicate modification: ⟦α β⟧ = λx. ⟦α⟧(x) ∧ ⟦β⟧(x)

Equations

• Semantics.Composition.Modification.predMod p q x = (p x && q x)

def Semantics.Composition.Modification.truePred {E : Type u_1} : E → Bool

Equations

• Semantics.Composition.Modification.truePred x✝ = true

theorem Semantics.Composition.Modification.predMod_comm {E : Type u_1} (p q : E → Bool) : predMod p q = predMod q p

theorem Semantics.Composition.Modification.predMod_assoc {E : Type u_1} (p q r : E → Bool) : predMod (predMod p q) r = predMod p (predMod q r)

theorem Semantics.Composition.Modification.predMod_true_right {E : Type u_1} (p : E → Bool) : predMod p truePred = p

theorem Semantics.Composition.Modification.predMod_true_left {E : Type u_1} (p : E → Bool) : predMod truePred p = p

The adjective classification hierarchy (intersective, subsective, privative, extensional) is in Lexical/Adjective/Classification.lean. This file provides the composition operation (Predicate Modification) that implements the intersective case.

def Semantics.Composition.Modification.predicateModification {F : Core.Logic.Intensional.Frame} (p₁ p₂ : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Equations

• (p₁ ⊓ₚ p₂) x = (p₁ x ∧ p₂ x)

def Semantics.Composition.Modification.«term_⊓ₚ_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem Semantics.Composition.Modification.predicateModification_comm {F : Core.Logic.Intensional.Frame} (p₁ p₂ : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) : p₁ ⊓ₚ p₂ = p₂ ⊓ₚ p₁

theorem Semantics.Composition.Modification.predicateModification_assoc {F : Core.Logic.Intensional.Frame} (p₁ p₂ p₃ : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) : p₁ ⊓ₚ p₂ ⊓ₚ p₃ = p₁ ⊓ₚ (p₂ ⊓ₚ p₃)

theorem Semantics.Composition.Modification.predicateModification_idem {F : Core.Logic.Intensional.Frame} (p : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) : p ⊓ₚ p = p

theorem Semantics.Composition.Modification.predicateModification_true_right {F : Core.Logic.Intensional.Frame} (p : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) : (p ⊓ₚ fun (x : F.Denot Core.Logic.Intensional.Ty.e) => True) = p

theorem Semantics.Composition.Modification.predicateModification_true_left {F : Core.Logic.Intensional.Frame} (p : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) : (fun (x : F.Denot Core.Logic.Intensional.Ty.e) => True) ⊓ₚ p = p

theorem Semantics.Composition.Modification.predicateModification_false_right {F : Core.Logic.Intensional.Frame} (p : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) : (p ⊓ₚ fun (x : F.Denot Core.Logic.Intensional.Ty.e) => False) = fun (x : F.Denot Core.Logic.Intensional.Ty.e) => False

theorem Semantics.Composition.Modification.predicateModification_false_left {F : Core.Logic.Intensional.Frame} (p : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) : (fun (x : F.Denot Core.Logic.Intensional.Ty.e) => False) ⊓ₚ p = fun (x : F.Denot Core.Logic.Intensional.Ty.e) => False

theorem Semantics.Composition.Modification.predicateModification_extension {F : Core.Logic.Intensional.Frame} (p₁ p₂ : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) : Core.Logic.Intensional.predicateToSet (p₁ ⊓ₚ p₂) = Core.Logic.Intensional.predicateToSet p₁ ∩ Core.Logic.Intensional.predicateToSet p₂

theorem Semantics.Composition.Modification.predicateModification_subset_left {F : Core.Logic.Intensional.Frame} (p q r : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) (h : Core.Logic.Intensional.predicateToSet p ⊆ Core.Logic.Intensional.predicateToSet q) : Core.Logic.Intensional.predicateToSet (p ⊓ₚ r) ⊆ Core.Logic.Intensional.predicateToSet (q ⊓ₚ r)

theorem Semantics.Composition.Modification.predicateModification_subset_right {F : Core.Logic.Intensional.Frame} (p q r : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) (h : Core.Logic.Intensional.predicateToSet p ⊆ Core.Logic.Intensional.predicateToSet q) : Core.Logic.Intensional.predicateToSet (r ⊓ₚ p) ⊆ Core.Logic.Intensional.predicateToSet (r ⊓ₚ q)

theorem Semantics.Composition.Modification.intersective_equivalence {F : Core.Logic.Intensional.Frame} (p q : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) (x : F.Entity) : (p ⊓ₚ q) x ↔ p x ∧ q x

(P ⊓ₚ Q)(x) ↔ P(x) ∧ Q(x)

theorem Semantics.Composition.Modification.intersective_equivalence_set {F : Core.Logic.Intensional.Frame} (p q : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) (x : F.Entity) : x ∈ Core.Logic.Intensional.predicateToSet (p ⊓ₚ q) ↔ x ∈ Core.Logic.Intensional.predicateToSet p ∧ x ∈ Core.Logic.Intensional.predicateToSet q

theorem Semantics.Composition.Modification.pm_entails_left {F : Core.Logic.Intensional.Frame} (p q : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) (x : F.Entity) (h : (p ⊓ₚ q) x) : p x

theorem Semantics.Composition.Modification.pm_entails_right {F : Core.Logic.Intensional.Frame} (p q : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) (x : F.Entity) (h : (p ⊓ₚ q) x) : q x

theorem Semantics.Composition.Modification.pm_intro {F : Core.Logic.Intensional.Frame} (p q : F.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) (x : F.Entity) (hp : p x) (hq : q x) : (p ⊓ₚ q) x

def Semantics.Composition.Modification.gray_sem : Montague.toyModel.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Equations

• Semantics.Composition.Modification.gray_sem Semantics.Montague.ToyEntity.john = True
• Semantics.Composition.Modification.gray_sem Semantics.Montague.ToyEntity.mary = True
• Semantics.Composition.Modification.gray_sem x = False

def Semantics.Composition.Modification.cat_sem : Montague.toyModel.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Equations

• Semantics.Composition.Modification.cat_sem Semantics.Montague.ToyEntity.pizza = True
• Semantics.Composition.Modification.cat_sem x = False

def Semantics.Composition.Modification.big_sem : Montague.toyModel.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Equations

• Semantics.Composition.Modification.big_sem Semantics.Montague.ToyEntity.book = True
• Semantics.Composition.Modification.big_sem x = False

def Semantics.Composition.Modification.grayCat_sem : Montague.toyModel.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Equations

• Semantics.Composition.Modification.grayCat_sem = Semantics.Composition.Modification.gray_sem ⊓ₚ Semantics.Composition.Modification.cat_sem

theorem Semantics.Composition.Modification.grayCat_empty : Core.Logic.Intensional.predicateToSet grayCat_sem = ∅

def Semantics.Composition.Modification.bigGrayCat_sem : Montague.toyModel.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Equations

• Semantics.Composition.Modification.bigGrayCat_sem = Semantics.Composition.Modification.big_sem ⊓ₚ (Semantics.Composition.Modification.gray_sem ⊓ₚ Semantics.Composition.Modification.cat_sem)

theorem Semantics.Composition.Modification.bigGrayCat_assoc : big_sem ⊓ₚ (gray_sem ⊓ₚ cat_sem) = big_sem ⊓ₚ gray_sem ⊓ₚ cat_sem

theorem Semantics.Composition.Modification.grayCat_order : gray_sem ⊓ₚ (big_sem ⊓ₚ cat_sem) = big_sem ⊓ₚ (gray_sem ⊓ₚ cat_sem)