写出了一个肥肠无厘头的规则但是仔细一想竟然还塔玛的是对的。

N ⊢ α，α ⊢ B β M
————————
N ⊢ B β M
————————
⊢ B β M N
————————
⊢ β(MN)

实际上它是从类型规则

N: α，M: α->β
————————
MN: β

变换出来的。但是前面的表达式神奇的地方在于，它并没有:和->，:是一个分层的解释，->则事实上是一个算子，合成类型用的。

前面的规则和标准的矢列演算规则的唯一区别是它使用了组合子在逻辑表达式里，这在逻辑的角度看显然是允许的。不同的地方是它有个applicative规则，类似蕴含引入。

但是这个推演系统牛逼的地方在于它是type-free typing，因为如果拿掉我们实现赋予希腊字母和英文字母的差别，一个当作项另一个当作类型，看成一个flat系统，把它是没类型可言的。

————————

说他塔玛的竟然是对的，是因为它符合柯霍同构和构造逻辑的解释，N的类型是α，和N是α的证明，是一回事。这是严格的，因为在希尔伯特风格的证明论里，只有modus ponens，这导致任何一个定理，你都可以把它前面的证明过程恢复出来，即保留

a∧(a⊃b) ⊃ b

的完整形式，这就是proof（项）的结构等价物。