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

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

```