O predykatywności Set i proof-irrelevance
Predykatywność Set
1. Używając prawa wyłączonego środka i
dependent_description można dowieść classic_set.
W pliku Coq.Logic.ClassicalDescription
znajdującym się w
bibliotece standardowej Coq jest sformalizowany dowód, że w logice
klasycznej
Axiom classic: forall P:Prop, P \/ ~ P.
z aksjomatu wyboru (axiom of unique choice, zwanego też
dependent_description)
Axiom dependent_description :
forall (A:Type) (B:A -> Type) (R:forall x:A,
B x -> Prop),
(forall x:A,
exists y :
B x, R x y /\ (forall y':B x, R x y' -> y = y')) ->
exists f : forall x:A, B x,
(forall x:A, R x (f x)).
wynika podwójna
negacja prawa wyłączonego środka w Set
Theorem
classic_set : ((forall P:Prop, {P} + {~ P})
-> False) -> False).
2. Używając impredykatywności Set można dowieść, że z prawa wyłączonego
środka w Set wynika proof_irrelevance_cci.
W pliku hurkens_Set.v jest formalizacja
faktu, że w
kontekście:
Variable bool : Set.
Variable p2b : Prop -> bool.
Variable b2p : bool -> Prop.
Hypothesis p2p1 : forall A:Prop, b2p (p2b A) -> A.
Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).
można dowieść dowolnego B, czyli że zachodzi:
Theorem paradox : forall B:Prop, B.
W pliku proof_irrelevance_Set.v
jest dowód, że z prawa
wyłączonego środka
Hypothesis em : forall A:Prop, {A} + {~ A}.
wynika że możemy zbudować kontekst taki jak w hurkens_Set.v i
udowodnić proof-irrelevance, czyli
Theorem proof_irrelevance_cci : forall (B:Set) (b1 b2:B), b1 = b2.
3. Używając silnej eliminacji można dowieść, że np true <> false
i mamy proof_irrelevance_contradiction.
Lemma proof_irrelevance_contradiction : (forall (B:Set) (b1 b2:B),
b1 = b2) -> False.
4. W pliku choice_em_contradiction.v
jest podsumowanie wszystkich
poprzednich faktow. Najpierw dowodzimy, że:
Lemma em_contradiction : (forall P : Prop, {P} + {~ P}) ->
False.
co jest prawdziwe, bo z prawa wyłączonego środka w Set mamy
proof-irrelevance, a proof-irrelevance nie jest
prawdziwa, np dla bool. Teraz z classic_set i
em_contradiction łatwo wynika False.
Pytanie: Gdzie była używana impredykatywność Set ?
Odpowiedź: W dowodzie classic_set i w pliku
hurkens_Set.v
Rozwiązania problemu:
- zabronić silnej eliminacji i nie rozróżniać true od false,
- nie używać logiki klasycznej,
- nie używać aksjomatu wyboru,
- zrobic Set predykatywny.
Wybrano ostatnie rozwiązanie, bo w Set bardzo rzadko się używa/przydaje
się impredykatywność. Gdy Set jest predykatywny termy takie jak
polimorficzna identyczność (fun
(A:Set)(a:A) => a) nadal są typowalne, ale przez Type a nie Set.
Uwaga: Żeby skompilować załączone pliki trzeba używać
opcji -impredicative-set (jak w Makefile'u).
Proof-irrelevance
Oprócz tego co opisane w punkcie 2 powyżej można też dowieść (plik proof_irrelevance_Prop.v)
Theorem proof_irrelevance_cci: forall P:Prop, P \/ ~ P ->
forall
(B:Set) (b1 b2:B), b1 = b2.
Prop jest sortem impredykatywnym, ale nie ma silnej eliminacji
(eliminacji z Prop w Type, rozróżniania dowodów), więc nie dostaniemy
sprzeczności takiej jak powyżej dla impredykatywnego Set.
Dowód, że
Theorem proof_irrelevance_cci: forall P:Prop, P \/ ~ P ->forall
(B:Prop) (b1 b2:B), b1 = b2.
znajduje się w plikach Coq.Logic.ProofIrrelevance
i Coq.Logic.Hurkens.
Daria