FOM: Franzen's remark and HA
Stephen G Simpson
simpson at math.psu.edu
Fri Feb 13 17:44:52 EST 1998
> Torkel Franzen said that "intuitionistically we have to distinguish"
> 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
More information about the FOM