Montague (1973) intensional examples [Mon73]

Toy examples in Montague's PTQ-style intensional logic:

• Hesperus/Phosphorus puzzle (co-reference vs co-intension)
• Belief contexts and substitution failure
• De dicto vs de re readings

Uses the infrastructure from Semantics/Intensional/Examples.lean.

@[reducible, inline]

abbrev Montague1973Attitudes.World : Type

Equations

• Montague1973Attitudes.World = Fin 4

inductive Montague1973Attitudes.ToyIEntity : Type

A small domain for examples

• john : ToyIEntity
• mary : ToyIEntity
• hesperus : ToyIEntity
• phosphorus : ToyIEntity

@[implicit_reducible]

instance Montague1973Attitudes.instReprToyIEntity : Repr ToyIEntity

Equations

• Montague1973Attitudes.instReprToyIEntity = { reprPrec := Montague1973Attitudes.instReprToyIEntity.repr }

def Montague1973Attitudes.instReprToyIEntity.repr : ToyIEntity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Montague1973Attitudes.instDecidableEqToyIEntity : DecidableEq ToyIEntity

Equations

• Montague1973Attitudes.instDecidableEqToyIEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Montague1973Attitudes.sleeps : Intensional.Denot ToyIEntity World (Intensional.Ty.e ⇒ Intensional.Ty.t).intens

"sleeps" as a world-dependent property.

Equations

• Montague1973Attitudes.sleeps 0 Montague1973Attitudes.ToyIEntity.john = True
• Montague1973Attitudes.sleeps 1 Montague1973Attitudes.ToyIEntity.mary = True
• Montague1973Attitudes.sleeps 2 Montague1973Attitudes.ToyIEntity.john = True
• Montague1973Attitudes.sleeps 2 Montague1973Attitudes.ToyIEntity.mary = True
• Montague1973Attitudes.sleeps w x = False

def Montague1973Attitudes.happy : Intensional.Denot ToyIEntity World (Intensional.Ty.e ⇒ Intensional.Ty.t).intens

"is happy" as a world-dependent property.

Equations

• Montague1973Attitudes.happy 0 Montague1973Attitudes.ToyIEntity.john = True
• Montague1973Attitudes.happy 0 Montague1973Attitudes.ToyIEntity.mary = True
• Montague1973Attitudes.happy 1 Montague1973Attitudes.ToyIEntity.mary = True
• Montague1973Attitudes.happy 2 Montague1973Attitudes.ToyIEntity.john = True
• Montague1973Attitudes.happy w x = False

def Montague1973Attitudes.morningStar : Intensional.Denot ToyIEntity World Intensional.Ty.indConcept

"the morning star" - an individual concept that picks out potentially different individuals in different worlds.

Equations

• Montague1973Attitudes.morningStar 0 = Montague1973Attitudes.ToyIEntity.hesperus
• Montague1973Attitudes.morningStar 1 = Montague1973Attitudes.ToyIEntity.hesperus
• Montague1973Attitudes.morningStar 2 = Montague1973Attitudes.ToyIEntity.phosphorus
• Montague1973Attitudes.morningStar 3 = Montague1973Attitudes.ToyIEntity.hesperus

def Montague1973Attitudes.eveningStar : Intensional.Denot ToyIEntity World Intensional.Ty.indConcept

"the evening star" - another individual concept

Equations

• Montague1973Attitudes.eveningStar 0 = Montague1973Attitudes.ToyIEntity.hesperus
• Montague1973Attitudes.eveningStar 1 = Montague1973Attitudes.ToyIEntity.phosphorus
• Montague1973Attitudes.eveningStar 2 = Montague1973Attitudes.ToyIEntity.hesperus
• Montague1973Attitudes.eveningStar 3 = Montague1973Attitudes.ToyIEntity.hesperus

theorem Montague1973Attitudes.extensions_equal_at_w0 : Intensional.down morningStar 0 = Intensional.down eveningStar 0

In the actual world (w0), morning star = evening star. But their INTENSIONS differ (they pick out different things in other worlds).

theorem Montague1973Attitudes.intensions_differ : morningStar ≠ eveningStar

def Montague1973Attitudes.believes_access : ToyIEntity → World → World → Bool

