FOM: intuitionistic and classical arithmetic

Neil Tennant neilt at
Thu Feb 12 16:14:28 EST 1998

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

	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

More information about the FOM mailing list