Formal Semantics in Modern Type Theories 本章研究现代类型理论中的正式语义（MTT-语义）。在第一章，尤其是1.4.1节，我们简要描述了如何在MTT-语义中解释一些基本的语言类别。现在，在上一章介绍了MTTs的一些基本结构后，我们处于更好的位置来研究MTT-语义的各种关键特性。我们将在以下几节中这样做：其中第一节，即3.1节，将继续1.4.1节的内容，详细解释如何解释一些基本的语言类别。
然后，在3.2节中，我们将阐述MTT语义学的几个与蒙塔古语义学不同的独特特点，从CNs-as-types范式开始（Ranta 1994; Luo 2012a）。一个常用名词（CN）例如"student"，可以解释为一个集合。在蒙塔古语义学中，用一个集合作为其解释来代表这个集合（例如，"student"被解释为表示学生的实体集合）1 $Student$ 类型，这个类型可以是一个基础类型，也可以是由其他类型定义的结构类型，这取决于当前的语义解释）。这个CNs-as-types（名词即类型）范式在3.2.1节中被介绍和详细阐述：它将该范式与CNs的辨识准则和集合/类型的建构概念联系起来，展示了MTTs的丰富类型结构在这个endeavor中发挥了关键的作用，并解释了这个范式相比传统的蒙塔古CNs-as-predicates（名词即谓词）范式有几个优点。
在MTT语义学中采用CNs作为类型的范例，拥有一个充足的子类型机制变得至关重要。如Ranta（1994）所承认，这已经是基础语义解释所必需的，尽管他的解决方案不完整，因为没有提出适当的子类型机制。在第3.2.2节中，我们将讨论MTT语义学中的子类型，并展示强制子类型（Luo 1999；Luo等人2012），如在2.4节中简要介绍的，在MTT语义学中起着重要的作用。我们还将考虑强制子类型如何提供有用的手段来处理语义解释中更高级的语言特性，如意义转移[meaning transfers]（Nunberg 1995）和语言强制[lingusistic coercions]（Asher和Luo 2013）。2
在3.3节中，以一个案例研究，我们将以传统分类法研究形容词修饰，展示各种形容词修饰如何在MTT语义学中建模。一方面，这显示了相当强大又丰富的类型结构，另一方面，说明了各种类型构造器如何在NL语义表示中应用。它还演示了如何在实践中应用CNs-as-types范式（此外，具体请参阅第4章和第5章）。
Basic linguistic categories 在1.4.1节中，我们简要地提到了基础语言类别在MTT-语义学中是如何被解读的，如表3.1所示，这与表1.3相同（请参见表1.1，了解示例的蒙塔古式语义）。在此，我们将更详细地解释这些内容。
Example
MTT-semantics
$\text{CN}$ man, human
$Man, Human : Type$
$\text{IV}$ talk
$talk : Human \rightarrow Prop$
$\text{ADJ}$ handsome
$handsome : Man \rightarrow Prop$
$\text{ADV}_{VP}$ quickly
$quickly : \Pi A:\mathsf{CN}. (A \rightarrow Prop) \rightarrow (Arop)$
$\text{Quantifier}$ some
$some : \Pi A:\mathsf{CN}. (A \rightarrow Prop) \rightarrow Prop$
$\text{Modified CN}$ handsome man
$\Sigma m: Man. handsome (m) : Type$
$\text{S}$ A man talks
$\exist m: Man.talk (m) : Prop$
表 3.1. Examples in MTT-semantics
在MTT-语义学中，常见名词解读为类型（详见3.2.1节），而动词和形容词解读为谓词，其作用域为动词或形容词可以有意义应用的对象。例如，正如表3.1的前三行所总结的，我们可以将“man”解释为一种类型（3.1），将“talk”解释为一种谓词（3.2），其作用域是人类，而将“帅气(handsome)”解释为一种谓词（3.3），其作用域是男人。
(3.1) $Man : Type$
(3.2) $talk : Human \rightarrow Prop$
(3.3) $handsome : Man \rightarrow Prop$
首先要注意的是，将CNs解读为类型而非谓词，其优势在于有效区分无意义和错误的表达。例如，在蒙塔古语义中，动词“talk”解释为谓词 $t a l k_{M}$ ，如（3.4）所示，其领域是所有实体的类型 $\mathbf{e}$ （如表1.1）。考虑句子（3.5），在蒙塔古语义中被赋予了（3.6）的解释，在MTT语义中则被赋予了（3.7）的解释，其中 $table _{M}: \mathbf{e} \rightarrow \mathbf{t}$ 是一个谓词，而 $Table$ 是一个类型。
(3.4) $\operatorname{talk}_{M}: \mathbf{e} \rightarrow \mathbf{t}$
(3.5) $\text{(#) A table talks.}$
(3.6) $(?) \exists x: \mathbf{e}. \operatorname{table}{M}(x) & \operatorname{talk} {M}(x)$
(3.7) $(#) \exists t: \operatorname{Table}. \operatorname{talk}(t)$
公式（3.6）是类型正确的，尽管在预期的模型中它是错误的，但这并不意味着（3.5）就毫无意义。另一方面， $talk (t)$ 的类型是错误的，因此公式（3.7）的类型也是错误的，这表明（3.5）是无意义的。我们认为，在这方面，MTT-语义学能更好地把握含义：通常情况下，句子（3.5）被视为无意义（除非在某些虚构的世界中），这正好被其在 MTT-语义学解释（3.7）中的类型错误所捕捉。这可以用稍微不同的方式来表述，即在 MTT-语义学中，选择性限制[selectional restriction]通过底层类型理论中的类型来捕捉：假设只有人类可以说话，$talk$ 不能应用于非人类的参数，如一张桌子 $t$ ，即在（3.7）中的 $talk(t)$ 的类型是错误的。注意，这是因为像 "$human$" 和 "$table$" 这样的名词短语解释为像 $Human$ 和 $Table$ 这样的类型，直观上是没有共同对象[common objects]的。3
另一个有趣的观察是，即使在如此简单的语义解释中，子类型化也已经发挥作用。例如，考虑例子（3.8）及其语义（3.9），如表3.1的最后一行所示。
(3.8) $\text{A man talks.}$
(3.9) $\exists m: \text{Man}. \text{talk}(m)$
有人会问：术语 $\operatorname{talk}(m)$ 及其公式（3.9）如何能被正确地类型化呢？$m$ 的类型是 $Man$ ，但 $talk$ 的定义域是 $Human$ ，而不是 $Man$ ！正如我们在2.4节简要讨论的，子类型在这里拯救了我们：$\operatorname{talk}(m)$ 是正确类型化的，因为 $Man$ 是 $Human$ 的子类型，因此 $m$ 可以视为一个能 $talk$ 的人类。另一种理解方式是，因为 $Man \leq H u m a n$ ，我们得出 $Human \rightarrow Prop \leq Man \rightarrow Prop$ （通过逆变性[contravariance]），因此 $talk$ 的类型是 $Man \rightarrow Prop$ ，可以应用到 $m$ 上。在3.2.2节中，我们将更详细地讨论MTT语义中的子类型。
如第二章所示，MTT为语义构造提供了有用的工具。例如，在表3.1中，"快速[quickly]"和"一些[some]"分别示例了动词修饰副词和量词的解释。这两者都使用了解释 $\mathrm {CN}$ 的宇宙 $\mathsf{CN}$ 上的 $\Pi$ 多态性，如2.3.2节所解释的。例如，在蒙塔古语义中，我们可以给出修饰动词的副词的语义类型，如(3.10)所示：它接收一个类型为 $\mathbf{e} \rightarrow \mathbf{t}$ 的谓词，并返回同类型的谓词。
(3.10) $\text{quickly}_{M}:(\mathbf{e} \rightarrow \mathbf{t}) \rightarrow(\mathbf{e} \rightarrow \mathbf{t})$
在蒙塔古语义学中，每个谓词都具有相同的类型 $\mathbf{e} \rightarrow \mathbf{t}$ ，因为只有一个实体域 $\mathbf{e}$ 。MTT语义学与此不同，其中CN解释为类型；实体类型不止一种，还有许多类型，例如Man、Table等。那么，像"quickly"这样的修饰动词的副词的类型是什么呢？在这里，类型宇宙和与之相关的 $\Pi$ 多态性机制变得有用：例如，"quickly"可以被赋予多态类型（3.11），它在 $\mathrm{CN}$ 的宇宙 $\mathsf{CN}$ 中量化，当应用到任何 $\mathrm{CN}\ A$ 时，$quickly (A):(A \rightarrow Prop ) \rightarrow (A \rightarrow Prop )$ 。举例来说，假设 $run : Human \rightarrow Prop$ ，那么"run quickly"类型为 $Human \rightarrow Prop$ 的 $quickly(Human, run)$ 。
(3.11) $\text{quickly} : \Pi A:\mathsf{CN}. (A \rightarrow Prop ) \rightarrow(A \rightarrow Prop )$
同样，量词也可以通过在宇宙 $\mathsf{CN}$ 上的 $\Pi$ 多态性进行类型化。以一个简单的例子来说，量词"some"可能通过逻辑量词 $\exists$ 在(3.12)中定义，以 $\mathsf{CN}$ 作为其限定的域，其类型化为(3.13)，如表3.1所示，即与可以应用到任何类型的逻辑量词 $\exists$ 不同，"some"只能解释 $\mathrm{CN}$ 。
(3.12) $\text{some} =\lambda A: \mathsf{CN}\ \lambda P: A \rightarrow Prop. \exists(A, P)$
(3.13) $\text{some} : \Pi A : \mathsf{CN}. (A \rightarrow \operatorname{Prop}) \rightarrow \operatorname{Prop}$
例如，（3.14）可以理解为（3.15），其中 $speak : Human \rightarrow Prop$ 且 $Student \leq Human$ 。换句话说，一些可以应用到 $Student$ ，如（3.15）。然而，一些不能应用到不解释 $\mathrm{CN}$ 的类型：例如，类型 $Prop \rightarrow Student$ 不解释任何 $\mathrm{CN}$ ，因此，（3.16）是类型错误的，因为 $Prop \rightarrow Student$ 不在 $\mathsf{CN}$ 的领域内。
(3.14) $\text{Some students spoke.}$
(3.15) $some(Student, speak)$
(3.16) $(#) some ( Prop \rightarrow Student, ...)$
$\Pi$ 多态性为我们提供了一种非常有用的表达工具，可以用来处理语义学研究中的各种语言现象。如果没有它，则很难看出如何在MTT语义中解读修饰动词的副词或量词。 $\Pi$ 多态性也用于其他语义结构中，包括例如次分形容词[subsective adjectives]如"大[large]"的构造（参见第3.3.2节）。
Several unique features of MTT-semantics 在这个部分，我们将详细阐述MTT语义学中的CNs-as-types范例以及另外两个相关特性（子类型和断言性解释）。这些特性是MTT语义学独有的，与传统的蒙塔古语义学有所不同。4
当现代类型理论用于形式语义时，CNs解释为类型，而不是谓词。换句话说：MTT-语义学采用的是CNs-作为类型的范例，这与Montague语义学中的CNs-作为谓词的范例不同。例如，考虑CN "book"：在Montague语义学中，它解释为谓词 $\operatorname{book}_{M}: \mathbf{e} \rightarrow \mathbf{t}$ ，而在现代类型理论中，它为 $B o o k$ 类型。
这种将名词类别视为类型的观念与Geach（1962）观察到的名词类别具有特殊性的观点密切相关。直观地说，一个名词类别确定了一个概念，这个概念不仅有一个应用准则，用来确定该概念是否适用于一个对象，还有一个辨识准则，用来确定该概念的两个对象是否相同。有人争论说，名词类别在这方面具有独特性，因为其他的词汇项，如动词和形容词，似乎没有这样的辨识准则（参见Baker（2003）等人的论证）。
辨识[identity]准则的概念起源可以追溯到弗雷格（1884）考虑抽象的数学对象，如数字或线条时。例如，在几何学中，方向的辨识准则是线条的平行性：线条 $A$ 的方向等于线条 $B$ 的方向，当且仅当 $A$ 和 $B$ 是平行的。吉奇注意到，这样的辨识准则存在于每一个$\mathrm{CN}$中，并且是计数的基础。古普塔（1980）对此进行了系统的研究，并给出了一些非常有趣的例子。例如，考虑以下两句话：
(3.17) $\text{EasyJet has transported 1 million passengers in 2010.}$ （2010年，易捷航空运送了一百万乘客。）
(3.18) $\text{EasyJet has transported 1 million persons in 2010.}$ （2010年，易捷航空运送了一百万人次。）
很容易看出，句子（3.17）并不暗示（3.18），因为有些人可能在2010年乘坐EasyJet旅行了不止一次。有人争论说，这是因为“乘客”和“人”这两个概念名词有着不同的辨识准则，这些标准是进行计数的基础，导致了这种现象（Geach 1962; Gupta 1980; Baker 2003）。5
辨识准则的概念和构造性的集合（类型）概念之间可以建立紧密的联系。在构造数学中，一个集合是一个"预设集"，它给出了其应用准则，同时还有一个等式，它给出了其辨识准则，用来确定集合中的两个对象是否相同（Bishop 1967；Beeson 1985）。一些现代类型理论，如Martin-Löf的类型理论（Martin-Löf 1975, 1984），最初是为了形式化构造数学而开发的，在这些理论中，每种类型都与这样的等式或辨识准则相关联。此外，值得注意的是，辨识准则的概念是对上下文敏感的。换句话说，名词类别的含义取决于其使用的上下文。例如，考虑"学生"这个词。在以下句子中，相关的辨识准则可能会有所不同，因为在（3.19）中，约翰可能教过几个班级，我们可能会合理地将在两个不同班级的学生计数两次，而在（3.20）中，我们会说在那种情况下"学生"与"人"有相同的辨识准则。
(3.19) $\text{John taught 500 students last year.}$ （去年，约翰教了500名学生。）
(3.20) $\text{1,000 students have applied for campus cards last year.}$ （去年有1,000名学生申请了校园卡。）
总的来说，一个CN应理解为一个集合等价类[setoid]，即一个类型和一个代表其相关辨识准则的等价关系的配对。CN与辨识准则相关并被形式解释为集合等价类的这一想法已在Luo(2012a)中被研究和发展。Chatzikyriakidis和Luo(2018)还指出，需要考虑不同辨识准则的更复杂情况相当罕见，在大多数现象中，相关CN的辨识准则基本相同，可以安全地忽略6
将CNs解释为类型只有在MTTs具有丰富的类型结构时才可行（而且，它们配备了适当的子类型概念 - 请参阅第3.2.2节关于子类型的内容）。例如，被交集形容词修饰的CNs可以通过 $\Sigma$ 类型来解释，如（3.21）所示（有关$\Sigma$类型，请参阅第2.2.2节）。
(3.21) $\text{handsome man} =\Sigma x :Man.handsome (x)$
注意，我们需要一种类型来代表“帅气男人”的语义 - 在（3.21）中，$\Sigma$类型起到了这个作用。我们是否有足够的类型构造器来解释各种语言合集？作为研究案例，在3.3节中，我们将考虑各种类别的形容词，并演示如何通过MTTs中的不同类型构造器来建模形容词的修饰：通过 $\Sigma$ 类型来实现交叉修饰[intersective modifications]，通过 $\Pi$ 多态性在宇宙 $\mathsf{CN}$ 上进行子集修饰[subsective modifications]，通过不相交联合类型进行负面修饰[privative modifications]，以及通过信念合集运算符[belief collection operator]进行非承诺性修饰[non-committal modifications]。这表明，MTTs具有足够且强大的类型构造器，用于表示可能由诸如CNs之类的语言实体引入的各种合集。换句话说，CNs-as-types范式在MTTs中是可行的，一般来说，MTTs通过强大的工具支持语义构造，如3.3节以及第4章和第5章所示。
有人认为，与Montagovian的CNs作为谓词范式相比，CNs作为类型范式具有若干优点，例如，通过可判定类型化来更好地处理选择限制、在语义解释中兼容使用子类型，以及对共谓词等高级语言特性的满意处理7 8
Subtyping in MTT-semantics 如2.4节所介绍，强制子类型化（Luo 1997；Luo等人 2012）为MTTs提供了一个适当的子类型化机制。在本节中，我们展示了子类型化是MTT语义成为一个可行的语义框架的关键机制，另一方面，它提供了强大的机制来形式化各种语言强制转换（Luo 2009c；Luo和Callaghan 1998）。
**子类型化：对MTT语义学至关重要。**我们首先解释子类型化在基本语义解释中的重要性。例如，假设约翰是个男人，而《战争与和平》$(W & P)$ 是一本沉重的书，如(3.22)和(3.23)所示。
(3.22) $j: Man$
(3.23) $W & P : heavy\ book$ ，其中 $\text{heavy book} =\Sigma x :Book.heavy (x)$
那么，我们应该如何解读（3.24-3.26）中的句子呢？假设"read"解释为谓词 $read : Human \rightarrow Book \rightarrow Prop$ ，那么（3.24-3.26）将分别被解释为（3.27-3.29）。但显然，乍看之下（3.27-3.29）中的任何公式都不是类型良好的：$read$ 需要其第一个参数为 $Human$ 类型，第二个参数为 $Book$ 类型，因此，在（3.27）和（3.29）中，我们不能把 $read$ 应用于 $j: Man$ ，而在（3.28）中，我们不能把 $read(h)$ 应用于 $W & P: \Sigma x: Book.heavy (x)$ 。
(3.24) $\text{John read a book.}$
(3.25) $\text{Somebody read "War and Peace".}$
(3.26) $\text{John read "War and Peace".}$
(3.27) $\exists b: B o o k . \operatorname{read}(j, b)$
(3.28) $\exists h: Human. \operatorname{read}(h, W & P)$
(3.29) $\operatorname{read}(j, W & P)$
子类型化将解决上述问题。对于上述示例，我们需要将子类型关系（3.30）和（3.31）纳入考虑，以使（3.27-3.29）类型正确。要理解这一点，只需注意子类型化通过像 $\Pi$ 和 $\Sigma$ 这样的类型构造器传播（在非依赖性情况下，还包括 $\rightarrow$ 和 $\times$ ）。例如，子类型化会逆变地[contravariantly]通过函数类型传播：如果 $A^{\prime} \leq A$ 和 $B \leq B^{\prime}$ ，那么 $A \rightarrow B \leq A^{\prime} \rightarrow B^{\prime}$ 。因此，我们有（3.32）这意味着 $read$ 可以应用于 $j: M a n$ ，而 $\operatorname{read}(h)$ 可以应用于 $W & P: \Sigma x :Book.heavy (x)$ ，从而（3.27-3.29）语义是类型正确的。
(3.30) $Man \leq Human$ (Every man is a human.「男人都是人」)
(3.31) $\Sigma x :Book.heavy (x) \leq Book$ (Every heavy book is a book.「重书都是书」)
(3.32) $( Human \rightarrow Book \rightarrow Prop ) \leq( Man \rightarrow \Sigma x: Book.heavy (x) \rightarrow Prop )$
子类型关系（3.30）和（3.31）可以通过强制子类型化来表示。如果 $M a n$ 是一个常量类型，我们可以假设存在一个常量强制子 $m h$ 使得 $Man \leq_{m h} Human$ 。如果将其定义为通过 $Man =\Sigma x :Human.male (x)$ 的 $\Sigma$ 类型，则根据（3.33），$Man$ 是 $Human$ 的子类型：第一投影是从 $\Sigma x: A . P(x)$ 到 $A$ 的强制子[coercion]，对于每个类型 $A$ 和谓词 $P: A \rightarrow Prop$ 。
(3.33) $\Sigma x: A . P(x) \leq_{\pi_{1}} A$
同样，厚重的书也是书，这也是由于(3.33)，我们有 $heavy\ book=\Sigma x :Book.heavy (x) \leq Book$ 。子类型关系(3.30)和(3.31)被实现后，公式(3.27-3.29)类型正确且它们分别解释了(3.24-3.26)中的句子。注意，尽管在强制子类型[coercive subtyping]中可以使用投影子类型关系[projective subtyping relation]（如公式3.33所示），但在传统的包容子类型[subsumptive subtyping]中，这种关系是不可用的。
备注.— 由于CNs解释为类型（例如，一些修饰的CNs视为$\Sigma$类型），一个动词可能需要有多种不同的类型。例如，在上面，"read" 需要同时具有（3.32）中的两种类型，以便语义（3.27-3.29）可以被正确类型化。这对于MTT语义来说是一个非常基本的问题，解决它是必要的。这个问题被Ranta（1994）（第62-64页）认识到，其中它称为"动词的多重分类[multiple categorization of verbs]"问题，并考虑了三种可能的解决方案，但没有一种是满意的。有一个最接近我们，它明确地使用第一投影 $\pi_{1}$ - 但这离一个完整的解决方案还差一步。使用强制子类型化（例如，将 $\pi_{1}$ 作为隐式强制），我们设法找到了一个解决方案，能够捕捉到预期的现象。
**强制子类型化：语义构造中的强大工具。**除了在MTT语义中进行基本解释的必要工具外，强制子类型化还提供了各种语义构造的强大工具，包括例如对剥夺性形容词修改的解释（参见第3.3.3节）以及对涉及共指述词的句子进行解释的点类型的规定（参见下文和第5章）。在这里，我们给出两个例子，展示如何将强制子类型化用作语义构造的有用工具。
我们的第一个例子，如Luo (2011b)所提出的，关注的是多义词[homonymy]问题，我们展示了当多义词的含义可以通过类型进行区分时，其义项枚举[sense enumeration]可以用强制子类型表示，这使得自动消歧[automated disambiguation]如预期那样进行。我们知道，一个词可能有几个不相关的含义。例如，"run"这个词在句子(3.34)和(3.35)中使用时，其含义在(3.36)和(3.37)中各不相同。
(3.34) $\text{John runs quickly.}$ （约翰跑得快。）
(3.35) $\text{John runs a bank.}$ （约翰经营一家银行。）
(3.36) $run _{1} : Human \rightarrow Prop$
(3.37) $run _{2}: Human \rightarrow Institution \rightarrow Prop$
为了表示一种词义选择模型，我们需要一个机制，能在解读句子时自动选择正确的含义。例如，当解读(3.35)时，应自动选择(3.37)中的 $run_{2}$ 。对于简单的多义词，可以通过重载（或特定场景的多态性）（Strachey 2000）来进行这样的表示。直观地说，在上述例子中，"run" 这个词被重载[overloaded]，因为它关联了不止一种含义。重载可以通过强制子类型化（Luo 1999; Bailey 1999）来支持，如下文所述。
假设"w"是一个多义词 $w_{i}: A_{i}(i=$ $1, \ldots, n$ ) ，如果 $j \neq k$ 则 $A_{j} \neq A_{k}$ 。让 $\mathbf{1}{w}$ 表示只有一个对象 $w: \mathbf{1} {w}$ 的归纳单元类型[inductive unit type]（有关单元类型的形式细节，请参见附录A2.4）。然后，多义词"w"的含义可以表示为强制转换子 $c_{i}: \mathbf{1}{w} \rightarrow A {i} (i=1, \ldots, n)$ ，定义如下：
$$
c_{i}(w)=w_{i}: A_{i}
$$
图 3.1. 使用强制子类型重载“ run”的语义
例如，单词 "run" 在 (3.36) 和 (3.37) 中分别具有两种含义，即 $run_{1}$ 和 $run_{2}$ 。这两种 "run" 的意义选择模型由以下两种强制性给出，即如图3.1所示：9 {1}\ \text{和}\ c {2}(\text {run})=\operatorname{run}_{2}
$$
例如，在任何需要 $Human \rightarrow Prop$ 类型的对象 $run$ 的语境 $\mathcal{C}{1}[ run ]$ 中，我们有
$$
\mathcal{C} {1}[run]=\mathcal{C}{1}\left[c {1}(r u n)\right]=\mathcal{C}{1}\left[run {1}\right]
$$
并且，在任何需要 $Human \rightarrow Institution \rightarrow Prop$ 的对象 $run$ 的上下文 $\mathcal{C}{2}[run]$ 中，我们有
$$
\mathcal{C} {2}[run]=\mathcal{C}{2}\left[c {2}(run)\right]=\mathcal{C}{2}\left[ run {2}\right]
$$
因此，通过自动插入强制性操作，句子(3.34)和(3.35)都将按照(3.39)和(3.40)正确解读，分别根据每个情况下的上下文类型要求选择预期的 $run {i} (i=1,2)$ 。在(3.39)中，选择了 $run {1}$ ，因为 $quickly (Human)$ （其类型在(3.38)中给出）要求其参数 $run$ 为 $Human \rightarrow Prop$ 类型的函数。在(3.40)中，选择了 $run_{2}$ ，因为 $run$ 需要一个 $Human \rightarrow Institution \rightarrow Prop$ 类型的函数。
(3.38) $quickly ( Human ):( Human \rightarrow Prop ) \rightarrow( Human \rightarrow Prop )$
因此，我们有(3.39)和(3.40)中的等式，它们根据强制子类型的强制定义规则而成立。
(3.39) $[[\text{John runs quickly}]]=q u i c k l y( run, j)= quickly (run_1, j)$
(3.40) $[[\text{John runs a bank} ]]=\exists b: Bank . run(j, b)=\exists b: Bank. run_{2}(j, b)$
我们使用了Coq证明助手(Coq 2010)来试验上述的感知选择模型[sense selection model]（Luo 2011b）：以上述的简单示例（3.39）和（3.40）为例，Coq代码可以在附录A7.2中找到。
注释：对于某些多义词，其不同的含义可能具有相同的类型，因此无法通过归类来区分。例如，当名词视为类型时，同音名词（例如"bank"）的消歧可能需要更多的语言信息（例如，在"bank"的情况下，它可能指的是一些金融事务）。为了做到这一点，我们可能需要借助部强制子[local coercions]以给出形式解释（有关更多信息，请参见罗（2011b））。
我们下一个例子取自Asher和Luo（2013），涉及到语言学上讨论的语言强制性，包括Pustejovsky（1995）等人在内的语言学文献中有详尽的讨论。它演示了强制子类型能有效应用于表示语言强制性，并且，有时候，依赖类型，如在以下例子中使用的参数化强制[parameterized coercions]，可以在表示复杂情况时发挥非常有帮助的作用。此外，我们将使用Davidson（1967）提出的事件语义框架[event semantics]，而在这些例子中，我们也将使用如Luo和Soloviev（2017）及第7.2节中研究的精细化事件类型[refined event types]，称为依赖事件类型，例如 $E v t_{A}(h)$ 。
请考虑以下涉及到"开始[start]"、"起始[begin]"和"结束[finish]"等时态动词，以及像"享受[enjoy]"这样的英文动词的例子：直观上，(3.41)与(3.42)在意义上是等价的，这说明"享受"需要一个事件作为其直接宾语。从语义上，我们将“享受”的定义为 $enjoy：Human \rightarrow Event \rightarrow Prop$ ，其中 $Event$ 是所有事件的类型，(3.43)的MTT语义解释应为(3.44)。
(3.41) $\text{Julie enjoyed (started/finished) a book.}$ （朱莉喜欢（开始/结束）一本书。）
(3.42) $\text{Julie enjoyed doing something with (e.g. reading, writing, ...) a book.}$ （朱莉喜欢做一些与书有关的事情（例如阅读、写作等）。）
(3.43) $\text{Julie enjoyed a book.}$ （朱莉喜欢一本书。）
(3.44) $\exists x: Book.enjoy(j, x)$
然而，$enjoy(j)$ 的领域类型是 $Event$ ，这与 $x$ 的类型 $Book$ 不同——那么在（3.44）中的 $enjoy (j, x)$ 如何能被正确地类型化呢？答案是，在强制子类型化的框架中，特别是在（3.45）中的子类型关系下，它声明 $reading : Book \rightarrow Event$ 作为一个强制转换，$enjoy (j, x)$ 被强制转换成（并且，从形式上讲，等同于） $enjoy (j, \operatorname{reading}(x))$ ，从而得到了正确的类型化。非正式地说，句子（3.43）被强制转换成（3.46），其语义（3.47）从形式上等同于（3.44）。
(3.45) $Book \leq_{\text {reading }} Event $
(3.46) $\text{Julie enjoyed reading a book.}$ （朱莉喜欢读书。）
(3.47) $\exists x: Book. enjoy (j, reading (x))$
注意，在以上内容中，我们只考虑了一种可能的强制子（3.45）：从“enjoy a book”到“enjoy reading a book”。然而，可能存在多种强制子：例如，（3.43）可能意味着“Julie enjoyed writing a book”，这些多重强制子可能具有不同的范围，甚至可能交织或重叠，如（3.48）所示，阅读和写作的强制范围交错重叠。
(3.48) $\text{Julie just started War and Peace,}\ \text{which Tolstoy finished after many years of hard work.}\ \text{But that will not last because she never gets through long novels.}$
（朱莉刚开始读《战争与和平》，这是托尔斯泰经过多年辛勤努力才完成的作品。但这种状况不会持久，因为她从未读完过长篇小说。）
在这样的情况下，依赖类型证明非常有用，实际上，它在Asher和Luo（2013）的研究中首次在文献中被用于形式化语言强制子。现在我们将使用Luo和Soloviev（2017）以及第7.2节研究的依赖事件类型的符号表示。我们不再考虑所有事件的单一类型 $Event$ ，而是考虑由各种“主题角色[thematic roles]”如动作者和受事者索引的精细事件类型10 $a$ 索引的系列事件类型 $\operatorname{Evt}{A}(a)$，其中 $a$ 的类型是动作者。人类是动作者：$Human \leq Agent$ ，对于任何 $h: Human$ ，${E v t {A}}(h)$ 是由 $h$ 进行的事件的类型。现在，我们可以假设在（3.48）的动词有以下类型：
$$
\begin{aligned}
& \text {start, finish, last}:\Pi h:Human.\left(\operatorname{Evt}{A}(h) \rightarrow\right. \text { Prop) } \
& \text { read, write : } \Pi h: Human. \left(\text { Book } \rightarrow \operatorname{Evt} {A}(h)\right)
\end{aligned}
$$
此外，请考虑在(3.49)中的强制操作11 $b: B o o k$ 定义。我们简化了第二种情况，假设如果他/她没有写这本书，我们会阅读这本书（我们可以考虑其他行动来考虑更多的子情况）。
(3.49) $Book \leq_{c(h)} \operatorname{Evt}_{A}(h)$ 其中 $h: Human$
(3.50) $c(h, b)= \begin{cases}\text {write}(h, b) & \text {if } h \text { wrote } b, \ \operatorname{read}(h, b) & \text {otherwise.}\end{cases}$
有了以上内容，我们现在可以将（3.48）解释为（3.51）（简化形式），其中 $j$ 和 $t$ 分别解释 "Julie" 和 "Tolstoy"，而 $\Sigma b: Book.long (b)$ 是解释"长篇书[long book]"的 $\Sigma$ -类型。在强制子类型中，（3.51）被强制转换并等同于（3.52），它在插入（3.49）中指定的强制转换后，变成了（3.53）。
(3.51)
$$
\begin{align}
&\ \ \operatorname{start}(j, W & P)\
&\wedge \operatorname{finish}(t, W & P)\
&\wedge \neg \operatorname{last}(j, W & P)\
&\wedge \forall l b:(\Sigma b: Book.long (b)) . \neg \operatorname{finish}\left(j, \pi_{1}(l b)\right)
\end{align}
$$
(3.52)
$$
\begin{align}
&\ \ \operatorname{start}(j, c(j, W & P))\
&\wedge \operatorname{finish}(t, c(t, W & P))\
&\wedge \neg \operatorname{last}(j, c(j, W & P))\
&\wedge \forall l b:(\Sigma b: Book.long (b)) . \neg \operatorname{finish}\left(j, c\left(j, \pi_{1}(l b)\right)\right)
\end{align}
$$
(3.53)
$$
\begin{align}
&\ \ \operatorname{start}(j, \operatorname{read}(j, W & P))\
&\wedge \operatorname{finish}(t, \operatorname{write} (t, W & P))\
&\wedge \neg \operatorname{last}(j, \operatorname{read}(j, W & P))\
&\wedge \forall l b:(\Sigma b: Book.long (b)) . \neg \operatorname{finish}\left(j, c\left(j, \pi_{1}(l b)\right)\right)
\end{align}
$$
为了更详细地解释，我们有关于 $start$ （每个上述公式的第一行）的以下等式：
$$
\operatorname{start}(j, W & P)=\operatorname{start}(j, c(j, W & P))=\operatorname{start}(j, \operatorname{read}(j, W & P))
$$
第一个等式成立是因为 $\operatorname{start}(j): \operatorname{Evt}{A}(j) \rightarrow \operatorname{Prop}$ 和 $W & P: B o o k \leq {c(j)} Evt_{A}(j)$，而第二个等式则根据 $c(j)$ 的定义。对于 $finish$ 和 $last$ 来说也是类似的。
如果仔细阅读，(3.53)就是(3.48)的预期语义。注意，在(3.53)的最后一个连词中，强制子 $c$ 仍然存在， $c\left(j, \pi_{1}(l b)\right)$ 无法进一步简化，因为 $l b$ 是个变量。
Judgmental interpretations and their propositional forms 在类型理论中，判断及其可推导性是基本概念：例如，断言 $a: A$ 断言对象 $a$ 是 $A$ 类型12 $Prop$ 类型的逻辑命题来解释。例如，(3.54)可以被赋予断言解释(3.55)，而(3.56)可以解释为 $Prop$ 类型的逻辑命题(3.57)。
(3.54) $\text{John is a human.}$
(3.55) $j : Human$
(3.56) $\text{ John talks.}$
(3.57) $\operatorname{talk}(j)$
在许多情况下，我们希望将一些断言性解释，比如(3.55)，转化为它们的“命题形式”：本节将对此主题进行非正式的介绍，主要关注为什么需要这样做以及如何去做。然后，在第7.1节，我们将更正式地介绍，重点在于介绍命题形式是如何引入的，更重要的是，如何合理地将其引入到MTTs中。13
一些判断是可推导的，代表正确的断言。例如，如果 $j: Man$ 和 $Man \leq Human$ ，那么上述解释(3.55)就是可导出的。一些判断则是不可推导的，作为断言解释，它们表明被解释的自然语言句子在通常情况下是无意义的。例如，(3.58)通常被认为是无意义的（除非在一些虚构的或特殊的环境中），并且其语义解释(3.59)是不可推导的。14
(3.58) $\text{(#) John is a table.}$
(3.59) $j: Table$
除了可推导和不可推导的断言外，有些断言只是潜在可推导的，因为我们没有足够的信息来进行确定，或者换句话说，一个断言是否可推导取决于环境是否被确定。例如，对于句子(3.60)，它的断言解释(3.61)是潜在可推导的，因为直观地说，约翰可能是个男学生，或者可能根本就不是学生：在前者情况下，(3.61)是可推导的，但在后者情况下是不可推导的。15
(3.60) $\text{John is a student.}$
(3.61) $j: Student$
由于断言并非命题，因此它们不能直接用于与其他命题解释的语义组合中。例如，考虑带有连词“和”的复合句子（3.62）。我们用来解释（3.62）的表达式（3.63）并不是一个结构完整的式子（或者等同于它，作为命题会类型错误），因为断言 $j: H uman$ 并不是逻辑命题，不能被用作连接词。
(3.62) $\text{John is a human and he is happy.}$
(3.63) (#) $(j: Human ) \wedge h a p p y(j)$
如何将断言性解释转化为命题，以便与其他命题性解释组合？让我们依次考虑不同类型的断言，从可推导的断言开始。
能推导时，断言性解释有一个简单的相应命题：如果 $a: A$ 是可推导的，其相应的命题是 $p_{A}(a)$ ，其中 $p_{A}: A \rightarrow Prop$ 定义如(3.64)，即对于任何类型为 $A$ 的对象，这是一个总是为真的常量谓词。例如，断言解释 $j: Human$ 对应于 $p_{\text {Human }}(j)$ ，因此，复合句子 (3.62) 可以解释为 (3.65)。换句话说，我们通过将 ( $j : Human$ ) 替换为 $p_{\text {Human }}(j)$ 使得从 (3.63) 得到 (3.65)。
(3.64) 对于任意 $x: A$ ，有 $p_{A}(x)= \mathbf{true}$
(3.65) $p_{\text {Human }}(j) \wedge \operatorname{happy}(j)$
请注意，虽然 $p_{A}$ 是一个简单的常量谓词，但它非平凡[non-trivial]，因为 $p_{A}(a)$ 的类型正确性预设了 $a$ 的类型为 $A$ 。换言之，$p_{A}(a)$ 的真实性（在元理论上）等同于断言 $a: A$ 的正确性（可推导性）。例如，当切仅当 $j: Human$ 可推导，$p_{\text {Human }}(j)$ 才为真。这就是为什么我们可以使用 $p_{A}(a)$ 作为可推导断言 $a: A$ 的命题形式。
一个不可推导的断言解释意味着被解读的句子是无意义的，正如（3.58-3.59）所示。然而，对这样的句子的否定通常是有意义的，如（3.66）所示，它否定了（3.58）。如果这样的句子用作条件的前提，那么整个句子也是有意义的。 （3.67）的句子就是这样的例子。
(3.66) $\text{John is not a table.}$
(3.67) $\text{If John were a table, Mary would be happy. }$
如何解读这样的句子呢16 $\neg$ 来否定断言解释 $j:Table$ - 因为由此产生的表达式(3.68)是不合法的，因为 $j:Table$ 并非一个命题。其次，我们不能简单地在元理论层面上否定断言 $j:Table$ ：这样做的结果(3.69)，只是一个元级别的陈述。第三，我们也不能使用谓词 $p_{T a b l e}$ ：如果像(3.70)那样做了，我们就默认了 $p_{\text {Table }}(j)$ 的良好类型性，这等同于推导出 $j:Table$ 。
(3.68) (#) $\neg(j: Table )$
(3.69) (#) $(j: Table)$ 不可推导
(3.70) (#) $\neg p_{\text {Table }}(j)$
换句话说，为了解释像（3.66）和（3.67）这样的复合句子，我们需要具备断言 $j:Table$ 的命题形式。而这样的命的确存在：命题 $\mathrm{\small IS}(Table,j)$ ，直观解释就是 " $j$ 是 $Table$ 类型 "。因此，现在可以将（3.66）和（3.67）分别解释为（3.71）和（3.72）。
(3.71) $\neg \mathrm{\small IS}( Table, j)$
(3.72) $\mathrm{\small IS} ( Table, j) \Rightarrow happy (m)$
总的来说，对于任何类型 $A$ 和 $T$ ，以及任何对象 $t: T$ ，如果一个断言解释 $t: A$ 是可推导的，那么它对应于其命题形式 $p_{A}(t)$ ，其中 $p_{A}$ 在 (3.64) 中定义。如果 $t: A$ 是不可推导的，并在某种负面语境[negative context]中以有意义的方式使用，那么其命题形式就是 $\mathrm{\small IS}(A, t)$ 。
备注.- 当一种断言解释只能潜在推导时，$\mathrm{\small IS}$-命题可暂时用作其命题形式。例如，句子（3.60）中的 $j: Student$ 的命题形式可能是 $\mathrm{IS} (Student, j)$ ，复合句子（3.73-3.75）可以分别解释为（3.76-3.78）。
(3.73) $\text{John is a student and he is happy.}$
(3.74) $\text{John is not a student.}$
(3.75) $\text{If John is a student, he is happy.}$
(3.76) $\mathrm{\small IS} ( Student, j) \wedge h a p p y(j)$
(3.77) $\neg \mathrm{\small IS}( Student, j)$
(3.78) $\mathrm{\small IS} ( Student,j) \Rightarrow h a p p y(j)$
但请注意，使用 $\mathrm{\small IS}$ 操作符的这些解释只是暂时性的，因为一旦环境完全确定，其中一些解释可能会变得不恰当。如果 $j:Student$ 可以推导出来，$\mathrm{\small IS} ( Student, j)$ 应该被 $p_{Student}(j)$ 所替代，尽管它们在逻辑上是等价的（参见第7.1节）。如果它不可推导，那么(3.77)和(3.78)的解释是可以的，但(3.76)是不恰当的（或者就像有些人所说的那样“过度生成[overgenerates]”），因为句子(3.73)通常是没有意义的。
除了断言解释外，一些自然语言句子也可能因其逻辑语义看似涉及错误类型的应用（或潜在的类型错误表达）而难以直接解读。这种情况通常出现在否定句或条件句中。例如，考虑(3.79)，这是一个关于一般动词"talk"（而非系动词"is"或"be"）的否定句。首先注意到，与通常情况下视为无意义的肯定句"Tables talk"不同，其否定句(3.79)是有意义的。然而，在解读它时，我们不能使用(3.80)，因为它涉及到的 $\operatorname{talk}(x)$ 是类型错误的（talk的参数是人，它不能应用于一张桌子）。还好，我们有一个命题 $\mathrm{\small DO}(\operatorname{talk}, x)$ ，直观上意味着" $x$ 在说话"。因此，否定句(3.79)可以被解读为(3.81)。同样地，条件句(3.82)不能被解读为(3.83)，而应解读为(3.84)。
(3.79) $\text{Tables do not talk.}$
(3.80) (#) $\forall x: Table. \neg \operatorname{talk}(x)$
(3.81) $\forall x :Table. \neg \mathrm{\small DO}(t a l k, x)$
(3.82) $\text{If a table talked, Mary would be surprised.}$
(3.83) (#) $\exists x: Table.talk (x) \Rightarrow surprised(m)$
(3.84) $\exists x: Table.\mathrm{\small DO} ( talk, x) \Rightarrow surprised (m)$
从技术上讲，算符 $\mathrm{\small IS}$ 和 $\mathrm{\small DO}$ 都可以通过否定算符 $\mathrm{\small NOT}$ 来定义，其类型在（3.85）中给出，并且 $\mathrm{\small IS}$ 和 $\mathrm{\small DO}$ 的定义通过 $\mathrm{\small NOT}$ 在（3.86）和（3.87）中分别给出。
(3.85) $\mathrm{\small NOT}: \Pi X: \mathsf{CN}\ \Pi p: X \rightarrow \operatorname{Prop}\ \Pi Y: \mathsf{CN}\ \Pi y: Y. Prop$
(3.86) 对于任意 $X: \mathsf{CN}$ 和 $y: B$ 有 $\mathrm{\small IS}(X, y)=\neg \mathrm{\small NOT}\left(X, p_{X}, B, y\right)$
(3.87) 对于任意 $p: A \rightarrow \operatorname{Prop}$ 和 $y: B$ 有 $\mathrm{\small DO}(p, y)=\neg \mathrm{\small NOT}(A, p, B, y)$
算符 $\mathrm{\small NOT}$ 已在（Xue等人，2018年，2020年；Chatzikyriakidis 和 Luo，2017b年）中被提出并研究过，且将在第7.1节中进一步研究。特别地，我们将探讨如何正式引入 $\mathrm{\small NOT}$ 。这需要通过添加 $\mathrm{\small NOT}$ 来扩展 MTTs，并证明其引入是合理的。这并非易事：在第7.1节中，将通过公理化方式引入 $\mathrm{\small NOT}$ ，并通过类型理论中的异构等式[heterogeneous equality]给出其合理性的证明（Xue等人，$2018年，2020年）。
Adjectival modification: a case study 在本部分，我们通过一个案例研究如何根据蒙塔古语言学传统中最基础的形容词分类（Kamp 1975）给予形容词修饰的语义解释。除了探究如何在MTT语义中建模形容词修饰，这个案例研究的另一动机是展示MTTs中丰富的类型结构是如何构建一系列强大且实用的语言特征的语义机制。
分类
推论
例子
类型/机制
Intersective（交叉）
$\operatorname{Adj}[\mathrm{N}] \Rightarrow \mathrm{N} & \mathrm{Adj}$ handsome man（俊友）
$\Sigma$ -类型
Subsective（细分）
$\operatorname{Adj}[\mathrm{N}] \Rightarrow \mathrm{N}$ large mouse（巨鼠）
$\Pi$ -多态
Privative（欠性）
$\operatorname{Adj}[\mathrm{N}] \Rightarrow \neg \mathrm{N}$ fake gun（假枪）
无交联合类型
Non-committal（诳语）
$\operatorname{Adj}[\mathrm{N}] \Rightarrow\ ?$ alleged criminal（谓之罪犯）
信念合集
表 3.2. 形容词的分类
这种形容词的分类考虑了四个主要的类别，如表3.2所示，根据形容词-名词配对所引出的基本推论，形容词分为交叉、细分、欠性和非承诺四类，如表3.2的第二列所示17
交叉形容词如“黑色的”，“英俊的”和“法国的”。以“黑猫”为例，相关推断如下：“黑猫”既是黑色的，又是猫。因此，黑猫也是黑色的哺乳动物，黑色的动物等等。在某种意义上，黑色这个属性（如果你愿意，也可以说是黑的色度）并不依赖于它是一只猫。这与细分形容词不同，后者表示的属性依赖于它们所修饰的名词类别。例如，一位熟练的外科医生是指在外科手术方面熟练的人，但这并不意味着他在所有方面都熟练。同样的道理也适用于尺寸形容词如大/小和高/矮。一只大老鼠可以说是作为老鼠很大，但并不意味着在说这老鼠是个巨型生物。细分形容词多少依赖于名词的语境，以便修饰后的CN（常名词）获得解释，而在交叉形容词的情况下，这种依赖性并不存在18 19
形容词修饰可以建模为从 $\mathrm{CNs}$ 到 $\mathrm{CNs}$ 的映射。在传统的蒙塔古语境中，由于 $\mathrm{CNs}$ 的语义解释是性质，我们可以将形容词修饰看作是从性质到性质的映射：例如，在"英俊的男人"中，它接受类型为 $(\mathbf{e} \rightarrow \mathbf{t}) \rightarrow(\mathbf{e} \rightarrow \mathbf{t})$ 的英俊和类型为 $\mathbf{e} \rightarrow \mathbf{t}$ 的男人，以产生另一个类型为 $\mathbf{e} \rightarrow \mathbf{t}$ 的英俊的男人。在MTT-语义学中，CNs解释为类型，这是不同的：形容词修饰接受一个形容词（建模为谓词）和一个 $\mathrm{CN}$ （建模为类型）作为输入，并产生另一种类型作为其结果。例如，修饰"英俊的男人"接受 $handsome:Man \rightarrow Prop$ 和 $Man$ 类型，并产生另一种类型。我们将在接下来的小节中展示的是，对于每一类形容词，如何设计这样的转换来建模形容词修饰。
备注 - 请注意，在我们的形容词修饰建模方法中，每类形容词的预期推理特性都只通过类型推导出来，而无需形式上的额外公理或者含义假设。我们认为这是一个重要且值得欢迎的结果。
使用 $\Sigma$ -类型进行形容词修饰的想法最初是由Mönnich（1985）、Sundholm（1986）和Ranta（1994）提出的。然而，这个解释不完整，因为它并没有为我们提供需要的适当的子类型机制，这是提议能够运作的必要条件（参见第68页的脚注21）。我们首先将解释如何使用 $\Sigma$ -类型来解释交集性形容词修饰，只是像以前那样简短提一下，然后解释我们的提议为什么是适当的。
正如本章前面所解释的， 在MTT语义学中，名词词组（CNs）视为类型，形容词则视为谓词，即类型 $A \rightarrow Prop$ 的函数，其中某个类型 $A:\mathsf{CN}$ 。举例来说，"黑色"的语义类型就是(3.88)，其中 $Object$ 是（物理）对象的类型。然后，"黑猫"的语义可以由在(3.89)中的 $\Sigma$ 类型给出，其中 $Cat$ 是猫的类型。
(3.88) $\text{black} : Object \rightarrow Prop$
(3.89) $\text{black cat} =\Sigma x: Cat. black (x)$
在这里，子类型通过类型构造器（如 $\Sigma$ ）传播的事实同样重要。我们应该理解，一只黑猫是个黑色的对象，这在子类型关系（3.91）中得到了体现，因为关系 $C a t \leq Object$ 通过 $\Sigma$ 传播。20
(3.91) $\Sigma x: Cat. black (x) \leq \Sigma x: Object. black (x)$
总的来说，我们主张，如Luo (2009c)所提出的，配备了相关的强制子类机制的 $\Sigma$ 类型为交叉形容词修饰提供了充分的语义解释。这个提议充分在两方面。首先，这种形容词修饰的期望推理符。交叉形容词与两种类型的推理相关，即，$\operatorname{Adj}[\mathrm{N}] \Rightarrow \mathrm{N} & Adj$ ，如表3.2中所示（例如，参见Kamp (1975)）。下面给出了第一种推理的例子，其中（3.92）给出了一个具体的例子，（3.93）指出了一般的非正式预期，（3.94）显示了解释这种修饰的类型 $\Sigma x: [[ N ]] . [ A d j ] $ 是 $[[ N ]]$ 的子类型，因此得到了预期的推理。这里需要一些解释。子类型关系（3.94）成立是因为我们总是将第一投影 $\pi_{1}$ 视为一种强制子；换句话说，一般来说，我们有 $\Sigma x: A . B(x) \leq_{\pi_{1}} A$ ，这是（3.94）的一个特殊情况。因此，子类型在这里起了作用：$\Sigma x: [[ N ]] . [ A d j ] $ 的每个对象都可以被视为 $[[ N ]]$ 类型的对象，因此黑猫是猫。
(3.92) $\text{A black cat is a cat.}$ （黑猫是猫）
(3.93) $\operatorname{Adj}[\mathrm{N}] \Rightarrow \mathrm{N}$
(3.94) $\Sigma x: [[ N ]] . [ A d j ] \leq [[ N ]]$
与交叉形容词相关的第二种推断对应于 $\Sigma$ 类型解释的第二个投影，如下面的(3.95-3.97)所示，最后一个实际上是直观明显的：如果 $p$ 的类型是一个 $\Sigma$ 类型，那么它必须是一个元组 $\left(n, p_{n}\right)$ ，其中 $n$ 的类型是 $[[ N ]]$ ，$p_{n}$ 是 $[ A d j ] $ 的证明（注意 $\left.\pi_{1}(p)=n\right)$ ，所以 $[ A d j ] $ 必须为真。
(3.95) $\text{A black cat is black.}$ （黑猫黑的）
(3.96) $\operatorname{Adj}[\mathrm{N}] \Rightarrow \operatorname{Adj}$
(3.97) 若 $p$ 类型为 $\Sigma x: [[ N ]] . [ A d j ] $ ，则 $[[ A d j ]]\left(\pi_{1}(p)\right)$ 为真
因此，就预期的推断而言，$\Sigma$ 类型的解释为交叉形容词修饰提供了合适的语义解读。
值得强调的是，上述使用 $\Sigma$ -类型来解释交叉形容词修饰的方法只有在两个条件下才能适用并有效21 $\Sigma$ -类型表示将无法正常工作。第二个条件更微妙，也更少被认识到 - 必须执行证明的无关性[proof irrelevance]；如果没有证明的不相关性，使用 $\Sigma$ -类型来表示形容词修饰将是不充分的。以 "black cat" 的解释（3.89）为例。要使用 $\Sigma x: Cat. black (x)$ 适当地表示 "black cat"，必须满足以下条件：两只黑猫只有在它们是同一只猫的情况下才是相同的，而与它们是如何证明为黑色无关。换句话说，对于同一只猫 $c$ ，$(c, p)$ 和 $\left(c, p^{\prime}\right)$ 应该是相同的，因为 $p$ 和 $p^{\prime}$ 是 $black (m)$ 的证明，那就应该视为同一只猫（证明的不相关性）。通过考虑（3.98）的语义解释，我们使用 $\Sigma$ -类型来解释 "乘飞机旅行的人"，可以意识到证明不相关性的必要性。
(3.98) $\text{Most persons who traveled by plane are happy.}$ （大多数乘飞机旅行的人都感到快乐）
请参阅罗氏（2012a，2019b）的更多详细信息和讨论，包括关于上述示例中的"大多数[most]"（也请查阅第15/16页的25/26脚注，以"大多数"为例的计数）。22
我们已经看到，交叉形容词可以解读为谓语，然后相应的形容词修饰可以通过带有子类型的$\Sigma$-类型进行解读。然而，这种情况对于细分形容词已经不再适用；特别是，这种简化的方法不能正确捕获细分形容词的含义。在某些情况下会导致过度生成。
例如，考虑形容词“小”。如果我们使用(3.99)和(3.100)来解释“小象[small elephant]”和“小动物[small animal]”，那么我们就会错误地得出每一头小象都是小动物的结论，正如(3.101)中的子类型关系所表达的那样，因为我们通常认为 $Elephant \leq Animal$ 。
(3.99) $\Sigma x: Elephant. SMALL(x)$
(3.100) $\Sigma x : Animal. SMALL(x)$
(3.101) (#) $\text{small elephant} \leq \text{small animal}$
考虑另一个例子：一位熟练的外科医生只在外科手术方面表现出其熟练，他可能并不是一位熟练的钢琴家，甚至可以肯定的是，他并不在所有方面都表现出熟练。实际上，“小”和“熟练”等形容词在应用于不同的名词时，可能会有不同的含义。
幸运的是，如Chatzikyriakidis和Luo（2013，2017a）所提出的，我们可以利用与宇宙 $\mathsf{CN}$ （参见第2.3.2节）相关的 $\Pi$ 多态性来得出一个简单的解决方案。这个想法是，一个小的部分性形容词的类型在 $\mathsf{CN}$ 上是多态的：例如，$small$ 有多态类型（3.102），并且，对于每一个常用名词 $A: \mathsf{CN}$ ，我们有一个谓词 $\operatorname{small}(A): A \rightarrow Prop$ 。有了这个类型，"小象"和"小动物"解释为（3.103）和（3.104）。这里，$small(Elephant)$ 和 $small(Animal)$ 是不同的谓词，就推不出错误的（3.101）了。
(3.102) $\Pi A: \mathsf{CN}. (A \rightarrow Prop )$
(3.103) $\text{small elephant} =\Sigma x : Elephant.small( Elephant,x)$
(3.104) $\text{small animal} =\Sigma x: Animal. small( Animal,x)$
我们主张，通过使用 $\Pi$ 多态性，上述解决方案很好地捕获了细分形容词的预期含义。这基本上是对一种直觉的实现，即细分形容词只与它在每个情况下修饰的特定 $\mathrm{CN}$ 有关。因此，小象只是相对于大象来说小，熟练的外科医生只是作为外科医生才熟练，等等。使用(3.102)中提出的类型，我们可以根据常用名词 $A: \mathsf{CN}$ 的选择，有不同实例的细分形容词，比如说 $small(A)$ 。
所以，总的来说，我们的建议是采用 $\Pi$ 多态性来给予细分形容词多态类型，然后使用 $\Sigma$ 类型来模拟细分形容词的修饰。显然这满足了细分形容词修饰的推理要求（3.105），就像上一节的类似论证足够证明这一点。
(3.105) $\operatorname{Adj}[\mathrm{N}] \Rightarrow \mathrm{N}$
注意，由于"普遍的[universal]"谓词 $SMALL$ 不再存在，我们就不会得出像(3.101)这样的（不希望的）推断。相反，我们只有"small"的多态语义解释的个体实例，比如 $small(Elephant)$ 、$small(Animal)$ 等。
“假的[fake]”、“虚构的[imaginary]”和“杜撰的[fictitious]”等形容词称为欠性形容词。通常，人们认为它们表现出的性质可以视为对它们修饰的名词的否定，如（3.106）中所示，并在（3.107）中予以示例。
(3.106) $\operatorname{Adj}[\mathrm{N}] \Rightarrow \neg \mathrm{N}$
(3.107) $\text{A fake gun is not a (real) gun.}$ （假枪不是[真]枪）
欠性形容词构成了可能是最具问题性的一类，因为人们对这些形容词是否真的引发了推断（3.106）并无普遍共识。例如，Partee (2010, 2007) 曾争辩过（我们认为其说法颇有说服力），依照（3.106）的定义，像“假[fake]”的形容词实际上并非真的具有欠性，反而，欠性形容词应该与类型转换和语言强制一起部分地解读。举例来说，在（3.108）和（3.109）的情况下，Partee认为，“皮毛[fur]”这个名词的含义应该扩大到既包括真皮毛也包括假皮毛。
(3.108) $\text{I don't care whether that fur is fake fur or real fur.}$ （我不在乎那件皮假皮还是真皮）
(3.109) $\text{I don't care whether that fur is fake or real.}$ （我并不在乎那件皮假的还是真的）
独立于Partee的研究(2007,2010)，第二作者在Luo (2011a)的研究中，也在MTT-语义学设定中考虑了类似的想法，提出使用不相交并集类型（参见第2.2.3节）来建模欠性形容词修饰[privative adjectival modification]。这个观点后来在Chatzikyriakidis和Luo的研究(2013,2017 a)中得到了报告，并将在这里进一步发展。让我们以“假的[fake]”为例来解释。
形容词"假的"可以用来修饰"枪"，如（3.107）所示。直观来说，所有枪的类型可能认为包括真枪和假枪。这可以通过（3.110）正式表达，它定义了所有枪的类型 $G$ 为真枪类型 $G_{R}$ 和假枪类型 $G_{F}$ 的不相交联合。形式来说，$G$ 由形如 $\operatorname{inl}(r)$ 和 $\operatorname{inr}(f)$ 的对象组成，对于真枪 $r: G_{R}$ 和假枪 $f: G_{F}$ 。
(3.110) $G=G_{R}+G_{F}$
现在可以在(3.111)和(3.112)中定义类型为 $G \rightarrow Prop$ 的谓词 $real_g$ 和 $fake_g$ ，其中 $r: G_{R}$ 和 $f: G_{F}$ 。这些谓词满足显而易见的属性，例如，对于任何枪 $x: G$ ，当且仅当 $\neg \operatorname{fake}{g}(x)$ 时， $\operatorname{real} {g}(x)$ 成立。
(3.111) $\operatorname{real}{g}(\operatorname{inl}(r))= \mathbf{true}$ 与 $\operatorname{real} {g}(\operatorname{inr}(f))= \mathbf{false}$
(3.112) $\text{fake}{g}(\operatorname{inl}(r))= \mathbf{false}$ 与 $\text{fake} {g}(\operatorname{inr}(f))= \mathbf{true}$
然后，我们可以使用 $\Pi$ 多态性来给出像"假的"（和"真实的"）这样的欠性形容词的一种通用的类型定义（3.113）。需要注意的是，这与Partee的观点一致，认为欠性形容词实际上是细分的 - 我们正在使用 $\Pi$ 多态性来定义细分形容词与欠性形容词的类型。当"假的"用来修饰一个特定的 $\mathrm{CN}$ ，其语义是 $A: \mathsf{CN}$ 时，我们得到了一个特定的 $\text{fake}(A)$ 用于那个名词：例如，修饰"枪"，其语义上表示为类型 $G$ ，我们得到 $\operatorname{fake}(G)$ ，实际上就是在(3.112)中定义的 $f a k e_{g}$ ，以及 $\operatorname{real}(G)$ ，在(3.111)中定义为 $real_{g}$ ，如(3.113-3.115)所示。
(3.113) $fake, real : \Pi A: \mathsf{CN}. (A \rightarrow Prop )$
(3.114) $\operatorname{fake}(G)=f a k e_{g}$
(3.115) $\operatorname{real}(G)=real_{g}$
现在，我们可以通过 $\Sigma$ 类型来定义欠性形容词的修改，如公式(3.116)和(3.117)所示。
(3.116) $\text{fake gun} =\Sigma g: G . \operatorname{f a k e}(G, g)$
(3.117) $\text{real gun} =\Sigma g: G \cdot \operatorname{real}(G, g)$
上述观点给出了预期的解释。例如，现在可以将句子（3.118）和（3.119）分别解释为（3.120）和（3.121）。请注意，在（3.121）中，只有由于子类型关系 $\Sigma g: G . \operatorname{fake}(G, g) \leq G$ ，$\neg \operatorname{real}(G, f)$ 才是类型良好（并且为真）。
(3.118) $\text{That gun is either real or fake.}$ （那把枪要么是真的，要么是假的）
(3.119) $\text{A fake gun is not a (real) gun.}$
(3.120) $\operatorname{real}(G, g) \vee \operatorname{fake}(G, g)$ ，其中 $g: G$ 是"that gun"的解释
(3.121) $\forall f:[\Sigma g: G . \operatorname{fake}(G, g)] . \neg \operatorname{real}(G, f)$
请参见附录A7.4中关于“假”和证明上述句子（3.118）正确性的Coq代码。
非承诺形容词类别包括那些不产生任何推断的形容词，如(3.122)所示。例如，所谓的罪犯可能是罪犯，也可能不是。非承诺形容词例子包括“所谓的[alleged]”，“预测的[predicted]”，“潜在的[potential]”，“存疑的[arguable]”，“有争议的[disputed]”和“有问题的[questionable]”。
(3.122) $\operatorname{Adj}(\mathrm{N}) \Rightarrow\ ?$
我们如何给这样的形容词及其修饰赋予语义呢？让我们以"所谓的"为例来尝试回答这个问题。什么是"所谓的凶手"呢？所谓的凶手是指有人指控他/她是凶手，然而，其他人可能并不这么认为。我们将提出的语义解释是：凶手是被某人指控为凶手的人。
这个观点的起源来自第一作者的提议，他提出了Ranta（1994）为了模拟“所谓”的信念语境的概念。不幸的是，像Chatzikyriakidis和Luo（2013，2017a）发现的那样，这个观点存在问题23
考虑形容词“所谓的”以及句子（3.123）和（3.124）。根据上述想法，（3.123）意味着有人声称约翰是凶手，如在（3.125）中正式表达，其中 $H_{h, alleged}(P)$ 直观地表达了“ $h$ 声称 $P$ 为真”，而 $\mathrm{\small IS}(Murderer,j)$ 是断言 $j: Murderer$ 的命题形式（参见第3.2.3节和第7.1节）。所以，非正式地说，（3.125）读起来是某个人 $h$ 声称约翰是个凶手。类似地，（3.124）可以解读为（3.126），非正式地表达，对于每个人类 $x$ ，如果有人 $h$ 声称 $x$ 是个凶手，玛丽就会憎恨 $x$ 。
(3.123) $\text{John is an alleged murderer.}$ （约翰是所谓的罪犯）
(3.124) $\text{Mary hates every alleged murderer.}$ （玛丽憎恨每一个所谓的罪犯）
(3.125) $\exists h: Human. H_{h, alleged}(\mathrm{\small IS}( Murderer,j))$
(3.126) $\forall x :Human. \left[\exists h:\right. Human. H_{h, alleged}(\mathrm{\small IS}( Murderer,\left.x))\right] \Rightarrow hate (m, x)$
对于每个非承诺形容词，我们有相应的模态运算符。例如，设 $P$ 为一个命题，那么对于"所谓的"，$H_{h,alleged}(P)$ 表示 $h$ 声称 $P$ ；对于"有争议"，$H_{h,disputed}(P)$表示 $P$ 被 $h$ 争议；以此类推。在这里，我们只考虑那些其相应行为由人类执行的非承诺性形容词。这些形容词包括"所谓"、"预测"和"有争议"等。总的来说，对于任何人 $h: Human$ 和任何非承诺性形容词 $A d j$ ，模态运算符 $H_{h, A d j}$ 是一个命题的谓词：
(3.127) $H_{h, A d j}: Prop \rightarrow Prop$
我们可以将 $H_{h, A d j}$ 视为一组命题。例如，$H_{h, \text { alleged }}$是 $h$ 提出的一组指控。我们认为，这种模态集合操作符为非承诺性形容词修改提供了充分的语义解释。
