FOM: 'Logical parsimony' of intuitionistic mathematics

[Neil Tennant]

Torkel says that "intuitionistically we have to distinguish" among

	(x)(Ey)P(x,y)
	--(x)(Ey)P(x,y)
	(x)--(Ey)P(x,y)

(P a primitive recursive predicate, the quantifiers ranging over N),
"without having a single example of a P for which we can prove
(intuitionistically) one but not all of the three statements.

Wouldn't thi s situation simply tell us more about arithmetic than
about logic? What about other theories besides arithmetic? And isn't
the situation (w.r.t. the first and third sentences at least) the
reason why some intuitionists would be happy with Markov's principle?

This is not so much a rebuttal as a request for information from any
foundationalist intuitionists out there (if they can disentangle themselves
from the aliens' antennae...)

Neil Tennant