Cooper (2023) Ch. 6 — Modality and Intensionality without Possible Worlds

@cite{cooper-2023} @cite{austin-1961} @cite{barwise-1989} @cite{kratzer-1991}

@cite{cooper-2023} Chapter 6 extends the modal type system framework from Ch1 with Prop-valued modal systems, topoi (replacing accessibility relations), Box/Diamond type constructors, Austinian/Russellian propositions, believe/know via long-term memory, points of view, and intensional transitive verbs.

This study formalises Ch. 6 directly. It was formerly substrate at Theories/Semantics/TypeTheoretic/Modality.lean but is genuinely a single-paper Cooper-textbook replication: only ChatzikyriakidisEtAl2025 (intentional identity) consumed it externally.

Layer 2 — Semantics: ModalSystem (Ch6, Prop) + bridge to ModalTypeSystem (Ch1, Bool), Topos ≃ Parametric Type (unified), NecTopos, PossTopos, Box/Diamond.

Bridges:

• ModalTypeSystem ↔ ModalSystem (Bool ↔ Prop)
• ModalSystem ↔ AccessRel (Kripke accessibility)
• know = believe + veridicality (abstract doxastic bridge)
• Topos → induced necessity/possibility (abstract Kratzer bridge)

§ 6.2–6.3 Modal type systems — extended

Chapter 1 introduced ModalTypeSystem (Def 54) with Bool-valued predicate assignments. Chapter 6 builds on this with four modal notions, each in restrictive (all possibilities share the type) and inclusive (some possibility has the type) variants.

A modal system of complex types TYPE_MC is a family of type systems indexed by "possibilities" where basic types and predicates are shared but witness assignments vary. §6.3, (1)–(4).

structure Phenomena.Modality.Studies.Cooper2023.Possibility (Ty Obj : Type) : Type

A possibility in a modal type system: an assignment of witnesses to types. Each possibility maps types (represented as Ty) to their set of witnesses. §6.3: possibilities differ in which objects witness which types.

The available field tracks which types are recognized in this possibility. Not every type need exist in every possibility — a type can be absent from a possibility entirely, which is distinct from being present but unwitnessed. This distinction is what separates inclusive from restrictive modal notions.

• available : Ty → Prop

  Which types are recognized (available) in this possibility. A type may be available without having witnesses (empty extension).

• witnesses : Ty → Obj → Prop

  Whether object a witnesses type T in this possibility

structure Phenomena.Modality.Studies.Cooper2023.ModalSystem (Ty Obj : Type) : Type 1

A modal system of complex types: a family of possibilities. §6.3, Def A9: TYPE_MC = ⟨Type_M, BType, ⟨PType_M⟩,...⟩_{M ∈ M}. The possibilities share the same types but differ in witness assignments.

• Poss : Type

  The index type for possibilities

• poss : self.Poss → Possibility Ty Obj

  The family of possibilities

def Phenomena.Modality.Studies.Cooper2023.ModalSystem.hasType {Ty Obj : Type} (ms : ModalSystem Ty Obj) (p : ms.Poss) (T : Ty) : Prop

Whether type T is available (recognized) in possibility p. §6.3: T ∈ Type_M means T is a type in the system associated with M.

Equations

• ms.hasType p T = (ms.poss p).available T

def Phenomena.Modality.Studies.Cooper2023.ModalSystem.ext {Ty Obj : Type} (ms : ModalSystem Ty Obj) (p : ms.Poss) (T : Ty) : Obj → Prop

Extension of a type in a possibility: the set of witnesses. §6.3, (1a): {a | a :{TYPE{M_i}} T}.

Equations

• ms.ext p T = (ms.poss p).witnesses T

Restrictive modal notions (§6.3, (1)/(3))

These quantify over ALL possibilities.

def Phenomena.Modality.Studies.Cooper2023.nec_equiv_r {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T₁ T₂ : Ty) : Prop

Restrictive necessary equivalence: T₁ ≈_r T₂ iff they have the same extension in all possibilities. §6.3, (1a).

Equations

• Phenomena.Modality.Studies.Cooper2023.nec_equiv_r ms T₁ T₂ = ∀ (p : ms.Poss), ms.ext p T₁ = ms.ext p T₂

def Phenomena.Modality.Studies.Cooper2023.nec_subtype_r {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T₁ T₂ : Ty) : Prop

Restrictive subtype: T₁ ⊑_r T₂ iff T₁'s extension ⊆ T₂'s in all possibilities. §6.3, (1b).

Equations

• Phenomena.Modality.Studies.Cooper2023.nec_subtype_r ms T₁ T₂ = ∀ (p : ms.Poss) (a : Obj), ms.ext p T₁ a → ms.ext p T₂ a

