FOM: intuitionistic and classical arithmetic
neilt at mercutio.cohums.ohio-state.edu
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.
More information about the FOM