查看“︁元定理”︁的源代码

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

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

==例子==
以下是元定理的一些例子：
* [[一階邏輯]]的[[演繹定理]]說一個有著<math>\Phi \rightarrow \Psi</math>這形式的句子在公理系統<math>A</math>中是可證明的，當且僅當句子<math>\Psi</math>是可從包含<math>\Phi</math>及所有的<math>A</math>的公理的公理系統中證明的。
* [[馮·諾伊曼-博內斯-哥德爾集合論]]的類存在性定理（class existence theorem）說對於任意[[量化 (數理邏輯)|量詞]]僅及於集合的公式，總存在一個包含[[集合 (數學)|集合]]的[[類 (數學)|類]]滿足這公式。
* [[皮亞諾公理]]之類的系統的[[一致性 (邏輯)|一致性證明]]。

==參見==
* [[元數學]]
* [[使用-提及區別]]

==參考資料==
* [[Geoffrey Hunter (logician)|Geoffrey Hunter]] (1969), ''Metalogic''.
* Alasdair Urquhart (2002), "Metatheory", ''A companion to philosophical logic'', Dale Jacquette (ed.), p.&nbsp;307

==外部連結==
* [http://www.encyclopediaofmath.org/index.php/Meta-theorem ''Meta-theorem'' at Encyclopaedia of Mathematics]
* {{MathWorld|urlname=Metatheorem|title=Metatheorem|author=Barile, Margherita}}

[[category:元定理|元定理]]
[[category:元邏輯學]]
[[category:數學術語]]