Science is a human activity (was: Python syntax in Lisp and Scheme)

[Cameron Laird]

would you kindly set right the guys (such as your
namesake) who (on c.l.lisp with copy to my mailbox but not to here) are
currently attacking me because, and I quote,
"""
Software is a department of mathematics.
"""

And anyone who doesn't think mathematics has its own
culture with ideas and even mistaken preferences for what
is right and wrong should read
The Mystery of the Aleph: Mathematics, the Kabbalah, and the Human Mind
to see how Cantor's ideas of transfinite numbers (and other ideas,
as I recall, like showing there are functions which are everywhere
continuous and nowhere differentiable) were solidly rejected by
most other mathematicians of his time.
Mathematicians are people as well.

.
.
.
And let no one assume that these are mere foibles of the
past that we moderns have overcome; mathematics remains
stunningly incoherent in what's labeled "foundations".
There's a wide, wide divergence between the intuitionism
working mathematicians practice, and the formalism they
profess.

'Good thing, too; our age enjoys the blessing of superb
mathematicians, and I'm relieved that philosophical in-
consistencies don't (appear to) slow them down.

[David C. Ullrich]

On Sat, 11 Oct 2003 14:21:32 -0000, ***@lairds.com (Cameron Laird)
wrote:

Well, since you crossposted this to sci.math you must be hoping

Post by Cameron Laird

would you kindly set right the guys (such as your
namesake) who (on c.l.lisp with copy to my mailbox but not to here) are
currently attacking me because, and I quote,
"""
Software is a department of mathematics.
"""

And anyone who doesn't think mathematics has its own
culture with ideas and even mistaken preferences for what
is right and wrong should read
The Mystery of the Aleph: Mathematics, the Kabbalah, and the Human Mind
to see how Cantor's ideas of transfinite numbers (and other ideas,
as I recall, like showing there are functions which are everywhere
continuous and nowhere differentiable) were solidly rejected by
most other mathematicians of his time.
Mathematicians are people as well.

.
.
.
And let no one assume that these are mere foibles of the
past that we moderns have overcome; mathematics remains
stunningly incoherent in what's labeled "foundations".
There's a wide, wide divergence between the intuitionism
working mathematicians practice,

Actually "inuitionism" has a certain technical meaning,
and actual intuitionism is not what most mathematicians
practice. But never mind, I believe I know what you meant.

Post by Cameron Laird
and the formalism they
profess.

Far be it from me to insist we've overcome the foibles
of the past. But:

It's certainly true that mathematicians do not _write_
proofs in formal languages. But all the proofs that I'm
aware of _could_ be formalized quite easily. Are you
aware of any counterexamples to this? Things that
mathematicians accept as correct proofs which are
not clearly formalizable in, say, ZFC?

Post by Cameron Laird
'Good thing, too; our age enjoys the blessing of superb
mathematicians, and I'm relieved that philosophical in-
consistencies don't (appear to) slow them down.

What's an actual example of one of those philosophical
inconsistencies that luckily doesn't slow us down?

************************

David C. Ullrich

[John]

Post by David C. Ullrich
Well, since you crossposted this to sci.math you must be hoping

Post by Cameron Laird

would you kindly set right the guys (such as your
namesake) who (on c.l.lisp with copy to my mailbox but not to here) are
currently attacking me because, and I quote,
"""
Software is a department of mathematics.
"""

And anyone who doesn't think mathematics has its own
culture with ideas and even mistaken preferences for what
is right and wrong should read
The Mystery of the Aleph: Mathematics, the Kabbalah, and the Human Mind
to see how Cantor's ideas of transfinite numbers (and other ideas,
as I recall, like showing there are functions which are everywhere
continuous and nowhere differentiable) were solidly rejected by
most other mathematicians of his time.
Mathematicians are people as well.

.
.
.
And let no one assume that these are mere foibles of the
past that we moderns have overcome; mathematics remains
stunningly incoherent in what's labeled "foundations".
There's a wide, wide divergence between the intuitionism
working mathematicians practice,

Actually "inuitionism" has a certain technical meaning,
and actual intuitionism is not what most mathematicians
practice. But never mind, I believe I know what you meant.

Post by Cameron Laird
and the formalism they
profess.

Far be it from me to insist we've overcome the foibles
It's certainly true that mathematicians do not _write_
proofs in formal languages. But all the proofs that I'm
aware of _could_ be formalized quite easily. Are you
aware of any counterexamples to this? Things that
mathematicians accept as correct proofs which are
not clearly formalizable in, say, ZFC?

How about the following?

C3 EyAx[x in y <-> Et(x in t) & A] (with y not free in A) Classification

C4 AyAx[Az(z in y <-> z in x) -> {(set y & set x) <-> y=x}]
(Equi-membered classes are identical iff these are sets.)

