FOM: Intuitionism

[William Tait]

In an earlier posting, I pointed out that, if an intuitionist were to 
treat ``P is provable'' as a mathematical proposition, then there would 
be no choice but to take it to be the same as or equivalent to P [and, 
in that case "either p is provable, not-p is provable, or neither is 
provable" reduces to excluded middle]. For, what would prove ``P is 
provable'' other than a proof of P. Here there is no appeal to anyone's 
authority: it only has to be agreed that, for an intuitionist,  a 
proposition is given precisely when it is specified what counts as a 
proof of it.

Jesper Carlson introduces the legitimate consideration that ``P is 
provable'' should not be taken to be a mathematical proposition---in 
which case, the original question of whether intuitionists would  accept 
the statment "either p is provable, not-p is provable, or neither is 
provable" as logically valid is ill-posed.

His report that Martin-Lof does not take ``P is provable'' to be a 
mathematical proposition would seem irrelevant to a discussion of 
foundations---though a report of M-L's argument might well be relevant.

Bill Tait