如果两件事不相等,他们是否相等？

Question

如果阿格达两个值,或一些其他的依赖性类型的语言,可以证明v?不是不等于v?,你能证明v?等号v?？

比如,有类型的功能((v? ? v? ? ?) ? ?) ? v? ? v?吗？

如果无法证明,这似乎可以安全地添加为公理,因为最多可以有一个值v? ? v?.

这个有趣的原因是双重否定((a ? ?) ? ?)形成了一个单子.通常你不能从它中提取值,但是你可以?从某些值中获取它们(如果你在经典逻辑monad中得出一个矛盾,你就会有矛盾).我想知道平等是否是可以提取的东西.

Answer 1

我认为法律在Agda或Coq中是不可证明的.

粗略地说,我们只有一个假设

(v1 = v2 -> False) -> False

我们需要证明这个论点v1 = v2.

考虑在基于后续的证明系统中的无切口证明.最后一条规则是什么？

它不能是一个介绍v1 = v2,因为Refl没有那种类型(v1,v2是不同的变量).

所以,它必须是对假设的消除,即

H1: (v1 = v2 -> False) -> False |- v1 = v2 -> False
H2: (v1 = v2 -> False) -> False , False |- v1 = v2
---------------------------------------------------  (->E)
(v1 = v2 -> False) -> False |- v1 = v2

但是,如果H1确实可以证明,我们也必须拥有

(v1 = v2 -> False) -> False |- False

我们从中得出

|- ((v1 = v2 -> False) -> False) -> False

这相当于

|- v1 = v2 -> False

没有任何其他假设,这显然是不可证明的v1,v2.实际上,否则我们可以将其概括为

|- forall v1 v2, v1 = v2 -> False

这显然是错的.

另一方面,我认为Agda/Coq/...符合排除中的法则,这意味着拟议的法律.因此,法律不能违反一致性.

Answer 2

双重否定消除在直觉主义类型理论中是无法证明的,就像chi在这里提出的那样,但它的否定也是无法证明的,所以它可以被认为是一致的.

然而,虽然经典公理不适用于所有类型,但它们可以证明是可判定的类型.可判定类型是可证明有人居住或无人居住的类型:

Decidable : Type -> Type
Decidable A = Either A (A -> False)

给定Decidable A,可以实现双重否定消除A:只是模式匹配Either A (A -> False),如果我们得到一个A,那么我们就完成了,如果我们得到A -> False,那么我们应用(A -> False) -> False并使用ex falso.

((a = b -> False) -> False) -> a = b如果一个特殊情况可证明(a b : A) -> Decidable (a = b),即A具有可判定的平等性.

至于(A -> False) -> False延续monad,当我们在这个monad中工作时,我们得到某种形式的经典推理,因为monadic join在这里对应于"quadruple"否定消除,所以not (not (not (not A))) -> not (not A)).我们也可以使用callCC与Peirce定律相对应的另一个经典陈述.

关于这一点有一个有趣的观察:我们可以采取任何经典证明,将所有命题提升Cont False(换句话说,加倍否定它们),并且我们得到相应的建设性证明,证明原始命题的双重否定.这意味着建构性逻辑可以证明古典逻辑能够模仿古典逻辑等价的一切,因为命题及其双重否定在经典上是等价的.