非直谓性 (类型论)

非直谓性一般来说是指某种定义是自指的, 在类型论中是宇宙的性质. 大致来说, 若如下规则成立 (省略类型所在的语境): 不包含于 (也就是说 大), 那么 是非直谓的的. 一般来说, 两个类型取 类型得到的新类型, 应该存在于较大的那个宇宙, 这个性质叫做直谓性. 而能违反这件事的性质就叫做非直谓性.

由于宇宙之间的大小关系在类型论中不好统一定义, 因此非直谓性往往对于每个类型论都有自己的版本.

在非类型论或者 Russell 简单类型论的讨论环境中, 非直谓一般指某种自指性.

1后果

非直谓宇宙在依值类型论中会破坏一致性, 参见 Berardi 悖论. 非直谓的命题宇宙则没有问题, 构造演算就是一个有直谓宇宙和非直谓命题宇宙的系统.

包含一个非直谓宇宙能大大提高类型论的证明论强度. 例如 Martin-Löf 类型论是直谓的, 在里面甚至不能定义 F 系统, 因为后者是非直谓的.

2相关概念

降级公理是定理形式的非直谓性, 和作为类型论规则的非直谓性拥有同样的证明论强度.

经典逻辑的公理如排中律, 选择公理蕴涵降级公理.

术语翻译

非直谓性英文 impredicativity