[Agda] MiniAgda with the excluded middle is also inconsistent

[Andreas Abel]

Hugo's proof is now also available in MiniAgda.

   http://www2.tcs.ifi.lmu.de/~abel/miniagda/index.html

Since I was too lazy to implement Set1, MiniAgda has now Set : Set, but 
this is not crucially exploited in the proof.

What is crucially exploited is the "smart case" which makes the 
constraint e = p available in checking the branch b in

   case e { p -> b }

Here is the full prove in (due to the absence of implicit arguments) 
painstaking detail.

Cheers,
Andreas



data Empty : Set {}

data Unit : Set
{ unit : Unit
}

data Or (A : Set) (B : Set) : Set
{ inl : A -> Or A B
; inr : B -> Or A B
}

data Eq (A : Set)(a : A) : A -> Set
{ refl : Eq A a a
}

fun cong : (F : Set -> Set) -> (G : Set -> Set) -> (A : Set) ->
   Eq (Set -> Set) F G -> Eq Set (F A) (G A)
{ cong F .F A (refl .(Set -> Set) .F) = refl Set (F A)
}

fun castLR : (A : Set) -> (B : Set) -> Eq Set A B -> A -> B
{ castLR A .A (refl .Set .A) a = a
}

fun castRL : (A : Set) -> (B : Set) -> Eq Set A B -> B -> A
{ castRL A .A (refl .Set .A) a = a
}

data I (F : Set -> Set) : Set {}

fun injI : (F : Set -> Set) -> (G : Set -> Set) -> Eq Set (I F) (I G) -> 
Eq (Set -> Set) F G
{ injI F .F (refl .Set .(I F)) = refl (Set -> Set) F
}

data InvI (A : Set) : Set
{ inv : (X : Set -> Set) -> Eq Set (I X) A -> InvI A
}

let EM : Set
        = (A : Set) -> Or A (A -> Empty)

fun em : EM {}  -- postulate excluded middle

fun cantor : Set -> Set
{ cantor A = case (em (InvI A))
   { (inl .(InvI A) .(InvI A -> Empty) (inv .A X p)) -> X A -> Empty
   ; (inr .(InvI A) .(InvI A -> Empty) bla) -> Unit
   }
}

{- now define (modulo casts and irrelevant cases)

    no  = \ f -> f f
    yes = \ f -> f f
-}

let no : cantor (I cantor) -> Empty
= \ f -> case (em (InvI (I cantor)))
   { (inl .(InvI (I cantor)) .(InvI (I cantor) -> Empty)
       (inv .(I cantor) X p)) ->
         f (castRL (X (I cantor))
                   (cantor (I cantor))
                   (cong X cantor (I cantor) (injI X cantor p))
                   f)
   ; (inr .(InvI (I cantor)) .(InvI (I cantor) -> Empty) g) ->
       g (inv (I cantor) cantor (refl Set (I cantor)))
   }


let yes : cantor (I cantor)
= case (em (InvI (I cantor)))
   { (inl .(InvI (I cantor)) .(InvI (I cantor) -> Empty)
       (inv .(I cantor) X p)) ->
         \ f -> (castLR (X (I cantor))
                   (cantor (I cantor))
                   (cong X cantor (I cantor) (injI X cantor p))
                   f) f
   ; (inr .(InvI (I cantor)) .(InvI (I cantor) -> Empty) g) -> unit
   }


eval let omega : Empty
           = no yes


herbelin a écrit :
> Hi,
> 
> I worked a bit on Chung-Kil's proof. We can make it almost the same
> proof pattern as when using impredicativity, basically building the Ω
> combinator, as shown in file cantor1.agda below.
> 
> I also have a more direct variant of this proof (file cantor2.agda
> below) but unfortunately, I could not succeed in telling Agda how to
> check it (the proofs seems OK to me, but typing needs to remember that
> some variable p has both type A and ¬A and I don't know how to hint
> this to Agda).
> 
> Basically, the shortened proof shows that excluded-middle is morally
> used only once, in hiding the antecedent of I at level Set1 in a case
> analysis to Set:
> 
>   cantor : Set -> Set
>   cantor a with exmid (invimageI a) -- invimageI is ∃x:Set->Set.(I x)=a
>   cantor a | inl (invelmtI x y) = x a -> Empty
>   cantor a | inr b = One
> 
> vs (in an impredicative system)
> 
>   cantor : Set -> Set
>   cantor a = ∀ (x : Set -> Set) -> Eq1 (I x) a -> x a -> Empty
> 
> I think we should also notice that the proof uses excluded-middle in
> Set1. I don't see how it could refute excluded-middle in Set0 since
> the use of excluded-middle here is really about contributing to embed
> some object in the Set1 level into the Set level.
> 
> Hugo
> 
-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/