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

[Jesse Alama <alama@stanford.edu>]

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?

Jesse

-- 
Jesse Alama (alama@stanford.edu)