Re: [mizar] weak types

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Freek Wiedijk wrote:

>
> >Does it means, that the system generates the sentence
> >             x >= 0 & sqrt x > a
>
> Yes, something like that.  Although in the theory this
> conjunction does not occur as such.
>
> >We experimented with something similar in seventies. Then for
> >
> >   not sqrt x > a
> >
> >we generated
> >
> >    x >=0 implies not sqrt x > a

My mistake. As I wrote that we were using the implication for a negative
occurrence so it must be
     not (x >=0 implies sqrt x > a)
i.e.
    x >= 0 & not sqrt x > a
as you rightfully observed. And no problem with antonyms.

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).

Another question what you do (or PVS) if such a formula occurs under
quantifier, and what about the definitional expansion? It is not clear
for me.

Andrzej