On Wed, May 30, 2012 at 8:19 AM, Bill Richter <rich...@math.northwestern.edu> wrote:
> BTW Makarius seemed to say on the Isabelle group that Mizar is exactly > FOL with some automation to relieve the tedious parts of FOL. Mostly yes. It is (a bit strengthened) ZFC/FOL with small amount of second-order automation to handle things like infinite axiom/theorem schemes and Fraenkel terms (which behave quite a bit like lambda abstractions). The main difference to HOL is that "weird sets" (like von Neuman ordinals) are part of the ZFC universe, which is (at least by default) prevented by the strong type discipline in HOL. HOL's (type-constrained) higher-order functions map to first-order citizens of ZFC. For practical purposes, there does not seem to be much difference. An overwhelming part of both systems is first-order reasoning. Josef ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
