Re: formal proof and ordinary mathematics (fwd)

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

> Date: Tue, 6 Oct 1998 11:18:43 -0600 (MDT)
> From: piotr@cs.ualberta.ca
> To: Forum Mizar <mizar-forum@mizar.uw.bialystok.pl>
> Subject: formal proof and ordinary mathematics (fwd)
> 
........
> It is the right time to summarize whatever ommisions were found
> in CCL and there is this erroneous construction of real numbers in one
> of the (Birkhoff's ?) books.


Definitely not Birkhoff! And this is not the point. Donald MacKenzie
asked about verifying the primary mathematical information (I like
the name "raw mathematics" better), not about sloppiness in popularizing
mathematics.

I better tell the story (as far as I recall):
Some years ago I had assigned a master thesis: construction of real
numbers using Dedekind cuts (actually lower open classes of Dedekind cuts).
The student followed a book (I do not remember authors, somewhere in the 
archive the information ((a copy of the Master Thesis)) is kept, I do not
think it is worth to dig it) in which the multiplication of irrational 
numbers was defined as collective multiplication of rational numbers 
belonging to them. I.e.
   R * S = { r * s: r in R, s in S }
A stupid mistake.

CCL (A Compendium of Continuous Lattices) is very rigorous, still we 
find some mistakes in it. Nothing serious, and again it is
secondary information, not raw mathematcis. We will prepare a report, after
checking wth the author(s) if we are right, but still it is not an answer
to Donald's question.

Some years ago Krzysztof Prazmowski found an error formalizing a 
published paper, but he does not remeber the paper. I do not remember, 
either.

The error was rather funny. The proof had the following structure
     P[x] implies Q[x]
      proof
       assume P[x];
        .......
       thus Q[x];
      end;
("x" - a free variable).

i.e. instead of assuming "for some x holds P[x]" the author assumed
"for all x holds P[x]".

Andrzej Trybulec