柯霍同构的真正含义在图一(1.2)这个大家不太熟悉的表达式里。这是柯里的推理组合子系统里的写法，之所以这个写法重要是因为我们在谈一个计算系统，于是逻辑的表达必须要考虑尽可能多的使用计算的形式，即λ。

全称量化组合子Π的定义有点出人意料；它实际上说的是，匿名函数(λu.M)应用在任何参数上都为真，用这样一种方法表达全称量化。

(∀u)M ≡ Π(λu.M)

理解这一点之后我们就能明白1.2表达的是，函数M具有这样一个特性：它的输入和输出的类型判定，携带了逻辑的蕴含信息，这就包含在F组合子的定义里。同时因为其演绎规则（图二），一次应用实现了一次类型上的modus ponens，证明论上称之为normalize proof。

这就是为什么一辈子没搞过定理证明器也没有搞过计算机语言的Curry，被命名了柯霍同构，因为是他发明的系统里定义的。