[FOM] excluded middle and constructive mathematics

[Nik Weaver]

Panu Raatikainen wrote:

>> But it is also important to return to reality from time to time. This is
>> where constructive mathematics comes in.
>
> These are strong claims, and we've heard them now and then before, but
> it would be nice to hear some convincing arguments supporting them...
> I've honestly tried hard to find one for some time, but have so far
> failed...

Panu --- this relates to the papers I announced yesterday.  I believe
that in certain settings of broad interest a definitive case can be
made for constructivism.  Specifically, excluded middle cannot be
assumed when we are reasoning about the general semantic notion of
a valid proof or about the general notion of a Fregean concept.

I could spell out why I think this, but maybe the easiest way to make
the point is just to say that I can give formal systems for reasoning
about provability and Fregean concepts, and these systems are consistent
but become inconsistent when LEM is added.

The systems are described in Section 6 of "The semantic conception of
proof" and Section 4 of "Reasoning about constructive concepts".  Direct
links are here:

http://math.wustl.edu/~nweaver/proof.pdf

http://math.wustl.edu/~nweaver/concepts.pdf

In those papers I go into some detail about the philosophical
justification for rejecting LEM in these settings, but in any case
the brute fact is that one can reason consistenly about concepts
which fall under themselves and sentences that assert their own
unprovability only from a constructive viewpoint.

Nik