Re: [mizar] weak types

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

Dear Andrzej,

>The problem arises, if I recall, with conditional proofs. For
>    sqrt x > a implies 'something'
>we had
>(*)    (x >= 0 implies sqrt x > a) implies 'something'
>the antecedent of an implication being in the negative position. It is
>of course the same as
>     x >= 0 & not sqrt x > a or 'something'.
>But if one assumes in the proof of (*)
>     sqrt x > a
>it is
>    x >= 0 & sqrt x > a
>not the antecedent of (*). I hope I got it right this time.
>So, the question is, if the deduction theorem holds for your system (or
>PVS).

I can't speak about PVS, but I don't really see the problem.
If you have x >= 0 & sqrt x > a you have sqrt x > a and then
you certainly have x >= 0 implies sqrt x > a, right?  So you
can apply the implication to the assumption then?

>Another question what you do (or PVS) if such a formula
>occurs under quantifier,

This is what the definition of "DC" in our paper tries to
address.

So I'm not sure exactly what a Mizar-like system that's build
on these principles should look like.  But I do think that
sqrt x > a should _not_ be an abbreviation of
x >= 0 & sqrt x > a.  Instead I think that to be allowed to
write down sqrt x > a you should be required to prove
x >= 0.  Apart from that you could use the existing
(permissive) semantics of Mizar as far as I'm concerned.

Freek