Montague (1973) intensional examples @cite{montague-1973}

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 Core/Logic/Intensional/Examples.lean.

@[reducible, inline]

abbrev Phenomena.Attitudes.Studies.Montague1973.World : Type

Equations

• Phenomena.Attitudes.Studies.Montague1973.World = Fin 4

inductive Phenomena.Attitudes.Studies.Montague1973.ToyIEntity : Type

A small domain for examples

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

@[implicit_reducible]

instance Phenomena.Attitudes.Studies.Montague1973.instReprToyIEntity : Repr ToyIEntity

Equations

• Phenomena.Attitudes.Studies.Montague1973.instReprToyIEntity = { reprPrec := Phenomena.Attitudes.Studies.Montague1973.instReprToyIEntity.repr }

def Phenomena.Attitudes.Studies.Montague1973.instReprToyIEntity.repr : ToyIEntity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Attitudes.Studies.Montague1973.instDecidableEqToyIEntity : DecidableEq ToyIEntity

Equations

• Phenomena.Attitudes.Studies.Montague1973.instDecidableEqToyIEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Attitudes.Studies.Montague1973.toyIFrame : Core.Logic.Intensional.Frame

Equations

• Phenomena.Attitudes.Studies.Montague1973.toyIFrame = { Entity := Phenomena.Attitudes.Studies.Montague1973.ToyIEntity, Index := Phenomena.Attitudes.Studies.Montague1973.World }

def Phenomena.Attitudes.Studies.Montague1973.sleeps : toyIFrame.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t).intens

"sleeps" as a world-dependent property.

Equations

• Phenomena.Attitudes.Studies.Montague1973.sleeps 0 Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.john = True
• Phenomena.Attitudes.Studies.Montague1973.sleeps 1 Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.mary = True
• Phenomena.Attitudes.Studies.Montague1973.sleeps 2 Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.john = True
• Phenomena.Attitudes.Studies.Montague1973.sleeps 2 Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.mary = True
• Phenomena.Attitudes.Studies.Montague1973.sleeps w x = False

def Phenomena.Attitudes.Studies.Montague1973.happy : toyIFrame.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t).intens

"is happy" as a world-dependent property.

Equations

• Phenomena.Attitudes.Studies.Montague1973.happy 0 Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.john = True
• Phenomena.Attitudes.Studies.Montague1973.happy 0 Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.mary = True
• Phenomena.Attitudes.Studies.Montague1973.happy 1 Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.mary = True
• Phenomena.Attitudes.Studies.Montague1973.happy 2 Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.john = True
• Phenomena.Attitudes.Studies.Montague1973.happy w x = False

def Phenomena.Attitudes.Studies.Montague1973.morningStar : toyIFrame.Denot Core.Logic.Intensional.Ty.indConcept

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

Equations

• Phenomena.Attitudes.Studies.Montague1973.morningStar 0 = Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.hesperus
• Phenomena.Attitudes.Studies.Montague1973.morningStar 1 = Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.hesperus
• Phenomena.Attitudes.Studies.Montague1973.morningStar 2 = Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.phosphorus
• Phenomena.Attitudes.Studies.Montague1973.morningStar 3 = Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.hesperus

def Phenomena.Attitudes.Studies.Montague1973.eveningStar : toyIFrame.Denot Core.Logic.Intensional.Ty.indConcept

"the evening star" - another individual concept

Equations

• Phenomena.Attitudes.Studies.Montague1973.eveningStar 0 = Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.hesperus
• Phenomena.Attitudes.Studies.Montague1973.eveningStar 1 = Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.phosphorus
• Phenomena.Attitudes.Studies.Montague1973.eveningStar 2 = Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.hesperus
• Phenomena.Attitudes.Studies.Montague1973.eveningStar 3 = Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.hesperus

theorem Phenomena.Attitudes.Studies.Montague1973.extensions_equal_at_w0 : Core.Logic.Intensional.down morningStar 0 = Core.Logic.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 Phenomena.Attitudes.Studies.Montague1973.intensions_differ : morningStar ≠ eveningStar

def Phenomena.Attitudes.Studies.Montague1973.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

