Re: Choice sequences, intuition, etc

Keith Ramsay wrote (in two articles):

I don't see anything worse, more ambiguous or less clear,
about free choice sequences than classical [stuff]

Well, as I understand it from your comments, this is quite
true provided we agree that what is really being defined
here is a *property* of (Free Choice) Sequences. And that
sequences per se are really little different from orthodox.
As I replied before, the issue (to me) is one of type-ing.

More below.

|Perhaps I should mention again that the modern constructivist
|view seems to be that Brouwerian math is effectively "merely"
|Bishop's (minimal, non-LEM) constructivism, + the AXIOM that
|"every function is uniformly continuous", (which may in turn be
|equivalent to other Fan-like or Konig-like statements).
|
|How this connects to FCSs I don't know. Anyone?
|I could always ask Douglas again, I suppose.

Perhaps you should.

Well I did. His answer wasn't utterly clear; but as I said,
he regards the effective content of FCS's to be their effect
on computational matters regarding the various versions of
fan theorems and bar theorems, some of which (he observed)
were merely assumed by Brouwer as being "obviously true"
of FCS's, and thus "axioms" (a concept Brouwer loathed, BTW).
Incidentally, he pointed out which variants of fan and bar
theorems are *still* undetermined to be equivalent to
various intuitionist "theorems" such as: every function
(with compact support) is continuous; or uniformly continuous.

He admitted that for the died-in-the-wool (philosophical)
constructivist, i.e. an Intuitionist, such an answer would be
incomplete, and such a person would regard a FCS as having
more to it; but implied that neither he nor I would be able
to make much of it. He didn't actually *sneer* when talking
about FCS and their adherents, but I came away with that feeling.

But if one has any interest at all in
what views were held by Brouwer, Bishop and so on, and how
that motivated their way of doing mathematics, you might be
better off just forgetting these axioms.

Regarding Brouwer I'm sure you're right. Regarding Bishop,
I doubt it. As to his motivations, someone else observed
that his claimed main motivation (as written in his preface)
was to keep mathematical statements "as meaningful as possible".
I have no doubt this is true. And, as I implied earlier,
he (Bishop) seems to have found that this could be done best
by eschewing ALL doubtful concepts, and that this included
LEM *and* FCS's. It is significant that neither in his
big book or elsewhere, did he attempt to use FCSs.

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

Incidentally, Douglas Bridges related two Bishop anecdotes,
which he regards as being his core original motivations.

The first, was when he was doing multivariate complex variable,
and looking at the spaces in multi-dimensional complex co-ordinates,
and found to his amazement that after he'd proved certain
things existed that he could NOT visualise them, or their spaces,
because of the non-constructive nature of them. As visualisation
was always a core component of his math, he was dismayed.

The second came when he was teaching a course in
"mathematics for gracious living", :) , i.e. math for
humanities students. He found that many of them were
very smart cookies, and they came up after his initial
logic lectures complaining that - "Hey this is rubbish
what you said about the implication connective,
(the classical one), it *obviously* doesn't mean that at all!"
After discussing and thinking about it, he realised that
they had a point, and began to explore constructivist
ideas more seriously.

So, that is a summary of Bishop's informal motivations,
and AFAICS it all adds up to a MINIMALIST approach
to math and its basic assumptions, and little else,
and that this agrees with his "meaningful" statements,
contrary to what some posters have claimed about this.

Beeson describes the Markov school as having assumed both
Markov's principle and Church's thesis, although he says that
they kept track of which theorems depended upon Markov's rule.

I'm sure this is right. Though "assuming Church's thesis"
hardly seems a radical move! I don't know of anyone who
seriously denies it. Perhaps they meant it applied
"more harshly" in some way? Perhaps they took it as
meaning that any function WAS a computable function?
That last statement is not CT at all!
_ _ _ _

let me try to rephrase it.
If a free choice sequence s has a property P, then
there exists some N such that every free choice sequence s'
that agrees with s for the first N terms also has property P.

This is a very clear and good statement, except that
(as claimed above) it seems to me a statement that is
essentially about PROPERTIES of sequences, rather than
sequences themselves. AFAICS, from an orthodox PoV,
it says, of "FCP"s, i.e. "Free Choice Properties", or maybe
"Finitely Computable Properties", [ HUZZAH! :) ], that:-

* If a sequence s has a FC property P, then
* there exists some N such that every sequence s' that
* agrees with s for the first N terms also has property P.

That strikes me as being a (minimally changed) version
of your version of the definition, that is now typed
in a way that an orthodox mathie can follow, AND still
contains the essential idea that a FCS contains.

It's a striking example of how the constructive concept of
existence is a generalization of the classical concept.

So in my translated view, this rather becomes "a striking
example of how the constructive concept of a concept
("property") is a particularisation of the classical concept".

OC, this disagreement about which is a subset of which,
has been going on since the dawn of constructivism!

The philosopher Dummett has argued that knowing how to use
a language should be nearly sufficient to allow one to know
what the sentences in it mean, and even what the individual
terms mean. (Frege had a similar idea that the meaning of
a term is given by how it contributes to the meaning of a
sentence in which it's used.)

I tend to agree with all this, but disagree that Brouwer
is exemplifying it in any way.

I think (hope) the idea of a FC property is now very clear,
classically, and (as usual) cannot see why properties such as
"counting from the left, there are always more 1's than 0's
in this sequence", clearly not a FC property, is in any way
deficient philosophically, or "unusable" in practice,
as you seem to claim. Sure, we cannot *check* it finitely
(other than by theory-rich means), but we can sure as hell
USE IT - one can think of many consequences, some practical,
that might follow from such a claim. It is quite "workable with"!

P.S. Don't think of this kind of thing in terms of
"transcendental vision". It's more like an attempt
at the opposite, a view that is entirely immanent.

HAH! Very cute! Nice one. :)

-- Workable William
.

Quantcast