Sutton (2024) — Common Nouns as Predicates vs. Types

@cite{sutton-2024} @cite{chatzikyriakidis-luo-2020} @cite{cooper-2023} @cite{luo-2012} @cite{pustejovsky-1995}

@cite{sutton-2024} surveys the choice between Montagovian predicate denotations (man : Entity → Bool) and TTR/MTT type denotations (Man : Type, with a : Man witnessing manhood). The choice is not a notational variant: it determines whether selectional restriction violations are type errors or merely false, and whether co-extensional predicates can be intensionally distinguished.

This study file owns both halves of the argument:

• §1. Bridge — formal equivalence where Montague and TTR coincide (basic extensional predication), via predToPtype/ptypeToPred.
• §2. Selectional restrictions as type errors — Sutton's §4 argument, demonstrated on a small Animate/Inanimate ontology.
• §3. Hyperintensionality — Sutton's §3.1 argument: TTR's IType preserves intensional distinctions Montague's predicate equality collapses (groundhog ≠ woodchuck).
• §4. Equivalence boundary — the exact extent of the equivalence.
• §5. SubtypeOf-bearing typed composition — Sutton's §4 / Luo's MTT direction: subtyping makes restrict work, removing instances breaks named theorems.
• §6. Complement coercion — meaning-changing type shifts (telic quale: "enjoy the book" → "enjoy reading the book"), contrasted structurally with restrict.

This file consolidates the former TypeTheoretic/CNsAsTypes.lean (§§1–4) and TypeTheoretic/Selectional.lean (§§5–6), absorbed here under their shared Sutton-2024 anchor. Neither had any external consumer beyond this study's argument.

def Phenomena.Polysemy.Studies.Sutton2024.predToPtype {E : Type} (p : E → Bool) : Semantics.TypeTheoretic.PredType E

Lift a Montague predicate E → Bool to a TTR ptype E → Type. The resulting type family is inhabited at e iff p e = true.

Equations

• Phenomena.Polysemy.Studies.Sutton2024.predToPtype p e = Semantics.TypeTheoretic.propT (p e = true)

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.predToPtype_decidable {E : Type} (p : E → Bool) (e : E) : Decidable (Nonempty (predToPtype p e))

Inhabitation of predToPtype p e is decidable (since p e = true is).

Equations

• Phenomena.Polysemy.Studies.Sutton2024.predToPtype_decidable p e = if h : p e = true then isTrue ⋯ else isFalse ⋯

def Phenomena.Polysemy.Studies.Sutton2024.ptypeToPred {E : Type} (P : Semantics.TypeTheoretic.PredType E) [(e : E) → Decidable (Nonempty (P e))] : E → Bool

Project a TTR ptype back to a Montague predicate. Requires decidable inhabitation (satisfied by any finite ptype).

Equations

• Phenomena.Polysemy.Studies.Sutton2024.ptypeToPred P e = decide (Nonempty (P e))

theorem Phenomena.Polysemy.Studies.Sutton2024.montague_ttr_equiv {E : Type} (p : E → Bool) (e : E) : p e = true ↔ Nonempty (predToPtype p e)

Bridge theorem: Montague predication and TTR type inhabitation agree when connected by predToPtype.

p e = true ↔ Nonempty (predToPtype p e) — the predicate holds of e iff the corresponding ptype is inhabited (has a witness).

theorem Phenomena.Polysemy.Studies.Sutton2024.roundtrip_pred {E : Type} (p : E → Bool) (e : E) : ptypeToPred (predToPtype p) e = p e

The round-trip ptypeToPred ∘ predToPtype recovers the original predicate.

theorem Phenomena.Polysemy.Studies.Sutton2024.propExtension_agrees {E : Type} (p : E → Bool) (e : E) : Semantics.TypeTheoretic.propExtension (predToPtype p) e ↔ p e = true

TTR propExtension coincides with our bridge on lifted predicates.

In Montague's STT, every entity has the same type e. A verb like "laugh" takes any entity and returns true or false. There is no structural distinction between a category mistake ("the chair laughed") and contingent falsity ("Mary didn't laugh").

