Двойное доказательство отрицания

Question

Извините за мой английский. Я использовал переводчик гугл.

Действительно ли доказать, что для произвольного типа (X: множество)?

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