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

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

Equations

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

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

Equations

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

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

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

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

theorem Semantics.Montague.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.Montague.Modification.predicateModification {m : Model} (p₁ p₂ : m.interpTy (Ty.e ⇒ Ty.t)) : m.interpTy (Ty.e ⇒ Ty.t)

Equations

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

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

Equations

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

theorem Semantics.Montague.Modification.predicateModification_comm {m : Model} (p₁ p₂ : m.interpTy (Ty.e ⇒ Ty.t)) : p₁ ⊓ₚ p₂ = p₂ ⊓ₚ p₁

theorem Semantics.Montague.Modification.predicateModification_assoc {m : Model} (p₁ p₂ p₃ : m.interpTy (Ty.e ⇒ Ty.t)) : p₁ ⊓ₚ p₂ ⊓ₚ p₃ = p₁ ⊓ₚ (p₂ ⊓ₚ p₃)

theorem Semantics.Montague.Modification.predicateModification_idem {m : Model} (p : m.interpTy (Ty.e ⇒ Ty.t)) : p ⊓ₚ p = p

theorem Semantics.Montague.Modification.predicateModification_true_right {m : Model} (p : m.interpTy (Ty.e ⇒ Ty.t)) : (p ⊓ₚ fun (x : m.interpTy Ty.e) => true) = p

theorem Semantics.Montague.Modification.predicateModification_true_left {m : Model} (p : m.interpTy (Ty.e ⇒ Ty.t)) : (fun (x : m.interpTy Ty.e) => true) ⊓ₚ p = p

theorem Semantics.Montague.Modification.predicateModification_false_right {m : Model} (p : m.interpTy (Ty.e ⇒ Ty.t)) : (p ⊓ₚ fun (x : m.interpTy Ty.e) => false) = fun (x : m.interpTy Ty.e) => false

theorem Semantics.Montague.Modification.predicateModification_false_left {m : Model} (p : m.interpTy (Ty.e ⇒ Ty.t)) : (fun (x : m.interpTy Ty.e) => false) ⊓ₚ p = fun (x : m.interpTy Ty.e) => false

theorem Semantics.Montague.Modification.predicateModification_extension {m : Model} (p₁ p₂ : m.interpTy (Ty.e ⇒ Ty.t)) : predicateToSet (p₁ ⊓ₚ p₂) = predicateToSet p₁ ∩ predicateToSet p₂

theorem Semantics.Montague.Modification.predicateModification_subset_left {m : Model} (p q r : m.interpTy (Ty.e ⇒ Ty.t)) (h : predicateToSet p ⊆ predicateToSet q) : predicateToSet (p ⊓ₚ r) ⊆ predicateToSet (q ⊓ₚ r)

theorem Semantics.Montague.Modification.predicateModification_subset_right {m : Model} (p q r : m.interpTy (Ty.e ⇒ Ty.t)) (h : predicateToSet p ⊆ predicateToSet q) : predicateToSet (r ⊓ₚ p) ⊆ predicateToSet (r ⊓ₚ q)

theorem Semantics.Montague.Modification.intersective_equivalence {m : Model} (p q : m.interpTy (Ty.e ⇒ Ty.t)) (x : m.Entity) : (p ⊓ₚ q) x = true ↔ p x = true ∧ q x = true

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

theorem Semantics.Montague.Modification.intersective_equivalence_set {m : Model} (p q : m.interpTy (Ty.e ⇒ Ty.t)) (x : m.Entity) : x ∈ predicateToSet (p ⊓ₚ q) ↔ x ∈ predicateToSet p ∧ x ∈ predicateToSet q

theorem Semantics.Montague.Modification.pm_entails_left {m : Model} (p q : m.interpTy (Ty.e ⇒ Ty.t)) (x : m.Entity) (h : (p ⊓ₚ q) x = true) : p x = true

theorem Semantics.Montague.Modification.pm_entails_right {m : Model} (p q : m.interpTy (Ty.e ⇒ Ty.t)) (x : m.Entity) (h : (p ⊓ₚ q) x = true) : q x = true

theorem Semantics.Montague.Modification.pm_intro {m : Model} (p q : m.interpTy (Ty.e ⇒ Ty.t)) (x : m.Entity) (hp : p x = true) (hq : q x = true) : (p ⊓ₚ q) x = true

def Semantics.Montague.Modification.gray_sem : toyModel.interpTy (Ty.e ⇒ Ty.t)

Equations

• Semantics.Montague.Modification.gray_sem Semantics.Montague.ToyEntity.john = true
• Semantics.Montague.Modification.gray_sem Semantics.Montague.ToyEntity.mary = true
• Semantics.Montague.Modification.gray_sem x = false

def Semantics.Montague.Modification.cat_sem : toyModel.interpTy (Ty.e ⇒ Ty.t)

Equations

• Semantics.Montague.Modification.cat_sem Semantics.Montague.ToyEntity.pizza = true
• Semantics.Montague.Modification.cat_sem x = false

def Semantics.Montague.Modification.big_sem : toyModel.interpTy (Ty.e ⇒ Ty.t)

Equations

• Semantics.Montague.Modification.big_sem Semantics.Montague.ToyEntity.book = true
• Semantics.Montague.Modification.big_sem x = false

def Semantics.Montague.Modification.grayCat_sem : toyModel.interpTy (Ty.e ⇒ Ty.t)

Equations

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

theorem Semantics.Montague.Modification.grayCat_empty : predicateToSet grayCat_sem = ∅

def Semantics.Montague.Modification.bigGrayCat_sem : toyModel.interpTy (Ty.e ⇒ Ty.t)

Equations

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

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

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