Sorry
Table of Contents
1 The Sorry Method
module Lib.Sorry where
1.1 Packages imports
import Stdlib.Prelude import Lib.Data.Empty import Lib.Data.Unit
1.2 The proof
As the system implements type in type, we can show that it is inconsistent. It allows us to use a "sorry" λ-term that shows everything. It is useful to build the structure of a proof.
data SET : U = set (X : U) (f : X → SET) SET/mem (a : SET) : SET → U = split set X f → (x : X) * (Path SET a (f x)) SET/nmem (a b : SET) : U = neg (SET/mem a b) RUSSEL-SET : SET = set ((s : SET) * (SET/nmem s s)) (λx. x.1) IN-RUSSEL-SET (X : SET) (t : SET/mem X RUSSEL-SET) : SET/nmem X X = J SET t.1.1 ( λY _. SET/nmem Y Y) ( t.1.2) X ( inv SET X t.1.1 t.2) RUSSEL-SET-NOT-IN-RUSSEL-SET : SET/nmem RUSSEL-SET RUSSEL-SET = λt. IN-RUSSEL-SET RUSSEL-SET t t IN-RUSSEL-SET' (X : SET) (f : SET/nmem X X) : SET/mem X RUSSEL-SET = ((X, f), refl SET X) falso : Empty = RUSSEL-SET-NOT-IN-RUSSEL-SET ( IN-RUSSEL-SET' RUSSEL-SET RUSSEL-SET-NOT-IN-RUSSEL-SET)
Thus, we can implement a term that proves anything.
falso' (P : U) : Unit → P = split star → falso' P star sorry (P : U) : P = falso' P star lock sorry -- sorry (P : U) : P = -- ex-falso P falso