對角線引理

对角线引理（diagonal lemma），又称为不动点定理（fixed point theorem）。在数理逻辑中，对角线引理表明了自然数的形式理论中自指句子的存在——尤其是那些强到足以表示所有可计算函数的形式理论。
由对角线引理确立其存在的句子，将可用于证明一些逻辑的基础限制，例如：哥德尔不完备定理或塔斯基不可定义定理。

引理的内容

令T为算术语言的一阶理论，且它能够表示所有可计算函数。令ψ为该语言中具有单一自由变量的一个式子。
对角线引理告诉我们：存在一个式子φ，使得φ↔ψ(#(φ))这式子在T里是可证明的。
直觉上，φ是一个表示“φ具有性质ψ”的自指句子。句子φ可被视为将每个式子θ映射到句子ψ(#(θ))的运算的不动点。这个证明构造出的句子φ并非字面上与ψ(#(φ))相同，但在理论T中它们是可证等价的。

历史

对角线引理跟可计算性理论中的Kleene's recursion theorem有密切的联系，证明方法也相似。
这个定理之所以被冠以“对角线”，是因为它与康托尔的对角论证法的形式很相近。“对角线引理”或“不动点”的词汇并未出现在哥德尔1931年所发表的划时代的论文中，也没有出现在塔斯基1936年的论文中。卡尔纳普是第一个人证明出：只要理论T满足某些条件，那么对于T中的任何式子ψ，都存在式子φ使得φ ↔ ψ(#(φ))在T中是可证的。由于在1934年尚未有可计算函数的概念，卡尔纳普是以别的用词去陈述该结论。Elliott Mendelson 认为是卡尔纳普首先指出哥德尔的论证中隐含地运用了对角线引理，而哥德尔则是在1937年注意到卡尔纳普的工作。