Re: Choice sequences, intuition, etc

OK then, sorry to be so late replying to these excellent articles
by Keith Ramsay, Neil Rickert and Daryl McCullough,
but now I have some free time again.
........

Daryl says (along with much explanatory detail):

I'm agreeing that there is a notion of a free choice property,
but that doesn't say what a free choice *sequence* is.

OK, I think I've got it. A free choice sequence is "merely"
a sequence for which the first k terms are known, for any k,
but for which any question essentially involving infinitely
many members, has no knowable answer.

Is that more or less right?

If so, I think this is actually a *better* definition than
the various others given, as it is simpler to understand,
and emphasizes that the essential point of intuitionism involves
*knowledge* about what is the case, as opposed to the orthodox
concern with merely what IS the case.

Now, for one reason or another, intuionists tend to shy away
strongly from this admission - that knowledge is a key element
of their PoV. I'm not sure why they should - they can hardly
be worried by what orthodox mathies think about its possible
vagueness, as their other pronouncements are regularly met
with such criticism anyway.

But I'm sure it's the case. Consider their interpretation of the
disjunctive connective - it says "either there is a construction
for p or there is one for q AND WE KNOW which it is".
Almost every book has such a phrase. Similar for the existential
quantifier: "there exists such a number and WE KNOW what it is,
or can constructively FIND IT OUT".

Knowledge is clearly involved right at the root.

So they may as well come clean and admit it, in this
(IMHO) much simpler definition of Choice Sequences.
.........

Keith observes:

It doesn't seem to me like you're really accepting the idea that
by specifying a different method of constructing the sequence,
one is specifying a different type of entity.

This brings up another gripe, that grates on me enormously.

I have been stressing the *types* of mathematical objects.
It seems to me that this was one of the huge clarifications
of C20 logic - its emphasis on types, and getting them clear,
before setting out on the actual math. And it seems to me
that intuiitionists also shy away from any mention of TYPE.
This gives rise to the feeling that they're being deliberately
obscure about it (which I'm sure they're not).

Sure, I accept that intuiitionist *types* might be different
from orthodox ones, just as their connectives and quantifiers
are, but they should at least mention them! Not shy away.

Classical mathematicians seem to be strongly drawn to
the impression that their philosophical critics are motivated
by some form of skepticism, a fearful desire to avoid notions
that carry some risk of being faulty

I doubt this is so, in most cases. Most orthodox mathies who
are interested enough to debate such matters, will (I guess)
think that Inties are motivated by the desire to increase
*meaning*, which is held to be *constructive* meaning,
or better yet (in this day and age) *algorithmic* meaning,
in math statements. As practitioners have explicitly stated
many times, and as orthodox mathies themselves see the great
benefit of.

Bishop describes... ...one such doubt is about
the rule of ex falso quodlibet, false->X for any X.

I heartily agree! Constructivists should avoid this like
the plague, IMHO, as I cannot see what earthy algorithmic
meaning could be given to it, in any particular case.
Can anyone else? I would love to hear, if so.

On the other hand, he writes elsewhere that reformulating
arguments to avoid negative statements-- by rewriting them
positively-- led to an improvement in the content.

Absolutely corect - a negative statement has little algorithmic
content in most cases; the only such, being in the procedure
that derives a contradiction. Not a lot. But positive statements
have immediate algorithmic content. To be pompous about it,
one might say, a positive statement is mathematical, but a negative
one is meta-mathematical - it describes what cannot be done
by positive (algorithmic) means. OC, traditional inties
do not recognise any meta-/mathematics distinction,
but I think modern constructivists like Bridges do.

If you want to avoid dubiousness, how about refraining from
induction on undecidable predicates?

Well, I think this is a rather tangential issue now, but it's
an interesting one. Before making a pronouncement either way,
I'd really like to see a decent example! I cannot for the life
of me think of any undecideable predicate (of naturals) that
could conceivably be proved (only) by induction. Sure there
are statements like "every halting machine does so-and-so",
but can anyone seriously consider there is a "so-and-so"
that can be proved by induction, ONLY? I'd love to see one!

| It is significant that neither in his
| big book or elsewhere, did he attempt to use FCSs.

Well, as Bridges seems to have pointed out to you, one doesn't
really get much computational "mileage" out of the concept.

EXACTLY SO! And as we seem to be agreed that Bishop considered
that mathematical meaning amounted to computational meaning,
this seems to suggest that he found NO MEANING to Choice Sequences.

