[Haskell-cafe] Re: forall & ST monad

[Heinrich Apfelmus]

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