On Wed, 30 May 2012, Josef Urban wrote:
> 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.
It is a bit difficult to have discussions stretched over several mailing
lists ...
Bill has quoted me in a too restrictive sense: I did not say "exactly" FOL
about Mizar, but characterization of Mizar by Josef is fine for me.
Concerning Isabelle, I need to try again to work against the standard
misconceptions by most outsiders. There are at least 3 different
conceptual layers involved:
* Isabelle/Pure as framework for unrestricted natural deduction
(nothing said about "order" of the logic yet),
* Isabelle/Isar as proof language on top of the framework, and
* Isabelle/HOL as the main application environment, including extra
tools.
If you start identifying Isabelle/HOL with "Isabelle", and pretending that
it is basically just "FOL" anyway, than you won't understand Isabelle.
We should probably switch back to the other mailing list to work this out
further ...
Makarius
------------------------------------------------------------------------------
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
