今天吃麦的时候的一个想法。

哥德尔不完备定理，被一致认为，还是动用了不动点的。但是这个不动点的形式不是等式系统里（例如λ演算）那种，要泛化一些。一方面它不是相等关系，而只是逻辑等价，另一方面它打破了元理论与目标语言的界限，「元理论可证性」被编码在目标语言里。这个事情会引起一些细节的技术问题，也不清楚它是大问题还是小问题。

持泛化不动点观点的包括Smullyan，Lawvere（1969不动点定理），以及一个在证明论角度看起来更令人满意的解释，使用模态逻辑定义可证性，有可证逻辑（de Jongh）。其特征是有可证性定义（模态算子），接受排中率，使用Kripke语义。不同于直觉逻辑。在这个系统里的不动点定理和哥德尔的证明最为接近。

----

但是在代数角度看事情简单很多。哥德尔使用完全构造性的做法构造了一个代数系统，某种自由代数，在这个代数空间里不动点是存在的；但是逻辑是它的一个投影代数，因为显而易见的原因，¬x=x不能被接受，所以不动点定理就毁掉了。这是特别直接的对哥德尔第一不完备定理的理解，不需要诉诸大量艰涩的逻辑学概念和细微的判定问题。

++++

这个看法可以让人回顾柯里的系统。柯里的系统源于Schonfinkel的系统。后者第一次构造了SK+单一逻辑组合子的系统，但是这个逻辑组合子的定义方式不唯一。Schonfinkel把它定义成不相容，Curry选择了几个不同的定义，包括F，功能组合子（这个是类型论的直接前身），包括Ξ，罗素的形式蕴含，也包括Π（全称量词）+⊃（实质蕴含）。

这里非常微妙的一点是，柯里悖论让逻辑和计算直接碰撞出悖论的是⊃，实质蕴含，而不是Ξ，形式蕴含。这是有区别的。因为，考虑上面说的代数和投影空间问题，存在可能性在高阶逻辑系统对应的代数结构里，不动点是没问题的，是投影到命题逻辑的时候出了问题。如果是这样的情况那柯里的系统没有要blame的。还可以想办法修修补补继续用。

这个系统最大的好处是不罗嗦。不扯那么多元/目标的蛋。

----

todo：

1 看一下柯里的书，是不是只有SKΞ表达不了⊃，跟SK⊃就不是一个系统。
2 了解一下这种高阶逻辑加SK的代数空间是什么样的。