structure Semantics.Intensional.IntensionalModel : Type 1

An intensional model extends a Montague model with possible worlds.

The base model provides the domain of entities (shared across worlds). The World type provides indices for evaluating intensions.

• base : Montague.Model

  The underlying extensional model

• World : Type

  The type of possible worlds

• worldDecEq : DecidableEq self.World

  Decidable equality on worlds

instance Semantics.Intensional.instDecidableEqWorld (m : IntensionalModel) : DecidableEq m.World

Make World decidable

Equations

• Semantics.Intensional.instDecidableEqWorld m = m.worldDecEq

@[reducible, inline]

abbrev Semantics.Intensional.Intension (m : IntensionalModel) (τ : Montague.Ty) : Type

An intension is a function from possible worlds to extensions.

Unified with Core.Intension — this is m.World → m.base.interpTy τ.

Equations

• Semantics.Intensional.Intension m τ = Core.Intension m.World (m.base.interpTy τ)

@[reducible, inline]

abbrev Semantics.Intensional.Proposition (m : IntensionalModel) : Type

A proposition is an intension of type t (BProp m.World).

Equations

• Semantics.Intensional.Proposition m = BProp m.World

@[reducible, inline]

abbrev Semantics.Intensional.PropertyIntension (m : IntensionalModel) : Type

A property intension: Core.Intension m.World (Entity → Bool).

Equations

• Semantics.Intensional.PropertyIntension m = Core.Intension m.World (m.base.Entity → Bool)

@[reducible, inline]

abbrev Semantics.Intensional.RelationIntension (m : IntensionalModel) : Type

A relation intension: Core.Intension m.World (Entity → Entity → Bool).

Equations

• Semantics.Intensional.RelationIntension m = Core.Intension m.World (m.base.Entity → m.base.Entity → Bool)

@[reducible, inline]

abbrev Semantics.Intensional.IntensionalModel.interpTyIntensional (m : IntensionalModel) (τ : Montague.Ty) : Type

Full intensional type interpretation (@cite{gallin-1975}). Equivalent to Intension m τ.

Equations

• m.interpTyIntensional τ = Semantics.Intensional.Intension m τ

def Semantics.Intensional.evalAt {m : IntensionalModel} {τ : Montague.Ty} (meaning : Intension m τ) (w : m.World) : m.base.interpTy τ

Evaluate an intension at a world to get its extension. Delegates to Core.Intension.evalAt.

Equations

• Semantics.Intensional.evalAt meaning w = Core.Intension.evalAt meaning w

def Semantics.Intensional.Proposition.evalAt {m : IntensionalModel} (p : Proposition m) (w : m.World) : Bool

Evaluate a proposition at a world

Equations

• p.evalAt w = p w

def Semantics.Intensional.Proposition.trueAt {m : IntensionalModel} (p : Proposition m) (w : m.World) : Prop

Check if a proposition is true at a world

Equations

• p.trueAt w = (p w = true)

structure Semantics.Intensional.IntensionalDerivation (m : IntensionalModel) : Type

An intensional semantic derivation.

Packages a world-parameterized meaning with its surface form and type. This is what RSA needs: a meaning that can be evaluated at any world.

• surface : List String
• ty : Montague.Ty
• meaning : Intension m self.ty

def Semantics.Intensional.IntensionalDerivation.evalAt {m : IntensionalModel} (d : IntensionalDerivation m) (w : m.World) : m.base.interpTy d.ty

Evaluate the derivation at a specific world

Equations

• d.evalAt w = d.meaning w

def Semantics.Intensional.IntensionalDerivation.trueAt {m : IntensionalModel} (d : IntensionalDerivation m) (h : d.ty = Montague.Ty.t) (w : m.World) : Bool

For type t, get the truth value at a world

Equations

• d.trueAt h w = cast ⋯ (d.meaning w)

def Semantics.Intensional.rigid {m : IntensionalModel} {τ : Montague.Ty} (ext : m.base.interpTy τ) : Intension m τ

Lift a constant extension to an intension (rigid designator). Delegates to Core.Intension.rigid.

Equations

• Semantics.Intensional.rigid ext = Core.Intension.rigid ext

def Semantics.Intensional.varying {m : IntensionalModel} {τ : Montague.Ty} (f : m.World → m.base.interpTy τ) : Intension m τ

Create a world-varying intension from a function.

Equations

• Semantics.Intensional.varying f = f

def Semantics.Intensional.someIntensional {m : IntensionalModel} [Fintype m.base.Entity] (P Q : PropertyIntension m) : Proposition m

"Some" with world-varying property: ∃x. P(w)(x) ∧ Q(w)(x)

Equations

• Semantics.Intensional.someIntensional P Q w = decide (∃ (x : m.base.Entity), P w x = true ∧ Q w x = true)

def Semantics.Intensional.everyIntensional {m : IntensionalModel} [Fintype m.base.Entity] (P Q : PropertyIntension m) : Proposition m

"Every" with world-varying property: ∀x. P(w)(x) → Q(w)(x)

Equations

• Semantics.Intensional.everyIntensional P Q w = decide (∀ (x : m.base.Entity), P w x = true → Q w x = true)

def Semantics.Intensional.noIntensional {m : IntensionalModel} [Fintype m.base.Entity] (P Q : PropertyIntension m) : Proposition m

"No" with world-varying property: ¬∃x. P(w)(x) ∧ Q(w)(x)

Equations

