元定理

在邏輯上，元定理是一個以元語言的對於形式系統的陳述。和在一個形式系統內證明的定理不同，元定理是在元理論中證明的，且可能涉及元理論中存在、但在對象理論中不存在的概念。

一個形式系統是由元語言和演繹系統（公理及推理規則）所決定的，這形式系統可用於證明系統中以形式語言表達的特定陳述；然而，元定理要以元定理系統以外的事物進行證明，而常見的元定理包括了集合論（尤其在模型論中）及Template:Link-en（尤其在證明論中）等等；此外，比起顯示特定的陳述可證明，元定理更常顯示說一大類的陳述是可證明的，或特定陳述是不可證明的。

例子

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

• 一階邏輯的演繹定理說一個有著$\mathrm{\Phi }\to \mathrm{\Psi }$這形式的句子在公理系統$A$中是可證明的，當且僅當句子$\mathrm{\Psi }$是可從包含$\mathrm{\Phi }$及所有的$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
• Template:MathWorld