Deepseek还是牛叉，折腾了很久终于彻底搞清楚蕴含左引入是如何在代数上理解的了。

这个不是什么突破性的东西，是一个很基本的东西。但是它处在戳破柯霍同构的代数解释的一个关键点上。

Γ⊢Δ,A B,Σ⊢Θ
———————(⊃-L)
A⊃B,Γ,Σ⊢Δ,Θ

蕴含的左引入是构造了一个剩余算子表达式，这一步即使在纯代数非逻辑视角下，也是处理掉了「元语言¹」意义上的融合，即我们有两个表达式，A≤B和C≤D，通过

B•(B⊃C)≤C

中介，可以把两个表达式合一，成为

A•(B⊃C)≤D

注意这一点在λ和逻辑上是双重成立的。对于λ，序是anti chain，即β相等关系。对于逻辑，序是蕴含序。

++++

所以从各种意义上上说，我很久之前迷恋过的四元泛逻辑规则

A⊢B C⊢D
--------------
B⊃C⊢A⊃D

是超级大杀器。这个规则我找了很久也没有发现它曾被比较系统的研究过的迹象，无论是搞数理逻辑的还是搞哲学或者泛逻辑的，都忽视了。但是它表达组合/传递的逻辑直觉是如此的清晰：如果有箭头A→B和C→D（你看这是多么宽泛的前提）如果存在箭头B→C，那么我们可以得出结论，A→D是可达的。对称的，我们也可以说如果如果存在D→A，我们可以得到C→B是可达的。这个对称性是解释柯霍同构重要的一环。

而根本上，柯霍同构是逻辑和λ在剩余格代数结构上的同构。这个不是完全同构的，因为对于逻辑而言，A⊃(B⊃C)和B⊃(A⊃C)是等价的，即前提可交换，因为一般不会禁止（小野宽晰的）融合的交换律。

而λ显然不是这样，XYZ不等于XZY，即参数序不可交换，就算把λ全部定义到逻辑表达式上也最多只有XYZ~XZY，是逻辑等价，不是相等。

++++

能看懂这篇的才能算是入门了类型论的代数角度。这个代数角度的重要性在于，它给出了柯霍同构的adequacy，即剩余格结构同构。但是通常和柯霍同构一起谈的直觉主义或者构造主义，以及λ演算，都不是必需的。我们完全可以扩展或换用其它演算体系，也把直觉主义当个P，仍然有柯霍同构。

实际上Caires和Pfenning在pi演算上找到的矢列演算规则下的Dual直觉线性逻辑与session type的同构就是一个好例子。这里的Dual是指线性和经典的上下文分开。这个很容易理解，session type描述通讯，消息是动态资源。

¹这里的元语言不限于逻辑，就算在使用加减或乘除或集合运算的剩余格结构，当有两个序条件时，把两者「合」在一起，也是这样的代数结构。序和格是伴随形式化研究成长起来的代数，适用的范围比逻辑和计算还广。