FOM: Intuitionism

[Jesper Carlstrom]

>== Original Message From Jesper Carlstrom <jesper at matematik.su.se>==
> 
> >On Fri, 17 May 2002, wiman lucas raymond wrote:
> >
> > > would an intuitionist accept the statment
> > > "either p is provable, not-p is provable, or neither is provable"?
> >
> >The principle
> >
> >   If a proposition cannot be known to be true,
> >   then it can be known to be false
> >
> >is defended from an intuitionistic point of view in Martin-Löf ... 
==<

On Sat, 18 May 2002, richman wrote:
> Is the principle supposed to apply to the statement?

If "neither is provable", then, in particular, p cannot be known to be
true. Hence p can be known to be false. But then -p can be known to be
true, so -p is provable, which contradicts the assumption.

All this seems trivial, but isn't when you, like Martin-Löf, distinguish
between "p true" and "p known to be true"; and between "proof" in the
sense of a mathematical object and "demonstration" in the sense of a
convincing argument. Making these distinctions, you have to decide to
which notion of proof ("proof" or "demonstration") "provable" refers. Note
that in ordinary mathematics, "provable" use to refer to the notion of
demonstration (and sometimes to deduction in a particular system).

Jesper Carlström