PTQ Syntactic Categories and the Category-to-Type Correspondence

[dowty-wall-peters-1981] Ch. 7, Definitions 7-1 through 7-3 [Mon73]

Montague's PTQ fragment defines an infinite set of syntactic categories recursively, then establishes a uniform correspondence between categories and IL types. This correspondence is the formal bridge from grammar to semantics: it guarantees that every expression of a given syntactic category translates into an IL expression of the corresponding logical type.

Key definitions

• PtqCat — syntactic categories (Def 7-1): t, e, A/B, A//B
• catToTy — the category-to-type function f (Bennett's Def 7-3)
• Named abbreviations for the PTQ categories from Table 7-1

The slash distinction

A/B and A//B are syntactically distinct but correspond to the same logical type ⟨⟨s, f(B)⟩, f(A)⟩. The difference is purely syntactic:

• A/B: B is in an extensional position (but the type still takes an intension)
• A//B: B is in an intensional (oblique) position

Both slash types take the intension of their argument as input. This is Montague's key design decision: uniformly intensionalize all functor-argument composition, then recover extensionality via meaning postulates when needed.

inductive Intensional.CategoryType.PtqCat : Type

PTQ syntactic categories ([dowty-wall-peters-1981] Def 7-1).

1. t and e are syntactic categories.
2. If A and B are syntactic categories, then A/B and A//B are syntactic categories.

A/B denotes a functor that combines with an expression of category B to yield an expression of category A. A//B is syntactically distinct but semantically equivalent (same IL type).

• t : PtqCat
• e : PtqCat
• slash : PtqCat → PtqCat → PtqCat
• dslash : PtqCat → PtqCat → PtqCat

def Intensional.CategoryType.instReprPtqCat.repr : PtqCat → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Intensional.CategoryType.instReprPtqCat : Repr PtqCat

Equations

• Intensional.CategoryType.instReprPtqCat = { reprPrec := Intensional.CategoryType.instReprPtqCat.repr }

@[implicit_reducible]

instance Intensional.CategoryType.instDecidableEqPtqCat : DecidableEq PtqCat

Equations

• Intensional.CategoryType.instDecidableEqPtqCat = Intensional.CategoryType.instDecidableEqPtqCat.decEq

def Intensional.CategoryType.instDecidableEqPtqCat.decEq (x✝ x✝¹ : PtqCat) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Intensional.CategoryType.instDecidableEqPtqCat.decEq Intensional.CategoryType.PtqCat.t Intensional.CategoryType.PtqCat.t = isTrue ⋯
• Intensional.CategoryType.instDecidableEqPtqCat.decEq Intensional.CategoryType.PtqCat.t Intensional.CategoryType.PtqCat.e = isFalse Intensional.CategoryType.instDecidableEqPtqCat.decEq._proof_1
• Intensional.CategoryType.instDecidableEqPtqCat.decEq Intensional.CategoryType.PtqCat.t (a.slash a_1) = isFalse ⋯
• Intensional.CategoryType.instDecidableEqPtqCat.decEq Intensional.CategoryType.PtqCat.t (a.dslash a_1) = isFalse ⋯
• Intensional.CategoryType.instDecidableEqPtqCat.decEq Intensional.CategoryType.PtqCat.e Intensional.CategoryType.PtqCat.t = isFalse Intensional.CategoryType.instDecidableEqPtqCat.decEq._proof_4
• Intensional.CategoryType.instDecidableEqPtqCat.decEq Intensional.CategoryType.PtqCat.e Intensional.CategoryType.PtqCat.e = isTrue ⋯
• Intensional.CategoryType.instDecidableEqPtqCat.decEq Intensional.CategoryType.PtqCat.e (a.slash a_1) = isFalse ⋯
• Intensional.CategoryType.instDecidableEqPtqCat.decEq Intensional.CategoryType.PtqCat.e (a.dslash a_1) = isFalse ⋯
• Intensional.CategoryType.instDecidableEqPtqCat.decEq (a.slash a_1) Intensional.CategoryType.PtqCat.t = isFalse ⋯
• Intensional.CategoryType.instDecidableEqPtqCat.decEq (a.slash a_1) Intensional.CategoryType.PtqCat.e = isFalse ⋯
• Intensional.CategoryType.instDecidableEqPtqCat.decEq (a.slash a_1) (a_2.dslash a_3) = isFalse ⋯
• Intensional.CategoryType.instDecidableEqPtqCat.decEq (a.dslash a_1) Intensional.CategoryType.PtqCat.t = isFalse ⋯
• Intensional.CategoryType.instDecidableEqPtqCat.decEq (a.dslash a_1) Intensional.CategoryType.PtqCat.e = isFalse ⋯
• Intensional.CategoryType.instDecidableEqPtqCat.decEq (a.dslash a_1) (a_2.slash a_3) = isFalse ⋯

@[reducible, inline]

abbrev Intensional.CategoryType.PtqCat.IV : PtqCat

IV = t/e — intransitive verb (phrase): run, walk, talk.

Equations

• Intensional.CategoryType.PtqCat.IV = Intensional.CategoryType.PtqCat.t.slash Intensional.CategoryType.PtqCat.e

@[reducible, inline]

abbrev Intensional.CategoryType.PtqCat.CN : PtqCat

CN = t//e — common noun: man, woman, fish, unicorn.

Equations

• Intensional.CategoryType.PtqCat.CN = Intensional.CategoryType.PtqCat.t.dslash Intensional.CategoryType.PtqCat.e

@[reducible, inline]

abbrev Intensional.CategoryType.PtqCat.T : PtqCat

T = t/IV = t/(t/e) — term phrase (NP): John, Mary, every man.

Equations

• Intensional.CategoryType.PtqCat.T = Intensional.CategoryType.PtqCat.t.slash Intensional.CategoryType.PtqCat.IV

@[reducible, inline]

abbrev Intensional.CategoryType.PtqCat.TV : PtqCat

TV = IV/T — transitive verb: find, lose, eat, seek.

Equations

• Intensional.CategoryType.PtqCat.TV = Intensional.CategoryType.PtqCat.IV.slash Intensional.CategoryType.PtqCat.T

@[reducible, inline]

abbrev Intensional.CategoryType.PtqCat.IAV : PtqCat

IAV = IV//IV — intransitive adverb: rapidly, slowly, allegedly.

Equations

• Intensional.CategoryType.PtqCat.IAV = Intensional.CategoryType.PtqCat.IV.dslash Intensional.CategoryType.PtqCat.IV

@[reducible, inline]

abbrev Intensional.CategoryType.PtqCat.DET : PtqCat

DET = T/CN — determiner: every, the, a(n).

Equations

• Intensional.CategoryType.PtqCat.DET = Intensional.CategoryType.PtqCat.T.slash Intensional.CategoryType.PtqCat.CN

@[reducible, inline]

abbrev Intensional.CategoryType.PtqCat.SAdv : PtqCat

t/t — sentence adverb: necessarily.

Equations

• Intensional.CategoryType.PtqCat.SAdv = Intensional.CategoryType.PtqCat.t.slash Intensional.CategoryType.PtqCat.t

@[reducible, inline]

abbrev Intensional.CategoryType.PtqCat.SCV : PtqCat

IV/t — sentence-complement verb: believe, assert.

Equations

• Intensional.CategoryType.PtqCat.SCV = Intensional.CategoryType.PtqCat.IV.slash Intensional.CategoryType.PtqCat.t

@[reducible, inline]

abbrev Intensional.CategoryType.PtqCat.ICV : PtqCat

IV//IV — infinitive-complement verb: try, wish.

Equations

• Intensional.CategoryType.PtqCat.ICV = Intensional.CategoryType.PtqCat.IV.dslash Intensional.CategoryType.PtqCat.IV

@[reducible, inline]

abbrev Intensional.CategoryType.PtqCat.Prep : PtqCat

IAV/T — preposition (VP-modifying): in, about.

Equations

• Intensional.CategoryType.PtqCat.Prep = Intensional.CategoryType.PtqCat.IAV.slash Intensional.CategoryType.PtqCat.T

def Intensional.CategoryType.catToTy : PtqCat → Ty

The category-to-type function f ([dowty-wall-peters-1981] Def 7-3).

Bennett's simplified system, adopted by DWP for the remainder of the book:

• f(t) = t
• f(CN) = f(IV) = ⟨e, t⟩ (basic syntactic categories)
• f(A/B) = f(A//B) = ⟨⟨s, f(B)⟩, f(A)⟩

Both slash types map to the same IL type: the functor always takes the intension ⟨s, f(B)⟩ of its argument, reflecting Montague's uniform intensionalization of functor-argument composition.

Equations

• Intensional.CategoryType.catToTy Intensional.CategoryType.PtqCat.t = Intensional.Ty.t
• Intensional.CategoryType.catToTy Intensional.CategoryType.PtqCat.e = Intensional.Ty.e
• Intensional.CategoryType.catToTy (a.slash a_1) = ((Intensional.CategoryType.catToTy a_1).intens ⇒ Intensional.CategoryType.catToTy a)
• Intensional.CategoryType.catToTy (a.dslash a_1) = ((Intensional.CategoryType.catToTy a_1).intens ⇒ Intensional.CategoryType.catToTy a)

Each named category maps to the type listed in DWP Table 7-3 (Bennett's version). These are definitional equalities.

theorem Intensional.CategoryType.catToTy_CN : catToTy PtqCat.CN = (Ty.e.intens ⇒ Ty.t)

CN : ⟨⟨s, e⟩, t⟩ — set of individual concepts.

theorem Intensional.CategoryType.catToTy_IV : catToTy PtqCat.IV = (Ty.e.intens ⇒ Ty.t)

IV : ⟨⟨s, e⟩, t⟩ — set of individual concepts. CN and IV have the same IL type (both "end in" ⟨e, t⟩ under Bennett).

theorem Intensional.CategoryType.catToTy_CN_eq_IV : catToTy PtqCat.CN = catToTy PtqCat.IV

CN and IV correspond to the same IL type.

theorem Intensional.CategoryType.catToTy_T : catToTy PtqCat.T = ((Ty.e.intens ⇒ Ty.t).intens ⇒ Ty.t)

T : ⟨⟨s, ⟨⟨s, e⟩, t⟩⟩, t⟩ — set of properties of individual concepts.

theorem Intensional.CategoryType.catToTy_TV : catToTy PtqCat.TV = (((Ty.e.intens ⇒ Ty.t).intens ⇒ Ty.t).intens ⇒ Ty.e.intens ⇒ Ty.t)

TV : ⟨⟨s, ⟨⟨s, ⟨⟨s, e⟩, t⟩⟩, t⟩⟩, ⟨⟨s, e⟩, t⟩⟩

theorem Intensional.CategoryType.catToTy_IAV : catToTy PtqCat.IAV = ((Ty.e.intens ⇒ Ty.t).intens ⇒ Ty.e.intens ⇒ Ty.t)

IAV : ⟨⟨s, ⟨⟨s, e⟩, t⟩⟩, ⟨⟨s, e⟩, t⟩⟩

theorem Intensional.CategoryType.catToTy_DET : catToTy PtqCat.DET = ((Ty.e.intens ⇒ Ty.t).intens ⇒ (Ty.e.intens ⇒ Ty.t).intens ⇒ Ty.t)

DET : ⟨⟨s, ⟨⟨s, e⟩, t⟩⟩, ⟨⟨s, ⟨⟨s, e⟩, t⟩⟩, t⟩⟩

theorem Intensional.CategoryType.catToTy_SAdv : catToTy PtqCat.SAdv = (Ty.t.intens ⇒ Ty.t)

t/t : ⟨⟨s, t⟩, t⟩ — set of propositions.

theorem Intensional.CategoryType.catToTy_SCV : catToTy PtqCat.SCV = (Ty.t.intens ⇒ Ty.e.intens ⇒ Ty.t)

IV/t : ⟨⟨s, t⟩, ⟨⟨s, e⟩, t⟩⟩

theorem Intensional.CategoryType.slash_dslash_same_type (a b : PtqCat) : catToTy (a.slash b) = catToTy (a.dslash b)

Single/double slash erase to the same type.

theorem Intensional.CategoryType.catToTy_slash_is_intens (a b : PtqCat) : catToTy (a.slash b) = ((catToTy b).intens ⇒ catToTy a)

All functor categories have intension types as their argument type.

theorem Intensional.CategoryType.catToTy_result (a b : PtqCat) : match catToTy (a.slash b) with | a_1 ⇒ τ => τ = catToTy a | x => False

A functor category's result type is the type of its output category.

theorem Intensional.CategoryType.catToTy_arg (a b : PtqCat) : match catToTy (a.slash b) with | σ.intens ⇒ a => σ = catToTy b | x => False

A functor category's argument type is the intensionalized type of its input category.

def Intensional.CategoryType.PtqCat.isConjoinable (c : PtqCat) : Bool

A PTQ category is conjoinable if its corresponding type is.

Equations

• c.isConjoinable = (Intensional.CategoryType.catToTy c).isConjoinable

theorem Intensional.CategoryType.t_conjoinable : PtqCat.t.isConjoinable = true

Sentences (t) are conjoinable.

theorem Intensional.CategoryType.IV_conjoinable : PtqCat.IV.isConjoinable = true

VPs (IV) are conjoinable (⟨⟨s,e⟩, t⟩ ends in t).

theorem Intensional.CategoryType.T_conjoinable : PtqCat.T.isConjoinable = true

Term phrases (T) are conjoinable (⟨⟨s, ⟨⟨s,e⟩,t⟩⟩, t⟩ ends in t).

theorem Intensional.CategoryType.e_not_conjoinable : PtqCat.e.isConjoinable = false

Entities (e) are not conjoinable.