Constructive Math query.

Many thanks to all those who have contributed to this thread,
especially Keith Ramsay, for his lengthy and helpful essays.

Keith inquires:

> | I would be surprised if Bill thinks your point clarifies anything.
> | But I could be wrong.

> Well, Bill, do you think I've clarified anything?

Well, perhaps clarified is not the term I'd have used, but certainly
your point elaborated helpfully and usefully on your earlier answer.

It also pinpointed a key philosphical test in this general area.
Maybe it's a litmus test differentiating between a mere constructivist
and a full-blown intuitionist; or maybe just between Brouwer and
everyone else. Though not quite everyone. Even Bishop himself,
generally regarded as a "minimalist" constructivist, (minimal in
respect of his separation from orthodox math), took a somewhat
Brouwerian "hard line" over this. There is an excerpt in his book,
which, when I showed it to Bridges (his co-author, more like editor),
he (Bridges) expressed his surprise that it had slipped through,
and also that Bishop himself would be so hard-nosed. The excerpt was:

"Since nothing is true unless and until it has been proved..."

This refusal to distinguish a difference between truth and proof
is perhaps characteristic of full-blown subjectivism in math,
and is strongly held by the ultra-finitists (calling themselves
merely "formalists") of today. As seen on the FoM mailing list.

IMHO it is the most untenable of phislosophical positions about math,
and indeed self-contradicting as I've elaborated on earlier occasions.

Keith's point is another assertion of the more orthodox and
"merely constuctive" viewpoint. That truth and proof are always
to be distinguished, and that the former, "unproved truth",
is a coherent concept.

It is further exemplified in Torkel's later test-example:

> Consider a statement of the form
>
> For every partial recursive function f, if f is total, then --f--.
>
> Do you agree that this is not constructively synonymous with "For
> every partial recursive function f, if we can prove that f is total,
> then ---f---"?

It is also at the root of Keith's first answer...

> | Is this still provable in constructive math? The proof seems
> | to require looking at unbounded distances down the sequence,
> | so I'm not sure.

> It might be a useful exercise to look at a classical proof and try to
> figure out which step it is that seems ... might be nonconstructive.

> Suppose we have an epsilon > 0. By Eudoxus' principle, which is
> constructive, epsilon>1/k for some integer k>0.

....which I did not find completely & totally helpful, even with
the later elaboration.

In particular, this recourse to Eudoxus, (which is not unlike my
original discomfort with looking unbounded distances down a sequence),
seems to be avoiding an issue.

To find k such that epsilon > 1/k involves looking "arbitrarily far"
down a sequence, which seems slightly nonconstructive, at least in some
views of the subject. (Though very Markovian OC!)

OC, it all depends on how epsilon "is given", itself a somewhat
vague term. If epsilon is given explicitly (in some sense),
there is no problem. But I'm fairly sure that there are ways
of "giving" an epsilon by using fickle sequences, so beloved of
early intuitionists, that might lead to trouble with Eudoxus.


So I am still somewhat unclear about it all. I'm pretty sure that
Keith is right about the views of *the most minimal possible
constructivist* - one who accepts all orthodox math except
the use of LEM. But I still get the feeling that most modern
constructivists (and the Bishop exerpt above is surely significant),
are rather stricter in their attitudes.

-----------------------------------------------------------------------
Bill Taylor W.Taylor@xxxxxxxxxxxxxxxxxxxxx
-----------------------------------------------------------------------
The intuitionist conflates existence with provability.
The Platonist conflates existence with consistency.
-----------------------------------------------------------------------

.

Relevant Pages

  • Re: Choice sequences, intuition, etc
    ... before setting out on the actual math. ... meaning could be given to it, ... but I think modern constructivists like Bridges do. ... of an algorithm for turning an algorithm for p into ...
    (sci.logic)
  • Re: Choice sequences, intuition, etc
    ... that constructive math is the math of ALGORITHMS - *where*, ... about free choice sequences than classical "arbitrary sets ... the views of constructivists and the logicians who want ... mathematics was as if operating in some kind of "base" theory. ...
    (sci.logic)
  • Re: Cantorian pseudomathematics
    ... > Jesse F. Hughes wrote: ... > every epsilon, the unit disk can be covered with finitely many possible ... the constructivists would consider the limit as epsilon goes to ...
    (sci.math)
  • Re: Cantorian pseudomathematics
    ... >> Jesse F. Hughes wrote: ... the constructivists would consider the limit as epsilon goes to ...
    (sci.math)