一致性 (类型论)

类型论有两种一致性:

•	逻辑一致性, 即 “空语境下空类型没有实例”. 这对应了传统数理逻辑中的一致性, 因为类型论中对命题 $P$ 的否定 $\neg P$ 往往 (极少有反例) 是定义为 $P\to \varnothing$ 的. 而如果 $P$ 和 $\neg P$ 同时成立, 那么 $\varnothing$ 对应的命题也成立, 而类型论的一致性的定义就否决了这种可能性.

•	语义一致性, 即 “存在模型”. 如果模型里, 空类型的实例的集合是空集, 那么语义一致性蕴涵逻辑一致性.

根据这两个定义, 证明一致性一般有两种手法:

•	证明典范性后直接得到逻辑一致性.

•	构造非平凡的模型, 通过语义一致性蕴涵逻辑一致性.

但实际上, 证明典范性也需要构造模型, 所以一般来说证明一致性的手法就可以说是构造模型.

一致性对类型论在逻辑里的应用非常重要, 参考类型论–范畴论–逻辑学类比.

术语翻译

一致性 • 英文 consistency