Doxastic accessibility relation: which worlds are compatible with what an agent believes. R(a, w, w') means w' is compatible with what a believes in w.

Equations

• Montague1973Attitudes.believes_access Montague1973Attitudes.ToyIEntity.john 0 0 = true
• Montague1973Attitudes.believes_access Montague1973Attitudes.ToyIEntity.john 0 2 = true
• Montague1973Attitudes.believes_access Montague1973Attitudes.ToyIEntity.mary 0 1 = true
• Montague1973Attitudes.believes_access Montague1973Attitudes.ToyIEntity.mary 0 2 = true
• Montague1973Attitudes.believes_access x✝² x✝¹ x✝ = (x✝¹ == x✝)

def Montague1973Attitudes.believe : Intensional.Denot ToyIEntity World (Intensional.Ty.e ⇒ Intensional.Ty.prop ⇒ Intensional.Ty.t)

"believe" as an attitude verb. ⟦believe⟧(a)(p)(w) = ∀w'. R(a,w,w') → p(w')

Equations

• Montague1973Attitudes.believe agent prop = ∀ (w' : Montague1973Attitudes.World), Montague1973Attitudes.believes_access agent 0 w' = true → prop w'

def Montague1973Attitudes.believeAt : World → Intensional.Denot ToyIEntity World (Intensional.Ty.e ⇒ Intensional.Ty.prop ⇒ Intensional.Ty.t)

Extended believe that's world-dependent.

Equations

• Montague1973Attitudes.believeAt evalWorld agent prop = ∀ (w' : Montague1973Attitudes.World), Montague1973Attitudes.believes_access agent evalWorld w' = true → prop w'

def Montague1973Attitudes.johnBelievesMary_deDicto : Intensional.Denot ToyIEntity World Intensional.Ty.t

"John believes Mary sleeps" (de dicto)

Equations

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

theorem Montague1973Attitudes.johnDoesNotBelieveMarySleeps : ¬johnBelievesMary_deDicto

John does NOT believe Mary sleeps: Mary doesn't sleep in w0 (John's accessible world).

def Montague1973Attitudes.johnBelievesJohnSleeps : Intensional.Denot ToyIEntity World Intensional.Ty.t

"John believes John sleeps" (de dicto)

Equations

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

theorem Montague1973Attitudes.johnBelievesJohnSleeps_true : johnBelievesJohnSleeps

John believes he sleeps: he sleeps in both w0 and w2.

def Montague1973Attitudes.someCookies : Intensional.Denot ToyIEntity World Intensional.Ty.prop

Proposition: "John ate some cookies" (simplified)

Equations

• Montague1973Attitudes.someCookies x✝ = True

def Montague1973Attitudes.allCookies : Intensional.Denot ToyIEntity World Intensional.Ty.prop

Proposition: "John ate all cookies" (simplified)

Equations

• Montague1973Attitudes.allCookies 0 = True
• Montague1973Attitudes.allCookies 1 = True
• Montague1973Attitudes.allCookies 2 = False
• Montague1973Attitudes.allCookies 3 = False

def Montague1973Attitudes.maryBelievesSome : Intensional.Denot ToyIEntity World Intensional.Ty.t

"Mary believes John ate some cookies"

Equations

• Montague1973Attitudes.maryBelievesSome = Montague1973Attitudes.believe Montague1973Attitudes.ToyIEntity.mary Montague1973Attitudes.someCookies

def Montague1973Attitudes.maryBelievesAll : Intensional.Denot ToyIEntity World Intensional.Ty.t

"Mary believes John ate all cookies"

Equations

• Montague1973Attitudes.maryBelievesAll = Montague1973Attitudes.believe Montague1973Attitudes.ToyIEntity.mary Montague1973Attitudes.allCookies

theorem Montague1973Attitudes.maryBelievesSome_true : maryBelievesSome

Mary believes John ate some cookies (trivially true proposition).

theorem Montague1973Attitudes.belief_intensional : Intensional.down morningStar 0 = Intensional.down eveningStar 0 ∧ morningStar ≠ eveningStar

Belief is intensional: co-extensional expressions can differ under belief.

theorem Montague1973Attitudes.up_down_identity {E W : Type} {τ : Intensional.Ty} (x : Intensional.Denot E W τ) (w : W) : Intensional.down (Intensional.up x) w = x

Up-down identity: applying down after up returns the original value.

Bridge to Direct Reference Theory

The morningStar/eveningStar individual concepts defined above are Fregean concepts (world-dependent). In contrast, proper names in Semantics.Reference.Basic are Kripkean rigid designators.

This section makes the distinction explicit, connecting the existing Hesperus/Phosphorus examples to the direct reference framework.

def Montague1973Attitudes.hesperus_rigid : Intensional.Intension World ToyIEntity

"Hesperus" as a Kripkean proper name: rigid designator.

Contrast with morningStar above, which is a Fregean individual concept that varies across worlds. The proper name always returns .hesperus.

Equations

• Montague1973Attitudes.hesperus_rigid = Intensional.Intension.rigid Montague1973Attitudes.ToyIEntity.hesperus

theorem Montague1973Attitudes.morningStar_not_rigid : ¬Intensional.Intension.IsRigid morningStar

morningStar is NOT rigid: it picks out different entities at different worlds. This contrasts with hesperus_rigid which IS rigid.

theorem Montague1973Attitudes.hesperus_rigid_isRigid : hesperus_rigid.IsRigid

hesperus_rigid IS rigid (a proper name in the Kripkean sense).

theorem Montague1973Attitudes.name_vs_concept_independence : hesperus_rigid.CoRefer morningStar 0 ∧ ¬hesperus_rigid.CoExtensional morningStar

Independence of names vs concepts: a Fregean individual concept (morningStar) can agree with a Kripkean name (hesperus_rigid) at one world while diverging at others.