Re: [mizar] be and being

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

On Wed, Dec 17, 2003 at 10:25:25AM +0100, Josef Urban wrote:
> On Tue, 16 Dec 2003, Piotr Rudnicki wrote:
> 
> > Therefore I propose that both 'be' and 'being' have an alias ':'
> > which is shorter and commonly used in this context in everyday
> > writing, not to mention some other system that use it.
> 
> You may be right, but concerning these writability/readability problems, I 
> would be quite careful.
> The next steps in this direction might be suggesting something like 
> "!" instead of "for", "?" instead of "ex", "~" instead of "not", or even 
> things like "Intro;" instead of all the initial "let" and "assume", etc.
> 
> These certainly improve writability, but Mizar might end up being as 
> readable as some other systems - have a look at the comparison texts 
> collected by Freek at http://www.cs.kun.nl/~freek/comparison/index.html.

Pity that Freek did not include in his comparison some other proof
helpers.  These days my favourite proof helper is "Algebra' by
MacLane and Birkhoff where the claims are written in this way (just a
few samples of theorems but they are consistent throughout)

   - For n x n matrices B and A over K, |BA| = |B| |A|

   - ... for each scalar k there is exactly one n-linear 
     form d_: (K^n)^n -> Kwith d_k(I) = k

   - Let L be any complete lattice, and let S be any subset of L
     such that (i) I in S, and (ii) T c< S implies inf T in S.  Then
     S is a complete lattice.

   - For each ideal A in a ring R there are unique binary operations of
     addition and multiplication on the quotient set R/A which ...

There is a lot of "let ... be ..." in this book but I have not seen
a single "being".

All what I propose is a one character alias for 'be' and 'being'.
Colon ':' should not cause much of a confusion because the context 
allows for good error recovery.

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr