Hi,
On Mon, 5 Nov 2007, Josef Urban wrote:
If Andrzej, Adam, and Artur do not read the arguments, or do not want to
discuss them, or do not think that the problem is worth discussing,
repetition is not likely to help.
It's not the case that I (and others) do not read the arguments. Our
discussion with Freek in Edinburgh, which actually revived this topic, also
shows that no one here tries to avoid discussion ;-)
To me, the point is that since Mizar types are not just syntactic replacement
for respective predicates, I can accept the fact that the system may treat
for a,X being set st a in X
and
for a being Element of X
a bit differently. Since there is no calculus of 'incorrect' expressions and
the type information _is_ subject to some inference rules (I hope Andrzej
will comment on that in more detail), allowing empty types would need more
tweaking with the code than just requiring 'by' after every 'consider'.
And I don't agree that empty types make formalization "much more natural" -
to me, they only make some rather imprecise formalizations just a bit more
natural.
Best,
Adam Naumowicz
======================================================================
Department of Applied Logic fax. +48 (85) 745-7662
Institute of Computer Science tel. +48 (85) 745-7559 (office)
University of Bialystok e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
======================================================================
What sometimes helped was a change of discussion forum: from English to
Polish, and from virtual to some nice real-world bar in Bialystok :-).
Josef
(ceterum censeo Carthaginem esse delendam :-)
On Mon, 5 Nov 2007, Freek Wiedijk wrote:
Hi,
We've had this topic many times before, but I would like
to bring it up once more: empty types in Mizar.
The reason is that I met Adam Naumowicz and Artur Kornilowicz
at the MathWiki workshop in Edinburgh, and that it then
became clear to me that both of them didn't see the point
of allowing empty types. Particularly Artur though that
having "permissive" mode definitions should be good enough
for me and that I should not be so difficult.
Before, I thought that it was just Andrzej that I couldn't
convince that Mizar is much worse for not having empty types.
But now I found out that it's _me_ that seems to be the
exception.
So is there _anyone_ on this list that understands that it's
_much_ more natural (and therefore leads to much better
formalizations) if you are allowed to have types that can
be empty?
One of my main arguments (I've said it before, but let's
say it once more) is that one should be able to have:
For _any_ set X, not just for non-empty sets. (In fact
I think the reason that there so many "non empty set"
reservations in MML is exactly because of the fact that this
equivalence is not possible. If you in the current system
write "Element of X", you don't get the correct meaning when
X is empty. So then one has to reserve X to be non empty,
to be able to prove the results. While if "Element of X"
had the _right_ meaning, then X could have ben any set.)
Anyway, I know it's probably useless posting this, but I
wanted to give it one more try.
So to know whether there's _anyone_ like me here: please
reply to this if you agree with me that it is crazy that
Mizar forbids empty types and that it would be a much better
system if it did not.
Freek