• Semantics.Intensional.noIntensional P Q w = decide ¬∃ (x : m.base.Entity), P w x = true ∧ Q w x = true

inductive Semantics.Intensional.ScalarWorld : Type

Worlds for scalar implicature reasoning.

These represent different states of affairs:

• none: No individuals satisfy the predicate
• someNotAll: Some but not all satisfy
• all: All individuals satisfy

• none : ScalarWorld
• someNotAll : ScalarWorld
• all : ScalarWorld

instance Semantics.Intensional.instDecidableEqScalarWorld : DecidableEq ScalarWorld

Equations

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

instance Semantics.Intensional.instReprScalarWorld : Repr ScalarWorld

Equations

• Semantics.Intensional.instReprScalarWorld = { reprPrec := Semantics.Intensional.instReprScalarWorld.repr }

def Semantics.Intensional.instReprScalarWorld.repr : ScalarWorld → ℕ → Std.Format

Equations

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

instance Semantics.Intensional.instInhabitedScalarWorld : Inhabited ScalarWorld

Equations

• Semantics.Intensional.instInhabitedScalarWorld = { default := Semantics.Intensional.instInhabitedScalarWorld.default }

def Semantics.Intensional.instInhabitedScalarWorld.default : ScalarWorld

Equations

• Semantics.Intensional.instInhabitedScalarWorld.default = Semantics.Intensional.ScalarWorld.none

def Semantics.Intensional.scalarModel : IntensionalModel

A simple intensional model for scalar implicatures. Uses ToyEntity as the domain.

Equations

• Semantics.Intensional.scalarModel = { base := Semantics.Montague.toyModel, World := Semantics.Intensional.ScalarWorld, worldDecEq := inferInstance }

instance Semantics.Intensional.scalarModelFinite : Fintype scalarModel.base.Entity

Fintype instance for scalarModel.base

Equations

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

def Semantics.Intensional.students_rigid : PropertyIntension scalarModel

"Students" is a rigid property (doesn't vary by world). In the toy model, John and Mary are students.

Equations

• Semantics.Intensional.students_rigid x✝ = Semantics.Lexical.Determiner.Quantifier.student_sem

def Semantics.Intensional.sleep_varying : PropertyIntension scalarModel

"Sleep" varies by world:

• none: nobody sleeps
• someNotAll: only John sleeps
• all: both John and Mary sleep

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Intensional.sleep_varying Semantics.Intensional.ScalarWorld.none = fun (x : Semantics.Intensional.scalarModel.base.Entity) => false

def Semantics.Intensional.someStudentsSleep_intensional : IntensionalDerivation scalarModel

"Some students sleep" as an intensional derivation.

Meaning varies by world:

• none: false (no students sleep)
• someNotAll: true (John sleeps)
• all: true (both sleep)

Equations

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

def Semantics.Intensional.everyStudentsSleep_intensional : IntensionalDerivation scalarModel

"Every student sleeps" as an intensional derivation.

Meaning varies by world:

• none: false (not all students sleep)
• someNotAll: false (Mary doesn't sleep)
• all: true (both sleep)

Equations

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

def Semantics.Intensional.someStudentsSleep_at (w : ScalarWorld) : Bool

Helper: directly evaluate "some students sleep" at a world

Equations

• Semantics.Intensional.someStudentsSleep_at w = Semantics.Intensional.someStudentsSleep_intensional.meaning w

def Semantics.Intensional.everyStudentsSleep_at (w : ScalarWorld) : Bool

Helper: directly evaluate "every student sleeps" at a world

Equations

• Semantics.Intensional.everyStudentsSleep_at w = Semantics.Intensional.everyStudentsSleep_intensional.meaning w

theorem Semantics.Intensional.some_false_at_none : someStudentsSleep_at ScalarWorld.none = false

"Some students sleep" is false when no one sleeps

theorem Semantics.Intensional.some_true_at_someNotAll : someStudentsSleep_at ScalarWorld.someNotAll = true

"Some students sleep" is true when some but not all sleep

theorem Semantics.Intensional.some_true_at_all : someStudentsSleep_at ScalarWorld.all = true

"Some students sleep" is true when all sleep

theorem Semantics.Intensional.every_false_at_none : everyStudentsSleep_at ScalarWorld.none = false

"Every student sleeps" is false when no one sleeps

theorem Semantics.Intensional.every_false_at_someNotAll : everyStudentsSleep_at ScalarWorld.someNotAll = false

"Every student sleeps" is false when some but not all sleep

theorem Semantics.Intensional.every_true_at_all : everyStudentsSleep_at ScalarWorld.all = true

"Every student sleeps" is true when all sleep

def Semantics.Intensional.phi {m : IntensionalModel} (d : IntensionalDerivation m) (h : d.ty = Montague.Ty.t) (w : m.World) : Bool

The literal semantics function φ for RSA.

This is the key connection: RSA's φ(u, w) is just evaluating the intensional meaning at world w.

φ(u, w) = ⟦u⟧(w)

Equations

• Semantics.Intensional.phi d h w = d.trueAt h w

theorem Semantics.Intensional.phi_def {m : IntensionalModel} (d : IntensionalDerivation m) (h : d.ty = Montague.Ty.t) (w : m.World) : phi d h w = d.trueAt h w

Theorem: φ is definitionally equal to evaluating the meaning at the world.

Note: d.evalAt w has type m.base.interpTy d.ty, which equals Bool when d.ty =.t. The phi function handles this type coercion.