def Phenomena.Modality.Studies.Cooper2023.nec_r {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

Restrictive necessity: T is necessary iff it has witnesses in all possibilities. §6.3, (1c).

Equations

• Phenomena.Modality.Studies.Cooper2023.nec_r ms T = ∀ (p : ms.Poss), ∃ (a : Obj), ms.ext p T a

def Phenomena.Modality.Studies.Cooper2023.poss_r {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

Restrictive possibility: T is possible iff it has witnesses in some possibility. §6.3, (1d).

Equations

• Phenomena.Modality.Studies.Cooper2023.poss_r ms T = ∃ (p : ms.Poss) (a : Obj), ms.ext p T a

Inclusive modal notions (§6.3, (2)/(4))

These quantify over possibilities where the type is available (recognized in the type system), not merely over those where it has witnesses. This distinction is the key difference from the previous (buggy) version, which used "has witnesses" as the guard — making nec_i a tautology.

§6.3, (2): "T ∈ Type_M" means the type is available in possibility M, which is strictly weaker than having witnesses there.

def Phenomena.Modality.Studies.Cooper2023.nec_equiv_i {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T₁ T₂ : Ty) : Prop

Inclusive necessary equivalence: T₁ ≈_i T₂ iff for all possibilities where both types are available, they have the same extension. §6.3, (2a).

Equations

• Phenomena.Modality.Studies.Cooper2023.nec_equiv_i ms T₁ T₂ = ∀ (p : ms.Poss), ms.hasType p T₁ → ms.hasType p T₂ → ms.ext p T₁ = ms.ext p T₂

def Phenomena.Modality.Studies.Cooper2023.nec_subtype_i {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T₁ T₂ : Ty) : Prop

Inclusive subtype: T₁ ⊑_i T₂ iff for all possibilities where both are available, T₁'s extension ⊆ T₂'s. §6.3, (2b).

Equations

• Phenomena.Modality.Studies.Cooper2023.nec_subtype_i ms T₁ T₂ = ∀ (p : ms.Poss), ms.hasType p T₁ → ms.hasType p T₂ → ∀ (a : Obj), ms.ext p T₁ a → ms.ext p T₂ a

def Phenomena.Modality.Studies.Cooper2023.nec_i {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

Inclusive necessity: T is necessary iff it has witnesses in all possibilities where T is available. §6.3, (2c).

This is strictly weaker than nec_r: a type can be inclusively necessary without being restrictively necessary, if there are possibilities where the type is simply not available.

Equations

• Phenomena.Modality.Studies.Cooper2023.nec_i ms T = ∀ (p : ms.Poss), ms.hasType p T → ∃ (a : Obj), ms.ext p T a

def Phenomena.Modality.Studies.Cooper2023.poss_i {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

Inclusive possibility: T is possible iff some possibility both has T available and has a witness. §6.3, (2d).

Equations

• Phenomena.Modality.Studies.Cooper2023.poss_i ms T = ∃ (p : ms.Poss), ms.hasType p T ∧ ∃ (a : Obj), ms.ext p T a

theorem Phenomena.Modality.Studies.Cooper2023.restrictive_subtype_implies_inclusive {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T₁ T₂ : Ty) : nec_subtype_r ms T₁ T₂ → nec_subtype_i ms T₁ T₂

Restrictive ⊑_r entails inclusive ⊑_i. §6.3, paragraph after (2): "if any of the restrictive definitions holds... then the corresponding inclusive definition will also hold."

theorem Phenomena.Modality.Studies.Cooper2023.restrictive_nec_implies_inclusive {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : nec_r ms T → nec_i ms T

Restrictive necessity entails inclusive necessity.

theorem Phenomena.Modality.Studies.Cooper2023.poss_i_implies_poss_r {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : poss_i ms T → poss_r ms T

Inclusive possibility implies restrictive possibility (drop the availability condition).

theorem Phenomena.Modality.Studies.Cooper2023.poss_r_implies_poss_i {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) (hcoh : ∀ (p : ms.Poss) (a : Obj), ms.ext p T a → ms.hasType p T) : poss_r ms T → poss_i ms T

Restrictive possibility implies inclusive possibility when witnessing implies availability (the standard coherence condition).

Bridge: ModalTypeSystem (Ch1) ↔ ModalSystem (Ch6)

Ch1's ModalTypeSystem is Bool-valued (finite, decidable). Ch6's ModalSystem is Prop-valued (more general). These conversion functions connect the two formalizations.

def Semantics.TypeTheoretic.ModalTypeSystem.toModalSystem {W Pred : Type} (mts : ModalTypeSystem W Pred) (Obj : Type) : Phenomena.Modality.Studies.Cooper2023.ModalSystem Pred Obj

Embed a Ch1 Bool-valued modal type system into a Ch6 Prop-valued modal system. Each predicate becomes a type; an object witnesses the type iff mts w P = true. All predicates are available in all possibilities (Bool-valued systems don't distinguish availability from witnessing).

Equations

• mts.toModalSystem Obj = { Poss := W, poss := fun (w : W) => { available := fun (x : Pred) => True, witnesses := fun (P : Pred) (x : Obj) => mts w P = true } }

def Phenomena.Modality.Studies.Cooper2023.ModalSystem.toModalTypeSystem {Ty Obj : Type} (ms : ModalSystem Ty Obj) [dec : (p : ms.Poss) → (T : Ty) → Decidable (∃ (a : Obj), ms.ext p T a)] : Semantics.TypeTheoretic.ModalTypeSystem ms.Poss Ty

Project a Ch6 Prop-valued modal system back to Ch1 Bool when witnesses are decidable. Requires a decision procedure for whether each type has a witness.

Equations

• ms.toModalTypeSystem p T = if ∃ (a : Obj), ms.ext p T a then true else false

theorem Semantics.TypeTheoretic.ModalTypeSystem.roundtrip {W Pred : Type} (mts : ModalTypeSystem W Pred) (w : W) (P : Pred) : ((mts.toModalSystem Unit).poss w).witnesses P () ↔ mts w P = true

Roundtrip: embedding then projecting back preserves the Bool-valued system.

Bridge: ModalSystem ↔ Core.Logic.Intensional.BAccessRel

A Cooper modal system induces a Kripke accessibility relation for each type T: R_T(p₁, p₂) holds iff every witness of T in p₁ is also a witness in p₂. This connects TTR's type-indexed modality to standard Kripke semantics.

def Phenomena.Modality.Studies.Cooper2023.ModalSystem.toAccessRel {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : ms.Poss → ms.Poss → Prop

Given a type T, derive a Kripke accessibility relation from a modal system. R_T(p₁, p₂) iff the extension of T at p₂ includes the extension at p₁. This makes □T at p = "T has witnesses in all R_T-accessible possibilities".

Equations

• ms.toAccessRel T p₁ p₂ = ∀ (a : Obj), ms.ext p₁ T a → ms.ext p₂ T a

theorem Phenomena.Modality.Studies.Cooper2023.nec_r_iff_forall_exists {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : nec_r ms T ↔ ∀ (p : ms.Poss), ∃ (a : Obj), ms.ext p T a

TTR necessity (nec_r) for type T is equivalent to: for all possibilities, T has witnesses. This is □T evaluated at the universal frame.

theorem Phenomena.Modality.Studies.Cooper2023.poss_r_iff_exists {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : poss_r ms T ↔ ∃ (p : ms.Poss) (a : Obj), ms.ext p T a

TTR possibility (poss_r) for type T is equivalent to: some possibility has a witness of T. This is ◇T evaluated at the universal frame.

theorem Phenomena.Modality.Studies.Cooper2023.ModalSystem.toAccessRel_refl {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) (p : ms.Poss) : ms.toAccessRel T p p

The derived accessibility relation is reflexive (every possibility includes its own witnesses).

§ 6.4 Box and Diamond type constructors

If T is a type, then □_r T, □_i T, ◇_r T, ◇_i T are types. □T is non-empty iff T is necessary; ◇T is non-empty iff T is possible. §6.4, (5)–(11).

def Phenomena.Modality.Studies.Cooper2023.BoxR {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

Box type (necessity): □T is inhabited iff T is necessary in the modal system. §6.4, (5)–(7). A witness of □T is a proof that T has witnesses in all (restrictive) or relevant (inclusive) possibilities.

Equations

• Phenomena.Modality.Studies.Cooper2023.BoxR ms T = Phenomena.Modality.Studies.Cooper2023.nec_r ms T

def Phenomena.Modality.Studies.Cooper2023.BoxI {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

Equations

• Phenomena.Modality.Studies.Cooper2023.BoxI ms T = Phenomena.Modality.Studies.Cooper2023.nec_i ms T

def Phenomena.Modality.Studies.Cooper2023.DiamondR {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

Diamond type (possibility): ◇T is inhabited iff T is possible. §6.4, (5), (9).

Equations

• Phenomena.Modality.Studies.Cooper2023.DiamondR ms T = Phenomena.Modality.Studies.Cooper2023.poss_r ms T

def Phenomena.Modality.Studies.Cooper2023.DiamondI {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

Equations

• Phenomena.Modality.Studies.Cooper2023.DiamondI ms T = Phenomena.Modality.Studies.Cooper2023.poss_i ms T

theorem Phenomena.Modality.Studies.Cooper2023.BoxR_implies_BoxI {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : BoxR ms T → BoxI ms T

□_r T → □_i T (restrictive box implies inclusive box).

theorem Phenomena.Modality.Studies.Cooper2023.DiamondI_implies_DiamondR {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : DiamondI ms T → DiamondR ms T

◇_i T → ◇_r T (inclusive diamond implies restrictive diamond).

theorem Phenomena.Modality.Studies.Cooper2023.DiamondR_implies_DiamondI {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) (hcoh : ∀ (p : ms.Poss) (a : Obj), ms.ext p T a → ms.hasType p T) : DiamondR ms T → DiamondI ms T

◇_r T → ◇_i T when witnessing implies availability.

theorem Phenomena.Modality.Studies.Cooper2023.BoxR_implies_DiamondR {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) (hne : Nonempty ms.Poss) : BoxR ms T → DiamondR ms T

□_r T → ◇_r T when the modal system has at least one possibility. The D axiom of modal logic.

§ 6.4 Topoi

A topos maps situations (of a background type) to types (the foreground). Topoi replace accessibility relations between possible worlds: they encode rules (epistemic, deontic) that license inferences from situations to types.

§6.4, (20): τ : Topos has bg : Type and fg : (bg → Type). τ(s) = τ.fg(s).

@[reducible, inline]

abbrev Phenomena.Modality.Studies.Cooper2023.Topos : Type (u_1 + 1)

A topos: a dependent type mapping background situations to foreground types. §6.4, (20): if τ : Topos, then τ has Bg : Type, fg : (Bg → Type). Topoi replace Kratzer's conversational backgrounds (modal base + ordering source) in the analysis of modality.

Definitionally Parametric Type (Discourse.lean §4.3): Topos's background- plus-foreground shape and Parametric Type's Bg/fg fields coincide. We adopt the abbrev so Cooper's §6.4 modality machinery and the §4.3 parametric content pattern share one underlying record.

Equations

• Phenomena.Modality.Studies.Cooper2023.Topos = Semantics.TypeTheoretic.Parametric Type

def Phenomena.Modality.Studies.Cooper2023.Topos.apply (τ : Topos) (s : τ.Bg) : Type

Apply a topos to a background situation: τ(s) = τ.fg(s). §6.4: τ(s) to represent τ.fg(s).

Equations

• τ.apply s = τ.fg s

Action rules with topoi (§6.4, (21)–(22))

Topoi are used with action rules:

• Epistemically: if s : τ.Bg, then infer there is something of type τ(s)
• Deontically: if s : τ.Bg, then an agent is allowed/obliged to create τ(s)

def Phenomena.Modality.Studies.Cooper2023.Topos.epistemicInference (τ : Topos) (s : τ.Bg) : Prop

Epistemic use of a topos: from a situation of the background type, infer the existence of something of the foreground type. §6.4, (21).

Equations

• τ.epistemicInference s = Nonempty (τ.fg s)

inductive Phenomena.Modality.Studies.Cooper2023.DeonticKind : Type

Deontic modality kind: affordance (allowed) vs obligation (obliged).

• affordance : DeonticKind
• obligation : DeonticKind

def Phenomena.Modality.Studies.Cooper2023.instReprDeonticKind.repr : DeonticKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Modality.Studies.Cooper2023.instReprDeonticKind : Repr DeonticKind

Equations

• Phenomena.Modality.Studies.Cooper2023.instReprDeonticKind = { reprPrec := Phenomena.Modality.Studies.Cooper2023.instReprDeonticKind.repr }

@[implicit_reducible]

instance Phenomena.Modality.Studies.Cooper2023.instDecidableEqDeonticKind : DecidableEq DeonticKind

Equations

• Phenomena.Modality.Studies.Cooper2023.instDecidableEqDeonticKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Necessity and possibility with topoi (§6.4, (23)–(24), version 4)

The final version of nec/poss uses topoi instead of an "ideal" type:

• nec(T, B, τ): s witnesses T's necessity w.r.t. background B and topos τ iff s :_p B, B ⊑ τ.Bg, and τ(s) ⊑ T
• poss(T, B, τ): s witnesses T's possibility w.r.t. B and τ iff s :_p B, B ⊑ τ.Bg, and τ(s) is compatible with T

@[reducible, inline]

abbrev Phenomena.Modality.Studies.Cooper2023.modalSubtype (B T : Type) : Prop

Subtyping in a modal type system: B ⊑_T T means all witnesses of B are also witnesses of T. §6.4: B ⊑_𝕋 τ.Bg.

Equations

• Phenomena.Modality.Studies.Cooper2023.modalSubtype B T = ∀ (x : B), Nonempty T

def Phenomena.Modality.Studies.Cooper2023.Compatible (T₁ T₂ : Type) : Prop

Compatibility: T₁ ⊤⊤ T₂ iff their meet is non-empty — there exists something of both types simultaneously. §6.4, (17).

Equations

• Phenomena.Modality.Studies.Cooper2023.Compatible T₁ T₂ = Nonempty (T₁ × T₂)

structure Phenomena.Modality.Studies.Cooper2023.NecTopos (T B : Type) (τ : Topos) : Type u_1

Witness condition for necessity with topoi (version 4). §6.4, (23): s :_p nec(T, B, τ) iff s :_p B, B ⊑_𝕋 τ.Bg, and τ(s) ⊑_𝕋 T.

We model this as: given a background witness s, a proof that the background subtypes the topos domain, and a coercion from s to the topos domain, the foreground τ(coerce(s)) is a subtype of T.

• sit : B

  A witness of the background type

• coerce : B → τ.Bg

  Coercion from background to topos domain

• sub : τ.fg (self.coerce self.sit) → T

  The topos applied at the coerced situation subtypes T

structure Phenomena.Modality.Studies.Cooper2023.PossTopos (T B : Type) (τ : Topos) : Type u_1

Witness condition for possibility with topoi (version 4). §6.4, (24): s :_p poss(T, B, τ) iff s :_p B, B ⊑_𝕋 τ.Bg, and τ(s) ⊤⊤ T. Possibility requires compatibility rather than subtyping.

• sit : B

  A witness of the background type

• coerce : B → τ.Bg

  Coercion from background to topos domain

• compat : Compatible (τ.fg (self.coerce self.sit)) T

  The topos applied at the coerced situation is compatible with T

def Phenomena.Modality.Studies.Cooper2023.necTopos_implies_possTopos {T B : Type} {τ : Topos} (hn : NecTopos T B τ) (hne : Nonempty (τ.fg (hn.coerce hn.sit))) : PossTopos T B τ

Necessity implies possibility (version 4): if T is necessary w.r.t. B and τ, and the topos foreground at the situation is non-empty, then T is possible.

Equations

• Phenomena.Modality.Studies.Cooper2023.necTopos_implies_possTopos hn hne = { sit := hn.sit, coerce := hn.coerce, compat := ⋯ }

Abstract bridge: Topos ↔ conversational background

Cooper's topoi parallel Kratzer's conversational backgrounds:

• A topos τ maps situations (bg) to types (fg): τ : bg → Type
• A conversational background f maps worlds to prop sets: f : W → Set Prop

Both serve as the contextual parameter determining modal flavor. Cooper explicitly notes (§6.4): "Topoi replace accessibility relations between possible worlds... encoding rules that license inferences."

The structural correspondence:

• Topos bg ↔ conversational background's domain (situations ↔ worlds)
• Topos fg ↔ propositions in the modal base (both constrain what's possible)
• NecTopos ↔ □ under a particular modal base
• PossTopos ↔ ◇ under a particular modal base

Full bridge importing Kratzer.lean is deferred to Theories/TTR/.

def Phenomena.Modality.Studies.Cooper2023.Topos.inducedNec (τ : Topos) : Prop

A topos induces a notion of necessity: for all situations of background type, the foreground type is inhabited. This parallels Kratzer's □ under a modal base.

Equations

• τ.inducedNec = ∀ (s : τ.Bg), Nonempty (τ.fg s)

def Phenomena.Modality.Studies.Cooper2023.Topos.inducedPoss (τ : Topos) : Prop

A topos induces possibility: some situation of background type has an inhabited foreground. This parallels Kratzer's ◇ under a modal base.

Equations

• τ.inducedPoss = ∃ (s : τ.Bg), Nonempty (τ.fg s)

theorem Phenomena.Modality.Studies.Cooper2023.Topos.nec_implies_poss (τ : Topos) (hne : Nonempty τ.Bg) (hn : τ.inducedNec) : τ.inducedPoss

Topos-induced necessity implies possibility (when the background is inhabited). The topos analogue of the D axiom (□p → ◇p).

Topos ↔ ModalSystem bridge

A topos τ : (bg → Type) induces a single-type modal system where:

• Possibilities are the situations (τ.Bg)
• There is one distinguished type (Unit)
• A possibility s has the type witnessed iff τ.fg(s) is inhabited

This connects Cooper's topos-based modality to the ModalSystem framework from §6.3. The induced accessibility relation is universal — every situation is accessible from every other — because topoi encode what follows at each situation rather than which situations are accessible. This is the formal content of Cooper's claim (§6.4) that "topoi replace accessibility relations between possible worlds."

def Phenomena.Modality.Studies.Cooper2023.Topos.toModalSystem (τ : Topos) : ModalSystem Unit Unit

Convert a topos to a single-type modal system. Possibilities are the background situations; the single type is witnessed at possibility s iff τ.fg(s) is inhabited.

Equations

• τ.toModalSystem = { Poss := τ.Bg, poss := fun (s : τ.Bg) => { available := fun (x : Unit) => True, witnesses := fun (x x_1 : Unit) => Nonempty (τ.fg s) } }

theorem Phenomena.Modality.Studies.Cooper2023.Topos.inducedNec_iff_nec_r (τ : Topos) : τ.inducedNec ↔ nec_r τ.toModalSystem ()

Topos-induced necessity = restrictive necessity in the derived modal system. ∀ s, Nonempty (τ.fg s) ↔ nec_r (τ.toModalSystem) ().

theorem Phenomena.Modality.Studies.Cooper2023.Topos.inducedPoss_iff_poss_r (τ : Topos) : τ.inducedPoss ↔ poss_r τ.toModalSystem ()

Topos-induced possibility = restrictive possibility in the derived modal system. ∃ s, Nonempty (τ.fg s) ↔ poss_r (τ.toModalSystem) ().

theorem Phenomena.Modality.Studies.Cooper2023.Topos.allAvailable (τ : Topos) (s : τ.Bg) : τ.toModalSystem.hasType s ()

All types are available in every possibility of a topos-derived system. This means inclusive and restrictive modal notions coincide for topoi — the distinction only matters when some types are absent from some possibilities.

theorem Phenomena.Modality.Studies.Cooper2023.Topos.nec_r_iff_nec_i (τ : Topos) : nec_r τ.toModalSystem () ↔ nec_i τ.toModalSystem ()

For a topos-derived modal system, nec_r = nec_i (restrictive = inclusive). Since every type is available in every possibility, the inclusive guard is vacuous.

theorem Phenomena.Modality.Studies.Cooper2023.Topos.accessRel_refl (τ : Topos) (s : τ.Bg) : τ.toModalSystem.toAccessRel () s s

The accessibility relation induced by a topos is reflexive: every situation is accessible from itself.

theorem Phenomena.Modality.Studies.Cooper2023.Topos.accessRel_characterization (τ : Topos) (s₁ s₂ : τ.Bg) : τ.toModalSystem.toAccessRel () s₁ s₂ ↔ Nonempty (τ.fg s₁) → Nonempty (τ.fg s₂)

The accessibility relation induced by a topos is: s₁ R s₂ iff whenever τ.fg(s₁) is inhabited, so is τ.fg(s₂). This captures Cooper's insight (§6.4) that the modal content is carried by the topos foreground rather than by the accessibility structure — the relation between situations is derived from the type-theoretic content, not stipulated as a primitive.

Broccoli example (§6.4, (25)–(31))

"Mary should eat her broccoli" — deontic (children must eat food on their plate) vs bouletic (children eat food they love). §6.4.

Two topoi τ₁ and τ₂ with the same foreground (eat) but different backgrounds:

• τ₁ (deontic): child has food on plate → child eats that food
• τ₂ (bouletic): child loves food → child eats that food

inductive Phenomena.Modality.Studies.Cooper2023.BrocInd : Type

Individuals in the broccoli scenario.

• broccoli : BrocInd
• mary : BrocInd
• plate : BrocInd

@[implicit_reducible]

instance Phenomena.Modality.Studies.Cooper2023.instReprBrocInd : Repr BrocInd

Equations

• Phenomena.Modality.Studies.Cooper2023.instReprBrocInd = { reprPrec := Phenomena.Modality.Studies.Cooper2023.instReprBrocInd.repr }

def Phenomena.Modality.Studies.Cooper2023.instReprBrocInd.repr : BrocInd → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Modality.Studies.Cooper2023.instDecidableEqBrocInd : DecidableEq BrocInd

Equations

• Phenomena.Modality.Studies.Cooper2023.instDecidableEqBrocInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Modality.Studies.Cooper2023.isBroccoli : BrocInd → Prop

Predicates for the broccoli scenario.

Equations

• Phenomena.Modality.Studies.Cooper2023.isBroccoli x✝ = (x✝ = Phenomena.Modality.Studies.Cooper2023.BrocInd.broccoli)

def Phenomena.Modality.Studies.Cooper2023.isChild : BrocInd → Prop

Equations

• Phenomena.Modality.Studies.Cooper2023.isChild x✝ = (x✝ = Phenomena.Modality.Studies.Cooper2023.BrocInd.mary)

def Phenomena.Modality.Studies.Cooper2023.isPlate : BrocInd → Prop

Equations

• Phenomena.Modality.Studies.Cooper2023.isPlate x✝ = (x✝ = Phenomena.Modality.Studies.Cooper2023.BrocInd.plate)

def Phenomena.Modality.Studies.Cooper2023.isFood : BrocInd → Prop

Equations

• Phenomena.Modality.Studies.Cooper2023.isFood x✝ = (x✝ = Phenomena.Modality.Studies.Cooper2023.BrocInd.broccoli)

def Phenomena.Modality.Studies.Cooper2023.have_ : BrocInd → BrocInd → Prop

Relations in the broccoli scenario.

Equations

• Phenomena.Modality.Studies.Cooper2023.have_ y z = (y = Phenomena.Modality.Studies.Cooper2023.BrocInd.mary ∧ z = Phenomena.Modality.Studies.Cooper2023.BrocInd.plate)

def Phenomena.Modality.Studies.Cooper2023.on_ : BrocInd → BrocInd → Prop

Equations

• Phenomena.Modality.Studies.Cooper2023.on_ x z = (x = Phenomena.Modality.Studies.Cooper2023.BrocInd.broccoli ∧ z = Phenomena.Modality.Studies.Cooper2023.BrocInd.plate)

def Phenomena.Modality.Studies.Cooper2023.love_ : BrocInd → BrocInd → Prop

Equations

• Phenomena.Modality.Studies.Cooper2023.love_ y x = (y = Phenomena.Modality.Studies.Cooper2023.BrocInd.mary ∧ x = Phenomena.Modality.Studies.Cooper2023.BrocInd.broccoli)

def Phenomena.Modality.Studies.Cooper2023.eat_ : BrocInd → BrocInd → Prop

Equations

• Phenomena.Modality.Studies.Cooper2023.eat_ y x = (y = Phenomena.Modality.Studies.Cooper2023.BrocInd.mary ∧ x = Phenomena.Modality.Studies.Cooper2023.BrocInd.broccoli)

structure Phenomena.Modality.Studies.Cooper2023.BroccoliBase : Type

The base situation type B for "Mary should eat her broccoli". §6.4, (26): [x=b:Ind, c₁:broccoli(x), y=m:Ind, c₂:child(y), z=p:Ind, c₃:plate(z), e₁:have(y,z), e₂:on(x,z), e₃:love(y,x)]

• x : BrocInd
• hx : isBroccoli self.x
• y : BrocInd
• hy : isChild self.y
• z : BrocInd
• hz : isPlate self.z
• e₁ : have_ self.y self.z
• e₂ : on_ self.x self.z
• e₃ : love_ self.y self.x

structure Phenomena.Modality.Studies.Cooper2023.DeonticBg : Type

The background type for τ₁ (deontic): food on child's plate. §6.4, (28a) background.

• x : BrocInd
• c₁ : isFood self.x
• y : BrocInd
• c₂ : isChild self.y
• z : BrocInd
• c₃ : isPlate self.z
• e₁ : have_ self.y self.z
• e₂ : on_ self.x self.z

structure Phenomena.Modality.Studies.Cooper2023.BouleticBg : Type

The background type for τ₂ (bouletic): food the child loves. §6.4, (28b) background.

• x : BrocInd
• c₁ : isFood self.x
• y : BrocInd
• c₂ : isChild self.y
• e₃ : love_ self.y self.x

def Phenomena.Modality.Studies.Cooper2023.eatType (y x : BrocInd) : Type

The eating type (foreground of both topoi).

Equations

• Phenomena.Modality.Studies.Cooper2023.eatType y x = PLift (Phenomena.Modality.Studies.Cooper2023.eat_ y x)

def Phenomena.Modality.Studies.Cooper2023.τ_deontic : Topos

Topos τ₁ (deontic): children eat food on their plate. §6.4, (28a).

Equations

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

def Phenomena.Modality.Studies.Cooper2023.τ_bouletic : Topos

Topos τ₂ (bouletic): children eat food they love. §6.4, (28b).

Equations

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

def Phenomena.Modality.Studies.Cooper2023.brocBase : BroccoliBase

A concrete base situation: broccoli on Mary's plate, Mary loves broccoli.

Equations

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

def Phenomena.Modality.Studies.Cooper2023.deonticBg : DeonticBg

The deontic background witnesses: food on plate.

Equations

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

def Phenomena.Modality.Studies.Cooper2023.bouleticBg : BouleticBg

The bouletic background witnesses: child loves food.

Equations

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

def Phenomena.Modality.Studies.Cooper2023.broccoliDeonticNec : NecTopos (PLift (eat_ BrocInd.mary BrocInd.broccoli)) BroccoliBase τ_deontic

Deontic reading: nec([e:eat(m,b)], T_broc, τ₁). §6.4, (29a): the deontic topos makes eating necessary.

Equations

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

def Phenomena.Modality.Studies.Cooper2023.broccolicBouleticNec : NecTopos (PLift (eat_ BrocInd.mary BrocInd.broccoli)) BroccoliBase τ_bouletic

Bouletic reading: nec([e:eat(m,b)], T_broc, τ₂). §6.4, (29b): the bouletic topos also makes eating necessary.

Equations

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

theorem Phenomena.Modality.Studies.Cooper2023.broccoli_both_topoi_yield_eat : (∃ (x : NecTopos (PLift (eat_ BrocInd.mary BrocInd.broccoli)) BroccoliBase τ_deontic), True) ∧ ∃ (x : NecTopos (PLift (eat_ BrocInd.mary BrocInd.broccoli)) BroccoliBase τ_bouletic), True

Both topoi yield the same eating conclusion, but differ in their preconditions: τ₁ requires food on plate (deontic obligation), τ₂ requires child loves food (bouletic desire).

§ 6.5 Intensionality without possible worlds

Propositions as types (not as sets of possible worlds). Two notions:

• Russellian proposition: a type T is "true" iff T is non-empty (inhabited)
• Austinian proposition: a pair ⟨s, T⟩ where s is a situation and T is a type; true iff s : T

§6.5, following @cite{austin-1961} and @cite{barwise-1989}.

@[reducible, inline]

abbrev Phenomena.Modality.Studies.Cooper2023.RussellianProp : Type 1

A Russellian proposition: identified with its type. True iff the type is inhabited. §6.5.

Equations

• Phenomena.Modality.Studies.Cooper2023.RussellianProp = Type

@[reducible, inline]

abbrev Phenomena.Modality.Studies.Cooper2023.AustinianProp (S : Type) : Type

An Austinian proposition: a situation paired with a classifying type. §6.5, following @cite{barwise-perry-1983} and @cite{austin-1961}.

True iff the situation is of the type. The situation and type are independent — the proposition claims that sit is of the situation type, but this need not hold. This is the canonical Austinian proposition type; see also TrueAustinianProp for the always-true special case.

Equations

• Phenomena.Modality.Studies.Cooper2023.AustinianProp = Semantics.TypeTheoretic.CheckableAustinian

structure Phenomena.Modality.Studies.Cooper2023.TrueAustinianProp : Type 1

A witnessed (always-true) Austinian proposition: a situation–type pair where the situation is bundled with its type, guaranteeing truth by construction. This is a special case — useful when you need to exhibit a true proposition without a separate truth check.

For the general (falsifiable) version, use AustinianProp.

• SitType : Type

  The type (situation type)

• sit : self.SitType

  The situation (witness of the type)

def Phenomena.Modality.Studies.Cooper2023.TrueAustinianProp.isTrue (p : TrueAustinianProp) : Prop

A TrueAustinianProp is always true (the situation witnesses the type).

Equations

• p.isTrue = Nonempty p.SitType

def Phenomena.Modality.Studies.Cooper2023.TrueAustinianProp.toAustinian (p : TrueAustinianProp) : AustinianProp p.SitType

A TrueAustinianProp embeds into an AustinianProp that is always true.

Equations

• p.toAustinian = { sit := p.sit, sitType := fun (x : p.SitType) => True }

theorem Phenomena.Modality.Studies.Cooper2023.TrueAustinianProp.toAustinian_isTrue (p : TrueAustinianProp) : Semantics.TypeTheoretic.CheckableAustinian.isTrue p.toAustinian

The embedded proposition is always true.

theorem Phenomena.Modality.Studies.Cooper2023.russellian_true_implies_trueAustinian {T : Type} (h : Semantics.TypeTheoretic.IsTrue T) : ∃ (p : TrueAustinianProp), p.SitType = T

If a Russellian proposition is true, there exists a true Austinian proposition. §6.5: "if a Russellian proposition containing the same type is true, then there is an Austinian proposition which is true."

Structural vs postulated subtyping (§6.5, (50))

Two kinds of subtyping:

• Structural: built into the type theory (e.g., [ℓ₁:T₁, ℓ₂:T₂] ⊑ [ℓ₁:T₁])
• Postulated: added via meaning postulates (e.g., sell(a,b,c) ⊑ buy(c,b,a))

Structural subtyping is hardwired; postulated subtyping is learned/acquired. §6.5, (50).

inductive Phenomena.Modality.Studies.Cooper2023.SubtypingKind : Type

Subtyping kind: structural (hardwired) vs postulated (learned). §6.5, (50).

• structural : SubtypingKind
• postulated : SubtypingKind

def Phenomena.Modality.Studies.Cooper2023.instReprSubtypingKind.repr : SubtypingKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Modality.Studies.Cooper2023.instReprSubtypingKind : Repr SubtypingKind

Equations

• Phenomena.Modality.Studies.Cooper2023.instReprSubtypingKind = { reprPrec := Phenomena.Modality.Studies.Cooper2023.instReprSubtypingKind.repr }

@[implicit_reducible]

instance Phenomena.Modality.Studies.Cooper2023.instDecidableEqSubtypingKind : DecidableEq SubtypingKind

Equations

• Phenomena.Modality.Studies.Cooper2023.instDecidableEqSubtypingKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Phenomena.Modality.Studies.Cooper2023.MeaningPostulate (T₁ T₂ : Type) : Type

A meaning postulate: a declared subtyping relationship between types. §6.5, (50b): sell(a,b,c) ⊑ buy(c,b,a) is a postulated subtyping that does not follow from the structure of the types.

• coerce : T₁ → T₂

  The postulated coercion

• kind : SubtypingKind

  The kind is always postulated

Buy/sell equivalence (§6.5, (50b))

A canonical example of postulated subtyping: the types for selling and buying events are distinct but related by a meaning postulate.

structure Phenomena.Modality.Studies.Cooper2023.SellEvent (E : Type) : Type

A sell event: seller sells thing to buyer.

• seller : E
• thing : E
• buyer : E

structure Phenomena.Modality.Studies.Cooper2023.BuyEvent (E : Type) : Type

A buy event: buyer buys thing from seller.

• buyer : E
• thing : E
• seller : E

def Phenomena.Modality.Studies.Cooper2023.structuralSubtype_example {T₁ T₂ : Type} : T₁ × T₂ → T₁

Structural subtyping example: a record with more fields subtypes one with fewer. §6.5, (50a): [ℓ₁:T₁, ℓ₂:T₂] ⊑ [ℓ₁:T₁].

Equations

• Phenomena.Modality.Studies.Cooper2023.structuralSubtype_example = Prod.fst

def Phenomena.Modality.Studies.Cooper2023.sellBuyPostulate (E : Type) : MeaningPostulate (SellEvent E) (BuyEvent E)

Postulated subtyping: sell(a,b,c) ⊑ buy(c,b,a). §6.5, (50b).

Equations

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

def Phenomena.Modality.Studies.Cooper2023.buySellPostulate (E : Type) : MeaningPostulate (BuyEvent E) (SellEvent E)

The reverse postulate: buy(a,b,c) ⊑ sell(c,b,a).

Equations

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

theorem Phenomena.Modality.Studies.Cooper2023.sell_buy_roundtrip {E : Type} (s : SellEvent E) : (buySellPostulate E).coerce ((sellBuyPostulate E).coerce s) = s

Roundtrip: sell → buy → sell = id (the postulates are inverses).

Believe and know (§6.5, (38)–(41))

Propositional attitudes are analyzed via matching against long-term memory. believe(a, T) is non-empty iff there exists T' in a's long-term memory such that T' ⊑_∼ T (subtype modulo relabelling).

§6.5, (40): e : believe(a, T) iff e : ltm(a, T') and T' ⊑_∼ T

structure Phenomena.Modality.Studies.Cooper2023.LTM (Agent : Type) : Type 1

An agent's long-term memory: maps agents to record types (their stored beliefs). §6.5, p.257: "r is a's total information state, then a's long-term memory will be r.ltm."

• memType : Agent → Type

  The type representing the agent's long-term memory

def Phenomena.Modality.Studies.Cooper2023.subtypeModRelabel (T₁ T₂ : Type) : Prop

Subtyping modulo relabelling: T₁ ⊑_∼ T₂ iff there is a relabelling η such that T₁ ⊑ [T₂]_η. §6.5, (39). We model this abstractly as the existence of a coercion.

Equations

• Phenomena.Modality.Studies.Cooper2023.subtypeModRelabel T₁ T₂ = Nonempty (T₁ → T₂)

def Phenomena.Modality.Studies.Cooper2023.believe {Agent : Type} (ltm : LTM Agent) (a : Agent) (T : Type) : Prop

Witness condition for believe(a, T): version (40). §6.5, (40): e : believe(a, T) iff e : ltm(a, T') and T' ⊑_∼ T.

Equations

• Phenomena.Modality.Studies.Cooper2023.believe ltm a T = Phenomena.Modality.Studies.Cooper2023.subtypeModRelabel (ltm.memType a) T

def Phenomena.Modality.Studies.Cooper2023.know {Agent : Type} (ltm : LTM Agent) (a : Agent) (T : Type) : Prop

Knowledge is veridical belief: know(a, T) requires believe(a, T) AND T true. This is a standard characterization; does not give a full definition of 'know' but discusses the connection.

Equations

• Phenomena.Modality.Studies.Cooper2023.know ltm a T = (Phenomena.Modality.Studies.Cooper2023.believe ltm a T ∧ Semantics.TypeTheoretic.IsTrue T)

theorem Phenomena.Modality.Studies.Cooper2023.know_implies_believe {Agent : Type} {ltm : LTM Agent} {a : Agent} {T : Type} : know ltm a T → believe ltm a T

Knowledge implies belief.

theorem Phenomena.Modality.Studies.Cooper2023.know_implies_true {Agent : Type} {ltm : LTM Agent} {a : Agent} {T : Type} : know ltm a T → Semantics.TypeTheoretic.IsTrue T

Knowledge implies truth (veridicality).

theorem Phenomena.Modality.Studies.Cooper2023.believe_closed_under_subtype {Agent : Type} {ltm : LTM Agent} {a : Agent} {T₁ T₂ : Type} (hb : believe ltm a T₁) (hsub : T₁ → T₂) : believe ltm a T₂

Belief is closed under (modulo-relabelling) subtyping. §6.5, (41): "for any relabelling η of T, s : believe(a, [T]_η)".

Abstract bridge: know = believe + veridicality

TTR's know = believe ∧ IsTrue mirrors the standard doxastic classification:

• know is veridical (factivity: know p → p)
• believe is non-veridical (believe p ↛ p)

This is the abstract pattern that connects to Doxastic.veridical in Theories/Semantics.Intensional/Attitude/Doxastic.lean. The full bridge (importing Doxastic) is deferred to a future Theories/TTR/ module.

theorem Phenomena.Modality.Studies.Cooper2023.know_iff_believe_and_true {Agent : Type} {ltm : LTM Agent} {a : Agent} {T : Type} : know ltm a T ↔ believe ltm a T ∧ Semantics.TypeTheoretic.IsTrue T

know is exactly believe + veridicality: the two components are independent.

theorem Phenomena.Modality.Studies.Cooper2023.believe_not_entails_true : ¬∀ (Agent : Type) (ltm : LTM Agent) (a : Agent) (T : Type), believe ltm a T → Semantics.TypeTheoretic.IsTrue T

Belief does not entail truth: an agent can believe a false type. This shows know is strictly stronger than believe. With memType = Empty, believe holds vacuously for any T (including Empty).

Points of view (§6.5, (55)–(60))

A point of view on a type T is a type T' that shares some labels/fields with T but provides alternative field types. Used for the Hesperus/Phosphorus puzzle and for intensional transitive verbs.

§6.5, (55): pov(T₁, T₂) — T₁ is a point of view on T₂. The key property: a situation can be described from different points of view.

We model this as: T₁ is a point of view on T₂ if there is a way to "merge" T₁ with T₂ (asymmetric merge).

structure Phenomena.Modality.Studies.Cooper2023.PointOfView (T₁ T₂ : Type) : Type 1

A point of view: T₁ is an alternative perspective on T₂. §6.5, (55): pov(T₁, T₂) — T₁ shares labels with T₂ but provides alternative field types. The merge field represents asymmetric merge (⊕) of T₂ with T₁.

• Merged : Type

  The result of asymmetric merge: T₂[⊕]T₁

• project : self.Merged → T₂

  The merged type subtypes T₂ (it's a version of T₂ with T₁'s perspective)

def Phenomena.Modality.Studies.Cooper2023.extMember {T : Type} (_a : T) : Prop

Extended membership: a :_E T iff a : T or some component of a is of type T. §6.5, (57): a :_E T iff either a : T or for some b ε a, b : T.

Equations

• Phenomena.Modality.Studies.Cooper2023.extMember _a = True

def Phenomena.Modality.Studies.Cooper2023.extMemberVia {Outer Inner : Type} (a : Outer) (extract : Outer → Inner) (T : Inner → Type) : Prop

Equations

• Phenomena.Modality.Studies.Cooper2023.extMemberVia a extract T = Nonempty (T (extract a))

Revised believe with points of view (§6.5, (58))

§6.5, (58) revises the witness condition for believe to account for points of view: e : believe(a, T) if e : ltm(a, T') and T' ⊑_∼ T OR e :_E believe(a, T₁) and e :E pov(T₂, T₁) and T₁[⊕]T₂ ⊑∼ T

def Phenomena.Modality.Studies.Cooper2023.believeWithPov {Agent : Type} (ltm : LTM Agent) (a : Agent) (T : Type) : Prop

Revised believe with point-of-view support. §6.5, (58).

Equations

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

theorem Phenomena.Modality.Studies.Cooper2023.believe_implies_believeWithPov {Agent : Type} {ltm : LTM Agent} {a : Agent} {T : Type} (h : believe ltm a T) : believeWithPov ltm a T

Direct belief implies belief-with-pov.

Hesperus/Phosphorus puzzle (§6.5, (52)–(53))

The ancients believed Hesperus (evening star) and Phosphorus (morning star) were different objects, but they are both Venus. In TTR, this is modeled via different labels in the long-term memory type: the names are associated with different paths in the record, so believe(ancients, [Hesperus rises in evening]) and believe(ancients, [Phosphorus rises in morning]) are non-trivially different.

inductive Phenomena.Modality.Studies.Cooper2023.CelestialBody : Type

• venus : CelestialBody

@[implicit_reducible]

instance Phenomena.Modality.Studies.Cooper2023.instReprCelestialBody : Repr CelestialBody

Equations

• Phenomena.Modality.Studies.Cooper2023.instReprCelestialBody = { reprPrec := Phenomena.Modality.Studies.Cooper2023.instReprCelestialBody.repr }

def Phenomena.Modality.Studies.Cooper2023.instReprCelestialBody.repr : CelestialBody → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Modality.Studies.Cooper2023.instDecidableEqCelestialBody : DecidableEq CelestialBody

Equations

• Phenomena.Modality.Studies.Cooper2023.instDecidableEqCelestialBody x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Phenomena.Modality.Studies.Cooper2023.AncientsLTM_Before : Type

Ancient's LTM type before learning Hesperus = Phosphorus. §6.5, (52): separate entries for Hesperus and Phosphorus.

• hesperus : CelestialBody
• hesperus_rises_evening : self.hesperus = CelestialBody.venus
• phosphorus : CelestialBody
• phosphorus_rises_morning : self.phosphorus = CelestialBody.venus

structure Phenomena.Modality.Studies.Cooper2023.AncientsLTM_Afterextends Phenomena.Modality.Studies.Cooper2023.AncientsLTM_Before : Type

Ancient's LTM type after learning they are the same. §6.5, (53): entries unified with identity constraint.

• hesperus : CelestialBody
• hesperus_rises_evening : self.hesperus = CelestialBody.venus
• phosphorus : CelestialBody
• phosphorus_rises_morning : self.phosphorus = CelestialBody.venus
• same : self.hesperus = self.phosphorus

theorem Phenomena.Modality.Studies.Cooper2023.ancients_separate_beliefs : ∃ (ltm : AncientsLTM_Before), ltm.hesperus = ltm.phosphorus

Before learning: the ancients can believe separately about Hesperus/Phosphorus. Even though both are Venus, the two record fields are distinct in the type.

@[implicit_reducible]

instance Phenomena.Modality.Studies.Cooper2023.instSubtypeOfAncientsLTM_AfterAncientsLTM_Before : AncientsLTM_After ⊑ AncientsLTM_Before

The identity becomes explicit only in the "after" type. Structural consequence: the after-type is a subtype of the before-type (it has more fields/constraints).

Equations

• Phenomena.Modality.Studies.Cooper2023.instSubtypeOfAncientsLTM_AfterAncientsLTM_Before = { up := Phenomena.Modality.Studies.Cooper2023.AncientsLTM_After.toAncientsLTM_Before }

theorem Phenomena.Modality.Studies.Cooper2023.learning_adds_constraint (ltm : AncientsLTM_After) : ltm.hesperus = ltm.phosphorus

Learning Hesperus = Phosphorus is adding a constraint (more fields).

Intensional transitive verbs (§6.5, (63)–(66))

Montague treated intensional verbs (seek, worship) as taking quantifier arguments. Cooper recasts this in TTR: predicates with arity ⟨Ind, Quant⟩ where the quantifier is the object argument.

Key concepts:

• p†: the extensional variant of an intensional predicate
• Meaning postulate (65): p(a, Q) ≈_𝕋 Q(λr:[x:Ind].[e:p†(a,r.x)])
• Success postulate (66): successful(seek(a,Q)) ⊑_𝕋 find(a,Q) (a successful search is a finding)

structure Phenomena.Modality.Studies.Cooper2023.IntensionalTV (E : Type) : Type 1

An intensional transitive verb: takes an individual and a quantifier. §6.5, (64): SemTransVerb(T_bg, p) for arity ⟨Ind, Quant⟩ = 'λc:T_bg. λQ:Quant. λr:[x:Ind]. [e : p(r.x, Q)]'

The p† variant is the extensional "dagger" form relating to individuals.

• pred : E → Semantics.TypeTheoretic.Quant E → Type

  The intensional predicate: Ind → Quant → Type

• dagger : E → E → Type

  The extensional dagger variant: Ind → Ind → Type

def Phenomena.Modality.Studies.Cooper2023.extensionalMP {E : Type} (itv : IntensionalTV E) (a : E) (Q : Semantics.TypeTheoretic.Quant E) : Prop

Meaning postulate (65) for extensional transitive verbs: p(a, Q) ≈ Q(λr:[x:Ind].[e:p†(a,r.x)]) §6.5, (65).

Equations

• Phenomena.Modality.Studies.Cooper2023.extensionalMP itv a Q = Nonempty (itv.pred a Q ≃ Q fun (x : E) => itv.dagger a x)

structure Phenomena.Modality.Studies.Cooper2023.SuccessPostulate (E : Type) : Type 1

Success postulate (66): a successful search is a finding. §6.5, (66): successful(seek(a, Q)) ⊑_𝕋 find(a, Q).

• seek : IntensionalTV E
• find : IntensionalTV E
• success (a : E) (Q : Semantics.TypeTheoretic.Quant E) (itv_success : Type) : (itv_success → self.seek.pred a Q) → itv_success → self.find.pred a Q

  If a successful seek is a subtype of find

Worship (§6.5, (69)–(75))

Worship requires:

1. Religious belief (intentionality): the subject believes in the deity
2. Specificity: the religious belief type is a subtype of the quantified type

§6.5, (75): e : worship(a, Q) iff for some T, (1) e : rbelieve(a, T) — a has T as a religious belief (2) T ⊑_∼ Q(λr:[x:Ind].worship†(a, r.x))

def Phenomena.Modality.Studies.Cooper2023.rbelieve {Agent : Type} (_ltm : LTM Agent) (rbelType : Agent → Type) (a : Agent) (T : Type) : Prop

Religious belief: a distinguished part of long-term memory. §6.5, (72)–(74).

Equations

• Phenomena.Modality.Studies.Cooper2023.rbelieve _ltm rbelType a T = Nonempty (rbelType a → T)

def Phenomena.Modality.Studies.Cooper2023.worshipSem {E : Type} (ltm : LTM E) (rbelType : E → Type) (worshipDagger : E → E → Type) (a : E) (Q : Semantics.TypeTheoretic.Quant E) : Prop

Witness condition for worship (§6.5, (75)). e : worship(a, Q) iff for some T: (1) e : rbelieve(a, T) (2) T ⊑_∼ Q(λr:[x:Ind].worship†(a, r.x))

Equations

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

Want (§6.5, (88)–(92))

The analysis of want uses desire states (parallel to LTM). want†(a, T) is non-empty iff a's desires include T (the desire type is a subtype of T, modulo relabelling).

§6.5, (90)–(92): want_P and want_Q related to want†; witness condition uses des(a, T') and T' ⊑_∼ T.

structure Phenomena.Modality.Studies.Cooper2023.AgentInfoState (Agent : Type) : Type 1

An agent's full information state: long-term memory, religious beliefs, desires. §6.5, (91). Distinct from the Ch4 TotalInfoState which pairs memory with a dialogue gameboard.

• ltm : Agent → Type

  Long-term memory type for each agent

• rbel : Agent → Type

  Religious belief type for each agent

• des : Agent → Type

  Desire type for each agent

def Phenomena.Modality.Studies.Cooper2023.desire {Agent : Type} (ais : AgentInfoState Agent) (a : Agent) (T : Type) : Prop

Desire predicate: des(a, T) iff a's desire state subtypes T. §6.5: "e : des(a, T) just in case T is a's desires in e."

Equations

• Phenomena.Modality.Studies.Cooper2023.desire ais a T = Phenomena.Modality.Studies.Cooper2023.subtypeModRelabel (ais.des a) T

def Phenomena.Modality.Studies.Cooper2023.wantDagger {Agent : Type} (ais : AgentInfoState Agent) (a : Agent) (T : Type) : Prop

Witness condition for want†(a, T). §6.5, (92): e : want†(a, T) if for some T', e : des(a, T') and T' ⊑_∼ T.

Equations

• Phenomena.Modality.Studies.Cooper2023.wantDagger ais a T = Phenomena.Modality.Studies.Cooper2023.desire ais a T

def Phenomena.Modality.Studies.Cooper2023.wantWithPov {Agent : Type} (ais : AgentInfoState Agent) (a : Agent) (T : Type) : Prop

want with point of view (§6.5, (92) second clause): e : want†(a, T) if for some T₁, T₂: e :_E want†(a, T₁) e :E pov(T₂, T₁) T₁[⊕]T₂ ⊑∼ T

Equations

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

def Phenomena.Modality.Studies.Cooper2023.bookPostulate {E : Type} (book_ : E → Semantics.TypeTheoretic.Quant E → Type) (be_ : E → Type) (a : E) (Q : Semantics.TypeTheoretic.Quant E) : Prop

Book as an intensional verb requiring existence. §6.5, (87): book(a, Q) ⊑_𝕋 Q(λr:[x:Ind].[e:be(r.x)]) This ensures that if a books Q, there is something that exists (be). Unlike seek, book implies existence but not specificity.

Equations

• Phenomena.Modality.Studies.Cooper2023.bookPostulate book_ be_ a Q = Nonempty (book_ a Q → Q fun (x : E) => be_ x)

Chapter 6 phenomena

inductive Phenomena.Modality.Studies.Cooper2023.TwoPred : Type

A simple two-possibility modal system.

• rain : TwoPred
• snow : TwoPred

@[implicit_reducible]

instance Phenomena.Modality.Studies.Cooper2023.instDecidableEqTwoPred : DecidableEq TwoPred

Equations

• Phenomena.Modality.Studies.Cooper2023.instDecidableEqTwoPred x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Phenomena.Modality.Studies.Cooper2023.TwoObj : Type

• obj_a : TwoObj
• obj_b : TwoObj

@[implicit_reducible]

instance Phenomena.Modality.Studies.Cooper2023.instDecidableEqTwoObj : DecidableEq TwoObj

Equations

• Phenomena.Modality.Studies.Cooper2023.instDecidableEqTwoObj x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Modality.Studies.Cooper2023.twoModal : ModalSystem TwoPred TwoObj

Equations

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

theorem Phenomena.Modality.Studies.Cooper2023.rain_necessary : nec_r twoModal TwoPred.rain

Rain is necessary (has witnesses in both possibilities).

theorem Phenomena.Modality.Studies.Cooper2023.snow_possible : poss_r twoModal TwoPred.snow

Snow is possible but not necessary.

theorem Phenomena.Modality.Studies.Cooper2023.snow_not_necessary : ¬nec_r twoModal TwoPred.snow

theorem Phenomena.Modality.Studies.Cooper2023.box_rain : BoxR twoModal TwoPred.rain

□_r rain is true.

theorem Phenomena.Modality.Studies.Cooper2023.diamond_snow : DiamondR twoModal TwoPred.snow

◇_r snow is true but □_r snow is false.

theorem Phenomena.Modality.Studies.Cooper2023.not_box_snow : ¬BoxR twoModal TwoPred.snow

theorem Phenomena.Modality.Studies.Cooper2023.snow_not_nec_i : ¬nec_i twoModal TwoPred.snow

When all types are available everywhere (as in twoModal), nec_i and nec_r agree: snow is not inclusively necessary either.

Restrictive vs inclusive distinction

A modal system where snow is only available in one possibility. This demonstrates that nec_i is strictly weaker than nec_r: snow is inclusively necessary (has witnesses wherever available) but not restrictively necessary (not available = not checked).

def Phenomena.Modality.Studies.Cooper2023.twoModalRestricted : ModalSystem TwoPred TwoObj

A modal system where snow is only a type in the first possibility. Rain is available everywhere; snow is only available at true.

Equations

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

theorem Phenomena.Modality.Studies.Cooper2023.restricted_snow_not_nec_r : ¬nec_r twoModalRestricted TwoPred.snow

Snow is NOT restrictively necessary: no witnesses at false.

theorem Phenomena.Modality.Studies.Cooper2023.restricted_snow_nec_i : nec_i twoModalRestricted TwoPred.snow

Snow IS inclusively necessary: the only possibility where snow is available (true) has a witness. The false possibility doesn't have snow as a type, so it's not checked.

theorem Phenomena.Modality.Studies.Cooper2023.nec_i_not_implies_nec_r : ¬∀ (Ty Obj : Type) (ms : ModalSystem Ty Obj) (T : Ty), nec_i ms T → nec_r ms T

This is the key result: nec_i does NOT imply nec_r. The inclusive/restrictive distinction is non-trivial.

def Phenomena.Modality.Studies.Cooper2023.samSellsBookToKim : SellEvent String

Buy/sell postulated subtyping phenomenon.

Equations

• Phenomena.Modality.Studies.Cooper2023.samSellsBookToKim = { seller := "Kim", thing := "Syntactic Structures", buyer := "Sam" }

def Phenomena.Modality.Studies.Cooper2023.kimBuysBookFromSam : BuyEvent String

Equations

• Phenomena.Modality.Studies.Cooper2023.kimBuysBookFromSam = { buyer := "Sam", thing := "Syntactic Structures", seller := "Kim" }

theorem Phenomena.Modality.Studies.Cooper2023.sell_matches_buy : (sellBuyPostulate String).coerce samSellsBookToKim = kimBuysBookFromSam

structure Phenomena.Modality.Studies.Cooper2023.SimpleWorld : Type

Belief phenomenon: an agent whose LTM subtypes a type believes it.

• raining : Bool

def Phenomena.Modality.Studies.Cooper2023.weatherLTM : LTM Unit

Equations

• Phenomena.Modality.Studies.Cooper2023.weatherLTM = { memType := fun (x : Unit) => Phenomena.Modality.Studies.Cooper2023.SimpleWorld }

theorem Phenomena.Modality.Studies.Cooper2023.agent_believes_weather : believe weatherLTM () SimpleWorld

def Phenomena.Modality.Studies.Cooper2023.hesperusType : Type

Point of view phenomenon: Hesperus/Phosphorus with a point of view.

Equations

• Phenomena.Modality.Studies.Cooper2023.hesperusType = Phenomena.Modality.Studies.Cooper2023.CelestialBody

def Phenomena.Modality.Studies.Cooper2023.phosphorusType : Type

Equations

• Phenomena.Modality.Studies.Cooper2023.phosphorusType = Phenomena.Modality.Studies.Cooper2023.CelestialBody

theorem Phenomena.Modality.Studies.Cooper2023.hesperus_phosphorus_same_entity : CelestialBody.venus = CelestialBody.venus

Both resolve to the same entity (Venus) but via different type paths.

Bridge: ModalSystem → Core.Intension

TTR's ModalSystem achieves intensionality without Intension W τ: a type T can have different extensions across possibilities, which is exactly what an intension does across worlds.

def Phenomena.Modality.Studies.Cooper2023.modalSystem_induces_intension {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Core.Intension ms.Poss (Obj → Prop)

A ModalSystem induces an intension for each type: the function mapping each possibility to the type's extension at that possibility.

Equations

• Phenomena.Modality.Studies.Cooper2023.modalSystem_induces_intension ms T p = ms.ext p T

def Phenomena.Modality.Studies.Cooper2023.ModalSystem.isRigidType {Ty Obj : Type} (ms : ModalSystem Ty Obj) (T : Ty) : Prop

A type is rigid in a modal system iff its extension is constant across all possibilities — matching Core.Intension.IsRigid.

Equations

• ms.isRigidType T = (Phenomena.Modality.Studies.Cooper2023.modalSystem_induces_intension ms T).IsRigid

MeaningPostulate enables belief transfer

A meaning postulate from T₁ to T₂ enables belief transfer: if an agent believes T₁ and there's a postulate T₁ → T₂, then the agent believes T₂.

theorem Phenomena.Modality.Studies.Cooper2023.meaningPostulate_transfers_belief {Agent : Type} {ltm : LTM Agent} {a : Agent} {T₁ T₂ : Type} (hb : believe ltm a T₁) (mp : MeaningPostulate T₁ T₂) : believe ltm a T₂

A meaning postulate from T₁ to T₂ enables belief transfer: if an agent believes T₁ and there's a postulate T₁ → T₂, then the agent believes T₂. This connects MeaningPostulate to the doxastic system.

TrueAustinianProp → AustinianProp

TrueAustinianProp carries its own witness (always true by construction). AustinianProp (= CheckableAustinian) is the general case that can be false. This bridge embeds the former into the latter.

def Phenomena.Modality.Studies.Cooper2023.cooperToGinzburg (ap : TrueAustinianProp) : AustinianProp ap.SitType

Embed a TrueAustinianProp (always true) into an AustinianProp.

A TrueAustinianProp carries its own witness, so the resulting AustinianProp is always true.

Equations

• Phenomena.Modality.Studies.Cooper2023.cooperToGinzburg ap = { sit := ap.sit, sitType := fun (x : ap.SitType) => True }

theorem Phenomena.Modality.Studies.Cooper2023.cooperToGinzburg_always_true (ap : TrueAustinianProp) : Semantics.TypeTheoretic.CheckableAustinian.isTrue (cooperToGinzburg ap)

The embedding preserves truth.

Cooper's foundational examples motivating intensional type theory. The groundhog/woodchuck and roundSquare/evenPrimeGt2 pairs demonstrate that TTR distinguishes types with the same extension — the structural commitment underlying all of Ch. 6's intensional content.

def Phenomena.Modality.Studies.Cooper2023.groundhog : Semantics.TypeTheoretic.IType

groundhog and woodchuck as intensional types: same carrier, different names. §1.3: types are not sets; two types can share all witnesses yet remain distinct.

Equations

• Phenomena.Modality.Studies.Cooper2023.groundhog = { carrier := Unit, name := "groundhog" }

def Phenomena.Modality.Studies.Cooper2023.woodchuck : Semantics.TypeTheoretic.IType

Equations

• Phenomena.Modality.Studies.Cooper2023.woodchuck = { carrier := Unit, name := "woodchuck" }

theorem Phenomena.Modality.Studies.Cooper2023.groundhog_woodchuck_ext_equiv : groundhog.extEquiv woodchuck

They are extensionally equivalent (same carrier).

theorem Phenomena.Modality.Studies.Cooper2023.groundhog_ne_woodchuck : ¬groundhog.intEq woodchuck

But they are intensionally distinct (different names). This is Cooper's key point: groundhog ≠ woodchuck in TTR, whereas in extensional set theory {marmota} = {marmota}.

def Phenomena.Modality.Studies.Cooper2023.roundSquare : Semantics.TypeTheoretic.IType

round_square and even_prime_gt_2 are both empty but distinct. §1.3: possible worlds cannot distinguish these since both have empty extension at every world. TTR can: they are different types.

Equations

• Phenomena.Modality.Studies.Cooper2023.roundSquare = { carrier := Empty, name := "round_square" }

def Phenomena.Modality.Studies.Cooper2023.evenPrimeGt2 : Semantics.TypeTheoretic.IType

Equations

• Phenomena.Modality.Studies.Cooper2023.evenPrimeGt2 = { carrier := Empty, name := "even_prime_gt_2" }

theorem Phenomena.Modality.Studies.Cooper2023.round_square_empty : Semantics.TypeTheoretic.IsFalse roundSquare.carrier

theorem Phenomena.Modality.Studies.Cooper2023.even_prime_gt2_empty : Semantics.TypeTheoretic.IsFalse evenPrimeGt2.carrier

theorem Phenomena.Modality.Studies.Cooper2023.empty_types_distinct : ¬roundSquare.intEq evenPrimeGt2

inductive Phenomena.Modality.Studies.Cooper2023.Ind : Type

Individuals in Cooper's fragment: Dudamel and Beethoven.

• dudamel : Ind
• beethoven : Ind

@[implicit_reducible]

instance Phenomena.Modality.Studies.Cooper2023.instReprInd : Repr Ind

Equations

• Phenomena.Modality.Studies.Cooper2023.instReprInd = { reprPrec := Phenomena.Modality.Studies.Cooper2023.instReprInd.repr }

def Phenomena.Modality.Studies.Cooper2023.instReprInd.repr : Ind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Modality.Studies.Cooper2023.instDecidableEqInd : DecidableEq Ind

Equations

• Phenomena.Modality.Studies.Cooper2023.instDecidableEqInd x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Phenomena.Modality.Studies.Cooper2023.Conductor : Ind → Type

Predicate "conductor": Dudamel is a conductor.

• mk : Conductor Ind.dudamel

inductive Phenomena.Modality.Studies.Cooper2023.Composer : Ind → Type

Predicate "composer": Beethoven is a composer.

• mk : Composer Ind.beethoven

def Phenomena.Modality.Studies.Cooper2023.conductorPpty : Semantics.TypeTheoretic.Ppty Ind

"conductor" content: Ppty Ind.

Equations

• Phenomena.Modality.Studies.Cooper2023.conductorPpty = Semantics.TypeTheoretic.semCommonNoun Phenomena.Modality.Studies.Cooper2023.Conductor

def Phenomena.Modality.Studies.Cooper2023.composerPpty : Semantics.TypeTheoretic.Ppty Ind

"composer" content: Ppty Ind.

Equations

• Phenomena.Modality.Studies.Cooper2023.composerPpty = Semantics.TypeTheoretic.semCommonNoun Phenomena.Modality.Studies.Cooper2023.Composer

def Phenomena.Modality.Studies.Cooper2023.dudamelQuant : Semantics.TypeTheoretic.Quant Ind

"Dudamel" content: Quant Ind (GQ).

Equations

• Phenomena.Modality.Studies.Cooper2023.dudamelQuant = Semantics.TypeTheoretic.semPropName Phenomena.Modality.Studies.Cooper2023.Ind.dudamel

def Phenomena.Modality.Studies.Cooper2023.beethovenQuant : Semantics.TypeTheoretic.Quant Ind

"Beethoven" content: Quant Ind (GQ).

Equations

• Phenomena.Modality.Studies.Cooper2023.beethovenQuant = Semantics.TypeTheoretic.semPropName Phenomena.Modality.Studies.Cooper2023.Ind.beethoven

@[reducible, inline]

abbrev Phenomena.Modality.Studies.Cooper2023.aConductor : Semantics.TypeTheoretic.Quant Ind

Step 3: "a conductor" — existential quantifier over conductors.

Equations

• Phenomena.Modality.Studies.Cooper2023.aConductor = Semantics.TypeTheoretic.semIndefArt Phenomena.Modality.Studies.Cooper2023.conductorPpty

@[reducible, inline]

abbrev Phenomena.Modality.Studies.Cooper2023.isAConductor : Semantics.TypeTheoretic.Ppty Ind

Step 5: "is a conductor" — property of being a conductor.

Equations

• Phenomena.Modality.Studies.Cooper2023.isAConductor = Semantics.TypeTheoretic.semBe Phenomena.Modality.Studies.Cooper2023.aConductor

@[reducible, inline]

abbrev Phenomena.Modality.Studies.Cooper2023.dudamelIsAConductor : Type

Step 7: "Dudamel is a conductor" — a proposition (type).

Equations

• Phenomena.Modality.Studies.Cooper2023.dudamelIsAConductor = Phenomena.Modality.Studies.Cooper2023.dudamelQuant Phenomena.Modality.Studies.Cooper2023.isAConductor

def Phenomena.Modality.Studies.Cooper2023.dudamelIsAConductorTrue : dudamelIsAConductor

"Dudamel is a conductor" is TRUE (the proposition type is inhabited).

Equations

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

@[reducible, inline]

abbrev Phenomena.Modality.Studies.Cooper2023.beethovenIsAConductor : Type

The analogous sentence with Beethoven.

Equations

• Phenomena.Modality.Studies.Cooper2023.beethovenIsAConductor = Phenomena.Modality.Studies.Cooper2023.beethovenQuant Phenomena.Modality.Studies.Cooper2023.isAConductor

instance Phenomena.Modality.Studies.Cooper2023.instIsFalseBeethovenIsAConductor : Semantics.TypeTheoretic.IsFalse beethovenIsAConductor

"Beethoven is a conductor" is FALSE (the proposition type is empty).

@[reducible, inline]

abbrev Phenomena.Modality.Studies.Cooper2023.aComposer : Semantics.TypeTheoretic.Quant Ind

"Beethoven is a composer" — TRUE.

Equations

• Phenomena.Modality.Studies.Cooper2023.aComposer = Semantics.TypeTheoretic.semIndefArt Phenomena.Modality.Studies.Cooper2023.composerPpty

@[reducible, inline]

abbrev Phenomena.Modality.Studies.Cooper2023.isAComposer : Semantics.TypeTheoretic.Ppty Ind

Equations

• Phenomena.Modality.Studies.Cooper2023.isAComposer = Semantics.TypeTheoretic.semBe Phenomena.Modality.Studies.Cooper2023.aComposer

@[reducible, inline]

abbrev Phenomena.Modality.Studies.Cooper2023.beethovenIsAComposer : Type

Equations

• Phenomena.Modality.Studies.Cooper2023.beethovenIsAComposer = Phenomena.Modality.Studies.Cooper2023.beethovenQuant Phenomena.Modality.Studies.Cooper2023.isAComposer

def Phenomena.Modality.Studies.Cooper2023.beethovenIsAComposerTrue : beethovenIsAComposer

Equations

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

§ 3.4 CnstrIsA — Construction-based "is a" (ex 85–92)

Cooper §3.4 shows that TTR can distinguish two analyses of "Dudamel is a conductor" that Montague collapses:

1. Compositional (via semBe + semIndefArt): the content involves existential quantification — ExistWitness Ind Conductor (λ y => propT (d = y)).

2. Construction-based CnstrIsA (§3.4, ex 87): the VP ↟ NP construction makes the VP content equal to the NP content directly — conductor(d).

The two are truth-conditionally equivalent (inhabited iff Dudamel is a conductor) but structurally distinct as types. This structural distinction is unavailable in Montague's system, where truth-conditional equivalence entails identity of denotation.

@[reducible, inline]

abbrev Phenomena.Modality.Studies.Cooper2023.cnstrIsA {E : Type} (pred : E → Type) (individual : E) : Type

CnstrIsA: construction-based content for "NP is a CN". §3.4, ex (87): VP → V NP ∧ CnstrIsA. The content is the predicate applied directly to the individual — no existential quantification. §3.4, ex (92a): [ e : conductor(d) ].

Equations

• Phenomena.Modality.Studies.Cooper2023.cnstrIsA pred individual = pred individual

@[reducible, inline]

abbrev Phenomena.Modality.Studies.Cooper2023.dudamelIsAConductor_cnstr : Type

Construction-based "Dudamel is a conductor" — direct predication.

Equations

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

def Phenomena.Modality.Studies.Cooper2023.dudamelIsAConductor_cnstr_true : dudamelIsAConductor_cnstr

CnstrIsA "Dudamel is a conductor" is TRUE.

Equations

• Phenomena.Modality.Studies.Cooper2023.dudamelIsAConductor_cnstr_true = Phenomena.Modality.Studies.Cooper2023.Conductor.mk

instance Phenomena.Modality.Studies.Cooper2023.instIsFalseCnstrIsAIndConductorBeethoven : Semantics.TypeTheoretic.IsFalse (cnstrIsA Conductor Ind.beethoven)

CnstrIsA "Beethoven is a conductor" is FALSE.

theorem Phenomena.Modality.Studies.Cooper2023.cnstrIsA_equiv_compositional (individual : Ind) (pred : Ind → Type) : Nonempty (cnstrIsA pred individual) ↔ Nonempty (Semantics.TypeTheoretic.ExistWitness Ind pred fun (y : Ind) => Semantics.TypeTheoretic.propT (individual = y))

The compositional and construction readings are truth-conditionally equivalent: both inhabited iff the individual has the property.

theorem Phenomena.Modality.Studies.Cooper2023.cnstrIsA_intensionally_distinct : ¬{ carrier := cnstrIsA Conductor Ind.dudamel, name := "conductor(d)" }.intEq { carrier := dudamelIsAConductor, name := "exist(conductor, be(d))" }

As ITypes, the compositional and construction readings are intensionally distinct.

@[reducible, inline]

abbrev Phenomena.Modality.Studies.Cooper2023.aConductorIsDudamel : Type

"A conductor is Dudamel" — only the compositional reading available.

Equations

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

def Phenomena.Modality.Studies.Cooper2023.aConductorIsDudamel_true : aConductorIsDudamel

Equations

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

theorem Phenomena.Modality.Studies.Cooper2023.reversed_equiv_compositional : Nonempty aConductorIsDudamel ↔ Nonempty dudamelIsAConductor

Cooper's Topos ↔ Kratzer's ⟨ModalBase, OrderingSource⟩

Cooper §6.4 explicitly positions topoi as the TTR replacement for Kratzer's conversational backgrounds: "topoi replace accessibility relations between possible worlds." This section makes the replacement claim Lean-checkable by constructing a faithful translation in both directions and proving equivalence on the necessity/possibility operators.

Translation (kratzerToTopos): a Kratzer triple ⟨f, g, w⟩ together with a proposition p induces a topos whose background is the Kratzer best-worlds set (from f/g at w) and whose foreground records membership in p.

Agreement theorem (kratzer_topos_nec_iff): Cooper's Topos.inducedNec on the translated topos coincides with Kratzer's necessity operator. Same for possibility.

Disagreement theorem (ttr_kratzer_collapse_disagree): Cooper's Topos.nec_implies_poss requires Nonempty τ.Bg as a side condition (empty topoi vacuously satisfy inducedNec but cannot satisfy inducedPoss). Kratzer's necessity → possibility (the D axiom) holds under the same side condition (Nonempty (bestWorlds f g w)). The two frameworks AGREE on D-axiom validity gating, contra a naive reading that TTR avoids the D-issue altogether.

This is the load-bearing comparison that previous prose-only deferrals in the Modality docstring (§6.4 prose, "Topoi replace Kratzer's conversational backgrounds...") promised but did not deliver.

def Phenomena.Modality.Studies.Cooper2023.kratzerToTopos {W : Type} (f : Core.Logic.Intensional.ModalBase W) (g : Core.Logic.Intensional.OrderingSource W) (w : W) (p : W → Prop) : Topos

Kratzer-to-Cooper translation. A modal base + ordering source + evaluation world + proposition induces a Cooper topos:

• Background: the Kratzer-best worlds (as a Subtype of W).
• Foreground: PLift of p evaluated at the world.

The Subtype encoding ensures the topos's Bg carries exactly the worlds Kratzer's Best(f,g,w) selects.

Equations

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

theorem Phenomena.Modality.Studies.Cooper2023.kratzer_topos_nec_iff {W : Type} (f : Core.Logic.Intensional.ModalBase W) (g : Core.Logic.Intensional.OrderingSource W) (w : W) (p : W → Prop) : (kratzerToTopos f g w p).inducedNec ↔ Semantics.Modality.Kratzer.necessity f g p w

Agreement on necessity. Cooper's Topos.inducedNec over the Kratzer-derived topos coincides with Kratzer's necessity f g p w.

theorem Phenomena.Modality.Studies.Cooper2023.kratzer_topos_poss_iff {W : Type} (f : Core.Logic.Intensional.ModalBase W) (g : Core.Logic.Intensional.OrderingSource W) (w : W) (p : W → Prop) : (kratzerToTopos f g w p).inducedPoss ↔ Semantics.Modality.Kratzer.possibility f g p w

Agreement on possibility. Cooper's Topos.inducedPoss over the Kratzer-derived topos coincides with Kratzer's possibility f g p w.

theorem Phenomena.Modality.Studies.Cooper2023.ttr_kratzer_d_axiom_agree {W : Type} (f : Core.Logic.Intensional.ModalBase W) (g : Core.Logic.Intensional.OrderingSource W) (w : W) (p : W → Prop) (hne : Nonempty { w' : W // w' ∈ Semantics.Modality.Kratzer.bestWorlds f g w }) : Semantics.Modality.Kratzer.necessity f g p w → Semantics.Modality.Kratzer.possibility f g p w

D axiom shared gating. Cooper's Topos.nec_implies_poss requires Nonempty τ.Bg because empty topoi satisfy inducedNec vacuously but fail inducedPoss. Translated through the bridge, the same side condition is Nonempty (bestWorlds f g w) — exactly when Kratzer's D axiom holds. The two frameworks agree on the side condition, contra a naive reading that one side avoids the issue.

theorem Phenomena.Modality.Studies.Cooper2023.ttr_kratzer_modal_arithmetic_agree {W : Type} (f : Core.Logic.Intensional.ModalBase W) (g : Core.Logic.Intensional.OrderingSource W) (w : W) (p : W → Prop) : ((kratzerToTopos f g w p).inducedNec ↔ Semantics.Modality.Kratzer.necessity f g p w) ∧ ((kratzerToTopos f g w p).inducedPoss ↔ Semantics.Modality.Kratzer.possibility f g p w)

The disagreement is structural, not modal. The bridge proves that TTR Topos-induced modality and Kratzer best-world modality are pointwise equivalent on the same data. So any apparent disagreement between the two frameworks (broccoli case studies, ought/can scenarios) is a disagreement about what counts as the right modal base + ordering source — not about the necessity/possibility primitives themselves.

This refutes the casual reading that "TTR replaces Kratzer's modal backgrounds with topoi" implies a different modal arithmetic. The arithmetic is the same; the framework difference is whether modal data lives in worlds (Kratzer) or situations (Cooper).