内涵类型论（intension type theory），哲学-哲学-逻辑学-逻辑，带有内涵语义的类型论。在蒙塔古语法中，采用的逻辑工具就是内涵类型论。从内涵语义学的角度看，命题、个体概念和性质分别是句子、词项和一阶谓词的内涵；从内涵类型论的角度分析，句子、词项和一阶谓词的内涵是从可能世界分别到真值、个体和个体集合的函项。在通常的外延类型论中，以表示个体的类型e和表示真值的类型t为基本类型，同时规定：若a和b是任意类型，则 也是类型。内涵类型论以外延类型论为基础，并增加一条规定：若a是类型，则 也是类型。这里的s本身不是一个类型，即不存在任何一种类型为s的表达式。s代表可能世界，其作用是与任意类型a形成新的类型。一个类型为 的表达式就是一个内涵表达式，也就是一个映射函项，其定义域为可能世界集，值域是作为类型为a的表达式的外延的集合。