FOM: intuitionistic and classical arithmetic

[Neil Tennant]

Further to the exchange with Torkel about the similarities and differences
between classical arithmetic (PA) and intuitionistic arithmetic (HA)---it
has just occurred to me that Harvey Friedman once reported the following
theorem:

	if S is Pi_0_2 then (if PA|-S then HA|-S)

If this is so, then Torkel's claim:

_____________
intuitionistically we have to
distinguish between e.g. (x)(Ey)P(x,y) (P a primitive recursive
predicate, the quantifiers ranging over N), --(x)(Ey)P(x,y) and
(x)--(Ey)P(x,y) without having a single example of a P for which we
can prove (intuitionistically) one but not all of the three statements.
_____________

can be strengthened: it will be *impossible* to find an example of such a P.

Neil Tennant