[Haskell-cafe] Re: forall & ST monad
Heinrich Apfelmus
apfelmus at quantentunnel.de
Wed Feb 25 08:31:53 EST 2009
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
More information about the Haskell-Cafe
mailing list