Chatzikyriakidis–Cooper–Gregoromichelaki–Sutton 2025: TTR intentional identity

[CCGS25] §2.3.2 treats [Gea67]'s Hob–Nob puzzle — "Hob thinks a witch has blighted Bob's mare, and Nob wonders whether she (the same witch) killed Cob's sow" — following [Ran94]'s belief-context analysis, recast by [Coo23] with record types in place of contexts: Hob's and Nob's belief contexts overlap with respect to a shared witch component, which need not be witnessed. Types, unlike sets of worlds, are individuated intensionally (extEquiv_not_intEq below), so two agents' attitudes can concern the same possibly-empty type.

This file formalizes the shared-component core of the account: Hob's and Nob's contents both have witchType as a meet component while that type is empty. The full analysis additionally aligns labels across the agents' belief contexts ("indexed by the same variable in their respective belief contexts"), giving sameness of discourse referent rather than merely of type; that refinement awaits dependent record substrate, and without it component-sharing alone cannot distinguish "the same witch" from "a witch of the same kind" — the distinction [Ede86]'s asymmetry data make empirically load-bearing.

Main declarations

• Examples.hobNob: Geach's sentence as a LinguisticExample
• witchType, hobContent, nobContent: the Hob–Nob model
• SharesComponent: a content has T as its left meet component
• intentional_identity: the contents share the empty witch type yet are intensionally distinct
• validates_hobNob: the model validates the empirical datum

Intensional types

[Coo23] §1.3: types are individuated beyond their extensions — a name-tagged wrapper over a Lean carrier suffices for the Hob–Nob model.

structure ChatzikyriakidisEtAl2025.IType : Type 1

An intensional type: a carrier tagged with an identity beyond its extension ([Coo23] §1.3).

• carrier : Type

  The underlying Lean type (extension carrier)

• name : String

  Intensional identity tag

def ChatzikyriakidisEtAl2025.IType.extEquiv (T₁ T₂ : IType) : Prop

Extensional equivalence: equivalent carriers.

Equations

• T₁.extEquiv T₂ = Nonempty (T₁.carrier ≃ T₂.carrier)

def ChatzikyriakidisEtAl2025.IType.intEq (T₁ T₂ : IType) : Prop

Intensional identity.

Equations

• T₁.intEq T₂ = (T₁ = T₂)

def ChatzikyriakidisEtAl2025.IType.meet (T₁ T₂ : IType) : IType

Meet: pair the carriers, compose the names — intensional identity is preserved through meet.

Equations

• T₁.meet T₂ = { carrier := T₁.carrier × T₂.carrier, name := T₁.name ++ " ∧ " ++ T₂.name }

TTR model of the Hob–Nob puzzle

def ChatzikyriakidisEtAl2025.witchType : IType

The shared witch type: empty carrier (no witch exists), individuated intensionally by its name.

Equations

• ChatzikyriakidisEtAl2025.witchType = { carrier := Empty, name := "witch" }

def ChatzikyriakidisEtAl2025.blightBobsMare : IType

"blighted Bob's mare" as a predicate type.

Equations

• ChatzikyriakidisEtAl2025.blightBobsMare = { carrier := Unit, name := "blighted_bobs_mare" }

def ChatzikyriakidisEtAl2025.killCobsSow : IType

"killed Cob's sow" as a predicate type.

Equations

• ChatzikyriakidisEtAl2025.killCobsSow = { carrier := Unit, name := "killed_cobs_sow" }

def ChatzikyriakidisEtAl2025.hobContent : IType

Hob's belief content: a witch who blighted Bob's mare.

Equations

• ChatzikyriakidisEtAl2025.hobContent = ChatzikyriakidisEtAl2025.witchType.meet ChatzikyriakidisEtAl2025.blightBobsMare

def ChatzikyriakidisEtAl2025.nobContent : IType

Nob's wonder content: the same witch type, met with killing Cob's sow.

Equations

• ChatzikyriakidisEtAl2025.nobContent = ChatzikyriakidisEtAl2025.witchType.meet ChatzikyriakidisEtAl2025.killCobsSow

def ChatzikyriakidisEtAl2025.SharesComponent (T C : IType) : Prop

C has T as its left meet component: witnesses of C are pairs whose first coordinate inhabits T. Two contents stand in intentional identity when they share a component in this sense.

Equations

• ChatzikyriakidisEtAl2025.SharesComponent T C = ∃ (X : ChatzikyriakidisEtAl2025.IType), C = T.meet X

theorem ChatzikyriakidisEtAl2025.sharesComponent_hobContent : SharesComponent witchType hobContent

theorem ChatzikyriakidisEtAl2025.sharesComponent_nobContent : SharesComponent witchType nobContent

theorem ChatzikyriakidisEtAl2025.isFalse_witchType : IsEmpty witchType.carrier

The witch type is empty: no witch exists.

theorem ChatzikyriakidisEtAl2025.hobContent_ne_nobContent : ¬hobContent.intEq nobContent

The two contents are intensionally distinct (their event components differ), even though both are empty.

theorem ChatzikyriakidisEtAl2025.extEquiv_not_intEq : hobContent.extEquiv nobContent ∧ ¬hobContent.intEq nobContent

The contents are extensionally equivalent (both carriers are empty) yet intensionally distinct — extensional equivalence does not entail intensional identity. An extensional semantics (Set W-style contents) identifies the two attitudes; TTR keeps them apart.

theorem ChatzikyriakidisEtAl2025.intentional_identity : SharesComponent witchType hobContent ∧ SharesComponent witchType nobContent ∧ ¬hobContent.intEq nobContent ∧ IsEmpty witchType.carrier

Intentional identity, TTR-style: Hob's and Nob's contents share the witch type as a common intensional component, are intensionally distinct contents, and the shared type is empty — both attitudes are "about the same witch-type" although no witch exists.

theorem ChatzikyriakidisEtAl2025.validates_hobNob : Examples.hobNob.judgment = Features.Judgment.acceptable ∧ SharesComponent witchType hobContent ∧ SharesComponent witchType nobContent ∧ IsEmpty witchType.carrier

The model validates Examples.hobNob's key judgment: the discourse is acceptable although no witch need exist, and the model supplies shared cross-attitude content built on an empty type.