Common Nouns as Predicates vs. Types @cite{sutton-2024}

@cite{chatzikyriakidis-luo-2020} @cite{cooper-2023} @cite{luo-2012}

Montague's STT treats common nouns as predicates: man : Entity → Bool. TTR treats them as types: Man : Type, where a : Man witnesses that a is a man. @cite{sutton-2024} §§3–5 argues these are not notational variants — the choice determines whether selectional restriction violations are type errors or merely false.

This file proves the equivalence where both approaches agree, and the separation where they diverge.

The bridge

Given a Montague predicate p : E → Bool, the corresponding TTR ptype is λ e => PLift (p e = true) — inhabited exactly when the predicate holds. The bridge theorem montague_ttr_equiv proves these give the same truth conditions for basic predication.

The separation

1. Selectional restrictions: In TTR, "the chair laughed" fails to compose (no witness of Animate for chair). In Montague, it composes fine and evaluates to false. The TTR approach makes category mistakes distinguishable from contingent falsity.

2. Hyperintensionality: Co-extensional Montague predicates are equal functions (funext). Co-extensional TTR ptypes can be distinct (different IType names). TTR preserves the groundhog/woodchuck distinction; Montague collapses it.

def Comparisons.CNsAsTypes.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

• Comparisons.CNsAsTypes.predToPtype p e = Semantics.TypeTheoretic.propT (p e = true)

instance Comparisons.CNsAsTypes.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

• Comparisons.CNsAsTypes.predToPtype_decidable p e = if h : p e = true then isTrue ⋯ else isFalse ⋯

def Comparisons.CNsAsTypes.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

• Comparisons.CNsAsTypes.ptypeToPred P e = decide (Nonempty (P e))

theorem Comparisons.CNsAsTypes.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 Comparisons.CNsAsTypes.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 Comparisons.CNsAsTypes.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 Comparisons.CNsAsTypes.Animate : Type

Ontological sorts (TTR types for entity subclasses).

• john : Animate
• mary : Animate

inductive Comparisons.CNsAsTypes.Inanimate : Type

• chair : Inanimate
• rock : Inanimate

inductive Comparisons.CNsAsTypes.FlatEntity : Type

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

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

instance Comparisons.CNsAsTypes.instDecidableEqFlatEntity : DecidableEq FlatEntity

Equations

• Comparisons.CNsAsTypes.instDecidableEqFlatEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Comparisons.CNsAsTypes.laughs_montague : FlatEntity → Bool

Montague predicate: laughs is defined on ALL entities.

Equations

• Comparisons.CNsAsTypes.laughs_montague Comparisons.CNsAsTypes.FlatEntity.john = true
• Comparisons.CNsAsTypes.laughs_montague Comparisons.CNsAsTypes.FlatEntity.mary = false
• Comparisons.CNsAsTypes.laughs_montague Comparisons.CNsAsTypes.FlatEntity.chair = false
• Comparisons.CNsAsTypes.laughs_montague Comparisons.CNsAsTypes.FlatEntity.rock = false

theorem Comparisons.CNsAsTypes.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 Comparisons.CNsAsTypes.montague_mary_didnt_laugh : laughs_montague FlatEntity.mary = false

theorem Comparisons.CNsAsTypes.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 Comparisons.CNsAsTypes.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

• Comparisons.CNsAsTypes.laughs_ttr Comparisons.CNsAsTypes.Animate.john = true
• Comparisons.CNsAsTypes.laughs_ttr Comparisons.CNsAsTypes.Animate.mary = false

theorem Comparisons.CNsAsTypes.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 Comparisons.CNsAsTypes.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 Comparisons.CNsAsTypes.montague_collapses_attitudes (p_groundhog p_woodchuck : FlatEntity → Bool) : (∀ (e : 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 Comparisons.CNsAsTypes.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 TypeTheoretic/Copredication.lean)

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

theorem Comparisons.CNsAsTypes.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.