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

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi Jesse,

It is typed first-order logic, with some small second-order additions 
(schemes, fraenkel terms). Both the types and the second-order things are 
translated to untyped FOL by the MPTP translation, but the MPTP 
translation of schemes and fraenkels is "lazy": it only adds the 
first-order scheme instances which are needed in MML proofs, and only 
creates in FOL the fraenkels which are used in MML. If you are interested 
only in "theoretical" equivalence, then you can say that the resulting FOL 
translation is infinite (though still recursive). Switching to finitely 
axiomatized set theory (NBG) could fix the infinity even in practice, 
obviously for some price in efficiency of automated reasoning.

As for the question how to practically translate Mizar types to FOL, the 
most obvious way (used by MPTP) is relativization:

for X,Y being finite set, f being Function of X,Y holds f is Relation of X,Y

translates to

for X,Y,f holds finite(X) & finite(Y) & Function(f,X,Y) implies 
Relation(f,X,Y)

More ingenious translations to FOL are possible, see e.g. 
http://www.logic.at/ftp98/papers/dahn.ps.gz .

Best,
Josef


On Wed, 31 Oct 2007, Jesse Alama wrote:

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