Hypothetical Judgments 和 Hypothetical Inductive Definitions

Hypothetical Judgements

之前一篇介绍了Judgements和Inductive Definition，这里通过给Judgements加上一些关系，同时扩展下Inductive Definition。

Derivability

Derivability指的是说，由某几个Judgements可以推导出某个Judgement。具体如下$$J_1,...,J_nvdash_R J$$这个式子的意思就是说，由(J_1,...,J_n,R)我们可以推导出(J)成立。这里(R)是公理集合，而(J_i)是临时公理。这个意思是说，当我们承认(J_i)成立的时候，我们可以推导出(J)。举个例子(potato~natvdash succ(potato)~nat)。这里当我们知道土豆是一个自然数的时候，那么我们可以推导出来(succ(potato))也是个自然数。但是反过来是不行的：(succ(potato)~natvdash potato~nat)是不成立的。因为我们没办法推导出来这个结论。

Derivability有几个性质：

Weakening: 是说，如果(Gammavdash J)，并且(GammasubseteqGamma')，那么我们有(Gamma'vdash J)。这个不难理解，当我们已经知道某个结论的时候，如果放宽要求，那么这个结论还是成立的
Reflexibility: (Jvdash J)，是说自己可以推导出自己
Transitivity: 是说如果(Gammavdash J)和(Gamma, Jvdash J')成立，那么(Gammavdash J')也是成立的。直觉上看就是(A)可以推导出(B)，同时(B)可以推导出(C)，那么我们可以直接从(A)推导到(C)。

Admissibility

Admissibility指的是说，如果某个假设成立，那么我们可以得到某个结论。具体如下$$J_1,..,J_nvDash_R J$$。这里(J_1,...,J_n)是假设，(R)是公理集合，而(J)是结论。换句话说，如果我们可以通过公理(R)推导出结论(J_1,...,J_n)，那么我们也可以推导出(J)。形式化表示出来是

[egin{aligned} &frac{}{J_1'}~frac{}{J_2'}~...~frac{}{J_n'}\ &frac{J_1,...,J_n}{J} end{aligned} ]

这里(R={frac{}{J_1'},...,frac{}{J_n'}})。

下面举个例子: (succ(a)~evenvDash a~odd)。意思就是，如果(succ(a))是一个偶数，那么(a)就是一个奇数。

Admissibility和Derivability对比

这两个概念很容易混淆，所以这里再说一次

(J_1,..,J_nvdash_R J)是说，通过({J_1,..,J_n}cup R)，我们可以推出(J)
(J_1,..,J_nvDash_R J)是说，如果(J_1,..,J_n)成立，那么我们可以由(R)推出(J)

还是不理解是不是？不要慌，让我们看下下面的例子：

(succ(potato)~nat vdash ~potato~nat)
(succ(potato)~nat vDash ~potato~nat)

这里再复习下什么是(nat)，具体可以看上一篇文章。

[frac{}{z~mathtt{nat}}~frac{a~mathtt{nat}}{mathtt{succ}(a)~mathtt{nat}} ]

(nat)是递归定义的，也就是说，首先定义(z)是一个(nat)。然后如果(a)是(nat)，那么(succ(a))也是(nat)。这两条我们可以看成是上面所说的公理集合(R)。然后对于例子1，也就是说我们在公理集合里面加入(frac{}{mathtt{succ}(potato)~mathtt{nat}})是没办法推导出(potato~nat)的。

但是对于例子2，确是成立的。证明方法其实在上一章已经说过了，这里不再重复。

不过我们可以证明(Gammavdash_R JRightarrow GammavDash_R J)。证明也很简单，如果我们可以通过(R)推导出(Gamma)也就是(vdash_RGamma)，那么我们就可以通过(R)推导出(J)也就是(vdash_R J)（通过Transitivity: (vdash_R Gamma, Gammavdash_R J)）。如果(vdash_RGamma)不成立，那么说明(GammavDash_R J)"天然"成立。

同时，Admissibility也有类似于Derivability的性质:

Reflexibility: (JvDash_R J)
Transitivity: 如果(GammavDash_R K)并且(Gamma,KvDash_R J)那么我们有(GammavDash_R J)
Weakening: 如果(GammavDash_R J)那么(Gamma,KvDash_R J)

Hypothetical Inductive Definitions

然后让我们把Hypothetical Judgement给整合到Inductive Definitions里面：

[frac{GammaGamma_1vdash J_1~GammaGamma_2vdash J_2~...~GammaGamma_nvdash J_n}{Gammavdash J} ]

这里(Gamma)是一个全局假设，也可以看做就是全局的公理，而(Gamma_i)称为局部假设或者局部公理。这个表示当(J_i)在假设(Gamma)和(Gamma_i)的情况下成立，那么由(Gamma)则可以推导出(J)。具体的在后面介绍具体的类型系统的时候可以体会到。

General Judgement因为目前用不到，所以这里不做介绍。