是否存在可以在经典逻辑中证明但在Agda中不能证明的命题

Question

除非我弄错了,否则没有证据证明

? {A : Set} ? ¬ (¬ A) ? A

在阿格达.

这意味着您不能通过矛盾使用证明.

许多数学教科书使用这些证明,所以我想知道:是否总能找到另一种建设性的证据？您是否可以仅使用建设性逻辑来编写代数教科书？

如果答案是否定的.这是否意味着建构性逻辑在某种意义上比经典逻辑更不强大？

Answer 1

实际上,在Agda中无法证明双重否定消除(以及在逻辑上等同于此的其他陈述).

-- Law of excluded middle
lem : ? {p} {P : Set p} ? P ? ¬ P

-- Double negation elimination
dne : ? {p} {P : Set p} ? ¬ ¬ P ? P

-- Peirce's law
peirce : ? {p q} {P : Set p} {Q : Set q} ?
  ((P ? Q) ? P) ? P

(如果你愿意,你可以证明这些在逻辑上是等价的,这是一个有趣的练习).但这是我们无法避免的结果 - 建构逻辑的一个重要问题是证明具有计算环境.然而,假设排除中间的法律基本上杀死了任何计算环境.

考虑以下命题:

end-state? : Turing ? Set
end-state? t = ...

simulate_for_steps : Turing ? ? ? Turing
simulate t for n steps = ...

Terminates : Turing ? Set
Terminates machine = ? ? ? n ?
  end-state? (simulate machine for n steps)

因此,如果存在数字n,则图灵机终止,使得在n步之后,机器处于结束状态.听起来很合理吧？当我们在混合中添加排除的中间时会发生什么？

terminates? : Turing ? Bool
terminates? t with lem {P = Terminates t}
... | inj? _ = true
... | inj? _ = false

如果我们排除了中间,那么任何命题都是可判定的.这也意味着我们可以决定图灵机是否终止,我们已经解决了暂停问题.所以我们可以有可计算性或经典逻辑,但不是两者都有!虽然排除的中间和其他等价语句可以帮助我们进行证明,但它的代价是程序的计算意义.

所以是的,从这个意义上讲,建设性逻辑不如经典逻辑强大.但是,我们可以通过双重否定翻译来模拟经典逻辑.请注意,以前原则的双重否定版本在Agda中有效:

¬¬dne : ? {p} {P : Set p} ? ¬ ¬ (¬ ¬ P ? P)
¬¬dne f = f ? g ? ?-elim (g (f ? const))

¬¬lem : ? {p} {P : Set p} ? ¬ ¬ (P ? ¬ P)
¬¬lem f = f (inj? (f ? inj?))

如果我们使用经典逻辑,那么您将使用双重否定消除来获取原始语句.甚至还有一个专门用于此转换的monad,请查看Relation.Nullary.Negation模块中的双重否定monad (在标准库中).

这意味着我们可以有选择地使用经典逻辑.从某些角度来看,由于这一点,建设性逻辑比经典逻辑更为强大.在经典逻辑中,你不能选择退出这些陈述,它们就在那里.另一方面,建设性逻辑不会强迫您使用它们,但如果您需要它们,您可以通过这种方式"启用"它们.

另一个无法在Agda中证明的声明是功能扩展性.但与经典陈述不同,这一陈述在建设性逻辑中是可取的.

ext : ? {a b} {A : Set a} {B : A ? Set b}
  (f g : ? x ? B x) ? (? x ? f x ? g x) ? f ? g

但是,这并不意味着它不具有建设性逻辑.它只是Agda所依据的理论的一个属性(主要是带有公理K的强度型理论),还有其他类型理论的含义,例如拉伸型理论的常用公式或Conor McBride's和Thorsten Altenkirch的观察类型理论.