Jeśli dwie rzeczy nie są równe, czy są równe?

Question

Jeśli dwie wartości w Agdzie lub innym, zależnie od tego używanym języku, możesz udowodnić, że v₁ nie jest równe v₂, czy możesz udowodnić, że v₁ jest równy v₂? To jest funkcja typu ((v₁ ≡ v₂ → ⊥) → ⊥) → v₁ ≡ v₂?

To wydaje się być czymś, co można bezpiecznie dodać jako aksjomat, jeśli nie można tego udowodnić, ponieważ nie może być najwyżej jednej wartości v₁ ≡ v₂.

Powodem tego jest to, że podwójna negacja ((a → ⊥) → ⊥) tworzy monad. Zwykle nie można wyodrębnić z niego wartości, ale można uzyskać od niego pewne wartości, takie jak ⊥ (jeśli wywodzisz sprzeczność w klasycznej monadzie logicznej, masz sprzeczność). Zastanawiałem się, czy równość jest czymś, co można wydobyć.

Answer 1

Uważam, że tego prawa nie da się udowodnić w Agdzie ani w Coq.

grubsza, mamy tylko jedną hipotezę

(v1 = v2 -> False) -> False 

i musimy udowodnić tezę v1 = v2.

Należy wziąć pod uwagę bezspoinowy dowód na to w systemie proofingu sekwencyjnego. Jaka byłaby ostatnia zasada?

Nie może być wprowadzeniem v1 = v2, ponieważ Refl nie ma tego typu (v1,v2 są odrębnymi zmiennymi).

Tak, to musi być wyeliminowanie hipotezy, czyli

H1: (v1 = v2 -> False) -> False |- v1 = v2 -> False 
H2: (v1 = v2 -> False) -> False , False |- v1 = v2 
--------------------------------------------------- (->E) 
(v1 = v2 -> False) -> False |- v1 = v2 

Jednak jeśli H1 jest rzeczywiście udowodnić, musimy również mieć

(v1 = v2 -> False) -> False |- False 

z którego czerpiemy

|- ((v1 = v2 -> False) -> False) -> False 

co jest równoważne z

|- v1 = v2 -> False 

co jest oczywiste, nie da się udowodnić bez innych założeń dotyczących v1,v2. Rzeczywiście, w przeciwnym razie możemy uogólnić to do

|- forall v1 v2, v1 = v2 -> False 

co jest oczywiście błędne.

Z drugiej strony uważam, że Agda/Coq/... są zgodne z Ustawą o wykluczeniu środkowym, co oznacza proponowane prawo. Dlatego prawo nie może naruszać spójności.

Answer 2

Eliminacja podwójnej negacji jest nie do udowodnienia w intuicjonistycznej teorii typów, jak przedstawiono tutaj chi, ale jej negacja jest również nie do udowodnienia, więc można ją konsekwentnie zakładać.

Jednakże, podczas gdy klasyczne aksjomaty nie są do udowodnienia dla wszystkich typów, można je udowodnić dla typów rozstrzygalnych.Rozstrzygalne typy są te, które są zamieszkane lub niezamieszkane provably:

Decidable : Type -> Type 
Decidable A = Either A (A -> False) 

Biorąc Decidable A można wdrożyć podwójną eliminację negacji na A: tylko wzór mecz na Either A (A -> False), a jeśli otrzymujemy A, to skończymy, jeśli otrzymujemy A -> False, następnie aplikujemy (A -> False) -> False i używamy ex falso.

Jako specjalny przypadek ((a = b -> False) -> False) -> a = b jest możliwy do sprawdzenia, jeśli (a b : A) -> Decidable (a = b), i. mi. A ma decydującą równość.

Jeśli chodzi o monadę kontynuacyjną (A -> False) -> False, kiedy pracujemy wewnątrz tej monady, otrzymujemy pewną formę klasycznego rozumowania, ponieważ sprzężenie monadyczne tutaj odpowiada "poczwórnej" eliminacji negacji, czyli not (not (not (not A))) -> not (not A)). Możemy również użyć callCC, co odpowiada Peirce's law, innym klasycznym stwierdzeniom.

Istnieje interesująca uwaga na ten temat: możemy wziąć dowolny klasyczny dowód, podnieść wszystkie propozycje do Cont False (innymi słowy, podwójnie je negować), a otrzymamy odpowiedni konstruktywny dowód, który potwierdza podwójną negację pierwotnej propozycji. Oznacza to, że logika konstruktywna może udowodnić wszystko, co logika klasyczna, modulo klasyczna logiczna równoważność, ponieważ twierdzenie i jego podwójna negacja są klasycznie równoważne.