And if orthodox mathies, and (merely) constructive mathies
can neither of them see any meaning in CSs, there is a strong
presumption that there IS none, and that Brouwerian inties
are in fact deluding themselves on this one.

Please shoot this down - then I would learn something new.
I realise that math ontology is not a voting matter,
but we-all simply cannot see what on earth they're on about.

| I think we may provisionally conclude that Bishop did NOT
| think that a Free Choice Sequence was a meaningful idea.

No, I don't agree.

Oh, here we are, an answer already! :)

In his textbook, when he mentions Brouwer's proof that
real-valued functions on [0,1] are uniformly continuous,
if you were right, one would expect
that he would say that this was just invalid,

...Instead he says that accepting it as a proof would destroy
the character of mathematics.

Well please forgive my density, but that seem pretty much
identical to me!

Then later he gives it a kind of partial defense, as a possibly
useful metamathematical result: without making certain kinds of
extraneous assumptions,

Well quite so - that is largely what Bridges' program of
reverse constructive math is all about; and why it is now
seen as an axiom, as I stressed.

I provisionally conclude from this exchange that

(i) Bishop DID regard the proof as invalid,
(but was maybe too loyal to say so outright);
(ii) he did NOT see any computational meaning to CSs; and so

(iii) he did not see any mathematical meaning, on the basis
of his philosophy as explicitly stated by him; so
(iv) you have NOT backed up your denial of my claim of (iii), and

(v) the strong presumtion remains that CSs have no meaning,
at least until some positive reasoning can inform us.
....

heard a version of this one (in mine it was "math for poets")

Nice. :)

Somehow the distinction in meaning between
an implication and its contrapositive entered into it.

Maybe so. Can you elaborate on how this may have gone?

I notice in teaching logic, that (classically) it seems best
to introduce it by DEFINING it as ~pvq, (after we have
already defined some other secondary connectives like XOR),
then give "static" examples like 6|n => 3|n , then mention
that "in real life" it usually seems to go with the idea of
*time* and (efficient) causality; but that as there is no
TIME in orthodox math truth, it doesn't really concern us.

That solves MY problems, and maybe many of theirs too.

As for me, I rather like, quite strongly, the constructive
interpretation of implication as asserting the existence
of an algorithm for turning an algorithm for p into
an algorithm for q. That strikes me as really cool,
and certainly a good place from which to start one's quest for
a formal constructivism. It is also type-ically interesting

| So, that is a summary of Bishop's informal motivations,
| and AFAICS it all adds up to a MINIMALIST approach to math

Minimalism doesn't constitute an approach.

We clearly disagree on this much, at least.

It wouldn't explain why he didn't become still more "minimalist".

I see no force in this objection. You only adduce EFQ.
Where did he ever use it? You almost seemed to imply he did,
but no reference was given. Can you think of a likely case?
I'd love to see one!

Meanwhile, I remain firm that minimalism was a partial motivation;
not "agressive minimalism", to be sure, but enough to exclude
unnecessary lack of algorithmic meaning.

One might also expect a minimalist to spend more time on
the axiomatic foundations of what he is doing.

Indeed so! For those of a reverse-math turn of mind, but...

Bishop never has seemed to have been
very much interested in inventorying what axioms he needed.

....Bishop was not so. He had had more than enough of pure logic,
of worthless debate, and merely wanted to DO constructive math,
not explore its theoretical boundaries, as those later have done.
He wanted to do MATH rather than logis, and to "get on with it"!

but if you want to know
the "practical" philosophy of it, pondering the axioms with
which other people formalized it, and how they relate to
other sets of axioms, is just barking up the wrong tree.

So on this part, we seem to agree again.

There are lots of cases to be sure where the goals of
getting at computational meaning and of reducing the
assumptions needed to a minimum are lined up.

Yes!

But where they don't line up, it's the computational meaning
that Bishop lines up with.

I'm sure he would! But I have not yet seen such a case! Show us.

Were Friedman to succeed well enough in extracting "nice"
computational meaning from large cardinal axioms, I trust Bishop
would've taken that as his cue to start using them in some way.

A fascinating speculation indeed!
But one whose answer we shall never know.

Ontology, the branch of philosophy dealing with the nature
and meaning of existence... ... ...
.... ...
Even if we don't accept them as completely accurate,
alleged departures from them deserve hightened scrutiny.

