双重否定证明

Question

对不起我的英语。我用谷歌翻译。

证明任意类型(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)读起来像是“所有的命题都不是假的”。但是⊥ (和许多其他的)是错误的，所以我们实际上可以反驳您的说法：

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

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