元定理

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

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

例子

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

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

参见

• 元数学
• 使用-提及区别

参考资料

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

外部链接

• Meta-theorem at Encyclopaedia of Mathematics
• Barile, Margherita. Metatheorem. MathWorld.