%%% Hurkens' simplification of Girard's paradox %%% (itself inspired by the Burali-Forti paradox for naive set theory) %%% %%% Kevin Watkins %%% July 2004 %%% %%% See "A simplification of Girard's paradox," Antonius J.C. Hurkens, %%% Proceedings TLCA'95. %% The consistent system HOL tp : type. o : tp. --> : tp -> tp -> tp. %infix right 0 -->. tm : tp -> type. \ : (tm A -> tm B) -> tm (A --> B). @ : tm (A --> B) -> (tm A -> tm B). %infix left 10 @. => : tm o -> tm o -> tm o. %infix right 5 =>. all : (tm A -> tm o) -> tm o. pf : tm o -> type. lam : (pf P -> pf Q) -> pf (P => Q). app : pf (P => Q) -> (pf P -> pf Q). %infix left 10 app. gen : ({T:tm A} pf (P T)) -> pf (all P). spec : pf (all P) -> ({T:tm A} pf (P T)). %infix left 10 spec. % Conversion rule apply = [x] [y] x @ y. beta : {P:((tm A -> tm B) -> (tm A -> tm B)) -> tm o} pf (P ([F] apply (\ F))) -> pf (P ([F] F)). % It is also consistent to add the following, but they are not % used in the paradox. alltp : (tp -> tm o) -> tm o. gentp : ({A:tp} pf (P A)) -> pf (alltp P). spectp : pf (alltp P) -> ({A:tp} pf (P A)). %infix left 10 spectp. %% The inconsistent system U % These constructors are not used except to establish the % existence of a "powerful universe". pi : (tp -> tp) -> tp. \\ : ({A:tp} tm (B A)) -> tm (pi B). @@ : tm (pi B) -> ({A:tp} tm (B A)). %infix left 10 @@. aapply = [x] [a] x @@ a. bbeta : {P:(({A:tp} tm (B A)) -> ({A:tp} tm (B A))) -> tm o} pf (P ([F] aapply (\\ F))) -> pf (P ([F] F)). %% Leibniz equality == : tm A -> tm A -> tm o = [T] [U] all[P:tm (A --> o)] P @ T => P @ U. %infix none 0 ==. refl : pf (T == T) = gen[P] lam[D] D. sub : pf (T == U) -> {P:tm A -> tm o} pf (P T) -> pf (P U) = [D] [P] [E] beta ([h] h ([x] P x) T => P U) (beta ([h] (\[x] P x) @ T => h ([x] P x) U) (D spec (\[x] P x))) app E. sym : pf (T == U) -> pf (U == T) = [D] sub D ([x] x == T) refl. %% Conversions ; : pf (S == T) -> pf (T == U) -> pf (S == U) = [D] [E] sub E ([x] S == x) D. %infix left 20 ;. conv : pf P -> pf (P == Q) -> pf Q = [D] [E] sub E ([x] x) D. %infix left 10 conv. %% Normalization % Definition of redices redex : tm A -> type. bred : {S:((tm A -> tm B) -> (tm A -> tm B)) -> tm C} redex (S ([F] apply (\ F))). bbred : {S:(({A:tp} tm (B A)) -> ({A:tp} tm (B A))) -> tm C} redex (S ([F] aapply (\\ F))). % Congruence rules for redices congred : {F:tm A -> tm B} redex T -> redex (F T) -> type. congred_b : congred F (bred ([h] R h)) (bred ([h] F (R h))). congred_bb : congred F (bbred ([h] R h)) (bbred ([h] F (R h))). fcongred : {F:(tm A -> tm B) -> tm C} ({x} redex (T x)) -> redex (F ([x] T x)) -> type. fcongred_b : fcongred F ([x] bred ([h] R h x)) (bred ([h] F ([x] R h x))). fcongred_bb : fcongred F ([x] bbred ([h] R h x)) (bbred ([h] F ([x] R h x))). ffcongred : {F:({A:tp} tm (B A)) -> tm C} ({x} redex (T x)) -> redex (F ([x] T x)) -> type. ffcongred_b : ffcongred F ([x] bred ([h] R h x)) (bred ([h] F ([x] R h x))). ffcongred_bb : ffcongred F ([x] bbred ([h] R h x)) (bbred ([h] F ([x] R h x))). % Leftmost-outermost redex lor : {T:tm A} redex T -> type. lor_bred : lor ((\[x] T x) @ U) (bred ([h] h ([x] T x) U)). lor_bbred : lor ((\\[x] T x) @@ U) (bbred ([h] h ([x] T x) U)). lor_\ : lor (\[x] T x) Redex' <- ({x} lor (T x) (Redex x)) <- fcongred ([f] \ f) ([x] Redex x) Redex'. lor_\\ : lor (\\[x] T x) Redex' <- ({x} lor (T x) (Redex x)) <- ffcongred ([f] \\ f) ([x] Redex x) Redex'. lor_@1 : lor (T @ U) Redex' <- lor T Redex <- congred ([x] x @ U) Redex Redex'. lor_@2 : lor (T @ U) Redex' <- lor U Redex <- congred ([x] T @ x) Redex Redex'. lor_@@ : lor (T @@ U) Redex' <- lor T Redex <- congred ([x] x @@ U) Redex Redex'. lor_=>1 : lor (T => U) Redex' <- lor T Redex <- congred ([x] x => U) Redex Redex'. lor_=>2 : lor (T => U) Redex' <- lor U Redex <- congred ([x] T => x) Redex Redex'. lor_all : lor (all[x] T x) Redex' <- ({x} lor (T x) (Redex x)) <- fcongred ([f] all f) ([x] Redex x) Redex'. % Proof of a single reduction step redconv : redex T -> {S:tm A} pf (T == S) -> type. redconv_b : redconv (bred R) _ (beta ([h] R ([F] apply (\ F)) == R h) refl). redconv_bb : redconv (bbred R) _ (bbeta ([h] R ([F] aapply (\\ F)) == R h) refl). % Normalize ahn : {T:tm A} pf (T == S) -> type. ahn_step : ahn T (Proof1 ; Proof2) <- lor T Redex <- redconv Redex S Proof1 <- ahn S Proof2. ahn_done : ahn T refl. % Without explicitly naming the term to normalize mknorm : pf (T == S) -> type. mknorm_ : mknorm Proof <- ahn _ Proof. % Convert any two convertible terms mkconv : {T:tm A} {U:tm A} pf (T == U) -> type. mkconv_ : mkconv T U (Proof1 ; sym Proof2) <- ahn T Proof1 <- ahn U Proof2. %% The paradox itself % Preliminaries al = [A] [P] all[x:tm A] P x. = all[p] p. not = [P] P => . set = [A] A --> o. lift : (tm A -> tm B) -> (tm (set B) -> tm (set A)) = [F] [T] \[x] T @ (F x). % These three definitions (and the associated conversion) are the % only ones making use of the full power of U-. univ = pi[X] (set (set X) --> X) --> set (set X). univ' = set univ. univ'' = set univ'. tau : tm univ'' -> tm univ = [T] \\[X] \[f] \[p] T @ (\[x] p @ (f @ (x @@ X @ f))). sigma : tm univ -> tm univ'' = [S] S @@ univ @ (\[t] tau t). % The following conversion is the defining property of a % "powerful universe". %solve _ : mkconv (\[x] sigma (tau x)) (\[x] lift (lift ([x] tau (sigma x))) x) Proof. omega : tm univ = tau (\[p] al(univ)[x] sigma x @ p => p @ x). delta : tm univ' = \[y] not (al(univ')[p] sigma y @ p => p @ (tau (sigma y))). theta : tm o = al(univ')[p] (al(univ)[x] sigma x @ p => p @ x) => p @ omega. done : type. %define part1 : pf theta = gen[p] lam[d] d spec omega conv (C1 p) app (gen[x] d spec (tau (sigma x)) conv (C2 p x)) %solve _ : {p} {x} (done <- mknorm (C1 p) <- mknorm (C2 p x)) -> done. %define part2 : pf (not theta) = lam[d] d spec delta conv C1 app (gen[x] lam[e] lam[f] f spec delta conv (C2 x) app e app (gen[p] f spec (\[y] p @ tau (sigma y)) conv (C3 x p))) app (gen[p] d spec (\[y] p @ tau (sigma y)) conv (C4 p)) %solve _ : {p} {x} (done <- mknorm C1 <- mknorm (C2 x) <- mknorm (C3 x p) <- mknorm (C4 p)) -> done. paradox : pf = part2 app part1.