FOM: Intuitionism

[Jesper Carlstrom]

On Tue, 21 May 2002 richman at acc.fau.edu wrote:

> Because intuitionists identify the assertion of p with the assertion of
> the provability of p, they could derive a contradiction from "neither is
> provable" by using the tautology "not-(not-p and not-not-p)".

I agree that if you identify "p is provable" with the proposition p, and
"not-p is provable" with not-p, and interpret "neither is provable" as
"not-p and not-not-p", then you may apply intuitionistic logic and reduce
the proposition to the equivalent "p or not-p".

The point is that these identifications are NOT made by Martin-Löf (though
he and many others call him an "intuitionist").

OK, he doesn't mention "p is provable", but it could naturally be
interpreted as "p true" or "p can be known to be true", depending on what
notion of proof is referred to by "provable" ("proof" or "demonstration").

So, Martin-Löf distinguishes between

   the proposition             p
   the judgement               p true
   the epistemic situation     p can be known to be true

Intuitionistic logic does not apply to judgements and epistemic
situations, simply because the BHK interpretation does not make sense for
them: they are not given by telling what counts as proofs of them. Thus,
since "p provable" is not a proposition in this interpretation, you cannot
apply intuitionistic logic to it (my "derivation" in the previous letter
was nothing but unwinding definitions and composing constructions).

Martin-Löf treats the problem in this spirit and I cited him because I
believe it would be of some interest to see the argument with all these
distinctions made. I'm afraid I'm not the right person to defend them so I
leave the discussion here, please refer to the paper cited for details. 

Jesper Carlström