From C3 it follows that there is a class of non-self-membered classes.

1) EyAx(x in y <-> Et(x in t) & ~(x in x)) C3

Hence

2) Ax(x in r <-> Et(x in t) & ~(x in x)) 1,EI

and

3) r in r <-> (Et(r in t) & ~(r in r)) 2,UI

so that

4) ~Et(r in t) 3

and

5) ~(set r) 4

and

6) ~(r=r) 5,C4

so that

7) Ex~(x=x) 6,EG

Post by David C. Ullrich

Post by Cameron Laird
'Good thing, too; our age enjoys the blessing of superb
mathematicians, and I'm relieved that philosophical in-
consistencies don't (appear to) slow them down.

What's an actual example of one of those philosophical
inconsistencies that luckily doesn't slow us down?
************************
David C. Ullrich

--John
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
"The most successful ideological effects are those which have
no need for words, and ask no more than complicitous silence."
--Pierre Bourdieu

[Michele Dondi]

On Sat, 11 Oct 2003 10:37:33 -0500, David C. Ullrich

Post by David C. Ullrich
It's certainly true that mathematicians do not _write_
proofs in formal languages. But all the proofs that I'm
aware of _could_ be formalized quite easily. Are you
aware of any counterexamples to this? Things that
mathematicians accept as correct proofs which are
not clearly formalizable in, say, ZFC?

I am not claiming that it is a counterexample, but I've always met
with some difficulties imagining how the usual proof of Euler's
theorem about the number of corners, sides and faces of a polihedron
(correct terminology, BTW?) could be formalized. Also, however that
could be done, I feel an unsatisfactory feeling about how complex it
would be if compared to the conceptual simplicity of the proof itself.


Just a thought,
Michele

[David C. Ullrich]

On Mon, 13 Oct 2003 16:19:58 +0200, Michele Dondi

Post by Michele Dondi
On Sat, 11 Oct 2003 10:37:33 -0500, David C. Ullrich

Post by David C. Ullrich
It's certainly true that mathematicians do not _write_
proofs in formal languages. But all the proofs that I'm
aware of _could_ be formalized quite easily. Are you
aware of any counterexamples to this? Things that
mathematicians accept as correct proofs which are
not clearly formalizable in, say, ZFC?

I am not claiming that it is a counterexample, but I've always met
with some difficulties imagining how the usual proof of Euler's
theorem about the number of corners, sides and faces of a polihedron
(correct terminology, BTW?) could be formalized. Also, however that
could be done, I feel an unsatisfactory feeling about how complex it
would be if compared to the conceptual simplicity of the proof itself.

Well it certainly _can_ be formalized. (Have you any experience
with _axiomatic_ Euclidean geometry? Not as in Euclid - no pictures,
nothing that depends on knowing what lines and points really are,
everything follows strictly logically from explictly stated axioms.
Well, I have no experience with such a thing either, but I know
it exists.)

