激烈的思考和阅读了几天最终意识到，使用命题逻辑的蕴含片段，保守定义type，和证明stlc里的柯霍同构，是足够的。但是对于mltt就不够了。

Seldin在文章里给出Curry的G组合子和Martin Löf Π的等价，概念上是没有错误的。但是严格的检查两者的符号使用方式，他们Split符号含义的方式不同。组合子逻辑的表达力过于强大了，一个符号要表达多少信息都可以全凭定义搞定，只要能保守定义写出来。但是逻辑里并不直接具有这种自由，需要先把原始概念全部清清楚楚的写出来，证出来，最后才能想办法抽象成（高阶）谓词函数。

具体的，在全称量化的处理上，mltt的Π表达式的formation规则，实际上是逻辑上的形式蕴含。当把它放到类型里时，mltt的做法保留了全称量化在类型表达式里，而Curry的G组合子里，并入了G的定义。类型模板（函数）里对变量的抽象只剩λ了。

因为∀u.M≡Π(λx.M)

这个Π是Church和Curry系统里的全称量化（组合子），mltt里选择了同一个符号，实际上Martin Löf熟悉Curry的系统。

∀或者Π在mltt的Π形成规则里留下了，在Seldin形式化的G组合子引入规则里，Π silently并入了G，表达式上只留下了λx.B抽象出依赖类型函数。

结论：要能证出mltt里的Π形成规则，引入和消去规则，需要使用高阶谓词逻辑而不是命题逻辑。命题逻辑只能搞出stlc。但是另一方面这样的系统又挺罕见的。Lesniewski和Tarski形式化的三个protothetic系统中，有两个是用蕴含做primitive的，刚好符合这里的需求（但不限制在经典逻辑内。

逻辑学里没有「古文」，每一个精简自洽的系统都有闪闪发光的时刻。#为往圣继绝学#