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

Question

除非我弄错了，没有证据证明

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

在 Agda 中。

这意味着您不能使用反证法。

许多数学教科书都使用这些类型的证明，所以我想知道:是否总是可以找到替代的建设性证明？例如，您能否仅使用构造逻辑编写代数教科书？

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

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 和 Thorsten 的常用公式Altenkirch 的观察类型理论。