• Phenomena.Attitudes.Studies.Montague1973.believes_access Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.john 0 0 = true
• Phenomena.Attitudes.Studies.Montague1973.believes_access Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.john 0 2 = true
• Phenomena.Attitudes.Studies.Montague1973.believes_access Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.mary 0 1 = true
• Phenomena.Attitudes.Studies.Montague1973.believes_access Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.mary 0 2 = true
• Phenomena.Attitudes.Studies.Montague1973.believes_access x✝² x✝¹ x✝ = (x✝¹ == x✝)

def Phenomena.Attitudes.Studies.Montague1973.believe : toyIFrame.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.prop ⇒ Core.Logic.Intensional.Ty.t)

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

Equations

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

def Phenomena.Attitudes.Studies.Montague1973.believeAt : World → toyIFrame.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.prop ⇒ Core.Logic.Intensional.Ty.t)

Extended believe that's world-dependent.

Equations

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

def Phenomena.Attitudes.Studies.Montague1973.johnBelievesMary_deDicto : toyIFrame.Denot Core.Logic.Intensional.Ty.t

"John believes Mary sleeps" (de dicto)

Equations

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

theorem Phenomena.Attitudes.Studies.Montague1973.johnDoesNotBelieveMarySleeps : ¬johnBelievesMary_deDicto

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

def Phenomena.Attitudes.Studies.Montague1973.johnBelievesJohnSleeps : toyIFrame.Denot Core.Logic.Intensional.Ty.t

"John believes John sleeps" (de dicto)

Equations

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

theorem Phenomena.Attitudes.Studies.Montague1973.johnBelievesJohnSleeps_true : johnBelievesJohnSleeps

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

def Phenomena.Attitudes.Studies.Montague1973.someCookies : toyIFrame.Denot Core.Logic.Intensional.Ty.prop

Proposition: "John ate some cookies" (simplified)

Equations

• Phenomena.Attitudes.Studies.Montague1973.someCookies x✝ = True

def Phenomena.Attitudes.Studies.Montague1973.allCookies : toyIFrame.Denot Core.Logic.Intensional.Ty.prop

Proposition: "John ate all cookies" (simplified)

Equations

• Phenomena.Attitudes.Studies.Montague1973.allCookies 0 = True
• Phenomena.Attitudes.Studies.Montague1973.allCookies 1 = True
• Phenomena.Attitudes.Studies.Montague1973.allCookies 2 = False
• Phenomena.Attitudes.Studies.Montague1973.allCookies 3 = False

def Phenomena.Attitudes.Studies.Montague1973.maryBelievesSome : toyIFrame.Denot Core.Logic.Intensional.Ty.t

"Mary believes John ate some cookies"

Equations

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

def Phenomena.Attitudes.Studies.Montague1973.maryBelievesAll : toyIFrame.Denot Core.Logic.Intensional.Ty.t

"Mary believes John ate all cookies"

Equations

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

theorem Phenomena.Attitudes.Studies.Montague1973.maryBelievesSome_true : maryBelievesSome

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

theorem Phenomena.Attitudes.Studies.Montague1973.belief_intensional : Core.Logic.Intensional.down morningStar 0 = Core.Logic.Intensional.down eveningStar 0 ∧ morningStar ≠ eveningStar

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

theorem Phenomena.Attitudes.Studies.Montague1973.up_down_identity {F : Core.Logic.Intensional.Frame} {τ : Core.Logic.Intensional.Ty} (x : F.Denot τ) (w : F.Index) : Core.Logic.Intensional.down (Core.Logic.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 Phenomena.Attitudes.Studies.Montague1973.hesperus_rigid : Core.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

• Phenomena.Attitudes.Studies.Montague1973.hesperus_rigid = Core.Intension.rigid Phenomena.Attitudes.Studies.Montague1973.ToyIEntity.hesperus

theorem Phenomena.Attitudes.Studies.Montague1973.morningStar_not_rigid : ¬Core.Intension.IsRigid morningStar

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

theorem Phenomena.Attitudes.Studies.Montague1973.hesperus_rigid_isRigid : hesperus_rigid.IsRigid

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

theorem Phenomena.Attitudes.Studies.Montague1973.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.