On Fri, Feb 20, 2009 at 11:33 AM, Kim-Ee Yeoh
Here's a counterexample, regardless of whether you're using constructive or classical logic, that (forall a. T[a]) -> T' does not imply exists a. (T[a] -> T').
Let a not exist, but T' true. Done.
That isn't quite a proper counterexample; if T' is true, that is, you can write a term of type T', then exists a. (T[a] -> T') is trivially true; here's a constructivist proof in Haskell: type T :: * -> * -- given type T' :: * -- given v :: T' v = given type A = () f :: T A -> T' f _ = v data E t t' where E :: forall t t' a. (t a -> t') -> E t t' proof :: E T T' proof = E f It believe that it's true that ((forall a. t a) -> t') does not entail (exists a. t a -> t') in constructivist logic, but I can't come up with a proof off the top of my head. Intuitively, to construct a value of type (E t t') you need to fix an "a", and I don't think it's possible to do so. On the other hand, "a" is hidden, so the only way to call the function inside of E t t' is to pass it something of type (forall a. t a), right? -- ryan