Re: [mizar]Possibly empty types

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi Andrzej,

your arguments are:

1) That the "permissive" definitions (e.g. "assume contradiction;", 
"assume Foo is meaningful") and definitions "breaking permissiveness" 
(e.g. "Element of {} is {}") are a "practical improvement" of Mizar.

2) That the possibly empty (weak) types lead into the danger of "ghost 
theories".

The answer (repeated here many times) to (2) is that your current 
"practical improvements" stated in (1) lead into the same ghost theories 
(for "permissive" definitions), and even worse ghost theories ("Horror!" 
in your words) for those which are "breaking" permissiveness.

The answer to (1) is that allowing weak types is even more practical than 
"permissive" definitions (because you don't repeat the assumption all the 
time), and at least as practical as "breaking permissiveness" (because 
instead of dealing with "Horror!" special-case solution, you deal with 
plain "false" special case).

So if you do not like "ghost theories", you should not allow your current 
"practical solutions". If you want your "practical improvements", then 
weak types are even more practical and simpler.

Josef