非直谓性
非直谓性大致都是说某种使用自己定义自己的一部分概念, 直谓性则指不这么做.
例 0.1. 我们可以定义某实数 为某实数集 的最小上界, 这个定义就是非直谓的, 因为定义 时使用的数据 也包含了 .
非直谓描述的是具体的定义方式. 某概念可能同时有直谓和非直谓的等价定义.
• | 在现代类型论中, 有直接使用 类型的规则叙述的非直谓性 (类型论). |
• | 更早的时期, 有更广泛的直谓、非直谓概念, 参见分歧类型论. |
• | 直谓数学指不使用任何非直谓定义的数学. 某些版本的 Martin-Löf 类型论作为数学基础就是直谓的. |
术语翻译
非直谓性 • 英文 impredicativity
直谓性 • 英文 predicativity