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:

  1. zabronić silnej eliminacji i nie rozróżniać true od false,
  2. nie używać logiki klasycznej,
  3. nie używać aksjomatu wyboru,
  4. 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
Valid CSS!