3

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

∀ {A : Set} → ¬ (¬ A) → A

在阿格达。

这意味着您不能使用矛盾证明。

许多数学教科书都使用这些证明，所以我想知道：是否总是有可能找到替代的建设性证明？例如，你能用建设性逻辑写一本代数教科书吗？

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

4

1 回答 1

7

事实上，双重否定消除（以及其他逻辑上等价的陈述）无法在 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 和 Thorsten 的常用公式Altenkirch 的观察型理论。

于 2014-02-15T23:45:58.223 回答