order是reachability的最基本形态。

我们有很多种方式从一个基本的order开始做扩展。

比如product/sum order是一种，它还是order。

pointwise order也是一种，这个感觉就不是order和order之间的composition了，直觉是提升了一层。逻辑里的实质蕴含和形式蕴含，如果把蕴含看作order，就是这种。如果从函数的角度看，它也很象类型和函数集的关系。我不知道范畴里的fiber是不是也是这个意思。

但是矢列演算里的⊢很诡异，如果我们把⊢写成≤，它的复合规则是：

A≤B，C≤D，可以复合成，AC≤BD

这里A/B/C/D都是string，可以为空，range over一个alphabet，alphabet里的每个symbol是一个逻辑公式。这样A/B/C/D就都是公式的序列，AB可以表达两个公式序列concat在一起成为一个新的序列。这就完整捕捉了矢列的代数含义。

但是我们马上就会发现我们不能使用≤表达序，如果用a和b表达基本公式（alphabet里的symbol），a≤b中的≤是序，但是如果出现ab≤cd，这里的≤就不是序了，因为generally，a,b⊢c,d和c,d⊢e,f，是不能把⊢看作二元关系序的传递性的，即两者可以推出a,b⊢e,f。造成这个现象的根本原因是逗号在⊢左侧和右侧的含义不同，左侧是融合，右侧是个我还不知道该怎么称呼的东西，经典逻辑下可以称为析取。

但cut规则不是完全不存在，如果是a,b⊢c,d和d,c⊢e,f，是可以cut成a,b,c⊢c,e,f的。

但是我们仍然应该把≤看作一种广义序。因为序其实有两个含义，一个是二元可比较关系，另一个是可达性，图意义上的。而矢列里的⊢，保留了对可达性的表达，但它是一种多元关系。

于是马上就有灵魂问题出现：对于这样的多元比较或多元可达，伽罗华连接是什么？