Whether the formal version would be totally incomprehensible
depends to a large extent on how sophisticated the formal
system being used is - surely if one wrote out a statement
of Euler's theorem in the language of set theory, with no
predicates except "is an element of" it would be totally
incomprehensible. Otoh in a better formal system, for
example allowing definitions, it could be just as comprehensible
as an English version. (Not that I see that this question has
any relevance to the existence of alleged philosophical
inconsistencies that haven't been specified yet...)

Post by Michele Dondi
Just a thought,
Michele

************************

David C. Ullrich

[Shmuel (Seymour J.) Metz]

Well it certainly _can_ be formalized. (Have you any experience with
_axiomatic_ Euclidean geometry?

That's not the same thing as formalized. Such authors as Hilbert left
out steps that were formally necessary but would have obscured the
reader's understanding.

[David C. Ullrich]

On Tue, 14 Oct 2003 14:38:42 -0400, "Shmuel (Seymour J.) Metz"

Post by Shmuel (Seymour J.) Metz

Well it certainly _can_ be formalized. (Have you any experience with
_axiomatic_ Euclidean geometry?

That's not the same thing as formalized.

Of course it's not. But it seems to me that his skepticism regarding
whether that proof _can_ be formalized must in fact be skeptism
regarding whether it's possible to state all the necessary axioms
and deduce the theorem without any appeal to the way things
look.

Post by Shmuel (Seymour J.) Metz
Such authors as Hilbert left
out steps that were formally necessary but would have obscured the
reader's understanding.

************************

David C. Ullrich

[Michele Dondi]

On Tue, 14 Oct 2003 17:18:34 -0500, David C. Ullrich

Post by David C. Ullrich
Of course it's not. But it seems to me that his skepticism regarding
whether that proof _can_ be formalized must in fact be skeptism
regarding whether it's possible to state all the necessary axioms
and deduce the theorem without any appeal to the way things
look.

As I have stressed in my other post, I'm *not* skeptic about the fact
that that proof can be formalized!

I'm simply puzzled thinking of how it would be done, since IMHO it is
a proof that indeed *does* make heavily appeal to the way things look,
and in this sense it is so simple that often one can find it in
popularization books.

(BTW) Also, since you mentioned axiomatic euclidean geometry, I just
don't know anything about it[*], but I don't know wether it is
possible in its formalism to define/talk about "continuous
transformations", that are indeed the basis of that proof.

So, if I am right in my assumption above, while the object of the
proof can be reasonably defined in axiomatic euclidean geometry,
either the theorem can't be proved in that teory or there exists an
alternative proof that does not use continuity arguments.


[*] This means: "so I may well be wrong"!


Michele

[Michele Dondi]

On Mon, 13 Oct 2003 18:03:02 -0500, David C. Ullrich

Post by David C. Ullrich

Post by Michele Dondi
I am not claiming that it is a counterexample, but I've always met
with some difficulties imagining how the usual proof of Euler's
theorem about the number of corners, sides and faces of a polihedron
(correct terminology, BTW?) could be formalized. Also, however that
could be done, I feel an unsatisfactory feeling about how complex it
would be if compared to the conceptual simplicity of the proof itself.

Well it certainly _can_ be formalized. (Have you any experience
with _axiomatic_ Euclidean geometry? Not as in Euclid - no pictures,

No, I have no experience with it. Just heard it exists: I presume
you're talking about the work of Hilbert... but then I'm not sure that
it provides a full formalization! It's clear though that it brings one
step forward towards formalization.

Post by David C. Ullrich
nothing that depends on knowing what lines and points really are,
everything follows strictly logically from explictly stated axioms.
Well, I have no experience with such a thing either, but I know
it exists.)

:-) [should have read ahead...]

Post by David C. Ullrich
Whether the formal version would be totally incomprehensible
depends to a large extent on how sophisticated the formal
system being used is - surely if one wrote out a statement
of Euler's theorem in the language of set theory, with no
predicates except "is an element of" it would be totally
incomprehensible. Otoh in a better formal system, for
example allowing definitions, it could be just as comprehensible
as an English version. (Not that I see that this question has

In any case I'm sure too that *that particular proof* can be
formalized! But, even if I am under the impression that most proofs,
for some meaning of "most", would be affected by the concern expressed
above, somehow I feel like the effect with this one would be "one
order of magnitude" stronger, to say the least!

Post by David C. Ullrich
any relevance to the existence of alleged philosophical
inconsistencies that haven't been specified yet...)

In fact, it has no relevance to that matter: I thought that my
introduction should have made that clear. My comment is something I
happend to think about sometimes; your words just reminded me of it
and this seemed to be the right chance to talk about it. No more than
that, no more than a naive comment...


Michele

[David Eppstein]

Post by Michele Dondi

Post by David C. Ullrich
It's certainly true that mathematicians do not _write_
proofs in formal languages. But all the proofs that I'm
aware of _could_ be formalized quite easily. Are you
aware of any counterexamples to this? Things that
mathematicians accept as correct proofs which are
not clearly formalizable in, say, ZFC?

I am not claiming that it is a counterexample, but I've always met
with some difficulties imagining how the usual proof of Euler's
theorem about the number of corners, sides and faces of a polihedron
(correct terminology, BTW?) could be formalized. Also, however that
could be done, I feel an unsatisfactory feeling about how complex it
would be if compared to the conceptual simplicity of the proof itself.

Which one do you think is the usual proof?
http://www.ics.uci.edu/~eppstein/junkyard/euler/

Anyway, this exact example was the basis for a whole book about what is
involved in going from informal proof idea to formal proof:
http://www.ics.uci.edu/~eppstein/junkyard/euler/refs.html#Lak

[Michele Dondi]

On Tue, 21 Oct 2003 20:33:23 -0700, David Eppstein

Post by David Eppstein

Post by Michele Dondi
I am not claiming that it is a counterexample, but I've always met
with some difficulties imagining how the usual proof of Euler's
theorem about the number of corners, sides and faces of a polihedron
(correct terminology, BTW?) could be formalized. Also, however that
could be done, I feel an unsatisfactory feeling about how complex it
would be if compared to the conceptual simplicity of the proof itself.

Which one do you think is the usual proof?
http://www.ics.uci.edu/~eppstein/junkyard/euler/

Uhmmm, let me see... 13! (no, not the factorial of 13)

Post by David Eppstein
Anyway, this exact example was the basis for a whole book about what is
http://www.ics.uci.edu/~eppstein/junkyard/euler/refs.html#Lak

D'Oh! Unfortunate choice of mine...


Michele