双重否定证明

Question

对不起我的英语。我使用了 Google 翻译。

任意类型 (X : Set) 的证明是否真实？

double-negation : ∀ X → ¬ (¬ X)
double-negation = ?

其中：

data ⊥ : Set where

data ¬_ (X : Set) : Set where
    ¬-constructor : (X → ⊥) → ¬ X

例如ℕ的证明很简单:

data ℕ : Set where
    zero : ℕ
    suc  : ℕ → ℕ

double-negation : ℕ → ¬ (¬ ℕ)
double-negation n =
    ¬-constructor negation-contradiction
    where
        negation-contradiction : ¬ ℕ → ⊥
        negation-contradiction (¬-constructor ν) = ν n

但是把ℕ换成X后，就无法检查了（因为n的类型未知，所以negation-contradiction的类型也未知。也不能被推断（我得到 ¬ n → ⊥））。

如何证明？

Answer 1

你无法证明

∀ X → ¬ (¬ X) (1)

请记住

ℕ → ¬ (¬ ℕ)

不是 (1) 的实例但是

∀ X → X → ¬ (¬ X)

可以证明。

Answer 2

∀ X → ¬ (¬ X) 读起来像 "all propositions are not false"。但是 ⊥（以及许多其他）是错误的，因此我们实际上可以反驳您的说法：

open import Function
open import Relation.Nullary
open import Data.Empty

nope : ¬ ((X : Set) -> ¬ (¬ X))
nope c = c ⊥ id

双重否定证明

Double negation proof

agda