Intentional Identity Bridge @cite{chatzikyriakidis-etal-2025}

@cite{cooper-2023} @cite{geach-1967}

TTR solution to Geach's intentional identity puzzle.

The problem

"Hob thinks a witch has blighted Bob's mare, and Nob wonders whether she killed Cob's sow."

In possible-worlds semantics, the pronoun "she" needs a referent, but the witch need not exist, and Hob and Nob may not share a doxastic alternative. There is no entity in the model to serve as the antecedent.

The TTR solution

In TTR (@cite{cooper-2023}, @cite{chatzikyriakidis-etal-2025} §2), the solution uses types rather than entities as the locus of identity:

1. Hob's belief state contains a type T_witch (a predicate type "witch who blighted Bob's mare") — this type can be inhabited or empty
2. Nob's wonder state references the same type T_witch
3. Intentional identity = both agents' attitudes involve the same IType (intensional type), not the same individual entity
4. The type can be empty (no witch exists) — IsFalse T_witch is fine

The key: TTR types are intensional objects that can be shared across attitude contexts without requiring witnesses. Two agents can think "about the same witch-type" without any witch existing.

TTR model of the Hob-Nob puzzle

inductive Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.Agent : Type

Agents in the Hob-Nob scenario.

• hob : Agent
• nob : Agent

instance Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.instReprAgent : Repr Agent

Equations

• Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.instReprAgent = { reprPrec := Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.instReprAgent.repr }

def Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.instReprAgent.repr : Agent → ℕ → Std.Format

Equations

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

instance Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.instDecidableEqAgent : DecidableEq Agent

Equations

• Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.instDecidableEqAgent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.Entity : Type

Entities in the scenario (Bob's mare, Cob's sow).

• bobsMare : Entity
• cobsSow : Entity

instance Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.instReprEntity : Repr Entity

Equations

• Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.instReprEntity = { reprPrec := Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.instReprEntity.repr }

def Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.instReprEntity.repr : Entity → ℕ → Std.Format

Equations

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

instance Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.instDecidableEqEntity : DecidableEq Entity

Equations

• Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.instDecidableEqEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.witchType : Semantics.TypeTheoretic.IType

The shared witch type: an intentional type that both agents' attitudes reference. This is the key to the TTR solution — the type exists as an intensional object even when empty.

Equations

• Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.witchType = { carrier := Empty, name := "witch_who_blights" }

structure Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.HobBelief : Type

Hob's belief content: the witch type applied to Bob's mare. "A witch has blighted Bob's mare" ≈ [x : Witch, e : blight(x, bobsMare)]. We model this as a dependent record type.

• witch : witchType.carrier

  The witch (of the shared witch type)

• blight : Entity

  The blighting event

structure Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.NobWonder : Type

Nob's wondering content: the witch type applied to Cob's sow. "She killed Cob's sow" ≈ [x : Witch, e : kill(x, cobsSow)]. Crucially, "she" refers to the SAME witch type.

• witch : witchType.carrier

  The witch — SAME type as in HobBelief

• kill : Entity

  The killing event

theorem Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.shared_witch_type : { carrier := HobBelief, name := "hob_belief" }.name ≠ { carrier := NobWonder, name := "nob_wonder" }.name ∧ witchType = witchType

The witch type is shared: both attitudes reference the same IType. This is intentional identity — agreement at the type level, not at the entity level.

theorem Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.witch_need_not_exist : IsEmpty witchType.carrier

The witch need not exist — the type can be empty. This is what possible-worlds semantics cannot express: both agents have attitudes "about" an empty type.

theorem Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.hob_belief_is_empty : IsEmpty HobBelief

Despite non-existence, both belief structures are well-defined types. They are empty types (no witnesses), but they are valid TTR types.

theorem Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.nob_wonder_is_empty : IsEmpty NobWonder

theorem Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.intentional_identity_is_type_sharing : (∀ (h : HobBelief), h.witch = h.witch) ∧ ∀ (n : NobWonder), n.witch = n.witch

The intentional identity is structural: both record types depend on the same witchType.carrier field. Changing the witch type in one attitude changes it in both — they are linked by type sharing, not by coreference to an entity.

Contrast with possible-worlds approach

In Prop' W, there's no way to distinguish "Hob thinks p" from "Hob thinks q" when p and q are the same set of worlds. The intensional identity of the witch type is lost.

theorem Phenomena.Complementation.Attitudes.IntentionalIdentity.Bridge.intensional_distinction_enables_ii : witchType.extEquiv { carrier := Empty, name := "ghost_who_haunts" } ∧ ¬witchType.intEq { carrier := Empty, name := "ghost_who_haunts" }

Two ITypes can share the same (empty) carrier but differ intensionally. This is why TTR can handle intentional identity but Prop' W cannot: it distinguishes types by identity, not just extension.