逻辑上,元定理是一个以元语言的对于形式系统的陈述。和在一个形式系统内证明的定理不同,元定理是在元理论中证明的,且可能涉及元理论中存在、但在对象理论中不存在的概念。

一个形式系统是由元语言和演绎系统(公理及推理规则)所决定的,这形式系统可用于证明系统中以形式语言表达的特定陈述;然而,元定理要以元定理系统以外的事物进行证明,而常见的元定理包括了集合论(尤其在模型论中)及原始归纳算术英语Primitive recursive arithmetic(尤其在证明论中)等等;此外,比起显示特定的陈述可证明,元定理更常显示说一大类的陈述是可证明的,或特定陈述是不可证明的。

例子

编辑

以下是元定理的一些例子:

  • 一阶逻辑演绎定理说一个有著 这形式的句子在公理系统 中是可证明的,当且仅当句子 是可从包含 及所有的 的公理的公理系统中证明的。
  • 冯·诺伊曼-博内斯-哥德尔集合论的类存在性定理(class existence theorem)说对于任意量词仅及于集合的公式,总存在一个包含集合满足这公式。
  • 皮亚诺公理之类的系统的一致性证明

参见

编辑

参考资料

编辑
  • Geoffrey Hunter (1969), Metalogic.
  • Alasdair Urquhart (2002), "Metatheory", A companion to philosophical logic, Dale Jacquette (ed.), p. 307

外部链接

编辑