In TTR/MTT, verbs can require arguments of specific types. "Laugh" takes Animate, not Entity. A chair is not Animate, so the predication doesn't compose — it's not false, it's ill-typed.

@cite{sutton-2024} §4: "In MTT [...] common nouns are interpreted as types [...] selectional restrictions are type requirements."

inductive Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.Animate : Type

Ontological sorts (TTR types for entity subclasses).

• john : Animate
• mary : Animate

inductive Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.Inanimate : Type

• chair : Inanimate
• rock : Inanimate

inductive Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.FlatEntity : Type

In Montague, everything is an Entity. Chairs and people cohabit.

• john : FlatEntity
• mary : FlatEntity
• chair : FlatEntity
• rock : FlatEntity

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.instDecidableEqFlatEntity : DecidableEq FlatEntity

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.instDecidableEqFlatEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.laughs_montague : FlatEntity → Bool

Montague predicate: laughs is defined on ALL entities.

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.laughs_montague Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.FlatEntity.john = true
• Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.laughs_montague Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.FlatEntity.mary = false
• Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.laughs_montague Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.FlatEntity.chair = false
• Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.laughs_montague Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.FlatEntity.rock = false

theorem Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.montague_chair_laughed : laughs_montague FlatEntity.chair = false

In Montague, "the chair laughed" composes and evaluates to false. It's the same kind of thing as "Mary didn't laugh" — both are false.

theorem Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.montague_mary_didnt_laugh : laughs_montague FlatEntity.mary = false

theorem Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.montague_conflates_mistakes : laughs_montague FlatEntity.chair = false ∧ laughs_montague FlatEntity.mary = false

There's no structural way to distinguish category mistakes from contingent falsity — both are just false.

def Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.laughs_ttr : Animate → Bool

TTR predicate: laughs is typed to require Animate arguments. "The chair laughed" doesn't evaluate to false — it doesn't typecheck.

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.laughs_ttr Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.Animate.john = true
• Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.laughs_ttr Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.Animate.mary = false

theorem Phenomena.Polysemy.Studies.Sutton2024.SelectionalDemo.ttr_distinguishes_sorts : (∀ (a : Animate), ∃ (b : Bool), laughs_ttr a = b) ∧ ∀ (e : FlatEntity), ∃ (b : Bool), laughs_montague e = b

