Re: [mizar] Formalizing undefinedness

["William M. Farmer" <wmfarmer@mcmaster.ca>]

Freek,

> So: does LUTINS (that's the name of the full IMPS logic, right?)
> support this kind of nonstrict predicate.  Or: does IMPS support it?

Yes, LUTINS is the logic of the IMPS theorem proving system.  LUTINS
does not technically include nonstrict predicates, but they can be
defined as "quasi-constructors" in IMPS.  Quasi-constructors are
user-defined, polymorphic operators that serve as global constants.
For example, there is a quasi-constructor "compose" that forms in any
theory the composition of two functions whose types match
appropriately.  =~ is system-defined quasi-constructor.

LUTINS does not have polymorphism, but effective polymorphism is
obtained in IMPS using quasi-constructors and the little theories
machinery.

Bill