上一个帖子里的猜想迅速被Gemini瓦解了。

柯里系统里的P，本质上它是需要用到bracket abstraction定义的，即

P = λx.λy.Ξ(Kx)(Ky)

原则上来说这是一个元语言定义，目标语言里没这种东西。但是可计算函数的牛叉之处在此，SK直接就可以实现它。

P = S(KΞ)K

演算下来是一样的。

----

这两行等式其实和哥德尔第一不完备定理的证明解释内涵高度一致，就是一个足够rich的系统是能simulate在元语言层面看到的它的行为/关系的。哥德尔花了45个引理和定理构造了哥德尔数打破这个次元壁，柯里的系统只有两行。[二哈][二哈]

但是不同的是。哥德尔的系统，函数和谓词是两个平层，保证停机，换句话说在目标语言内不允许不动点定理直接对逻辑系统发起攻击，而柯里的系统逻辑是完全暴露的，不动点定理直接向逻辑开火导致不一致。

----

但真的不知道除了Jan von Plato伉俪，还有哪些数学家能接受干掉收缩规则的逻辑系统。这是另一个解决柯里悖论的方式，而且它是铁打的逻辑规则安全帽，只要有cut elimination，即逻辑本身一致，那么不管它和什么系统混合，都一定还是一致的。这也是一个非常强的特性了，堪比一阶逻辑。