Ryan Ingram wrote:
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.
Here's something close to a counterexample, but I'm really confused. The objects of discourse are red, blue and green glass marbles T[a] = a is red \/ a is blue S = forall a. T[a] = all marbles are red or blue Now, (forall a. T[a]) -> S is clearly true while exists a. (T[a] -> S) should be nonsense: having one example of a marble that is either red or blue does in no way imply that all of them are, at least constructively. (It is true classically, but I forgot the name of the corresponding theorem.) I'm not quite sure how to make that rigorous; I would like to turn the above into a proper model of intuitionistic logic. The other problem is that in Haskell, forall does not quantify over glass marbles, but over types/propositions. Take T[a] = a S = forall a. T[a] = _|_ Once again, (forall a. T[a]) -> S is true, but what about exists a. (a -> _|_) = exists a. not a ? I mean, a can be a proposition now, so what about taking a = forall b.b = _|_ ? Does exists a imply that the example proposition constructed should true or is it enough to be able to construct a proposition at all? Regards, apfelmus -- http://apfelmus.nfshost.com