natural deduction的横线只是一个书写方式。

每当我们加入一种新的符号，我们都要给出这种符号的对应rule，在这个语境下能进行互动。

所以，横线的意义是一个函数，把横线上面接收到的几个assumption，作为一个一系列输入，进入横线右边的标识的函数，然后输出conclusion。

横线中上面的某一个assumption，可以用它的proof来替换。本质上是函数的组合。

所以一个natural deduction其实描述了一大堆函数串接的过程。在这个证明中的每一条线，线的上方的一行都是这个函数的输入，下面一行都是这个函数的输出。而他们组成的整体，刚好最上面的一行是输入，最下面的一行是输出。

当然我们会需要一种情况，就是需要一些假设的东西，它可能并不一定成立。

一个系统总有称之为公理的东西，它可能长成各种样子，有的有横线，有的没有。从函数式编程的角度，它们都是函数，只不过有的有输入，有的没有罢了。

这些东西统一构成了环境。环境就是你能用的所有规则。

hypothetical judgements是什么呢？可以认为是一种特殊的rule。

就比如在群论当中通常是不一定交换律成立的，但是假设它成立了会怎么样怎么样。这个时候环境发生了变化。

为了方便，我们保持环境上大体的统一，而把它作为假设。这是一种区隔开来的rule。

构造主义逻辑里面解放一个变量的本质，其实就是因为横线永远只接受的是上面一行的那个生产出来的conclusion作为输入，但是如果我们想让横线把一个整个作为输入，就采用了解放变量这种记法。

至于为什么要发明蕴含标记呢？本质上这又是横线的另一种表达方式，为了方便让横线的最下面永远是一行，比较看起来好找。