不知道有什么意义。但是Gentzen的sequent...

不知道有什么意义。但是Gentzen的sequent calculus里，cut rule是admissible but not derivable，让我有点小震惊。这套几十页的ppt给了admissibility很好的代数解释，但是阿拉还看不懂。

因为柯霍同构，逻辑问题的代数解释如果有意义，那么可以预见，类型问题的代数解释一样有意义。而且不用研究，大量阅读逻辑学家的论文捡现成的用就行了