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

[David C. Ullrich]

On Mon, 13 Oct 2003 16:19:58 +0200, Michele Dondi
<bik.mido at tiscalinet.it> wrote:

>On Sat, 11 Oct 2003 10:37:33 -0500, David C. Ullrich
><ullrich at math.okstate.edu> wrote:
>
>>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...)


>Just a thought,
>Michele

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

David C. Ullrich