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 Xa 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