inductive Semantics.Montague.Ty : Type

Semantic types (Montague's type theory).

• e : Ty
• t : Ty
• s : Ty
• fn : Ty → Ty → Ty

def Semantics.Montague.instReprTy.repr : Ty → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Montague.instReprTy.repr Semantics.Montague.Ty.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Semantics.Montague.Ty.e")).group prec✝
• Semantics.Montague.instReprTy.repr Semantics.Montague.Ty.t prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Semantics.Montague.Ty.t")).group prec✝
• Semantics.Montague.instReprTy.repr Semantics.Montague.Ty.s prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Semantics.Montague.Ty.s")).group prec✝

instance Semantics.Montague.instReprTy : Repr Ty

Equations

• Semantics.Montague.instReprTy = { reprPrec := Semantics.Montague.instReprTy.repr }

instance Semantics.Montague.instDecidableEqTy : DecidableEq Ty

Equations

• Semantics.Montague.instDecidableEqTy = Semantics.Montague.instDecidableEqTy.decEq

def Semantics.Montague.instDecidableEqTy.decEq (x✝ x✝¹ : Ty) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Montague.instDecidableEqTy.decEq Semantics.Montague.Ty.e Semantics.Montague.Ty.e = isTrue ⋯
• Semantics.Montague.instDecidableEqTy.decEq Semantics.Montague.Ty.e Semantics.Montague.Ty.t = isFalse Semantics.Montague.instDecidableEqTy.decEq._proof_1
• Semantics.Montague.instDecidableEqTy.decEq Semantics.Montague.Ty.e Semantics.Montague.Ty.s = isFalse Semantics.Montague.instDecidableEqTy.decEq._proof_2
• Semantics.Montague.instDecidableEqTy.decEq Semantics.Montague.Ty.e (a ⇒ a_1) = isFalse ⋯
• Semantics.Montague.instDecidableEqTy.decEq Semantics.Montague.Ty.t Semantics.Montague.Ty.e = isFalse Semantics.Montague.instDecidableEqTy.decEq._proof_4
• Semantics.Montague.instDecidableEqTy.decEq Semantics.Montague.Ty.t Semantics.Montague.Ty.t = isTrue ⋯
• Semantics.Montague.instDecidableEqTy.decEq Semantics.Montague.Ty.t Semantics.Montague.Ty.s = isFalse Semantics.Montague.instDecidableEqTy.decEq._proof_5
• Semantics.Montague.instDecidableEqTy.decEq Semantics.Montague.Ty.t (a ⇒ a_1) = isFalse ⋯
• Semantics.Montague.instDecidableEqTy.decEq Semantics.Montague.Ty.s Semantics.Montague.Ty.e = isFalse Semantics.Montague.instDecidableEqTy.decEq._proof_7
• Semantics.Montague.instDecidableEqTy.decEq Semantics.Montague.Ty.s Semantics.Montague.Ty.t = isFalse Semantics.Montague.instDecidableEqTy.decEq._proof_8
• Semantics.Montague.instDecidableEqTy.decEq Semantics.Montague.Ty.s Semantics.Montague.Ty.s = isTrue ⋯
• Semantics.Montague.instDecidableEqTy.decEq Semantics.Montague.Ty.s (a ⇒ a_1) = isFalse ⋯
• Semantics.Montague.instDecidableEqTy.decEq (a ⇒ a_1) Semantics.Montague.Ty.e = isFalse ⋯
• Semantics.Montague.instDecidableEqTy.decEq (a ⇒ a_1) Semantics.Montague.Ty.t = isFalse ⋯
• Semantics.Montague.instDecidableEqTy.decEq (a ⇒ a_1) Semantics.Montague.Ty.s = isFalse ⋯

def Semantics.Montague.«term_⇒_» : Lean.TrailingParserDescr

Equations

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

def Semantics.Montague.Ty.et : Ty

Equations

• Semantics.Montague.Ty.et = (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

def Semantics.Montague.Ty.eet : Ty

Equations

• Semantics.Montague.Ty.eet = (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

def Semantics.Montague.Ty.ett : Ty

Equations

• Semantics.Montague.Ty.ett = ((Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t) ⇒ Semantics.Montague.Ty.t)

def Semantics.Montague.Ty.st : Ty

Equations

• Semantics.Montague.Ty.st = (Semantics.Montague.Ty.s ⇒ Semantics.Montague.Ty.t)

def Semantics.Montague.Ty.se : Ty

Equations

• Semantics.Montague.Ty.se = (Semantics.Montague.Ty.s ⇒ Semantics.Montague.Ty.e)

structure Semantics.Montague.Model : Type 1

• Entity : Type
• World : Type
• decEq : DecidableEq self.Entity

def Semantics.Montague.Model.interpTy (m : Model) : Ty → Type

Interpretation of types in a model.

Equations

• m.interpTy Semantics.Montague.Ty.e = m.Entity
• m.interpTy Semantics.Montague.Ty.t = Bool
• m.interpTy Semantics.Montague.Ty.s = m.World
• m.interpTy (a ⇒ a_1) = (m.interpTy a → m.interpTy a_1)

inductive Semantics.Montague.ToyEntity : Type

• john : ToyEntity
• mary : ToyEntity
• pizza : ToyEntity
• book : ToyEntity

instance Semantics.Montague.instReprToyEntity : Repr ToyEntity

Equations

• Semantics.Montague.instReprToyEntity = { reprPrec := Semantics.Montague.instReprToyEntity.repr }

def Semantics.Montague.instReprToyEntity.repr : ToyEntity → ℕ → Std.Format

Equations

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

instance Semantics.Montague.instDecidableEqToyEntity : DecidableEq ToyEntity

Equations

• Semantics.Montague.instDecidableEqToyEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Montague.toyModel : Model

Equations

• Semantics.Montague.toyModel = { Entity := Semantics.Montague.ToyEntity, decEq := inferInstance }

structure Semantics.Montague.LexEntry (m : Model) : Type

• ty : Ty
• denot : m.interpTy self.ty

def Semantics.Montague.Lexicon (m : Model) : Type

Equations

• Semantics.Montague.Lexicon m = (String → Option (Semantics.Montague.LexEntry m))

def Semantics.Montague.ToyLexicon.john_sem : toyModel.interpTy Ty.e

Equations

• Semantics.Montague.ToyLexicon.john_sem = Semantics.Montague.ToyEntity.john

def Semantics.Montague.ToyLexicon.mary_sem : toyModel.interpTy Ty.e

Equations

• Semantics.Montague.ToyLexicon.mary_sem = Semantics.Montague.ToyEntity.mary

def Semantics.Montague.ToyLexicon.sleeps_sem : toyModel.interpTy (Ty.e ⇒ Ty.t)

Equations

• Semantics.Montague.ToyLexicon.sleeps_sem Semantics.Montague.ToyEntity.john = true
• Semantics.Montague.ToyLexicon.sleeps_sem Semantics.Montague.ToyEntity.mary = false
• Semantics.Montague.ToyLexicon.sleeps_sem x = false

def Semantics.Montague.ToyLexicon.laughs_sem : toyModel.interpTy (Ty.e ⇒ Ty.t)

Equations

• Semantics.Montague.ToyLexicon.laughs_sem Semantics.Montague.ToyEntity.john = true
• Semantics.Montague.ToyLexicon.laughs_sem Semantics.Montague.ToyEntity.mary = true
• Semantics.Montague.ToyLexicon.laughs_sem x = false

def Semantics.Montague.ToyLexicon.sees_sem : toyModel.interpTy (Ty.e ⇒ Ty.e ⇒ Ty.t)

Equations

• Semantics.Montague.ToyLexicon.sees_sem Semantics.Montague.ToyEntity.mary Semantics.Montague.ToyEntity.john = true
• Semantics.Montague.ToyLexicon.sees_sem Semantics.Montague.ToyEntity.john Semantics.Montague.ToyEntity.mary = true
• Semantics.Montague.ToyLexicon.sees_sem obj subj = false

def Semantics.Montague.ToyLexicon.eats_sem : toyModel.interpTy (Ty.e ⇒ Ty.e ⇒ Ty.t)

Equations

• Semantics.Montague.ToyLexicon.eats_sem Semantics.Montague.ToyEntity.pizza Semantics.Montague.ToyEntity.john = true
• Semantics.Montague.ToyLexicon.eats_sem Semantics.Montague.ToyEntity.pizza Semantics.Montague.ToyEntity.mary = true
• Semantics.Montague.ToyLexicon.eats_sem obj subj = false

def Semantics.Montague.ToyLexicon.reads_sem : toyModel.interpTy (Ty.e ⇒ Ty.e ⇒ Ty.t)

Equations

• Semantics.Montague.ToyLexicon.reads_sem Semantics.Montague.ToyEntity.book Semantics.Montague.ToyEntity.john = true
• Semantics.Montague.ToyLexicon.reads_sem Semantics.Montague.ToyEntity.book Semantics.Montague.ToyEntity.mary = true
• Semantics.Montague.ToyLexicon.reads_sem obj subj = false

def Semantics.Montague.ToyLexicon.pizza_sem : toyModel.interpTy (Ty.e ⇒ Ty.t)

Equations

• Semantics.Montague.ToyLexicon.pizza_sem Semantics.Montague.ToyEntity.pizza = true
• Semantics.Montague.ToyLexicon.pizza_sem x = false

def Semantics.Montague.ToyLexicon.book_sem : toyModel.interpTy (Ty.e ⇒ Ty.t)

Equations

• Semantics.Montague.ToyLexicon.book_sem Semantics.Montague.ToyEntity.book = true
• Semantics.Montague.ToyLexicon.book_sem x = false

def Semantics.Montague.apply {m : Model} {σ τ : Ty} (f : m.interpTy (σ ⇒ τ)) (x : m.interpTy σ) : m.interpTy τ

Equations

• Semantics.Montague.apply f x = f x

structure Semantics.Montague.SemanticDeriv (m : Model) : Type

• words : List Word
• ty : Ty
• meaning : m.interpTy self.ty

def Semantics.Montague.interpSV (m : Model) (subj : m.interpTy Ty.e) (verb : m.interpTy (Ty.e ⇒ Ty.t)) : m.interpTy Ty.t

Equations

• Semantics.Montague.interpSV m subj verb = Semantics.Montague.apply verb subj

def Semantics.Montague.interpSVO (m : Model) (subj : m.interpTy Ty.e) (verb : m.interpTy (Ty.e ⇒ Ty.e ⇒ Ty.t)) (obj : m.interpTy Ty.e) : m.interpTy Ty.t

Equations

• Semantics.Montague.interpSVO m subj verb obj = Semantics.Montague.apply (Semantics.Montague.apply verb obj) subj

def Semantics.Montague.neg {m : Model} (p : m.interpTy Ty.t) : m.interpTy Ty.t

Sentence negation. See Core.Proposition.Decidable.pnot for the world-indexed version with proven DE property.

Equations

• Semantics.Montague.neg p = !p

def Semantics.Montague.conj {m : Model} (p q : m.interpTy Ty.t) : m.interpTy Ty.t

Equations

• Semantics.Montague.conj p q = (p && q)

def Semantics.Montague.disj {m : Model} (p q : m.interpTy Ty.t) : m.interpTy Ty.t

Equations

• Semantics.Montague.disj p q = (p || q)

def Semantics.Montague.interpNegSV (m : Model) (subj : m.interpTy Ty.e) (verb : m.interpTy (Ty.e ⇒ Ty.t)) : m.interpTy Ty.t

Equations

• Semantics.Montague.interpNegSV m subj verb = Semantics.Montague.neg (Semantics.Montague.interpSV m subj verb)

def Semantics.Montague.interpNegSVO (m : Model) (subj : m.interpTy Ty.e) (verb : m.interpTy (Ty.e ⇒ Ty.e ⇒ Ty.t)) (obj : m.interpTy Ty.e) : m.interpTy Ty.t

Equations

• Semantics.Montague.interpNegSVO m subj verb obj = Semantics.Montague.neg (Semantics.Montague.interpSVO m subj verb obj)

def Semantics.Montague.isTrue (m : Model) (meaning : m.interpTy Ty.t) : Prop

Equations

• Semantics.Montague.isTrue m meaning = (meaning = true)

theorem Semantics.Montague.double_negation {m : Model} (p : m.interpTy Ty.t) : neg (neg p) = p

def Semantics.Montague.predicateToSet {m : Model} (p : m.interpTy (Ty.e ⇒ Ty.t)) : Set m.Entity

Convert a predicate e → t to a Set (the extension).

Equations

• Semantics.Montague.predicateToSet p = {x : m.Entity | p x = true}

noncomputable def Semantics.Montague.setToPredicate {m : Model} (s : Set m.Entity) [DecidablePred fun (x : m.Entity) => x ∈ s] : m.interpTy (Ty.e ⇒ Ty.t)

Equations

• Semantics.Montague.setToPredicate s x = if x ∈ s then true else false

def Semantics.Montague.inExtension {m : Model} (p : m.interpTy (Ty.e ⇒ Ty.t)) (x : m.Entity) : Bool

Equations

• Semantics.Montague.inExtension p x = p x

theorem Semantics.Montague.sleeps_extension : predicateToSet ToyLexicon.sleeps_sem = {ToyEntity.john}

theorem Semantics.Montague.laughs_extension : predicateToSet ToyLexicon.laughs_sem = {ToyEntity.john, ToyEntity.mary}

theorem Semantics.Montague.john_in_sleeps : inExtension ToyLexicon.sleeps_sem ToyEntity.john = true

theorem Semantics.Montague.mary_not_in_sleeps : inExtension ToyLexicon.sleeps_sem ToyEntity.mary = false

theorem Semantics.Montague.john_mary_in_laughs : inExtension ToyLexicon.laughs_sem ToyEntity.john = true ∧ inExtension ToyLexicon.laughs_sem ToyEntity.mary = true

def Semantics.Montague.uncurry {m : Model} (f : m.interpTy (Ty.e ⇒ Ty.e ⇒ Ty.t)) : m.Entity × m.Entity → Bool

Equations

• Semantics.Montague.uncurry f (x_1, y) = f y x_1

def Semantics.Montague.curry {m : Model} (r : m.Entity × m.Entity → Bool) : m.interpTy (Ty.e ⇒ Ty.e ⇒ Ty.t)

Equations

• Semantics.Montague.curry r y x = r (x, y)

theorem Semantics.Montague.curry_uncurry {m : Model} (f : m.interpTy (Ty.e ⇒ Ty.e ⇒ Ty.t)) : curry (uncurry f) = f

theorem Semantics.Montague.uncurry_curry {m : Model} (r : m.Entity × m.Entity → Bool) : uncurry (curry r) = r

def Semantics.Montague.seesRelation : ToyEntity × ToyEntity → Bool

Equations

• Semantics.Montague.seesRelation (Semantics.Montague.ToyEntity.john, Semantics.Montague.ToyEntity.mary) = true
• Semantics.Montague.seesRelation (Semantics.Montague.ToyEntity.mary, Semantics.Montague.ToyEntity.john) = true
• Semantics.Montague.seesRelation x✝ = false

theorem Semantics.Montague.sees_uncurry_matches (p : ToyEntity × ToyEntity) : uncurry ToyLexicon.sees_sem p = seesRelation p

Intensional Semantics

World-indexed types for modal semantics, kind reference, etc.

@[reducible, inline]

abbrev Semantics.Montague.IntensionalProp (Entity World : Type) : Type

Equations

• Semantics.Montague.IntensionalProp Entity World = (World → Entity → Bool)

@[reducible, inline]

abbrev Semantics.Montague.Proposition (World : Type) : Type

Equations

• Semantics.Montague.Proposition World = BProp World

@[reducible, inline]

abbrev Semantics.Montague.IntensionalVP (Entity World : Type) : Type

Equations

• Semantics.Montague.IntensionalVP Entity World = (Entity → Semantics.Montague.Proposition World)

def Semantics.Montague.Proposition.neg {World : Type} (p : Proposition World) : Proposition World

Equations

• p.neg w = !p w

def Semantics.Montague.IntensionalVP.neg {Entity World : Type} (vp : IntensionalVP Entity World) : IntensionalVP Entity World

Equations

• vp.neg x w = !vp x w

def Semantics.Montague.IntensionalProp.exists {Entity World : Type} (domain : List Entity) (prop : IntensionalProp Entity World) (vp : IntensionalVP Entity World) : Proposition World

Equations

• Semantics.Montague.IntensionalProp.exists domain prop vp w = domain.any fun (x : Entity) => prop w x && vp x w