这个逻辑表达式的含义是集合论视角对函数类型的定义。其中f和g都看作是集合的特征函数，即fu可以理解为u∈f，gv可以理解为v∈g。于是下面这个表达式的含义是，函数h满足这个逻辑表达式。

∀u.fu⊃g(hu)

基于组合子形式做如下变换，先引入B组合子把hu的括号去掉

∀u.fu⊃Bghu

引入Ξ，ΞXY≡∀u.Xu⊃Yu，这是Curry对形式蕴含的定义，形式蕴含最初来自Russell。

Ξf(Bgh)

然后我们对h做抽象，采用h[]的简易写法

h[Ξf(Bgh)]
S h[Ξf] h[Bgh]
S (S h[Ξ] h[f]) (Bg)
S (S (KΞ) (Kf)) (Bg)

最后这个表达式很容易验证，把它应用在h上

S (S (KΞ) (Kf)) (Bg) h
(S (KΞ) (Kf)) h (Bgh)
(KΞh) (Kfh) (Bgh)
Ξf(Bgh)

说明抽象是对的。于是我们得到了第一个奇怪的结论

h ∈ S (S (KΞ) (Kf)) (Bg)

Curry对类型的定义是引入F组合子作为原始组合子，这个系统称为F1，使用Ξ的系统称为F2。F和Ξ可以互相定义的。但是我确实没想到

F x y z ≡ Ξx(Byz)

Ffgh这样的表达式，今天我们可以直觉的写成

h : f → g

实际上我们能把→对应组合子计算出来，即

S (S (KΞ) (Kf)) (Bg) h ≅ → f g h

等我忙完手中的活儿完全推导一下这个→组合子是个什么东西。在Curry的系统里它就应该是F的定义。