Re: [mizar] mizar and many-sorted first-order logic

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

Hi Jesse,

>What's the relation between the MIZAR logic and first-order logic?  It
>seems to me that it is indeed first-order logic, but how to show that?
>It seems to me that one idea would be to translate MIZAR into
>many-sorted first-order logic, and then use the fact that many-sorted
>first-order logic is equivalent to one-sorted first-order logic.  Or
>could it be that perhaps MIZAR is a true (non-equivalent) extension of
>first-order logic?

Maybe <http://www.cs.ru.nl/~freek/mizar/miztype.pdf> is relevant
for this question too?

Freek