Re: [mizar] Strong Mizar wish: linking to consider

[Freek Wiedijk <freek@cs.kun.nl>]

Hi Markus,

Thanks for your comment!

>>   consider x such that
>>  A1: P x and
>>  A2: Q x by ...;
>>   then R x by ...;

>>   1. "ex x st P x"
>>   2. "P x & Q x"
>>   3. "P x"
>>   4. "Q x"

>As I understand it, Mizar only has singleton facts.  So
>probably your proposal number 2 would probably come close to
>the most desirable behaviour.

Sorry, but I don't understand why you say this.  If Mizar has
only singleton facts, then proposal 2 should _not_ be the
one, right, because that is _not_ a singleton fact.  So
proposal 2 wouldn't fit in the general Mizar style.

>Note that number 1 does not make too much sense from the
>user's perspective, since the existential statement is just
>an internal auxiliary thing to justify that consider/obtain
>in the first place.

I just added it because, when I discussed this issue with
prof.  Trybulec in Bialystok once, he thought that that one
would be the natural choice.  He then said I might discuss it
on Mizar forum, but only now I got irritated enough by this
missing feature that I actually did do so.

I still think it should be 4!  If you want 2 you can write:

     consider x such that
    A1: P x &
        Q x by ...;
     then R x by ...;

isn't it?

Freek