@[reducible, inline]

abbrev Semantics.Attitudes.Intensional.World : Type

Canonical 4-world type for modal examples. Alias for Core.Proposition.World4.

Equations

• Semantics.Attitudes.Intensional.World = Core.Proposition.World4

def Semantics.Attitudes.Intensional.allWorlds : List World

List of all worlds.

Equations

• Semantics.Attitudes.Intensional.allWorlds = Core.Proposition.FiniteWorlds.worlds

Intension Types

@[reducible, inline]

abbrev Semantics.Attitudes.Intensional.Ty.intens (τ : Montague.Ty) : Montague.Ty

Shorthand for intension type (s ⇒ τ)

Equations

• Semantics.Attitudes.Intensional.Ty.intens τ = (Semantics.Montague.Ty.s ⇒ τ)

@[reducible, inline]

abbrev Semantics.Attitudes.Intensional.Ty.prop : Montague.Ty

Proposition type: intension of truth values

Equations

• Semantics.Attitudes.Intensional.Ty.prop = Semantics.Attitudes.Intensional.Ty.intens Semantics.Montague.Ty.t

@[reducible, inline]

abbrev Semantics.Attitudes.Intensional.Ty.indConcept : Montague.Ty

Individual concept: intension of entities

Equations

• Semantics.Attitudes.Intensional.Ty.indConcept = Semantics.Attitudes.Intensional.Ty.intens Semantics.Montague.Ty.e

Intensional Models

structure Semantics.Attitudes.Intensional.IModel : Type 1

An intensional model specifies an entity domain.

• Entity : Type

  The domain of entities

• decEq : DecidableEq self.Entity

  Decidable equality on entities

def Semantics.Attitudes.Intensional.IModel.interpTy (m : IModel) : Montague.Ty → Type

Interpretation of types in an intensional model

Equations

• m.interpTy Semantics.Montague.Ty.e = m.Entity
• m.interpTy Semantics.Montague.Ty.t = Bool
• m.interpTy Semantics.Montague.Ty.s = Semantics.Attitudes.Intensional.World
• m.interpTy (σ ⇒ τ) = (m.interpTy σ → m.interpTy τ)

Up/Down Operators

def Semantics.Attitudes.Intensional.up {m : IModel} {τ : Montague.Ty} (x : m.interpTy τ) : m.interpTy (Ty.intens τ)

The "up" operator (^): convert extension to intension (constant function). In Montague's notation: ^α is the intension of α.

Equations

• Semantics.Attitudes.Intensional.up x x✝ = x

def Semantics.Attitudes.Intensional.down {m : IModel} {τ : Montague.Ty} (f : m.interpTy (Ty.intens τ)) (w : World) : m.interpTy τ

The "down" operator (ˇ): evaluate intension at a world. In Montague's notation: ˇα is the extension of α at the evaluation world.

Equations

• Semantics.Attitudes.Intensional.down f w = f w

theorem Semantics.Attitudes.Intensional.up_eq_rigid {m : IModel} {τ : Montague.Ty} (x : m.interpTy τ) : up x = Core.Intension.rigid x

The up operator equals Core.Intension.rigid.

theorem Semantics.Attitudes.Intensional.down_eq_evalAt {m : IModel} {τ : Montague.Ty} (f : m.interpTy (Ty.intens τ)) (w : World) : down f w = Core.Intension.evalAt f w

The down operator equals Core.Intension.evalAt.