I rather tend to agree with all you say in this section.

So you are in effect relocating the contribution of the reference
to the meaning of the sentence to the other part of the sentence.

I think I get you; and tend to agree.

...somewhat analogous to the way in which we might say that
an element of the integers mod 17 is essentially an integer,
but that we define a distinct notion of equality for elements
of the integers mod 17, namely, equivalence mod 17.

This is certainly a good example of something!

But I'm not sure what. It's certainly how I treat modular
arithmetic for first-years - I loathe the thought of heading
into sets - that can be done later as an example of equivalence
classes, when we come to that. For actually DOING mod arithmetic,
it's nothing but a mighty confusion for innocents!

Your example seems to me not so much applicable to CSs, but
as a good example of Conway's cry for "Mathematician's Lib",
wherein we can define equality however we damn well please!

a free choice sequence is "really not the same thing" as
a generic sequence, and that both points of view
are valid in a sense.

But once again, the standard intuitionist fear and loathing
of considering any form of strict typing, prevents us from
seeing exactly what they're on about. I think typing is CRUCIAL.
.........

Neil says:

It seems that Neil was speaking more of
the development of cultural intuitions. I had been speaking
more of individual, personal intuition(s).

I'm not sure that's a clear distinction. We derive our personal
intuition within a culture. And what could "cultural intuitions"
even mean, other than typical personal intuitions of members
of the culture?

Oh come come, please, try to be a little accomodating.
Most people can see a clear difference between personal and
cultural matters, most of the time. Tradition, literature,
concensus, politics, these are all involved in various ways.
You know all this!

In the case of math intuitions, timing (history) is crucial too.

We teachers must always be on the alert not to crush students'
intuitions or overbully them too definitely along one track.

We university teachers mostly see students after their math
intuitions are already well formed.

Obviously that's true regarding N, and basic calculus;
but regarding these "higher matters" about the existence
and nature of setlike things, constructive things, etc,
that is far from so; and crucial in university math.

Sure, I agree that sets of size larger than c are,
in some sense surreal.

Excellent! Many folk here regard this as objectionably arrogant.

So is the set of ordinals less than the first uncountable ordinal.
And the Stone Cech compactification of the reals always
seemed highly surreal (this, of course is larger than c).

And might I add free ultrafilters in general, nonmeasurable sets,
and nonconstructive ordinals?

[AISI], constructivism wants to stick to the synthetic approach,
yet still pretend that what is done is relevant to physics.

I think that may be now definitely OTT.
I can't think what it means. Perhaps you might elaborate, Neil?

A physicist wants to consider the point of intersection of two
idealized light rays. I cannot think of any reason to consider
that point... ...mathematically constructible?

OUCH! You probably know my views well enough by now,
to know that I regard such issues as violent context errors.
I have no idea of the meaning ascribable to such category errors.

So I guess your original remark above, your complaint about
constructivism, will remain opaque to me, if it essentialy
involves such things. Regarding the modelling of physics
by math, I see no essential difference between the two math's.

-- Bombastic Bill
.

Relevant Pages

  • Re: binary file compare...
    ... that the math is fundamentally wrong is quite another. ... Any algorithm failing to handle all contingencies is flawed. ... The meaning of 2) is that the designer missed or left out something. ... The more complicated the math the harder it is to keep a higher form of math from checking (or improperly displacing) a lower one. ...
    (comp.lang.python)
  • Re: A quote (and question) about intuitionism
    ... |Is that a definition of truth? ... then, according to the meaning, the statement is sometimes ... So for me the evidence I have for FLT is ... If I understand correctly, constructivists, roughly speaking, ...
    (sci.math)
  • Re: Explaining Time Dilation
    ... >> Did you not read all my predictions which are at variance with the ... Did you comprehend my meaning when I stated that Einstein ... Math is precise about observed effects but never about ...
    (sci.physics.relativity)
  • Re: A quote (and question) about intuitionism
    ... |Is that a definition of truth? ... then, according to the meaning, the statement is sometimes ... considered appropriate by a lot of constructivists, ... fact that we have ways of discovering facts about the past. ...
    (sci.math)
  • Constructive Math query.
    ... especially Keith Ramsay, for his lengthy and helpful essays. ... respect of his separation from orthodox math), ... OC, it all depends on how epsilon "is given", itself a somewhat ... constructivists, ...
    (sci.logic)