双重否定证明

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)

这可以证明.