Re: Choice sequences, intuition, etc


On Nov 21, 10:11 pm, Bill Taylor <w.tay...@xxxxxxxxxxxxxxxxxxxxx>
wrote:
|So, let's posit that the Twin Prime conjecture was proved from
|some other multi-quantifier arithmetic conjecture, and also from
|its negation. But that neither proof gave any hint as to bounds
|for finding new twin primes.
|
|The orthodox mathie now says, "TPC is true, and has been proved".
|
|But (I guess) the constructivist would say no more than
|"If `conjecture' is either true or false, then TPC is true",
|if even that.
|
|Is that correct?

The meta-theorem still covers this case. Generally, if you
have a Turing machine, and prove classically that for each
input the machine halts, then the proof can be converted
into a constructive proof.

I don't know what your underlying point is going to be here,
but in a more general case, you could have it that
"If A is true or false, then B" has been constructively
proven without B being constructively proven. The classical
mathematician, believing the law of excluded middle, would
count B as proven. From "if A is true or false then B" one
can also infer "B is not false", which again, by double
negation elimination, is taken classically as signifying
that B is true.

The case having the smallest "logical complexity" in which
this occurs is when it's proven nonconstructively that some
Diophantine equation has finitely many solutions. It's hard
to make much of a philosophical point there because there
is too little besides a difference in terminology separating
the two ways of thinking about the situation. Constructively
one would say that it's been proven that there are not
infinitely many solutions, and not necessarily that there
are finitely many. Classically one would say that it's been
proven that there are finitely many, but without necessarily
giving a way of finding an upper bound on them.

The mathematician working constructively, by having this
issue directly visible (the theorem is stated differently)
might be expected to have more interest in getting this
additional fact (if it is one) that there are finitely many
solutions. But it's not necessarily so. They might also be
expected to be less interested in merely showing that there
are not infinitely many solutions, but this is also not
necessarily so either. I think generally mathematicians
working both ways find the issue obvious enough.

It's in more involved cases that the two philosophies are
more likely to give rise to really different mathematical
interests.

[...]
|Which, to me, means to see them in the light of clarity
|and precision, which I take to be the essence of any
|mathematical endeavour; and to be able to handle examples,
|and apply them, at least to other math.
|
|To a large extent, Keith, for all his efforts, has been failing
|in this with me (if not with others). You seem to have been
|more helpful, a good deal more, but are now looking like drying up.

Well look, Bill, if free choice sequences had ever been one
of my main interests, you might be "getting" more of what
you want to get. But it's always been a kind of sidelight.
Even people with a more professional interest in this kind
of thing seem usually to mention free choice sequences
mainly because of their status as something that Brouwer
took seriously. If it seemed like you were engaged in
some kind of serious study of Brouwer, trying to help you
do that also might seem more interesting.

I hunted around in the library a bit and found less than I
expected. I did a Mathematical Reviews search for "free
choice sequence" and got very little. There were some
references to _Foundations of Intuitionist Mathematics_ by
Kleene and Vesley. (The library catalog asked me if I had
meant to search for "Kleenex Wesley", which however matched
no entries.)

Kleene and Vesley had allegedly provided one of the best
axiomatizations of intuitionist mathematics at the time,
decades ago. The aspect related to free choice sequences
was very small, however. They essentially just added axioms
for Bar Induction and the Fan theorem, so that Brouwer's
theorem would be a theorem.

As far as I can tell, Bishop got the essential point. I
might rephrase it by saying that Brouwer beefed up a bit
the meaning of the universal quantifier over real numbers.
If you prove that every real number has a property P,
without making certain kinds of assumptions, it has to be
that your result would apply equally well to free choice
sequence real numbers, and hence that certain metatheorems
apply. I'm not terribly familiar with those metatheorems;
that functions on [0,1] that you prove are pointwise
continuous without making special assumptions are always
uniformly continuous is pretty famous.

Keith Ramsay
.

Relevant Pages
Quantcast