In TTR, contingent falsity (Mary doesn't laugh) is well-typed but false. Category mistakes (chair laughs) don't typecheck at all. The selectional restriction prevents composition, rather than evaluating to false.

Montague predicates are functions E → Bool. Two predicates with the same extension are definitionally equal by funext. TTR types carry intensional identity — two types can have the same witnesses yet remain distinct.

@cite{sutton-2024} §3.1: "there is nothing which prevents two types from being associated with exactly the same set of objects."

theorem Phenomena.Polysemy.Studies.Sutton2024.HyperDemo.montague_extensional {E : Type} (p q : E → Bool) (h : ∀ (e : E), p e = q e) : p = q

Two Montague predicates with the same extension are equal.

theorem Phenomena.Polysemy.Studies.Sutton2024.HyperDemo.montague_collapses_attitudes (p_groundhog p_woodchuck : SelectionalDemo.FlatEntity → Bool) : (∀ (e : SelectionalDemo.FlatEntity), p_groundhog e = p_woodchuck e) → p_groundhog = p_woodchuck

The consequence for attitude reports: Montague cannot distinguish "John believes a groundhog is outside" from "John believes a woodchuck is outside" — the belief content is the same function. TTR can.

theorem Phenomena.Polysemy.Studies.Sutton2024.HyperDemo.ttr_preserves_attitudes : have groundhog := { carrier := Unit, name := "groundhog" }; have woodchuck := { carrier := Unit, name := "woodchuck" }; groundhog.extEquiv woodchuck ∧ ¬groundhog.intEq woodchuck

TTR preserves the distinction: groundhog ≠ woodchuck as ITypes, even when co-extensional. Attitude verbs can be sensitive to this.

For basic extensional predication over a fixed domain without selectional restrictions or attitude contexts, Montague predicates and TTR ptypes are interchangeable. The bridge is predToPtype/ ptypeToPred, and the equivalence is montague_ttr_equiv.

The approaches diverge exactly when:

1. Selectional restrictions matter (§2)
2. Hyperintensional contexts arise (§3)
3. Copredication requires dot types (see Studies/Gotham2017.lean)

These are precisely @cite{sutton-2024}'s arguments for rich type theories.

theorem Phenomena.Polysemy.Studies.Sutton2024.equivalence_boundary {E : Type} (p : E → Bool) : (∀ (e : E), p e = true ↔ Nonempty (predToPtype p e)) ∧ ∀ (e : E), ptypeToPred (predToPtype p) e = p e

Summary: the predicate/type duality is an equivalence modulo three phenomena. We can state the exact boundary.

Makes SubtypeOf from TypeTheoretic/Core.lean load-bearing by wiring it into typed composition. Verbs declare the ontological sort they require; composition through restrict succeeds only when SubtypeOf A B is available. Removing a SubtypeOf instance breaks the downstream derivation — that is the "load" the instance bears.

inductive Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.Human : Type

• john : Human
• mary : Human

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instDecidableEqHuman : DecidableEq Human

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instDecidableEqHuman x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprHuman : Repr Human

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprHuman = { reprPrec := Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprHuman.repr }

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprHuman.repr : Human → ℕ → Std.Format

Equations

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

inductive Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.Animal : Type

• fido : Animal

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instDecidableEqAnimal : DecidableEq Animal

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instDecidableEqAnimal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprAnimal : Repr Animal

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprAnimal = { reprPrec := Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprAnimal.repr }

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprAnimal.repr : Animal → ℕ → Std.Format

Equations

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

inductive Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.Animate : Type

Animate: the union of Human and Animal. Domain of "laugh", "sleep".

• human : Human → Animate
• animal : Animal → Animate

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instDecidableEqAnimate.decEq (x✝ x✝¹ : Animate) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instDecidableEqAnimate : DecidableEq Animate

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instDecidableEqAnimate = Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instDecidableEqAnimate.decEq

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprAnimate : Repr Animate

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprAnimate = { reprPrec := Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprAnimate.repr }

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprAnimate.repr : Animate → ℕ → Std.Format

Equations

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

inductive Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.PhysObj : Type

• table : PhysObj
• book_phys : PhysObj

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instDecidableEqPhysObj : DecidableEq PhysObj

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instDecidableEqPhysObj x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprPhysObj : Repr PhysObj

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprPhysObj = { reprPrec := Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprPhysObj.repr }

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprPhysObj.repr : PhysObj → ℕ → Std.Format

Equations

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

inductive Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.Info : Type

• hamlet_info : Info

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instDecidableEqInfo : DecidableEq Info

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instDecidableEqInfo x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprInfo : Repr Info

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprInfo = { reprPrec := Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprInfo.repr }

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprInfo.repr : Info → ℕ → Std.Format

Equations

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

inductive Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.Entity : Type

Top-level entity sort. Everything coerces here.

• animate : Animate → Entity
• physObj : PhysObj → Entity
• info : Info → Entity

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instDecidableEqEntity : DecidableEq Entity

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instDecidableEqEntity = Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instDecidableEqEntity.decEq

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instDecidableEqEntity.decEq (x✝ x✝¹ : Entity) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprEntity : Repr Entity

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprEntity = { reprPrec := Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprEntity.repr }

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instReprEntity.repr : Entity → ℕ → Std.Format

Equations

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

Each instance is load-bearing: removing it breaks a named theorem below. The hierarchy:

Human ⊑ Animate ⊑ Entity
Animal ⊑ Animate
PhysObj ⊑ Entity
Info ⊑ Entity

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instHumanAnimate : Human ⊑ Animate

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instHumanAnimate = { up := Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.Animate.human }

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instAnimalAnimate : Animal ⊑ Animate

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instAnimalAnimate = { up := Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.Animate.animal }

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instAnimateEntity : Animate ⊑ Entity

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instAnimateEntity = { up := Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.Entity.animate }

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instPhysObjEntity : PhysObj ⊑ Entity

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instPhysObjEntity = { up := Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.Entity.physObj }

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instInfoEntity : Info ⊑ Entity

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instInfoEntity = { up := Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.Entity.info }

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instHumanEntity : Human ⊑ Entity

Composite: Human ⊑ Entity via Human ⊑ Animate ⊑ Entity.

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instHumanEntity = Semantics.TypeTheoretic.subtypeTrans

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instAnimalEntity : Animal ⊑ Entity

Composite: Animal ⊑ Entity.

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.instAnimalEntity = Semantics.TypeTheoretic.subtypeTrans

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.restrict {A B : Type} [h : A ⊑ B] (P : Semantics.TypeTheoretic.Ppty B) : Semantics.TypeTheoretic.Ppty A

Restrict a property to a subtype domain. Given P : Ppty B and [SubtypeOf A B], produce Ppty A by coercing the argument up before applying P.

This is typed function application: the semantic analogue of checking that the argument type is a subtype of the parameter type. If no SubtypeOf instance exists, composition fails at the Lean type level — a category mistake, not a truth-value failure.

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.restrict P a = P (Semantics.TypeTheoretic.SubtypeOf.up a)

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.laughs : Semantics.TypeTheoretic.Ppty Animate

"laugh" selects for Animate.

Equations

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

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.thinks : Semantics.TypeTheoretic.Ppty Human

"think" selects for Human.

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.thinks Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.Human.john = Unit
• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.thinks Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.Human.mary = Unit

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.falls : Semantics.TypeTheoretic.Ppty Entity

"fall" accepts any Entity.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.falls (Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.Entity.physObj a) = Unit
• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.falls (Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.Entity.info a) = Empty

Each theorem exercises a specific SubtypeOf instance. Removing the instance makes the theorem fail to typecheck — the instance literally bears the load of the derivation.

theorem Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.john_laughs : Semantics.TypeTheoretic.IsTrue (restrict laughs Human.john)

theorem Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.mary_doesnt_laugh : Semantics.TypeTheoretic.IsFalse (restrict laughs Human.mary)

theorem Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.fido_laughs : Semantics.TypeTheoretic.IsTrue (restrict laughs Animal.fido)

theorem Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.john_falls : Semantics.TypeTheoretic.IsTrue (restrict falls Human.john)

theorem Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.table_falls : Semantics.TypeTheoretic.IsTrue (restrict falls PhysObj.table)

theorem Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.info_doesnt_fall : Semantics.TypeTheoretic.IsFalse (restrict falls Info.hamlet_info)

Compositional derivations with typed NPs

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.johnQ : Semantics.TypeTheoretic.Quant Human

"john" as a typed quantifier over Human.

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.johnQ = Semantics.TypeTheoretic.semPropName Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.Human.john

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.fidoQ : Semantics.TypeTheoretic.Quant Animal

"fido" as a typed quantifier over Animal.

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.fidoQ = Semantics.TypeTheoretic.semPropName Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.Animal.fido

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.aHumanWhoThinks : Semantics.TypeTheoretic.Quant Human

"a human who thinks" = typed indefinite with Human restrictor.

Equations

• Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.aHumanWhoThinks = Semantics.TypeTheoretic.semIndefArt Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.thinks

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.johnLaughsDeriv : Type

"john laughs" = ⟦john⟧(restrict ⟦laugh⟧) Uses instHumanAnimate to compose Human quantifier with Animate VP.

Equations

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

theorem Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.john_laughs_deriv_true : Semantics.TypeTheoretic.IsTrue johnLaughsDeriv

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.fidoLaughsDeriv : Type

"fido laughs" = ⟦fido⟧(restrict ⟦laugh⟧) Uses instAnimalAnimate.

Equations

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

theorem Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.fido_laughs_deriv_true : Semantics.TypeTheoretic.IsTrue fidoLaughsDeriv

def Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.aThinkingHumanLaughs : Type

"a human who thinks laughs" = ⟦a human who thinks⟧(restrict ⟦laugh⟧) Uses instHumanAnimate. The ExistWitness requires a Human who both thinks (restrictor) and laughs (scope, via coercion).

Equations

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

theorem Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.a_thinking_human_laughs : Semantics.TypeTheoretic.IsTrue aThinkingHumanLaughs

theorem Phenomena.Polysemy.Studies.Sutton2024.SubtypeDemo.coercion_coherence (P : Semantics.TypeTheoretic.Ppty Entity) (h : Human) : restrict P h = restrict (restrict P) h

Direct Human ⊑ Entity and chained Human ⊑ Animate ⊑ Entity produce the same result. This is the content of the coherence requirement on subtyping: the diagram commutes.

Unlike SubtypeOf (identity-preserving: a human IS an animate entity), complement coercion is meaning-changing: the coerced entity is a DIFFERENT thing. "John enjoyed the book" doesn't mean John enjoyed a physical object — it means he enjoyed reading it. The book is coerced to an event via the telic quale.

This is a distinct mechanism from subtyping, and conflating them would lose the meaning change.

inductive Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.Activity : Type

• reading : SubtypeDemo.PhysObj → Activity
• building : SubtypeDemo.PhysObj → Activity

def Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.instDecidableEqActivity.decEq (x✝ x✝¹ : Activity) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.instDecidableEqActivity : DecidableEq Activity

Equations

• Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.instDecidableEqActivity = Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.instDecidableEqActivity.decEq

def Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.instReprActivity.repr : Activity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.instReprActivity : Repr Activity

Equations

• Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.instReprActivity = { reprPrec := Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.instReprActivity.repr }

class Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.ComplementCoercion (A B : Type) : Type

Complement coercion: a meaning-changing type shift triggered by type mismatch. The coerce function produces a new entity in the target type, not a view of the old one.

• coerce : A → B

@[implicit_reducible]

instance Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.instComplementCoercionPhysObjActivity : ComplementCoercion SubtypeDemo.PhysObj Activity

Telic quale: books coerce to reading events.

Equations

• Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.instComplementCoercionPhysObjActivity = { coerce := Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.Activity.reading }

def Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.enjoy : Semantics.TypeTheoretic.Ppty Activity

"enjoy" selects for Activity.

Equations

• Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.enjoy (Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.Activity.reading a) = Unit
• Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.enjoy (Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.Activity.building a) = Unit

def Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.coerceApply {A B : Type} [ComplementCoercion A B] (P : Semantics.TypeTheoretic.Ppty B) : Semantics.TypeTheoretic.Ppty A

Compose through complement coercion. Structurally parallel to restrict but semantically different: the argument changes identity.

Equations

• Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.coerceApply P a = P (Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.ComplementCoercion.coerce a)

theorem Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.enjoy_book : Semantics.TypeTheoretic.IsTrue (coerceApply enjoy SubtypeDemo.PhysObj.book_phys)

"enjoy the book" via complement coercion.

theorem Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.enjoy_table : Semantics.TypeTheoretic.IsTrue (coerceApply enjoy SubtypeDemo.PhysObj.table)

restrict ≠ coerceApply

The structural distinction: restrict composes with SubtypeOf.up (the argument IS-A member of the supertype), while coerceApply composes with ComplementCoercion.coerce (the argument is MAPPED TO a different entity). Both produce Ppty A from Ppty B, but the semantic relationship is different.

Consequence: "John fell" (restrict: John is an entity) and "John enjoyed the book" (coerceApply: the book became a reading event) are composed by different mechanisms, and the type system keeps them apart.

theorem Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.restrict_is_subsumption {A B : Type} [h : A ⊑ B] (P : Semantics.TypeTheoretic.Ppty B) (a : A) : SubtypeDemo.restrict P a = P (Semantics.TypeTheoretic.SubtypeOf.up a)

restrict preserves identity: coercion is a subsumption.

theorem Phenomena.Polysemy.Studies.Sutton2024.ComplementDemo.coerceApply_is_shift {A B : Type} [h : ComplementCoercion A B] (P : Semantics.TypeTheoretic.Ppty B) (a : A) : coerceApply P a = P (ComplementCoercion.coerce a)

coerceApply changes identity: coercion is a type-shift.