Choice sequence lessons.
Bill Taylor
for me, (and others). I thought I'd start up a new thread
title, because the other one has got a bit long, and anyway
this is rather more specialised.
> Both constructivists and platonists can and should say:
>
> "If `conjecture' is either true or false, then TPC is true",
>
> is proven constructively, but TPC is not (yet) proven
> constructively. Or: the statement TPC, - when interpreted
> constructively - has not been proven yet.
> But somehow I doubt that that enlightens you.
No, that's fine. For the most part I have little problem
understanding merely-minimal-constructivist notions.
It's just choice sequences that I'm at sea with.
> Sometimes the interests and/or basic attitude of people are
> so far apart that even communication is close to impossible -
> or at best useless.
I do not agree with such counsels of despair. It just means that
we must exercise more care, empathy and consideration, to achieve
communication. We are intellectuals here, not street louts!
> I do agree that every mathematical notion that can be sensibly
> claimed to make sense should have at least some counterpart
> in whatever philosophy of mathematics one adheres to.
Glad to hear it!
I have been working on the assumption that this is so.
> One is the intuitionistic philosophy of mathematics.
> The second is the practice of intuitionistic mathematics.
> A third is the notion of a choice sequence.
That's a good trichotomy!
> As far as i'm concerned, an `orthodox mathie' should be able to
> understand the latter (and to a lesser extent also the second),
Interesting that your "to a lesser extent" is the wrong way round
(for me) - I see the practice here (UC) quite regularly, but the CS
part remains obscure, (till now), and also to my practitioners(!)
> even if appalled or puzzled by the intuitionistic philosophy.
A very good proviso, for me at least. We shall leave it.
> However, the system I was planning to describe does give
> a number of pretty good `entry points' to explain and
> discuss the issues involved in intuitionism / constructivism.
No no! Please continue with your original plan. I only interrupted
because it appeared you were withdrawing. But you're not,
so please comntuinue with your plan.
And your comment about textbooks being more helpful does
NOT apply - they cannot or will not start out by empathising
where the orthodox mathie stands. But you do.
>> Well let me summarise. AIUI, choice sequences are integer
>> sequences of which we may ask and know ANY question regarding
>> a finite number of terms, but which we may not (always) know
>> and not (always) ask things essentially involving infinite
>> numbers of terms. Is that more or less correct?
> My attempt:
> Choice sequences are sequences that are produced step-by-step,
> in the course of time, and at every moment of their existence
> are in an unfinished state.
I understand the intuition (whether or not I agree with it).
You were describing the intuition, whereas I had been attempting
more to deal with the necessary formalisation, (though in
common language). I think that is why we had different tones.
> If you can bear with me; I prepared a reasonably good `lesson 3',
> but am struggling a bit with articulating `lesson 2'.
Keenly awaiting. Do not let my earlier remarks deter you from
your original plan.
"""""""""
Let's first do an exercise for lesson 1.
> Recall that FS stands for fixed sequence, CS for `choice sequence'
To interject briefly, not seriously - from your above description
CS ought really to stand for "continuing sequence", (!),
or even "continuable sequence", whereas FS might be
"full sequence" or "finished sequence".
> Let's use `x = y' as shorthand for `forall i [ x(i) = y(i) ]',
> for any x,y for which the latter makes sense.
>
> Question: which of the following statements are true:
>
> forall x:FS exists y:CS [ x = y ]
> forall x:CS exists y:FS [ x = y ]
OK, let me try to just guess the answers first off - based on
your intuitive descriptions above. (I can check out the game
based interpretation after this).
I'd say that (i) is true, (we can choose whatever we like,
even a finished sequence); and that (ii) is false, (there's
no reason to expect any fixed sequence can be attached to
our free choices).
That seems to be it for now.
Cheers, Bill.
Herman Jurjus
>> Let's first do an exercise for lesson 1.
>>
>> Recall that FS stands for fixed sequence, CS for `choice sequence'
>
> To interject briefly, not seriously - from your above description
> CS ought really to stand for "continuing sequence", (!),
> or even "continuable sequence", whereas FS might be
> "full sequence" or "finished sequence"
When contrasting choice sequences with fixed sequences, you're quite
right. Feel free to use those, for now.
I do think that the name choice sequences becomes more understandable
when we contrast it with 'recursive sequence'. But let's leave that for
later.
>> Let's use `x = y' as shorthand for `forall i [ x(i) = y(i) ]',
>> for any x,y for which the latter makes sense.
>>
>> Question: which of the following statements are true:
>>
>> forall x:FS exists y:CS [ x = y ]
>> forall x:CS exists y:FS [ x = y ]
>
> OK, let me try to just guess the answers first off - based on
> your intuitive descriptions above. (I can check out the game
> based interpretation after this).
>
> I'd say that (i) is true, (we can choose whatever we like,
> even a finished sequence); and that (ii) is false, (there's
> no reason to expect any fixed sequence can be attached to
> our free choices).
10 points out of 10.
Here follows the next lesson :-)
So we have
forall x:FS exists y:CS [ x = y ] (1) false
forall x:CS exists y:FS [ x = y ] (2) true
Now let us introduce another type or sort, called Cov.
When a player has to deliver a value for a variable of type Cov,
this means he has to deliver the entire sequence of all values
(i.e. an FS), but in an envelope, 'under cover', say, to
an impartial judge, who will consequently disclose the
individual values x(1), x(2), ... one at a time to the adversary
player.
In other words, an x of type Cov is like a fixed/full sequence that's
only partially known, and more and more 'knowledge' about it
is disclosed in the course of time, so to say. Is that the same as a
CS? Let's see:
Consider the following sentences:
forall x:FS exists y:Cov [ x = y ] (3)
forall x:Cov exists y:FS [ x = y ] (4)
The former is true, the latter false, so in that respect,
Cov seems similar to CS.
But now consider:
forall x:Cov exists y:CS [ x = y ] (5)
forall x:CS exists y:Cov [ x = y ] (6)
The former is true, but the latter is not.
Moreover, there's a difference between the following games:
forall x:CS exists y:FS [ x = y ] (repeating 2)
and
forall x:Cov exists y:FS [ x = y ] (repeating 4)
Both are false: they can't be won by proponent.
But in the former, opponent has a winning strategy, while in the
latter that's not the case, because proponent could (as a huge
coincidence) 'guess' the right sequence.
So it seems fair to say that the types Cov and CS are different.
You could say that in contrast with Cov, the 'crux' of the type
CS is not lack of knowledge but 'volatility': lack of determinateness.
===
Since this lesson has come out a bit short, let's include a bit more
'standard' stuff, too, in the same post:
We still haven't defined the semantics of 'and' and 'or'.
For now, let's do it as follows. Both conjunction and disjunction
denote games to be played in parallel. In the case of conjunction,
proponent needs to win both games to win the combined game,
in the case of disjunction proponent needs to win one of the games
to win the combined game.
Now consider the following two sentences:
forall x:CS [(forall i [x(i) = 0]) or (exists j [x(j) > 0])]
forall x:CS exists n
[(n = 0 and forall i [x(i) = 0]) or (n = 1 and exists j [x(j) > 0])]
The first will come out as true, since proponent can do the following:
Proponent waits until opponent has defined i. If opponent never gives
any value to i, then the game is won by proponent. If opponent does
mention i, then proponent defines j to have the same value as opponent
gave to i, and wins the game.
(Intuitionists will see issues with this, but let's leave that for later.)
On the other hand, the second sentence will come out as false,
because opponent can do the following:
Opponent starts to enumerate the sequence x as a sequence of 0s:
x(1) = 0, x(2) = 0, ... until proponent has mentioned a value for n.
If n = 1, opponent keeps doing this ad infinitum, and wins the game.
If n = 0, opponent continues with x(37) = 1, and wins the game.
We can now introduce 'constructive-or' as a shorthand:
p c-or q is defined as 'exists n [ (n=0 and p) or (n=1 and q) ]'
So that we have:
forall x:CS [(forall i [ x(i) = 0 ]) or (exists j [ x(j) > 0 ])]
: true
forall x:CS [(forall i [ x(i) = 0 ]) c-or (exists j [ x(j) > 0 ])]
: false
Question:
Which of the following do you think are true:
forall x:FS [(forall i [x(i) = 0]) or (exists j [x(j) > 0])]
forall x:FS [(forall i [x(i) = 0]) c-or (exists j [x(j) > 0])]
(The background of this question is that intuitionists will find the
type FS much more esoteric than CS. But more about that, later.)
Now let's discuss negation. We have left negation out of
our system, because we already have it, sort of.
With dialog-game semantics, there are at least two natural ways
to define negation. One is 'players-change-sides negation',
the other is 'De Morgan negation'.
The latter means that we define negation as a shorthand:
~forall x:<some type> [...] := exists x:<same type> [~(...)]
and similar for 'exists / forall',
~(p and q) = (~p or ~q)
and similar for 'or / and'.
Then, whenever the negations are defined at the lowest level,
for basic predicates, we're free to use the negation symbol.
In our system, we have De Morgan negation available,
because for example, '~(n = m)' is equivalent to something
like 'n < m or m > n'.
===
Everything still clear so far?
Exercise (to prepare for what is to follow) :
According to the semantics we have described up to now, would you say
the following sentence is true or false?
exists x:CS forall k exists n forall i>=n [x(i) = k] (7)
And this one?
exists x:FS forall k exists n forall i>=n [x(i) = k] (8)
(Note that we can write the last bit of the sentence as
... forall i[i<n or x(i) = k]
so we can take the liberty to write it this way.)
So far for this time.
(BTW, what we're doing so far is very close to Japaridze's Computability
Logic. But perhaps you already noticed that?)
--
Cheers,
Herman Jurjus
Herman Jurjus
> So we have
>
> forall x:FS exists y:CS [ x = y ] (1) false
> forall x:CS exists y:FS [ x = y ] (2) true
Euh... that should be the other way around, of course:
forall x:FS exists y:CS [ x = y ] (1) true
forall x:CS exists y:FS [ x = y ] (2) false
(The problem with these names is that they could also stand for 'free
(choice) sequence' and 'complete(d) sequence'. Argh, i should have used
other names.)
--
Cheers,
Herman Jurjus
Bill Taylor
but thought I'd just make a note now.
I answered your first question "by intuition", but now looking
back at your earlier game-play semantics for truth, I see
the answers were much more obvious.
> > Question: which of the following statements are true:
>
> > forall x:FS exists y:CS [ x = y ]
> > forall x:CS exists y:FS [ x = y ]
It's quite obvious on the game interpretation that
top is true and bottom is false.
Incidentally, that led me to think that the key difference
between FS and CS is that FS's are given "all at once",
within some fixed time for the whole sequence, so might
be called "Fast Sequences" - they come at you super fast,
in fact - and hence FS. :)
On this rendering CS's would be "slow sequences",
they only come as fast as you ask for terms, so to speak.
Maybe "Crawling Sequences" would fit the CS designation.
So there we are - Fast sequences and Crawlers.
I like this a lot. ;-)
-- Schoolboy Bill
Bill Taylor
game-theoretic semantics of a while ago. You wrote:
>>>>
Instead of the classical Tarski-semantics, we define
a -different semantics- for this language, as follows.
With every sentence, we associate a game with two players, a
proponent,
and an opponent, and we will call a sentence true if opponent can
'always win' the game, i.e. has a winning strategy. [This still leaves
numerous variations open; but that can be of later concern.]
The game takes place in a time frame t1, t2, ...
Opponent is responsible for the universally quantified variables,
proponent for the existential variables. The game is played by both
players providing concrete values for variables for which they are
responsible, at whatever time points they like (within the timeframe).
But for the various sorts, different rules apply:
If a player is responsible for a variable of sort N, his only
obligation
is that at some t_i, some (natural number) value is given by him.
<<<<
This doesn't look right to me. Specifically, where you say,
> call a sentence true if opponent can 'always win' the game,
Surely this should read,
"if the last player mentioned can always win the game."
e.g. the sentence (all m) (exist n) n>m is trivially true,
and the PROponent wins it, as he produces the n.
I hope this was just a trivial boo-boo, and not an important subtlety!
Can you just confirm my correction before we go on, please?
-- Worried William
P.S. Inserting dummy quantified variables at any point might
suggest a change, but has no effect on "truth", in fact.
Herman Jurjus
> Herman - I have a problem here, with the introduction of your
> game-theoretic semantics of a while ago. You wrote:
...
> This doesn't look right to me. Specifically, where you say,
>
>> call a sentence true if opponent can 'always win' the game,
O dear - that should be proponent, of course.
Sorry for the confusion.
--
Cheers,
Herman Jurjus
Bill Taylor
I think so.
> Exercise (to prepare for what is to follow) :
> According to the semantics we have described up to now, would you say
> the following sentence is true or false?
>
> exists x:CS forall k exists n forall i>=n [x(i) = k] (7)
>
> And this one?
> exists x:FS forall k exists n forall i>=n [x(i) = k] (8)
Well, either there's another typo, or these are really
trivial examples, or I'm completely missing the point.
Both of these seem to say, there is a sequence which
becomes ultimately constant on ANY value at all.
So they are both trivially false.
-- Wondering William
Herman Jurjus
In a sense, you're right. And even 'the' intuitionist agrees with you,
this time. However, the semantics i gave so far doesn't: it makes the
CS-version true. That's why i brought the example up; there's some
explaining to do.
Let's first see why (7) comes out as true with our semantics.
Proponent can do the following: start mentioning x(1) = 0, x(2), ...
until opponent mentions k; say k = 4. Suppose x(37) = 0 is the last
value mentioned by proponent at that moment. Then proponent continues
x(38) = 4, x(39) = 4, ... and puts n = 38.
So it appears that the sentence
exists x:CS forall k exists n forall i>=n [x(i) = k]
is true in our semantics; but it also seems rather grotesque
(also in intuitionists' ears, as said).
Let me try to explain how one could view the situation.
Suppose we wanted to change our semantics so that this
sentence should come out as false. What could we do?
In other variants of dialog/game semantics players are
sometimes allowed to 'change their minds' about earlier moves.
But this doesn't help us in our case.
(Let's say proponent behaves as before: he starts x(1) = 0, x(2), ...
until opponent mentions k; say k = 4, and x(37) = 0 is the last value
mentioned by proponent at that moment; proponent continues
x(38) = 4, x(39) = 4, ... and n = 38.
Now if opponent changes k to 5, and at that moment, say,
x(45) = 4 is mentioned last, proponent can continue
x(46) = 5, x(47) = 5, ... and change n to 46.
After all, the 'exists n' clause lies within the scope of the forall k
quantifier, so after a change of k it's only fair to let proponent
also change the value of n.)
So the usual idea of 'change of mind' is not enough, here.
What we could do, however, is to grant opponent the right to
request one or more -duplicate instances- of subgames.
For our example sentence, this means that opponent can
request one extra 'forall k' game, so that two forall k games
are played in parallel, and the game will then be lost for proponent,
as is easy to see.
This seems to correspond nicely with the argument that
immediately comes to mind in one way or another when we
try to articulate why we find sentence (7) so outrageous:
'there doesn't exist a sequence that has both a tail of 4s and
at the same time a tail of 5s'.
Next step:
But... if we grant -both- players the right to request duplicate games,
then our system will collapse to classical logic. Or at least,
constructive disjunction will become indistinguishable from
ordinary disjunction.
Think for example about the sentence
forall x:CS [ x = 0 c-or x # 0 ]
(Here we write x = 0 as shorthand for 'forall i [x(i) = 0]' and x # 0
for 'exists i [x(i) > 0]'.)
If proponent is allowed to request a duplicate for the c-or game,
proponent can suddenly win:
forall x:CS [ (x = 0 c-or x # 0) and (x = 0 c-or x# 0) ]
is true in our semantics.
(Sketch of the winning strategy: play 'double copy cat', claim x = 0 in
one game, and x # 0 in the other).
So roughly speaking we have the following options:
1) Accept that for choice sequences, a strange sentence like (7) is true
2) Accept that our system collapses to flat classical logic
3) Accept asymmetry between the two players
[With option 3) we mean: only opponent is granted the right to
request duplicate games.]
Because of historically grown language habits, intuitionists
talk as if they've chosen 3).
Although they reject (7), they could accept it in the following form:
exists x:CS ~(exists k) [~(x is stationary with eventual value k)] (8)
This could be read as:
i can give a sequence (produced consecutively, step-by-step),
so that at no moment of time you can give a k and
claim to know for sure that my sequence will satisfy
'x is not stationary with eventual value k'
Note three things, here:
A. Once one sacrifices the symmetry between the players,
the De Morgan negation will no longer coincide with 'players-change-
sides' negation. The '~' in sentence (8) is to be understood as
players-change-sides negation.
B. The difference between option 1) and 3) is superficial, namely only
a matter of language/syntax. The 'constructive contents' of (7)
is the same as that of (8), in the sense that they both express
the winnability of the same game.
C. And btw, sentence (7) is another example of something that's
valid for CS, but not for FS, nor for Cov.
===
So, are you still (or again) following me, so far?
--
Cheers,
Herman Jurjus
Herman Jurjus
[...]
> If proponent is allowed to request a duplicate for the c-or game,
> proponent can suddenly win:
> forall x:CS [ (x = 0 c-or x # 0) and (x = 0 c-or x# 0) ]
> is true in our semantics.
Correction; it should be:
forall x:CS [ (x = 0 c-or x # 0) or (x = 0 c-or x# 0) ]
With 'or' instead of 'and'.
--
Cheers,
Herman Jurjus
Bill Taylor
> >> According to the semantics we have described up to now,
> >> would you say the following sentence is true or false?
>
> >> exists x:CS forall k exists n forall i>=n [x(i) = k] (7)
> >> exists x:FS forall k exists n forall i>=n [x(i) = k] (8)
> > So they are both trivially false.
> In a sense, you're right. And even 'the' intuitionist agrees
(This remark seems to suggest that the "game semantics" is
NOT appropriate for Intuitionism, but let that go for now.)
> this time. However, the semantics i gave so far doesn't:
> it makes the CS-version true.
I do not see this at all!
And I am not convinced by your playing fast and loose with
the game interpretation - you never said anything earlier
about "playing games in succession" or "simultaneously",
which you now seem to be relying on in an essential way.
This habit of changing the interpretations, or extending them,
as one goes along, is one of the things that (as I noted earlier)
really grates on me that intuitionists seem to do a lot of.
Anyway, let's forget the games for the moment, and go back to (7),
which you seem to want to be true. If it is true, then there must
be a fault in this obvious-looking argument, so where is it?
** exists x:CS forall k exists n forall i>=n [x(i) = k]
(7)
implies (by specialization)
** exists x:CS such that exists n forall i>n [x(i) = 6]
: AND exists m forall i>m [x(i) = 7]
which implies
** exists x:CS such that exists k forall i>k [7 = x(i) = 6]
by taking the k = max(m,n) above.
This is false. So either you forbid specialization,
or you forbid something about the use of AND,
or you forbid the taking of the max of two naturals.
Which of these is it that you forbid, and can you
explain what is dodgy about it? Thanks!
No need to mention games.
-- Badly baffled Bill
Herman Jurjus
> I'm becoming unhappy!
I was already afraid i had muddied the water too much.
>>>> According to the semantics we have described up to now,
>>>> would you say the following sentence is true or false?
>>>> exists x:CS forall k exists n forall i>=n [x(i) = k] (7)
>>>> exists x:FS forall k exists n forall i>=n [x(i) = k] (8)
>
>>> So they are both trivially false.
>
>> In a sense, you're right. And even 'the' intuitionist agrees
>
> (This remark seems to suggest that the "game semantics" is
> NOT appropriate for Intuitionism, but let that go for now.)
That's why i brought this example up. As it stands, the game semantics
does indeed NOT directly represent how intuitionists reason about choice
sequences. It was a bit of a warning intermezzo, so to say.
Yet, i do think the system is strongly related to intuitionistic logic
and also to the way intuitionists talk and think about choice sequences,
but only after some extra explanations, which i gave in the sequel.
Apparently that sequel was not clear enough. I'll see if i can improve
on that, but it may take a few days.
>> this time. However, the semantics i gave so far doesn't:
>> it makes the CS-version true.
>
> I do not see this at all!
>
> And I am not convinced by your playing fast and loose with
> the game interpretation - you never said anything earlier
> about "playing games in succession" or "simultaneously",
> which you now seem to be relying on in an essential way.
Before, i didn't mention playing games in succession, because i wasn't
thinking of the games as 'to be played in succession'. The moves (all
moves) were all thought to be made in one time frame t1, t2, t3, ... And
they still are.
> This habit of changing the interpretations, or extending them,
> as one goes along, is one of the things that (as I noted earlier)
> really grates on me that intuitionists seem to do a lot of.
What i intended to do was to start with a simple system and then lead
you in a number of steps to one, more extensive system. Perhaps i should
have given you the large chunk in one post. The reason i didn't was
that, imo, the simple system should be more than enough to:
1) make the notion of choice sequence clear
2) give enough 'hooks' to discuss constructivism/intuitionism
> Anyway, let's forget the games for the moment, and go back to (7),
> which you seem to want to be true.
Let's keep the game semantics in for a moment.
Where do you see a mistake with what i said:
Proponent can do the following: start mentioning x(1) = 0, x(2), ...
until opponent mentions k; say k = 4. Suppose x(37) = 0 is the last
value mentioned by proponent at that moment. Then proponent continues
x(38) = 4, x(39) = 4, ... and puts n = 38.
Do you disagree that, -with- the game semantics, this game is won for
proponent?
> If it is true, then there must
> be a fault in this obvious-looking argument, so where is it?
>
> ** exists x:CS forall k exists n forall i>=n [x(i) = k]
> (7)
>
> implies (by specialization)
>
> ** exists x:CS such that exists n forall i>n [x(i) = 6]
> : AND exists m forall i>m [x(i) = 7]
>
> which implies
>
> ** exists x:CS such that exists k forall i>k [7 = x(i) = 6]
>
> by taking the k = max(m,n) above.
>
>
> This is false. So either you forbid specialization,
I'm not sure about this, but i think that the game semantics makes
specialization true, but 'only once'.
BTW Do you know linear logic? Or computability logic?
(And did you read the sequel of my post? Because that explained how one
can make a variant of the game-semantics in which your argument does go
through.)
> or you forbid something about the use of AND,
> or you forbid the taking of the max of two naturals.
>
> Which of these is it that you forbid, and can you
> explain what is dodgy about it? Thanks!
>
> No need to mention games.
Yes there is. Because outside the game semantics, i don't make any claim
about (7) being true. [And btw, i think this is the crucial remark in
the entire discussion.]
As a more general remark (perhaps it helps clear the air):
Semantics is leading, here. There are no rules of logic (here) other
than 'observations after the fact'.
--
Cheers,
Herman Jurjus
Herman Jurjus
> Bill Taylor wrote:
>> I'm becoming unhappy!
[...]
> Apparently that sequel was not clear enough. I'll see if i can improve
> on that, but it may take a few days.
After rereading my post and your reply to it, i think it's better not to
make a second attempt, but instead to ask: did you even bother to read
the entire post?
--
Cheers,
Herman Jurjus
Bill Taylor
> >>> So they are both trivially false.
> >> In a sense, you're right.
> >> And even 'the' intuitionist agrees
> As it stands, the game semantics
> does indeed NOT directly represent how intuitionists
> reason about choice sequences.
Oh. But wasn't that what you were trying to get across?
> It was a bit of a warning intermezzo,
Well, it seems a very roundabout way of doing things,
but no doubt you know what you're doing. But am I to
gather that this game-theory semantics is NOT
what I am to finally understand?
>> & I am not convinced by your playing fast & loose with
>> the game interpretation - you never said anything
>> earlier about "playing games in succession" or
>> "simultaneously", which you now seem to be
> relying on in an essential way.
>
> Before, i didn't mention playing games in succession,
> because i wasn't
> thinking of the games as 'to be played in succession'.
Hmmm. But you raised the matter yourself.
I'm well confused here.
> have given you the large chunk in one post.
> The reason i didn't was
> that, imo, the simple system should be
> more than enough to:
> 1) make the notion of choice sequence clear
> 2) give enough 'hooks' to discuss
> constructivism/intuitionism
Well it's certainly given me enough things
to get confused about.
> Let's keep the game semantics in for a moment.
> Where do you see a mistake with what i said:
>
> Proponent can do the following:
> start mentioning x(1) = 0, x(2), ...
> until opponent mentions k; say k = 4.
> ... Then proponent continues
> x(38) = 4, x(39) = 4, ... and puts n = 38.
>
> Do you disagree that, -with- the game semantics,
> this game is won for proponent?
Yes, I'm entirely happy with that; and this seems to
happily prove the statement...
(exist x:CS)(exist n) (all i>n) x(i) = 4 .
But you are about to go on to generalize "4", to make
(exist x:CS)(all m)(exist n)(all i>n) x(i) = m
and I don't see how you're going to do that under game
or any other semantics; when all you get AFAICS is
(all m)(exist x:CS)(exist n)(all i>n) x(i) = m .
Obviously I'm missing some subtle point here. What?
> BTW Do you know linear logic?
Only vaguely. Isn't that "limited resources" logic?
> Or computability logic?
No. Is that much the same?
> (And did you read the sequel of my post?
Yes; but I want to take things one at a time, because,
(like all students), if I get lost early on, I'd better
untangle it or else I'll have no chance with the later
bits. If you're getting frustrated, we could always take
this to private email. I doubt anyone else is reading
along all that amount.
> Semantics is leading, here. There are no rules of logic
> (here) other than 'observations after the fact'.
I'm not sure what you mean by this. Surely we are
still heading toward a place where we will eventually
be using a formal system? Or does that not fully
exist for intuitionism?
-- Wildly whirling William
Herman Jurjus
> Herman Jurjus <hjm...@hetnet.nl> wrote:
>
>>>>> So they are both trivially false.
>>>> In a sense, you're right.
>>>> And even 'the' intuitionist agrees
>
>> As it stands, the game semantics
>> does indeed NOT directly represent how intuitionists
>> reason about choice sequences.
>
> Oh. But wasn't that what you were trying to get across?
Yes, and i still am on track, i thought.
Did you really -read- the 2 December post?
>> It was a bit of a warning intermezzo,
>
> Well, it seems a very roundabout way of doing things,
> but no doubt you know what you're doing. But am I to
> gather that this game-theory semantics is NOT
> what I am to finally understand?
Yes it is. Did you really -read- the 2 December post?
>>> & I am not convinced by your playing fast & loose with
>>> the game interpretation - you never said anything
>>> earlier about "playing games in succession" or
>>> "simultaneously", which you now seem to be
>> relying on in an essential way.
>>
>> Before, i didn't mention playing games in succession,
>> because i wasn't
>> thinking of the games as 'to be played in succession'.
>
> Hmmm. But you raised the matter yourself.
No i didn't. Didn't intend to, anyway.
> I'm well confused here.
Let me repeat what you snipped:
The moves (all moves) were all thought to be made in one time frame t1,
t2, t3, ... And they still are.
We only extend the game semantics by allowing the players to make more
moves than just supplying values for variables. We also allow them to
request duplicate instances for subgames. That is: making such a request
is considered a move in the game, that has to be done at some timepoint
in the frame t1, t2, t3, ... I assumed that that was immediately clear
from what i wrote, but apparently not.
For example:
In (the game for) a sentence that starts with:
exists x:CS forall k [...]
the following could happen:
- at t=17, opponent makes the move: 'i request an instance of the
forall k game, with k = 4'
- at t=18, opponent makes the move: 'i request an instance of the
forall k game, with k = 5'
Since the sequence x is being made step by step, in the course of time,
these two games will then 'in effect' be played 'in parallel'.
Another thing we didn't mention yet: we allow the players to make any
number of moves, at any timepoint within the frame t1, t2, ...
In particular, it's ok if opponent and proponent each make a move at,
say, t=17. (We could adopt other conventions, too, but that wouldn't
make much difference.)
>> have given you the large chunk in one post.
>> The reason i didn't was
>> that, imo, the simple system should be
>> more than enough to:
>> 1) make the notion of choice sequence clear
>> 2) give enough 'hooks' to discuss
>> constructivism/intuitionism
>
> Well it's certainly given me enough things
> to get confused about.
Don't despair - when your confusion will be overcome, you'll be a wiser
and richer man.
>> Let's keep the game semantics in for a moment.
>> Where do you see a mistake with what i said:
>>
>> Proponent can do the following:
>> start mentioning x(1) = 0, x(2), ...
>> until opponent mentions k; say k = 4.
>> ... Then proponent continues
>> x(38) = 4, x(39) = 4, ... and puts n = 38.
>>
>> Do you disagree that, -with- the game semantics,
>> this game is won for proponent?
>
> Yes, I'm entirely happy with that;
Stop - hold - wait. Good.
Now: do you agree that -with the game semantics given so far-, the
sentence translates into the above game? And that hence with this
semantics, the sentence is by definition true -for that semantics-?
> and this seems to
> happily prove the statement...
>
> (exist x:CS)(exist n) (all i>n) x(i) = 4 .
>
> But you are about to go on to generalize "4", to make
>
> (exist x:CS)(all m)(exist n)(all i>n) x(i) = m
>
> and I don't see how you're going to do that under game
> or any other semantics; when all you get AFAICS is
>
> (all m)(exist x:CS)(exist n)(all i>n) x(i) = m .
>
> Obviously I'm missing some subtle point here. What?
What you fail to do is: use the game semantics to evaluate the sentences.
Instead, you intuitively grasp the situation, and use your usual,
classical language habits to formulate it into sentences.
What i'm asking you to do instead (and what so far i thought you could
follow), is to -evaluate- or -interpret- sentences in a different way:
by translating the sentence to a game, and call the sentence true iff
that game is winnable. (And to attach no further meaning to it.)
Note: i'm not asking you to -consider- the (classical interpretation of
the) sentence true, but to -call- the sentence true -in our semantics-,
which is reasonable, because it is true in our semantics. That fact
-means- no more than that the game is winnable.
And you already said you understood that that game was winnable, right?
So where's the problem?
Now you might wonder why i use the standard notations forall / exists,
when the result is so weird?
My reply:
1) Read the rest of the 2 Dec post more carefully.
2) Please observe that if you apply the game semantics to the fragment
(N, FS), everything behaves as usual.
It's by introducing the type CS that suddenly some connectives and
quantifiers become 'ambiguous' - in the sense that there become several
possible (and natural) 'game-like implementations' available.
>> (And did you read the sequel of my post?
>
> Yes; but I want to take things one at a time, because,
> (like all students), if I get lost early on, I'd better
> untangle it or else I'll have no chance with the later
> bits.
The sequel already addressed your concern, imo.
At least, it was certainly not a 'later bit'. Once you've digested that
entire post, i think your puzzlement will be over.
I'll send one more post that perhaps helps.
>> Semantics is leading, here. There are no rules of logic
>> (here) other than 'observations after the fact'.
>
> I'm not sure what you mean by this.
What i mean with that is: i ask you to evaluate sentences according to
the game-semantics, and attach no other meaning to the sentences.
[Just in case you don't realize it yet: there's no a priori reason to
think that any semantics will satisfy any of the properties that FOL
has. Even for Tarski semantics, it had to be proven.]
Perhaps it eases your mind if i say (once more) that on the (N, FS)
fragment, our semantics is the same, good old, classical semantics.
> Surely we are
> still heading toward a place where we will eventually
> be using a formal system?
We already have a formal system.
We have described (admittedly a bit sketchily) a semantics for a formal
language. This semantics can be fully worked out in terms of ZFC, or
whatever you like.
> Or does that not fully
> exist for intuitionism?
I hope i don't sound too patronizing, but imo -that- is a 'later bit'.
--
Cheers,
Herman Jurjus
Herman Jurjus
>>> As it stands, the game semantics
>>> does indeed NOT directly represent how intuitionists
>>> reason about choice sequences.
>>
>> Oh. But wasn't that what you were trying to get across?
>>> It was a bit of a warning intermezzo,
>>
>> Well, it seems a very roundabout way of doing things,
>> but no doubt you know what you're doing. But am I to
>> gather that this game-theory semantics is NOT
>> what I am to finally understand?
And a few lines later:
> I'll send one more post that perhaps helps.
Perhaps it's good idea to give a description (partially recap) of the
system(s) that i'm trying to communicate.
We have just three languages, and one semantics.
Two of these languages translate into the third, one as a
fragment-embedding and one is just syntactic reformulation.
To put it a bit quickly, these languages are:
A) forall, c-forall, exists, c-exists, and, c-and, or, c-or, neg
B) forall, exists, and, or, (c-or, neg = DeMorgan negation)
C) forall, exists, and, or, neg
Language B) is the language we used so far, C) describes
the constructivistic language habits.
We have a translation from B) to A) and one from C) to A),
the map from C) to A) being 'only syntactic sugar'.
The translation from B) to A) is as follows:
- 'forall' maps to 'c-forall'
- 'exists' maps to 'c-exists'
- 'and' maps to 'and'
- 'or' maps to 'or'
- 'c-or' maps to 'c-or'
- neg: resolve as DeMorgan negation first, then apply the mapping above
The translation from C) to A) is as follows:
- 'forall' maps to 'forall'
- 'exists' maps to 'c-exists'
- 'and' maps to 'and'
- 'or' maps to 'c-or'
- 'neg' maps to 'neg'
The semantics for language A) is as follows (again just a sketch):
- 'forall' : opponent gives value(s); requests of duplicate
game-instances allowed
- 'exists' : proponent ... idem
- 'c-forall' : opponent gives value(s); no duplicates allowed
- 'c-exists' : proponent ... idem
- 'and', 'or': games are played in parallel
- 'p c-or q' is short for 'c-exists n[(n=0 and p) or (n=1 and q)]
- 'p c-and q' is short for 'neg( neg(p) c-or neg(q))'
- 'neg': players change sides
(Example follows, further below.)
BTW, we also have a second, different translation from C) to A):
- 'forall' maps to 'forall'
- 'exists' maps to 'exists'
- 'and' maps to 'and'
- 'or' maps to 'or'
- 'neg' maps to 'neg'
(Simple embedding, hence.)
With this translation, you 'get' classical logic.
You also 'get' classical logic if you restrict to the (N, FS) fragment,
because in that fragment there's no difference between or and c-or,
exists and c-exists, etc.
To get back to our example:
The sentence
exists x:CS forall k exists n forall i>=n [x(i) = k]
(from language B)
translates in system A) as:
c-exists x:CS c-forall k c-exists n c-forall i>=n [x(i) = k]
and that corresponds in language C) to:
exists x:CS ~exists k ~exists n ~exists i>=n ~[x(i) = k)]
The game that is claimed to be winnable in each of these cases is the same.
So although, in this case, the B) sentence is not -directly- what
intuitionists accept, there exists a sentence in intuitionistic language
that 'expresses the same reality' - i.e. that makes the same claim.
That's why i think the B) system is still quite appropriate for our
purposes: explaining choice sequences to classical minds.
(Explaining the intuitionistic language habits is a different challenge.)
What i'd hoped was that i could mention this just once, as an
intermezzo, and continue with my story, keeping these two issues apart:
explaining choice sequences, and explaining the intuitionistic language
habits.
Especially since the full system A) is more complex to elaborate
completely and formally, with all these duplicate instances of games
that can be run in parallel.
I hope this clearifies things a bit?
--
Cheers,
Herman Jurjus
Herman Jurjus
> We have just three languages, and one semantics.
> Two of these languages translate into the third, one as a
> fragment-embedding and one is just syntactic reformulation.
That's as clear as porridge. Let me try again:
We have just three languages, and one semantics.
Two of these languages translate into the third.
One translation is a fragment-embedding and the other translation is
just syntactic reformulation.
--
Cheers,
Herman Jurjus
Herman Jurjus
> Herman Jurjus <hjm...@hetnet.nl> wrote:
>> BTW Do you know linear logic?
>
> Only vaguely. Isn't that "limited resources" logic?
>
>> Or computability logic?
>
> No. Is that much the same?
Both logics, but especially the latter one, are strongly related to game
semantics. With such semantics, the usual connectives and quantifiers
tend to 'split up' in numerous variations, and the logics you end up
with are rather weak, but also more weird and more complex and therefore
a lot of fun.
When you indicated you felt comfortable with my game-speak i (mis)took
that as a sign that you not only knew about these logics, but were
familiar and comfortable with them.
Our recent communication glitch could very well have been caused by that
misunderstanding.
I also have the impression that most of the issues you had/have with the
2 December post have very little to do with choice sequences or
constructivism/intuitionism as such, but more with a lack of
appreciation for the game-semantics's way of doing logic (or at least
for the flavour i had in mind).
Perhaps it's good if you first get yourself acquainted more with
Japaridze's Computability logic. And now that i've begun to sound like a
pedantic teacher anyway: you could start with some publications, here:
http://www.csc.villanova.edu/~japaridz/study.html
--
Cheers,
Herman Jurjus
Keith Ramsay
|Let's first see why (7) comes out as true with our semantics.
|Proponent can do the following: start mentioning x(1) = 0, x(2), ...
|until opponent mentions k; say k = 4. Suppose x(37) = 0 is the last
|value mentioned by proponent at that moment. Then proponent continues
|x(38) = 4, x(39) = 4, ... and puts n = 38.
|
|So it appears that the sentence
| exists x:CS forall k exists n forall i>=n [x(i) = k]
|is true in our semantics; but it also seems rather grotesque
|(also in intuitionists' ears, as said).
I suspect that the semantics would come closer to the
intended semantics (by Brouwer) if you required that the
choice sequence be generated by an ally who is given
access to the allies (of either player) who are generating
choice sequences that have already been started, to
query terms of their sequences.
Keith Ramsay
Herman Jurjus
Something like that was what i already had in mind.
But... how would that help in the above sample sentence?
Allowing the k-player to play two k-games in parallel also does the
trick, btw.
--
Cheers,
Herman Jurjus
Bill Taylor
I can now return to the schoolroom!
I have re-read the whole thread, (excluding the very last post on
the three different languages), and think I am now somewhat
on top of things, with a new terminology I have come up with,
for my own convenience.
But before I go on, I would like once again, to re-state my
standard RANT here, which Keith Ramsay, Darryl McCullough,
and others have chided me for, but which I stick to anyway.
So if you, they, or anyone else, (assuming there IS anyone else!),
wishes to, please just whoosh past this next section.
RANT BEGINS___________________
I rant about the constructivist's hi-jacking of standard
math-language terms to use in their own interpretation,
rather than coming up with new ones of their own!
It is EXTREMELY confusing to have standard words like "truth",
"proof", "there exists", "not" (even!), "sequence" and many
others, have two quite different meanings depending on context.
Now OC math is full of words and symbols that have somewhat
different meanings according to context. But this is different,
(m'lud, I must distinguish!) In the constructive case I get
the very strong feeling that it is done not for convenience,
but specifically FOR PROSELYTIZATION. And if that is so, it is
a very sneaky thing indeed. They try (I suspect) to ensnare
unsuspecting innocents into accepting their own ideas under
the umbrella of ordinary mathematical thinking; or something
like that. Now it is frequently replied, that no-one has
a right to exclusive use/definition of everyday words,
and that their right is just as good as the orthodox mathie.
BUT THIS IS NOT SO! The orthodox have "first dibs" on these
disputed terms, from Frege, Cantor, Hilbert, Russell and
others in late C19 to early C20, specifically for the orthodox
("existential") PoV. The specifically constructive interpretations
came noticeably later, beginning about 1920. Therefore, I assert,
(uselessly, OC!), that it is up to the those of a constructive
("algorithmic") bent, to find new ones. After all, they HAVE
done so in some cases, to great effect - for example the phrase
"inhabited set" is a beauty!
_________________________________RANT ENDS
Well, now that I've had my bleating whinge, and turned off
most of my intended audience, I will continue with the choice
sequence material.
I said I had a new viewpoint on it, and there are two aspects
to this, dealing with things that have hindered my understanding,
(specifically because of that bleat topic!)
_______________
a) The first is, that it now seems to me, that we should NOT be
speaking of "choice sequences" at all! - but of "SEQUENCE SYSTEMS".
That is, a whole system of *generating* a sequence. This highlights
the system itself, rather than an actual sequence, which may never
exist at all in its entirety, as we see with choice sequence
systems. So an ordinary (fixed) sequence comes with a very
boring "system", which basically amounts to just a definition,
typed and presented in the usual undergrad way. One might
also be able to speak of *random* sequence systems, for those
who want to do so, as some intuitionists in the past have done.
And mostly, here, we will be speaking of "free choice systems",
which can have all the game-theoretic or other properties
that Herman and/or other inties want!
And it meshes very well with one of Herman's earlier remarks...
> You could say that in contrast with Cov, the 'crux' of the type CS
> is not lack of knowledge but 'volatility': lack of determinateness
If we understand that we are dealing with sequence SYSTEMS,
rather than mere sequences, then there is no longer much problem.
With this new terminology, I hope everyone would be satisfied.
It certainly makes a lot more sense to me, anyway!!
_____________________________________________________end of (a)
b) The second of our changes is much more minor, and indeed
hardly a terminology change at all.
It involves a conflation that often causes ruptures in English
(natural language) interpretations of things - the difference
between "ANY" and "ALL". (!)
For negative statements, they are clearly distinct:-
NOT ALL of the students will pass. (some fail)
vs NOT ANY of the students will pass. (all fail)
For interogative sentences it is also the case:-
Will ALL of the students pass? (extreme optimism)
Will ANY of the students pass? (extreme pessimism)
But for positive declarative sentences they may co-incide:-
ANY of the students can pass, if they work hard.
ALL of the students can pass, if they work hard.
No doubt all this is old hat to linguistic philosophers and old
grammarians, and there are doubtless exceptional cases
either way. (Indeed I use one below!)
However, this is, I suggest, at the root of my problems with
Herman's "funny sentence", that we have spent so much time on.
______________________end of (b)
So here it is again:-
## exists x:CS forall k exists n forall i>=n [x(i) = k] (7)
> Let's first see why (7) comes out as true with our semantics.
Yes, now I have no problem at all with your game semantics.
I had no problem before; but I kept getting my wheels stuck,
because of the (IMHO) bad usage of the terms, that co-opting
of orthodox terms as in my rant. But now all is clear.
With a *choice sequence system*, it is quite clear that the above
is true, on the game-semantics that Herman gave so clearly.
And it clears up the last tincture of unhappiness,
if we use the quantifier language I suggested...
## exists x:CSS for ANY k exists n forall i>=n [x(i) = k] (7A)
Now it is as plain as day that I can use my free-choice system
to counter ANY k the opponent might put up; as long as
I don't have to be able to counter EVERY k he might put up,
all simultaneously. The simultaneity seems to make the difference,
here. As with the following (exceptional) case:-
I can beat up anyone in the class!
I can beat up everyone in the class!
The latter clearly doesn't follow from the former,
if simultaneity is required in "all".
So, I think I might be happier now. I wonder if we might keep
these two linguistic conventions in mind, a & b, as we go on?
............
> So, are you still (or again) following me, so far?
I hope so. I haven't commented on many other details,
as this post is already too long!
> Semantics is leading, here. There are no rules of logic (here)
> other than 'observations after the fact'.
I think I understand this remark much better now, too.
SO; all in all, if you agree (more or less) with what I've said,
especially points a & b, then I can happily go on and read
the latest three-languages post, and you can prepare
the next lesson for your incredibly thick-headed student.
-- Bone-headed Bill
Herman Jurjus
> I have re-read the whole thread, (excluding the very last post on
> the three different languages), and think I am now somewhat
> on top of things, with a new terminology I have come up with,
> for my own convenience.
>
> But before I go on, I would like once again, to re-state my
> standard RANT here, which Keith Ramsay, Darryl McCullough,
> and others have chided me for, but which I stick to anyway.
Oh, i will not chide you for that.
Some of my best friends are of the same opinions.
Your rant has been noted, and we may get back to it, later.
This is exactly the point, indeed.
What i don't understand is that you didn't pick that up from my story.
Because that's what i talked about: 'multiple instances of the forall-k
game'. Ok; apparently i have to work on my writing skills.
About point b): yup; you got it - that's it.
(I could expound on it a bit further, but that will perhaps
muddy the water too much.)
About point a), i'm not sure that i understand you.
I do have the impression that you're getting it, but
i've had that impression before, and were proven wrong
a number of times, so let me just tell you how i would
say it.
The notion of choice sequence is too subtle to be
represented by a mere set of elements. Therefore
the next best thing we can do is to create a system
that defines a meaning for (a large collection of)
sentences in which choice sequences occur (and to
expect no more, on the formal side). [1][2]
That said, for me, the notion of a choice sequence is
as directly intuitive and clear as the intuitive picture
of the sequence of natural numbers 0, 1, 2, ...
But the latter paragraph shows a level of 'disagreement of philosophy'
that we would probably also have if we both spoke about something
uncontroversial like 1 + 1 = 2.
So, by all means, do go ahead and read that three-language post...
Notes:
[1]That's why i called CS, Cov, etc. 'types' instead of sets,
and that's also what i meant when i said (right at the start)
that we were going to make an alternative semantics for a familiar
logical language, and that was the way to 'define' the notion
choice sequence for you: explain how you could reason about them.
[2]It's tempting to use the phrase 'non-standard semantics'
here, but it would be a lie. As said, for the fragment (N, FS),
our semantics is the -same- as the usual, classical one.
It's only when we introduce the type CS that some connectives and
quantifiers suddenly need disambiguation.
So perhaps it makes more sense to call our system a -generalization-
of the standard semantics, a bit in the way that category theory can be
seen as a generalization of set theory.
--
Cheers,
Herman Jurjus
Herman Jurjus
> Bill Taylor wrote:
>> b) The second of our changes is much more minor, and indeed
>> hardly a terminology change at all.
>>
>> It involves a conflation that often causes ruptures in English
>> (natural language) interpretations of things - the difference
>> between "ANY" and "ALL". (!)
>>
>> For negative statements, they are clearly distinct:-
>>
>> NOT ALL of the students will pass. (some fail)
>> vs NOT ANY of the students will pass. (all fail)
>>
>> For interogative sentences it is also the case:-
>>
>> Will ALL of the students pass? (extreme optimism)
>> Will ANY of the students pass? (extreme pessimism)
>>
>> But for positive declarative sentences they may co-incide:-
>>
>> ANY of the students can pass, if they work hard.
>> ALL of the students can pass, if they work hard.
>>
>> No doubt all this is old hat to linguistic philosophers and old
>> grammarians, and there are doubtless exceptional cases
>> either way. (Indeed I use one below!)
>>
>> However, this is, I suggest, at the root of my problems with
>> Herman's "funny sentence", that we have spent so much time on.
>
> This is exactly the point, indeed.
> What i don't understand is that you didn't pick that up from my story.
> Because that's what i talked about: 'multiple instances of the forall-k
> game'. Ok; apparently i have to work on my writing skills.
[...]
> About point b): yup; you got it - that's it.
> (I could expound on it a bit further, but that will perhaps
> muddy the water too much.)
On second thoughts, i -must- expound on it.
Question: how would you reduce your 'forall' to game-speak?
(I.e. explain it in terms of players, moves, and winning conditions.
I think we both understand how to deal with 'for any'.)
--
Cheers,
Herman Jurjus
Bill Taylor
> On second thoughts, i -must- expound on it.
Often it hits one that way!
> Question: how would you reduce your 'forall' to game-speak?
Well, perhaps I'm being simple-minded, but it doesn't seem TOO
difficult.
If proponent claims "(exist x) (forall y) (exist z) Pxyz"
where x, y, z can be any stated types, and P is a finitely checkable
predicate (recursive), then for this statement to be true...
proponent must produce an x, then
opponent must produce any finite number of y's, then
for each one proponent must produce its own z, and
they both can check that Pxyz is true.
Now that I've written it, it seems blindingly obvious, in fact,
and I'm wondering why you asked me, so I'm pretty sure
I've overlooked some trivial point!
-- Basic Bill
Bill Taylor
OK, I'm still behind on the "three-languages" posting,
(it turns out I'm busier than I expected to be right now!), so this
response is somewhat out of order, but hey! - this is Usenet.
>> But before I go on, I would like once again, to re-state my
>> standard RANT here, which Keith Ramsay, Darryl McCullough,
>> and others have chided me for, but which I stick to anyway.
> Oh, i will not chide you for that.
Good-oh! It's nice to find someone from the dark side who
is sympathetic to this cause!
> Some of my best friends are of the same opinions.
But would you want your daughter to marry one?
....................
> This [ANY rather than ALL] is exactly the point, indeed.
Excellent. It seems we are in full agreement on one thing, then.
> i don't understand ... that you didn't pick that up from my story.
Stupidity, Herman, stupidity! Sometimes I wonder how I ever
managed to learn any math at all! And perhaps the ingrainedness
of orthodox (existential) thinking runs far deeper than we both
might have suspected. Maybe this is a point that proselytisers
such as yourself have still not fully taken on board?
It seems there is always massive trouble with this ingrainedness.
That's why I feel you(all) must take stronger steps to phrase
things in an existentially acceptable way; (while OC not warping
the essential nature of your content!) A heavy task.
> Ok; apparently i have to work on my writing skills.
Rather, your empathetic skills.
> About point b): yup; you got it - that's it.
Good-oh.
> (I could expound on it a bit further, but that will perhaps
> muddy the water too much.)
I hope my response to your followup on this was acceptable?
> About point a), i'm not sure that i understand you.
This all comes from my trying to see things in an "existential"
way. I see it my way, you yours, but we can still come to
an agreement, I'm sure, even though we use different language.
The existential (orthodox) view is a very "static" one, and
the intuitionist view is a very "dynamic" one. The very idea
of choice sequences is one of dynamic change, volatility, as
you put it earlier. I remain hopeful that it *can* be adequately
expressed in existential language. One of my math-phil friends
once observed that although he was extremely sympathetic to
constructivist views, he HAD to part company with them when
they insisted on an essential *temporality* in math. That things
could be true now when they weren't true 200 years ago.
He, and I, and most orthodox mathies, find this idea extremely
repulsive, philosophically speaking, even anti-mathematical;
but there is no reason (I hope) that this opposition in math
philosophy should lead to a failure of "operational" understanding.
That's why I'm persisting with trying to find out what choice
sequences "really are", when the temporality of existence is
spirited away, as it has been with traditional computability.
> The notion of choice sequence is too subtle to be
> represented by a mere set of elements.
Very much so! The dynamic aspect is being emphasized.
Your task is to expound it, and mine is to re-cast your
exposition into temporality-free language.
That is why I spoke of "sequence SYSTEMS". I envisage these
as being like black boxes, *which have a pre-ordained aspect*,
(as I recall maybe even you agreed to - repeating the same
operations from the start should give the same results);
but black boxes which MAY vary according to what input is
fed into them, as per your game semantics. This is very
similar to the standard idea of a function, where the same
input must give the same output every time, even though
the innards of the box are left unrestricted - maybe a formula,
maybe a machine, maybe a look-up table. But whereas standard
math stops there, intuitionist math goes on to extend the idea
to allowing the inputs to depend on the quantifiers in some way.
I don't see any irresolvable conflict here, do you?
> That said, for me, the notion of a choice sequence is
> as directly intuitive and clear as the intuitive picture
> of the sequence of natural numbers 0, 1, 2, ...
Certainly not to me, yet. And I doubt it will ever be clear
in the way it is to you. But there's no reson that it can't
become clear in an existential way, a black-box way, I hope.
So I must continue to beg your indulgence to let me keep talking
in existential terms, even if you think I'm missing the point -
I simply *cannot* bring myself to think of math in dynamic terms.
Other than modelling dynamism by static concepts, OC, as is
the case in the calculus of motion and in computability.
> the latter paragraph shows a level of 'disagreement of philosophy'
Indeed so, but as I said, it needn't be fatal.
> we would probably also have if we both spoke about something
> uncontroversial like 1 + 1 = 2.
If there *were* one (which I doubt), it would be more immediately
resolvable. Linguistic preferences seldom make any operational
differences. The minimal-constructivist has long since found
this to be the case.
So bye for now, till I've read the 3-language post again.
-- Beetling-off Bill
Herman Jurjus
> This all comes from my trying to see things in an "existential"
> way. I see it my way, you yours, but we can still come to
> an agreement, I'm sure, even though we use different language.
>
> The existential (orthodox) view is a very "static" one, and
> the intuitionist view is a very "dynamic" one. The very idea
> of choice sequences is one of dynamic change, volatility, as
> you put it earlier. I remain hopeful that it *can* be adequately
> expressed in existential language. One of my math-phil friends
> once observed that although he was extremely sympathetic to
> constructivist views, he HAD to part company with them when
> they insisted on an essential *temporality* in math. That things
> could be true now when they weren't true 200 years ago.
The latter is a philosophic view that we can both safely ignore (or
explicitly deny if you wish) in the entire discussion. It has nothing to
do with understanding choice sequences, as far as i'm concerned.
Surely you agree that the 'temporality' involved in choice sequences (as
we deal with them in our game semantics) is a totally different kind of
temporality?
I mean, when a certain sentence (game) is true (winnable), then that was
the case 200 year ago, too.
[Answer whenever you like, as usual.]
--
Cheers,
Herman Jurjus
Bill Taylor
> > they insisted on an essential *temporality* in math. That things
> > could be true now when they weren't true 200 years ago.
>
> The latter is a philosophic view that we can both safely ignore (or
> explicitly deny if you wish) in the entire discussion.
Indeed so. That was one of the main points in my own post.
> It has nothing to do with understanding choice sequences, as far as i'm concerned.
Quite so. I'm glad to hear it.
> Surely you agree that the 'temporality' involved in choice sequences (as
> we deal with them in our game semantics) is a totally different kind of
> temporality?
Yes; which is why I like to describe it in atemporal language,
such as "sequence systems". You have not objected to my sequence
systems nomenclature, not to my game-interpretation to the quantifier
(for all) as opposed to (for any), so I presume we are happy with
those.
> I mean, when a certain sentence (game) is true (winnable), then that was
> the case 200 year ago, too.
Indeed so! We seem to be of one mind in these matters.
I have caught up on the 3-language post, which seems all OK,
though clearly I will have to keep copies by my bedside and desk.
There's another linguistic re-interpretation I'd like to suggest,
however,
for those constructivists who like to keep their orthodox pupils
onside.
Just as we have agreed that (Ax) should be read "for ANY x"
rather than "for ALL x", I would like to suggest a similar thing for
(Ex).
It seems to mean "there exists such an x, and I know of a finite
method
to find one", or words to that effect. My suggestion is merely that
this
be read, "there is an explicit x". Seems ideal to me. The word
"explicit"
is used quite often, informally, in math, and this seems a good place
to give it some approach toward a formal appearance. I like it.
And as similar remarks apply to constructive disjunction, which is
in effect a special case of the above, I similarly suggest we read
p v q as "explicitly either p or q". Not quite such a nice
piece
of grammar, but equally short, and to the point.
So summarizing...
notation orthodox interp. constructive interp.
===========================================
p v q p OR q (or both) explicitly p OR q
p ^ q p AND q p AND q
(Ax) for all x for any x
(Ex) there exists an x there exists an explicit x
p => q ~p v q (still to come)
~p p is false (still to come)
p p is true there is a constructive
proof of p
I put the last one in just to complete the set (so far).
It may well be constructively unsound, but the orthodox
column emphasizes the idea that p iff "p" is true.
-- Watertight William
> [Answer whenever you like, as usual.]
Too kind, too kind.
As we seem to have caught up with each other again,
it must be time for the next lesson! :)
-- Breathless Bill
Herman Jurjus
> Herman Jurjus <hjur...@hetnet.nl> wrote:
>
>>> they insisted on an essential *temporality* in math. That things
>>> could be true now when they weren't true 200 years ago.
>> The latter is a philosophic view that we can both safely ignore (or
>> explicitly deny if you wish) in the entire discussion.
>
> Indeed so. That was one of the main points in my own post.
>
>> It has nothing to do with understanding choice sequences, as far as i'm concerned.
>
> Quite so. I'm glad to hear it.
>
>> Surely you agree that the 'temporality' involved in choice sequences (as
>> we deal with them in our game semantics) is a totally different kind of
>> temporality?
>
> Yes; which is why I like to describe it in atemporal language,
> such as "sequence systems".
May i ask how you envision this term 'sequence system' to be used?
As an alternative for what i call 'type' (CS, Cov, FS)?
Or as an alternative for what i call 'game'?
Or as an alternative for what i call 'game semantics' (=language + some
map from sentences to games).
Or even as an alternative for 'choice sequence', singular?
Perhaps you can give a few examples of sentences in which the term
'sequence system' occurs, as you'd like it to be used?
Personally, i prefer strong focus on the word 'game', which suggests
being both 'static' and 'dynamic' at the same time: the moves are made
against a certain time-frame, but the game as a whole is a fixed thing.
It also suggests some sort of 'interaction' going on, which i think is
the crucial term in this whole story.
> You have not objected to my sequence
> systems nomenclature, not to my game-interpretation to the quantifier
> (for all) as opposed to (for any), so I presume we are happy with
> those.
See my separate post on this (to be written and posted yet).
>> I mean, when a certain sentence (game) is true (winnable), then that was
>> the case 200 year ago, too.
>
> Indeed so! We seem to be of one mind in these matters.
>
> I have caught up on the 3-language post, which seems all OK,
> though clearly I will have to keep copies by my bedside and desk.
>
> There's another linguistic re-interpretation I'd like to suggest,
> however,
> for those constructivists who like to keep their orthodox pupils
> onside.
>
> Just as we have agreed that (Ax) should be read "for ANY x"
> rather than "for ALL x", I would like to suggest a similar thing for
> (Ex).
>
> It seems to mean "there exists such an x, and I know of a finite
> method
> to find one", or words to that effect.
If i take a look at my game semantics, i don't see anything that
remotely looks like 'and i know of a finite method to find one'.
Do you?
Also: for universal quantification, you have two variants (forall,
forany). But what is the second variant in the existential case?
> My suggestion is merely that
> this
> be read, "there is an explicit x". Seems ideal to me. The word
> "explicit"
> is used quite often, informally, in math, and this seems a good place
> to give it some approach toward a formal appearance. I like it.
As long as it's not meant as an alibi to bypass focus on the -underlying
game- of every sentence (and i have the impression that's what you do).
What we're doing is: every sentence is translated as a game. If you look
for nomenclature that will bury these games, we will soon be talking
past each other again, i fear.
> And as similar remarks apply to constructive disjunction, which is
> in effect a special case of the above, I similarly suggest we read
> p v q as "explicitly either p or q". Not quite such a nice
> piece
> of grammar, but equally short, and to the point.
>
> So summarizing...
>
> notation orthodox interp. constructive interp.
> ===========================================
> p v q p OR q (or both) explicitly p OR q
> p ^ q p AND q p AND q
> (Ax) for all x for any x
> (Ex) there exists an x there exists an explicit x
> p => q ~p v q (still to come)
> ~p p is false (still to come)
>
> p p is true there is a constructive
> proof of p
I miss a column for game-semantics interpretations, correct?
> I put the last one in just to complete the set (so far).
> It may well be constructively unsound, but the orthodox
> column emphasizes the idea that p iff "p" is true.
I don't see any relation between my game semantics and 'emphasis on
proof'. Do you?
> -- Watertight William
>
>> [Answer whenever you like, as usual.]
>
> Too kind, too kind.
>
> As we seem to have caught up with each other again,
> it must be time for the next lesson! :)
Almost there - just polishing some parts.
--
Cheers,
Herman Jurjus
Herman Jurjus
> On Dec 17, 10:30 pm, Herman Jurjus <hjur...@hetnet.nl> wrote:
>
>> On second thoughts, i -must- expound on it.
>
> Often it hits one that way!
>
>> Question: how would you reduce your 'forall' to game-speak?
>
> Well, perhaps I'm being simple-minded, but it doesn't seem TOO
> difficult.
>
> If proponent claims "(exist x) (forall y) (exist z) Pxyz"
> where x, y, z can be any stated types, and P is a finitely checkable
> predicate (recursive), then for this statement to be true...
>
> proponent must produce an x, then
> opponent must produce any finite number of y's, then
> for each one proponent must produce its own z, and
> they both can check that Pxyz is true.
Very good! Very clear 'game thinking'.
> Now that I've written it, it seems blindingly obvious, in fact,
> and I'm wondering why you asked me, so I'm pretty sure
> I've overlooked some trivial point!
Well, i can think of more variants than the two we now have.
1) If you have infinitely many classmates, and you have to beat them
all, you would't get away with taking on only finitely many of them,
would you?
Imo the 'true', full, classical, platonistic 'for -all-' allows the
y-player (i.e. opponent) to give -any- number of y's, even possibly
uncountably many, if wanted.
And the y-player can thus force proponent to play numerous different
instances of the y-z-subgame. (And proponent needs to win them all.)
2) There is also a variant in which the player is allowed to give only a
finite number of y's, but /per time-point/. So that later in the game he
can decide to start new instances of the y-z-subgame. (In total effect,
however, only countably many, because the time-axis of our games is
countable.)
So we now clearly see at least four variants of universal
quantification, that is: four more or less natural game-related
interpretations of universal quantification (namely your 'forall', your
'for any', and the above two). Agreed?
Also: it's quite easy to give sentences that show the differences
between all of them.
(Perhaps this makes another nice exercise?)
--
Cheers,
Herman Jurjus
Bill Taylor
> May i ask how you envision this term 'sequence system' to be used?
> As an alternative for what i call 'type' (CS, Cov, FS)?
> Or even as an alternative for 'choice sequence', singular?
It can be used in either of these contexts, in exactly the same way
that you use "Choice Sequence". i.e. we can either speak of
an individual Sequence System, or of the type "Sequence System".
> Perhaps you can give a few examples of sentences in which the term
> 'sequence system' occurs, as you'd like it to be used?
A: A Fixed Sequence is a Sequence System of a particularly simple
kind.
And in particular, the Fibonacci sequence is a very simple
example
of a Fixed Sequence, and thus of a Sequence System.
B: (exists) x:SS (any k) (exists t) u>t => x(u) = k
B is just your "funny sentence" again, (this time with the proper
"any" used).
By using the term "SS" though, we emphasise that the sequence
is not given "all at once" and "in advance". OK?
> If i take a look at my game semantics, i don't see anything that
> remotely looks like 'and i know of a finite method to find one'.
> Do you?
No, of course not, I was just trying to tie together the game
semantics
intuitionism with the traditional sort, as much as possible.
> > My suggestion is merely that this be read,
> > "there is an explicit x". Seems ideal to me. The word "explicit"
> > is used quite often, informally, in math, and this seems a good place
> > to give it some approach toward a formal appearance. I like it.
>
> As long as it's not meant as an alibi to bypass focus on the -underlying
> game- of every sentence (and i have the impression that's what you do).
No, I'm not aware of trying to bypass anything; just keeping the
various
types of intuitionism tied together as closely as may be.
> What we're doing is: every sentence is translated as a game. If you look
> for nomenclature that will bury these games, we will soon be talking
> past each other again, i fear.
So no, I'm keeping two parallel (and possibly incompatible) systems
running in parallel, as far as may be.
> > So summarizing...
>
> > notation orthodox interp. constructive interp.
> > ===========================================
> > p v q p OR q (or both) explicitly p OR q
> > p ^ q p AND q p AND q
> > (Ax) for all x for any x
> > (Ex) there exists an x there exists an explicit x
> > p => q ~p v q (still to come)
> > ~p p is false (still to come)
>
> > p p is true there is a constructive
> > proof of p
>
> I miss a column for game-semantics interpretations, correct?
Correct. Good point!
Maybe it would be best if YOU were to fill it in?
> I don't see any relation between my game semantics and 'emphasis on
> proof'. Do you?
As above.
> > As we seem to have caught up with each other again,
> > it must be time for the next lesson! :)
>
> Almost there - just polishing some parts.
Excellent!
-- Bill
Herman Jurjus
> On Dec 20, 4:37 am, Herman Jurjus <hjur...@hetnet.nl> wrote:
>
>> May i ask how you envision this term 'sequence system' to be used?
>> As an alternative for what i call 'type' (CS, Cov, FS)?
>> Or even as an alternative for 'choice sequence', singular?
>
> It can be used in either of these contexts, in exactly the same way
> that you use "Choice Sequence". i.e. we can either speak of
> an individual Sequence System, or of the type "Sequence System".
>
>> Perhaps you can give a few examples of sentences in which the term
>> 'sequence system' occurs, as you'd like it to be used?
>
> A: A Fixed Sequence is a Sequence System of a particularly simple
> kind.
> And in particular, the Fibonacci sequence is a very simple
> example
> of a Fixed Sequence, and thus of a Sequence System.
>
> B: (exists) x:SS (any k) (exists t) u>t => x(u) = k
>
> B is just your "funny sentence" again, (this time with the proper
> "any" used).
Ok, i think i now understand what you want.
May i suggest the term 'sequence process' instead? Or even 'sequential
process'?
> By using the term "SS" though, we emphasise that the sequence
> is not given "all at once" and "in advance". OK?
>
>> If i take a look at my game semantics, i don't see anything that
>> remotely looks like 'and i know of a finite method to find one'.
>> Do you?
>
> No, of course not, I was just trying to tie together the game
> semantics
> intuitionism with the traditional sort, as much as possible.
That's what i was afraid of. Just fyi, imo, the connection between 'my'
system and constructivism is somewhere else than where i see you look.
You're of course free to do whatever you like, but i would advice
against this 'tying together' in this case, as it will probably
-increase- your confusion. (Without intending to offend you: it's a bit
like WM who keeps mixing -his- preconceptions about mathematics with
modern mathematics, and then ends up hopelessly confused about the
status of the latter.)
>>> My suggestion is merely that this be read,
>>> "there is an explicit x". Seems ideal to me. The word "explicit"
>>> is used quite often, informally, in math, and this seems a good place
>>> to give it some approach toward a formal appearance. I like it.
>> As long as it's not meant as an alibi to bypass focus on the -underlying
>> game- of every sentence (and i have the impression that's what you do).
>
> No, I'm not aware of trying to bypass anything; just keeping the
> various
> types of intuitionism tied together as closely as may be.
The way you tie them up shows me that you're looking in the wrong
direction. (I will try to convince you of that, in the posts to come.)
To put it more generally: it's ok that you try to rephrase everything in
your own words: it creates a feedback loop. So, please keep doing that.
But, when i don't immediately respond to something, please bear in mind
that that doesn't indicate agreement. I'd like to preserve the right to
get back to anything you say, in a later stage.
>> What we're doing is: every sentence is translated as a game. If you look
>> for nomenclature that will bury these games, we will soon be talking
>> past each other again, i fear.
>
> So no, I'm keeping two parallel (and possibly incompatible) systems
> running in parallel, as far as may be.
>
>>> So summarizing...
>>> notation orthodox interp. constructive interp.
>>> ===========================================
>>> p v q p OR q (or both) explicitly p OR q
>>> p ^ q p AND q p AND q
>>> (Ax) for all x for any x
>>> (Ex) there exists an x there exists an explicit x
>>> p => q ~p v q (still to come)
>>> ~p p is false (still to come)
>>> p p is true there is a constructive
>>> proof of p
>> I miss a column for game-semantics interpretations, correct?
>
> Correct. Good point!
> Maybe it would be best if YOU were to fill it in?
Well, one crucial point of 'my' system is that there are too few
-lines-. In game semantics, the connectives and quantifiers split up in
many different ones. And classical logic and constructive logic then
become two different fragments of one larger (but weaker) logic.
As for details, the 'three language post' as you so nicely baptized it
pretty much sums it up.
>> I don't see any relation between my game semantics and 'emphasis on
>> proof'. Do you?
>
> As above.
>
>>> As we seem to have caught up with each other again,
>>> it must be time for the next lesson! :)
>> Almost there - just polishing some parts.
>
> Excellent!
Unfortunately i will be rather busy again, for at least a few days.
Merry Christmas and a Happy New Year!
--
Cheers,
Herman Jurjus
Bill Taylor
> > proponent must produce an x, then
> > opponent must produce any finite number of y's, then
> > for each one proponent must produce its own z, and
> > they both can check that Pxyz is true.
>
> Very good! Very clear 'game thinking'.
Good. Thanks.
> Well, i can think of more variants than the two we now have.
>
> 1) If you have infinitely many classmates, and you have to beat them
> all, you would't get away with taking on only finitely many of them,
> would you?
>
> Imo the 'true', full, classical, platonistic 'for -all-' allows the
> y-player (i.e. opponent) to give -any- number of y's, even possibly
> uncountably many, if wanted.
Yes, such things occurred to me OC, but I dismissed them as
they didn't seem to fully conform to the true spirit of the game idea.
But yes we should keep them in mind.
> So we now clearly see at least four variants of universal
> quantification, that is: four more or less natural game-related
> interpretations of universal quantification (namely your 'forall', your
> 'for any', and the above two). Agreed?
Yep. They are...
"for any particular one of..."
"for all of any particular finite collection of..."
"for all of any particular countable collection of..."
"for all of..."
The first is my "any", the last is calssical. "Particular" could be
"explicit".
> Also: it's quite easy to give sentences that show the differences
> between all of them.
I would expect so!
-- Wrapping-up William
Keith Ramsay
|> I suspect that the semantics would come closer to the
|> intended semantics (by Brouwer) if you required that the
|> choice sequence be generated by an ally who is given
|> access to the allies (of either player) who are generating
|> choice sequences that have already been started, to
|> query terms of their sequences.
|
|Something like that was what i already had in mind.
|But... how would that help in the above sample sentence?
I make the claim, and set my ally in the sound-proof booth
generating a sequence, not knowing what k is. Then you
say, k=7. In order to have a winning strategy, I have to be
able to get my ally to switch to saying all 7s. But he
doesn't know that k=7.
The thing that seems unreasonable about the interpretation
making those sample sentences "true" is that eventually
the terms of the free choice sequence can depend upon
the selection of k.
Keith Ramsay
Keith Ramsay
On Dec 14, 9:51 pm, Bill Taylor <w.tay...@math.canterbury.ac.nz>
wrote:
|BUT THIS IS NOT SO! The orthodox have "first dibs" on these
|disputed terms, from Frege, Cantor, Hilbert, Russell and
|others in late C19 to early C20, specifically for the orthodox
|("existential") PoV. The specifically constructive interpretations
|came noticeably later, beginning about 1920.
No, the history is more complicated than you're making it
out to be. (And why would "dibs" be a good policy
anyway? It freezes bad terminology into place.)
The terms are much older than any of these named
individuals. There were arguments about what existence
should be taken to mean, in mathematics, going back to
ancient times, and the idea that it should be taken to
refer to a mental construction is very old. Certainly it's
older than Frege; Frege felt the need to argue against it.
Cantor himself described sets as being formed by some
kind of mental act of gathering together.
Brouwer's "On the untrustworthiness of the principles of
logic" dates to 1908. Kronecker was complaining in
constructive terms about Cantor decades before.
In order to say that the constructive interpretation is
late, you're taking these things as not constituting
instances of "the specifically constructive interpretation",
and in order to say that the "orthodox" interpretation is
old, you're taking things that were said by these guys as
being instances of it. But I don't think you're maintaining
a consistent standard here. I think that since the classical
interpretation seems so reasonable and unproblematic to
you, you give sketchy presentations of it much more of a
free ride, while you don't count a constructive interpretation
as having really been given until it's been given in such a
way that you can read it through the lenses of your
habitual classical mathematical viewpoint. Someone says
that a set of natural numbers is an arbitrary collection of
them, with each natural number independently being
either in it or not, without it having to be given by a rule
or anything of the kind (?), and presumably you find this
an adequate explanation. (Do you have a better one?)
But someone tells you that a free choice sequence is
understood constructively to be given by a process that
only specifies finitely many terms at any given time, and
you feel uneasy and wish a lot of elaboration.
Frege uses the law of excluded middle and argues for
"realism" in the philosophical sense (as used e.g. by
Dummett). Is this sufficient to count as a description of
what the "orthodox" interpretation is? Does rejection of
the law of excluded middle, and an anti-realist
philosophical argument count as a description of the
constructive interpretation? What if it is accompanied by
claims to the effect that mathematical existence should be
proven by construction? I would be tempted to say that until
the double-negation interpretation came along, we didn't
really have a solid understanding of what classical
existence meant.
The main thing is, though, that you're just being a very
lazy reader. You're proposing that absurdly redundant
language be used, in order to save you a very small burden
of remembering the context. Duplicates of very nearly
every mathematical term would need to be formulated.
We might as well add "->REMEMBER PARAGRAPH 1, BILL<-" to
each line of a paper; that would be less redundant than
what you're asking for.
If anyone should happen to require a systematic
reinterpretation of all terminology, they should be given
similar slack. Indeed, in mathematical logic, this is
done, when, for example, a logician says that he's
going to assume for the duration of an argument
that we're working within a particular model of set
theory or with some unusual logic. Certainly they
should provide such a warning, but I can't recall
anyone making an analogous complaint about them
when they did. It'd be very impractical to heed it.
I would call it in general a very bad idea to say
that the person who is not making an assumption
is the one who needs to keep reminding the reader
that they are not doing so; it just happens that in
this case the assumption in question is so very well
ingrained that it needs to be pointed out.
Keith Ramsay
Bill Taylor
> No, the history is more complicated than you're making it
> out to be.
As is all history. I might say the same of your potted summary.
> The terms are much older than any of these named individuals.
Of course! But it only came to the crunch with Brouwer.
Before that it was merely philosophical argument. After that,
it was two different types of math, with different working
assumptions. At that time, I insist, it was up to the newbie
and his followers to make different terms for different things.
> The main thing is, though, that you're just being a very
> lazy reader.
And perhaps you are being a hypocritical debater?
> You're proposing that absurdly redundant language be used,
Nonsense.
> Duplicates of very nearly
> every mathematical term would need to be formulated.
Rubbish. Most would be the same.
Your suggestions are counsels of confusion.
They are outrageously anti-mathematical.
-- Battling Bill
abo
wrote:
>
> RANT BEGINS___________________
>
> I rant about the constructivist's hi-jacking of standard
> math-language terms to use in their own interpretation,
> rather than coming up with new ones of their own!
I agree!
>
> It is EXTREMELY confusing to have standard words like "truth",
> "proof", "there exists", "not" (even!), "sequence" and many
> others, have two quite different meanings depending on context.
...
> Now it is frequently replied, that no-one has
> a right to exclusive use/definition of everyday words,
> and that their right is just as good as the orthodox mathie.
>
> BUT THIS IS NOT SO! The orthodox have "first dibs" on these
> disputed terms, from Frege, Cantor, Hilbert, Russell and
> others in late C19 to early C20, specifically for the orthodox
> ("existential") PoV. The specifically constructive interpretations
> came noticeably later, beginning about 1920. Therefore, I assert,
> (uselessly, OC!), that it is up to the those of a constructive
> ("algorithmic") bent, to find new ones.
As Keith replies, the history is more complicated. In any case, the
"I was here first" may work on the playground, but I don't think it is
appropriate here. So, while I agree with your main point, I don't
think you should be using history as justification. The reason why
intuitionists should use different terms (or at least, stick
"Intuitionist" in front, such as "there Intuitionistically exists") is
just that there *is* an orthodox meaning, which almost everyone uses.
And, as in many things, numbers count. The word 'revolution,' when
applied to a political event, first meant a *return* to a status quo
(the use came from astronomy). Now it means a *breaking* from a
status quo. Today, if someone came along and started using
'revolution' in its original way, then I think the rest of us would
find that very confusing and inadvisable, even though he would win the
"I was here first" argument. It's confusing because the numbers are
against him; there's an orthodox meaning, and the original meaning is
just not the orthodox any longer.
If understand Keith's reply to you, then he is suggesting that he is
fine with a "paragraph 1", where the Intuitionist explains he is using
his terms in an unorthodox way. IMHO this is not ideal, but it is
satisfactory.
Bill Taylor
> > I rant about the constructivist's hi-jacking of standard
> > math-language terms to use in their own interpretation,
> > rather than coming up with new ones of their own!
>
> I agree!
Excellent fellow! ;-)
> As Keith replies, the history is more complicated.
Yes, as I noted, it always is.
> "I was here first" may work on the playground, but I don't think
Once it has become established, then yes, I think it is so!
"Becoming established", OC, meshes with your own criterion of
"majority rules" - the two criteria tend to be one of a piece.
But however it may have been, it is surely an unwarranted
confusion (if not worse!) to use the same terms, knowing that
by many they will be misinterpreted. And I think this is even
more critical when a minority is trying to convert a majority,
or at least seek to increase their understanding.
And in despite your (& Keith's) claims, many (most?) books and
papers do NOT start off with "we are using all these terms in
their intuitionistic sense.
> such as "there Intuitionistically exists")
There's no need for such a locution; "there exists an explicit..."
would be quite helpful to both sides. I'm sure such brief and
simple expressions could be found in most cases.
I already mentioned "inhabited set".
> The word 'revolution,'
Hardly a comparable case! We are talking near-simultaneity
here, not centuries-apart. OC many words change their meanings
over the centuries. Actually, one of my very favorites along
these lines is a pair of words that have almost exactly *swapped*
their meanings over the years! These are "awful" & "terrific".
A classic pair!
-- Wordish William
Keith Ramsay
wrote:
|> You're proposing that absurdly redundant language be used,
|
|Nonsense.
|
|> Duplicates of very nearly
|> every mathematical term would need to be formulated.
|
|Rubbish. Most would be the same.
Let's consider some examples, shall we? There are different
senses of "exists", "or", "<>", "function", "real number",
"convergent", "continuous", "measurable", "integral"...
and it goes downhill from there, since usually a term which
is defined in terms of one of these terms also acquires a
different meaning.
To the extent that one says that the words are being used
to mean the same thing, it's by relying upon an embedding
of some kind, and it's not entirely clear that any of them is
100% faithful. One constructivist acquaintance commented
that the meaning of 3<pi<4 is different.
It's commonplace for authors to adopt a nomenclature that
a formalist might approve of, and ignore meaning entirely,
but refer simply to constructively or classically provable
theorems, etc.
Keith Ramsay
Keith Ramsay
wrote:
|But however it may have been, it is surely an unwarranted
|confusion (if not worse!) to use the same terms, knowing that
|by many they will be misinterpreted.
You're the only person I know who has this problem. Have
you considered the possibility that it's due to your own
practices?
|And in despite your (& Keith's) claims, many (most?) books and
|papers do NOT start off with "we are using all these terms in
|their intuitionistic sense.
Where are your examples of confusing usage? What I can
remember from Brouwer, Bishop, Bridges, Richman, etc.
gives the reader more in the way of preamble than would
be normally expected in a technical field, not just letting
the reader know that the paper is working constructively,
but giving some pointers on it (and not just assuming that
the reader either has or will acquire an adequate
background before reading the paper, as is common).
The inability to assume that your reader has what would
be in any other field minimal prerequisites, is a big
impediment.
Keith Ramsay
Keith Ramsay
|> No, of course not, I was just trying to tie together the game
|> semantics
|> intuitionism with the traditional sort, as much as possible.
|
|That's what i was afraid of. Just fyi, imo, the connection between
'my'
|system and constructivism is somewhere else than where i see you
look.
|
|You're of course free to do whatever you like, but i would advice
|against this 'tying together' in this case, as it will probably
|-increase- your confusion.
Yes, very much so, but for him not to lump them together would
require effort. So be prepared to have to keep sorting them out
for him.
Keith Ramsay
Keith Ramsay
wrote:
|> such as "there Intuitionistically exists")
|
|There's no need for such a locution; "there exists an explicit..."
|would be quite helpful to both sides.
This would be a handy phrase in some cases except that
it's already acquired a different and informal connotation
in classical mathematics, conflicting with the one you're
proposing that it be given. Try looking up "explicit" in
the online mathematical reviews sometime for examples
of how it's typically used.
Given a continuous function f, where f(0)<0<f(1), the
smallest zero of f is an explicit example of a zero of
f, but does not serve to show constructively that there
exists a zero of f. Lots of nonconstructive constructions
are termed "explicit", in what I think is the intended
meaning of the word.
On the other hand, once it was shown that the sign of
pi(n)-li(n) changed (and it was constructively shown, by
the same token), then "the first change of sign" is a
validly constructed example of such a sign-change.
However, when people ask for an "explicit" example,
they usually intend for it to be more completely
computed in some loose sense, like 2^2^23+5, rather
than "the first example". There are Nim-like games
where it's possible to prove that the first player has
a winning strategy, and it is constructive due to the
game being finite, but an "explicit" strategy would
ordinary mean one spelled out more concretely than
"search the move tree".
|I'm sure such brief and
|simple expressions could be found in most cases.
|I already mentioned "inhabited set".
What substitute for "real number" would you recommend?
It'd better be rather good, since you're asking for it to be
used throughout a field.
Keith Ramsay
Keith Ramsay
|On Dec 27, 3:38 am, Bill Taylor <w.tay...@math.canterbury.ac.nz>
|wrote:
||But however it may have been, it is surely an unwarranted
||confusion (if not worse!) to use the same terms, knowing that
||by many they will be misinterpreted.
|
|You're the only person I know who has this problem. Have
|you considered the possibility that it's due to your own
|practices?
I'll note that even though Abo says it would be good to keep
explaining these things throughout, he doesn't say he ever
found it very confusing. He can feel free to be a second
example of this if he likes. And I think if either of you ever
had to read more than little snippets of constructive
mathematics he might well change his mind about requiring
the extra verbiage throughout.
As long as constructive mathematics is dealt with as a little
"toy" field, a miniature amusement, a sidelight, there are
lots of goofy requirements that can be maintained. If you
ever mean to scale it up to "industrial" capacity, though,
requiring that so much get specially labeled every time
is pointlessly inefficient. Every reference to a real number,
if you want it to be a real number in the constructive sense,
every inequality, if you want it to be <> and not just the
negation of =, if you want it to be < and not just the
negation of >=, every use of "or" and "exists", and so on.
Nonstandard analysis quite rightly doesn't get asked to
undergo such a labeling exercise; it has its own
terminology where quite ordinarily "set" means something
different from what is usually meant by set, and so on for
everything that depends upon that. To ask them to refrain
from embedding their work within a blanket disclaimer
would be unreasonable in much the same way.
Keith Ramsay
Bill Taylor
> |But however it may have been, it is surely an unwarranted
> |confusion (if not worse!) to use the same terms, knowing
> |that by many they will be misinterpreted.
>
> You're the only person I know who has this problem.
Seemingly you have a limited mathematical acquaintance.
> Have you considered the possibility that it's due to
> your own practices?
Yes, but I reluctantly came to dismiss this easy way out
after finding so many like-minded mathies, most of whom
have just given up at an early stage due to (avoidable)
confusion on the part of expositors.
> The inability to assume that your reader has what would
> be in any other field minimal prerequisites, is a big
> impediment.
And yet we are still waiting for the Halmos of intuitionism!
-- Waiting William
Bill Taylor
> Given a continuous function f, where f(0)<0<f(1), the
> smallest zero of f is an explicit example of a zero of
> f, but does not serve to show constructively that there
> exists a zero of f. Lots of nonconstructive constructions
> are termed "explicit", in what I think is the intended
> meaning of the word.
That's a good example! Well, if "explicit" is booked,
then they could use "locatable"; the above example
would show there is not necessarily a locatable real
being a zero of such an f.
> |I'm sure such brief and
> |simple expressions could be found in most cases.
> |I already mentioned "inhabited set".
>
> What substitute for "real number" would you recommend?
As I say, "locatable real" seems to fit the bill, covers
the essence (AIUI) of the constructive idea, and isn't
too cumbersome. "Placed real" is even shorter, but perhaps
a bit too woolly. But it isn't a difficult exercise!
> It'd better be rather good,
De gustibus non est disputandum.
> since you're asking for it to be used throughout a field.
And quite reasonably, I still aver. The confusion
otherwise engenderable is both unnecessary and
still (I suspect) a little bit dishonest.
-- Bi-terminologous Bill
Herman Jurjus
Best wishes for 2009 to you all!
But good grief - what happened to this thread during my absence?
Anyway; now that Bill's rant has 'hijacked' the thread, it may make
sense to deal with that matter first.
>> RANT BEGINS___________________
>>
>> I rant about the constructivist's hi-jacking of standard
>> math-language terms to use in their own interpretation,
>> rather than coming up with new ones of their own!
>
> I agree!
FWIW: even i agree with it --- partially.
But before i go into that, may i first ask:
What -relevance- do you (or Bill himself) see of Bill's rant for the
system that i presented (with CS, FS and game semantics)?
Bill, do you still find that your rant is relevant for that system?
Because from where i'm standing, it looks like a 'YANCL' (yet another
non-classical logic), and there's nothing directly intuitionistic about
it. No more than about, say, fuzzy logic or modal logic, or ...
(As i said, and thought was also understood by Bill in the meantime:
everything about the game semantics and the types mentioned is
susceptible to (and intended for) elaboration in terms of ZFC, and
moreover the fragment (N, FS) is exactly equivalent to the orthodox
semantics.)
Just for you abo, in case you missed some of the previous posts:
The system was not announced as an intuitionistic system, but as a way
to explain -choice sequences- for classical mathematicians. Thereby
hoping that the label 'specifically intuitionist' would get removed from
that notion.
--
Cheers,
Herman Jurjus
Bill Taylor
> But good grief - what happened to this thread during my absence?
The usual!
> Anyway; now that Bill's rant has 'hijacked' the thread,
Hmmm. I did advise people to ignore it, but what good is that?
> it may make sense to deal with that matter first.
It seems unlikely to ever get it fully "dealt with".
There are hot opinions on either side, seemingly.
> >> I rant about the constructivist's hi-jacking of standard
> >> math-language terms to use in their own interpretation,
> >> rather than coming up with new ones of their own!
>
> > I agree!
>
> FWIW: even i agree with it --- partially.
Splendid.
> But before i go into that, may i first ask:
>
> What -relevance- do you (or Bill himself) see of Bill's rant for
> the system that i presented (with CS, FS and game semantics)?
> Bill, do you still find that your rant is relevant for that system?
Not yet. But I expect to. And even now I'd much prefer to rename
"choice sequences" as a particular type of "sequence system",
of which a classical sequence is another type. So, CSS, maybe.
> Because from where i'm standing, it looks like a 'YANCL' (yet another
> non-classical logic), and nothing directly intuitionistic about it.
I agree, as yet, that seems so. OTOH, YANCL is not necessarily going
to be much use for an orthodox mathie, when he tries to understand
something non-classical; wouldn't you tend to agree?
> No more than about, say, fuzzy logic or modal logic,
This is a family newsgroup... there's no need to use bad
language! :)
> everything about the game semantics and the types mentioned is
> susceptible to (and intended for) elaboration in terms of ZFC,
A noble goal, and I hope it will be a successful one.
> moreover the fragment (N, FS) is exactly equivalent to the orthodox
> semantics.)
That, at least, is a blessing for me.
-- Blessed Bill
Herman Jurjus
> Herman Jurjus writes:
>
>> But good grief - what happened to this thread during my absence?
>
> The usual!
>
>> Anyway; now that Bill's rant has 'hijacked' the thread,
>
> Hmmm. I did advise people to ignore it, but what good is that?
>
>> it may make sense to deal with that matter first.
>
> It seems unlikely to ever get it fully "dealt with".
> There are hot opinions on either side, seemingly.
>
>>>> I rant about the constructivist's hi-jacking of standard
>>>> math-language terms to use in their own interpretation,
>>>> rather than coming up with new ones of their own!
>>> I agree!
>> FWIW: even i agree with it --- partially.
>
> Splendid.
>
>> But before i go into that, may i first ask:
>>
>> What -relevance- do you (or Bill himself) see of Bill's rant for
>> the system that i presented (with CS, FS and game semantics)?
>> Bill, do you still find that your rant is relevant for that system?
>
> Not yet. But I expect to. And even now I'd much prefer to rename
> "choice sequences" as a particular type of "sequence system",
> of which a classical sequence is another type. So, CSS, maybe.
Just fyi, i'd prefer to refrain from any speaking names and just talk
about 'the type CS' and 'the type FS', being two possible ways to
formalize the (ambiguous) notion 'sequence'.
So that we'd say 'CS-sequence', 'FS-sequence', etc.
BTW, when i hear 'sequence' i immediately hear a time aspect:
Latin 'sequi' = 'to follow', and 'sequential' practically -means-
'step by step, in the course of time, one after the other'.
I also think of music (Sequenz), and of software (streams vs arrays),
both cases in which there clearly is a time component. But it's a
kindergarten notion: immediately clear and utterly trivial.
All still just fyi: if we would use speaking names, mine would be:
CS-sequence: 'sequence', or at most 'sequential process'
FS-sequence: 'arrangement'
(so as to bring out more clearly its static character)
'System' sounds to me like something that could -contain- types, rather
than the other way around.
>> Because from where i'm standing, it looks like a 'YANCL' (yet another
>> non-classical logic), and nothing directly intuitionistic about it.
>
> I agree, as yet, that seems so. OTOH, YANCL is not necessarily going
> to be much use for an orthodox mathie, when he tries to understand
> something non-classical; wouldn't you tend to agree?
We are now getting to the real issue:
What makes you think 'choice sequence' is a non-classical notion?
>> No more than about, say, fuzzy logic or modal logic,
>
> This is a family newsgroup... there's no need to use bad
> language! :)
Ah - can you tell more about the background of that attitude?
Because that may be the real cause of the problem.
>> everything about the game semantics and the types mentioned is
>> susceptible to (and intended for) elaboration in terms of ZFC,
>
> A noble goal, and I hope it will be a successful one.
Imho, it's a -trivial- task, from the sketch i've given so far.
I was thinking of leaving it to the reader to fill in the details.
Apparently you have difficulties doing that? What are those difficulties?
BTW, the goal was already successfully completed; it's called
'Computability logic'.
>> moreover the fragment (N, FS) is exactly equivalent to the orthodox
>> semantics.)
>
> That, at least, is a blessing for me.
That confirms once more that the problem you have is not related to
intuitionism at all. It's about having a too narrow view of classical
mathematics. Many classical mathematicians have no problem understanding
this game semantics, including the type CS.
And my guess is that you too wouldn't have a problem with that, if you
just could bring yourself to cut the link between 'choice sequence' and
'intuitionism'.
So once more: the game semantics that i sketched is a -classical
system-, not an intuitionistic one.
--
Cheers,
Herman Jurjus
Bill Taylor
> Just fyi, i'd prefer to refrain from any speaking names and just
> talk about 'the type CS' and 'the type FS',
Sounds reasonable. We should try to find middle grounds,
I guess, at least for the purposes of this thread.
> BTW, when i hear 'sequence' i immediately hear a time aspect:
....
> FS-sequence: 'arrangement'
> (so as to bring out more clearly its static character)
This last comment is very apt, and doubtless you have etymology
on your side for the former. But abo's point about established
usages still holds, so I must regretfully discard these terms.
To accommodate us both, therefore, and as you dislike "system",
it seems we must stick to CS & FS for types, and CSO & FSO for
individuals of that type, (O for object).
> We are now getting to the real issue:
> What makes you think 'choice sequence' is a non-classical notion?
History. (Surely that answer was obvious?)
> >> No more than about, say, fuzzy logic or modal logic,
>
> > This is a family newsgroup... there's no need to use bad
> > language! :)
>
> Ah - can you tell more about the background of that attitude?
> Because that may be the real cause of the problem.
Maybe. Let's take modal logic first. I have no objection
to people studying modal, temporal, linear, paraconsistent,
constructive, 2nd-order, whatever logics they like. As long as
the logics are clearly (formally) specified, they are all part
of math, and no less worthy of study as any other part of math.
I just don't think they have anything to do with founding math
in a philosophically acceptable way. As I said before, MHO is
that math is an essentially atemporal matter, and most if not
all of those others have a distinctly temporal aspect to them.
AFAICS the battle for the proper founding of math was fought
and WON in the 1880-1930 period, and FOL= is the clear and
undisputed WINNER, and has been accepted as such by the vast
majority of working mathies and philosophers of math. The others
are fun, intriguing, possibly even useful, but they are not the
true mathematical state of affairs. MHO; but with vast support.
However, "fuzzy logic" is (probably) a whole nother matter!
I don't know what it is, never heard the term, but I guess it is
part of the whole near-crackpot subculture of fuzzy math at large.
I regard this whole area as stupid and anti-mathematical,
insofar as it will (as it usually does) eschew any hard-edged
formalization at all. That is the case for the few bits
I've seen, anyway.
> >> everything about the game semantics and the types mentioned is
> >> susceptible to (and intended for) elaboration in terms of ZFC,
>
> > A noble goal, and I hope it will be a successful one.
>
> Imho, it's a -trivial- task, from the sketch i've given so far.
> I was thinking of leaving it to the reader to fill in the details.
> Apparently you have difficulties doing that? What are those difficulties?
I was thinking e.g. of our various interpretations of A as for-all
or for-any. That hardly seems classically resolvable?
> > That, at least, is a blessing for me.
>
> That confirms once more that the problem you have is not related
> to intuitionism at all.
That is absolutely correct! I can relate to minimal
constructivism, as I've said, but not to intuitionism.
I still don't even know (fully) what it IS!
> It's about having a too narrow view of classical mathematics.
No. I see it as having *adopted* the classical view.
> Many classical mathematicians have no problem understanding
> this game semantics, including the type CS.
"Many" sounds like a bit of an overstatement. I know of none
who have even *heard of it*, and of none who can bond with it,
with the exception of Keith Ramsey and Thomas Forster. No doubt
there are others whom I know of, I just don't know their PoVs.
> And my guess is that you too wouldn't have a problem with that,
> if you just could bring yourself to cut the link between
> 'choice sequence' and 'intuitionism'.
That's a mighty thick historical rope to cut! Intuitionists
*invented* the term and concept of choice sequence, specifically
for intuitionistic purposes, and no-one I know before this thread
has ever suggested cutting it! But if we stick to CSOs and FSOs
we might manage.
> So once more: the game semantics that i sketched is a -classical
> system-, not an intuitionistic one.
I think this is rather too glib! Apart from my quantifier
comments above, there is still my original complaint/query that
you haven't yet said what (classical!) type of thing a CSO
actually IS. You said, (effectively), "let's forget about that
just for now, and concentrate on what it does, how it interacts
with things in a gamelike manner", which is fine, I agreed to go
along with that. But it severely prevents it (for now) being
regarded as a CLASSICAL THING. It is NOT, because it has
(as yet), no classical STATUS.
Do you not see the force of this complaint, and its problematic
nature for an orthodox mathie like me (and thousands more)?
-- Timeless Taylor
Keith Ramsay
On Dec 31 2008, 6:29 am, Bill Taylor <w.tay...@math.canterbury.ac.nz>
wrote:
|Keith Ramsay <kram...@aol.com> wrote:
|> |But however it may have been, it is surely an unwarranted
|> |confusion (if not worse!) to use the same terms, knowing
|> |that by many they will be misinterpreted.
|
|> You're the only person I know who has this problem.
|
|Seemingly you have a limited mathematical acquaintance.
And how would you know?
I once tried to make a complete list of mathematical acquaintances,
and now and then I realize that I've left somebody out. It's true that
I haven't met as many mathematicians lately as I used to.
|> Have you considered the possibility that it's due to
|> your own practices?
|
|Yes, but I reluctantly came to dismiss this easy way out
|after finding so many like-minded mathies, most of whom
|have just given up at an early stage due to (avoidable)
|confusion on the part of expositors.
Figuring that it might be *you* who needs to study is the
easy way out, huh?
When you write "mathies", it always suggests to me a lack of interest
in distinguishing between people who actually *work* at their
mathematics, and people who merely sort of play around with it on the
side.
This is no more impressive than it would be if you were to dig up
innumerable lazy calculus students who feel that calculus class is
being made incredibly and unnecessarily hard by hard-hearted calculus
instructors. Such students are prone to assuming that there has to be
something other than effort distinguishing them from those who have
gained an understanding of the subject.
I know people who have diligently worked to understand constructive
mathematics, and none of them have come out the other side saying,
"gosh gee, they could've made this WAY easier if they'd only
done...". I don't know how it is you can feel so confident that there
is some "royal road" here.
|> The inability to assume that your reader has what would
|> be in any other field minimal prerequisites, is a big
|> impediment.
|
|And yet we are still waiting for the Halmos of intuitionism!
I don't know why you think intuitionism, per se, is something to be
popularized. It has historical interest, in the sense of being the
view of Brouwer. If you care about that, read Brouwer.
For constructivism, read Bishop, or Bishop and Chang. I don't know
what problem you have with that, or what, if you understand that kind
of material, poses a problem for you elsewhere.
Keith Ramsay
Keith Ramsay
On Dec 31 2008, 6:43 am, Bill Taylor <w.tay...@math.canterbury.ac.nz>
wrote:
|Keith Ramsay <kram...@aol.com> wrote:
|> Given a continuous function f, where f(0)<0<f(1), the
|> smallest zero of f is an explicit example of a zero of
|> f, but does not serve to show constructively that there
|> exists a zero of f. Lots of nonconstructive constructions
|> are termed "explicit", in what I think is the intended
|> meaning of the word.
|
|That's a good example! Well, if "explicit" is booked,
|then they could use "locatable"; the above example
|would show there is not necessarily a locatable real
|being a zero of such an f.
Terminology like "locatable real" adds to the confusion. People say
things similar to this when they're talking about constructive
mathematics, more often "constructible real" or "constructive real",
and it does confuse them; this is not a hypothetical case.
It's unwittingly misleading. Perhaps the main thing is that it makes
it appear as though the constructive concept were somehow derived from
the classical concept. It looks like we had an idea of "real", and
then restricted it to get the idea of "locatable real". It makes it
sound like we're dealing in a *more* complicated notion of real than
classical mathematicians are, as if constructivism were about adding
complex bells-and-whistles to classical mathematics. It makes it sound
like we're dealing in less generality than classical mathematics.
Good constructive mathematics is elegant and general. Your proposal
would munge the elegance of it and make it look like it's naturally
derivative from classical mathematics.
There is a natural, straightforward way to derive classical concepts
from corresponding constructive concepts. Where constructive
mathematics has concepts X, Y, and Z, classical mathematics has the
concepts LEM->X, LEM->Y, and LEM->Z, where LEM is the law of excluded
middle. (One might take the axiom of choice instead.) Terminology
should not be designed in a way that disguises this straightforward
relationship, or make it look like we took "LEM->X" and somehow
restricted it to turn it into something still more complicated, rather
than simply recognized that behind it, there is a natural concept, X.
I understand that classical mathematicians prefer to disguise the
complexity of their constructions, by making their uses of the law of
excluded middle invisible, or to put it another way, to drop double
negatives (which would tell you what the constructive content
is...). I'm able to change contexts, so that I understand what I'm
reading, when they do that.
I don't see that I'm asking for anything more than that of the
classical mathematician, who's reading some constructive mathematics.
The classical mathematician doesn't feel like they need to warn us
that they're doing classical mathematics; but for you, it seems that
merely warning the reader that constructive mathematics is being done
is not enough? (And I doubt very much that you actually intend to do
very much reading of constructive mathematics, do you?)
In this country lots of gay people want to be allowed to marry, and
have their marriage be treated the same way as it is for the rest of
us. Their opponents keep insisting that they have "dibs" on the
definition of marriage. They want marriages between same-sex couples
to be labelled something different... to emphasize their view that
there's something weird or defective about it. What they want is for
everyone to be committed to calling it something that implies that
opposite-sex marriage is the norm, and same-sex marriage is some phony
imitation of it. Imposing alien terminology on a mathematical field is
not as cruel as this, but also presumes that maintaining what
outsiders count as "normal" contexts for words overrides insiders'
need to follow their own natural course.
|> |I'm sure such brief and
|> |simple expressions could be found in most cases.
|> |I already mentioned "inhabited set".
|
|> What substitute for "real number" would you recommend?
|
|As I say, "locatable real" seems to fit the bill, covers
|the essence (AIUI) of the constructive idea,
No. What, from a constructive point of view, is a "real", when it is
"not locatable"? It's a terrible hack.
When one is doing something simple, one is entitled to use simple
terminology. This is far more important than maintaining some imagined
precedent. I think this is perhaps my main point here.
|and isn't
|too cumbersome. "Placed real" is even shorter, but perhaps
|a bit too woolly. But it isn't a difficult exercise!
|
|> It'd better be rather good,
|
|De gustibus non est disputandum.
I agree with an acquaintance whose motto was, De gustibus *est*
disputandum. I don't think it makes sense to say on the one hand,
let's not dispute mere tastes in terminology, and on the other hand,
let's impose policies like "first dibs" on terminology. Terminology is
too nearly a matter of taste to begin with.
|> since you're asking for it to be used throughout a field.
|
|And quite reasonably, I still aver. The confusion
|otherwise engenderable is both unnecessary and
|still (I suspect) a little bit dishonest.
This kind of suspicion strikes me as shabby. I don't know what you
think I think I could be accomplishing by pretenses here. Constructive
mathematics should be pursued without needlessly muddling it up in
order to satisfy the demands of people who can't be bothered to
remember whether the mathematics they are reading is constructive or
not, and that's really what I think.
I still don't know what you think of the analogous case of nonstandard
analysis. Do you really think that nonstandard analysis needs to have
this extra verbiage woven into its fabric, to keep from confusing
people who've somehow forgotten that what they're reading is
nonstandard analysis? I think this kind of mathematics is liable to
become more common in the future, not so much nonstandard analysis per
se, but relativizations of pieces of mathematics between contexts
where the individual terms mean different things.
This is where a lot of important advances have been made already; in
abstract algebra, the fact that we can "overload" symbols like + and *
to refer to arbitrary binary operations, not necessarily our old,
familiar addition and multiplication, is very useful. We could say,
well, since you're defining a *different kind of thing*, you ought to
use a *different symbol*. So + is right out-- better use a circled
plus or something similarly goofy looking. But that would've been
petty.
It's hard enough as it is, for people accustomed to classical
mathematics to rid themselves of interference from their old habits of
mind. We have a way of unwittingly making things complicated in
constructive mathematics, because we revert to ways of doing things
that just detour us away from the natural constructive way of doing
it. If you get into the habit of assuming that it's a "deformation"
from the natural way of doing things, that it's a massaged form of
classical mathematics, it can take a long time to learn good
constructive habits. I say this from personal experience. The students
who start out free of this kind of prejudice seem to have an easier
time of it (from what I've heard).
Keith Ramsay