FOM: Franzen's remark and HA

[Stephen G Simpson]

I said:
 > Torkel Franzen said that "intuitionistically we have to distinguish"
 > among
 > 
 >    forall x exists y P(x,y)
 > 
 >    not not forall x exists y P(x,y)
 > 
 >    forall x not not exists y P(x,y)
 > 
 > where P(x,y) is primitive recursive.  ...

 > Is there anything left of Franzen's claim?

After saying that, I thought about it some more and realized that
these three sentences are probably not provably equivalent to each
other in HA.  (Harvey also pointed this out to me.  I think Harvey can
supply specific counterexamples.)  So Franzen's remark is perfectly
valid.  And Franzen's general point, that intuitionistic logic is much
more complicated and problematic than classical logic, is also well
taken.

-- Steve