[FOM] Formalization Thesis
freek at cs.ru.nl
Thu Jan 10 05:50:34 EST 2008
>I would prefer if my posts were not so easily branded as
My excuses. I was criticising the opinion, not the person,
but even so I should have been more polite.
>I always thought that HOL and Isabelle rely on rather large
>amounts of type theory. Is it not the case that Isabelle
>essentially verifies the correctness of a proof by type
>checking? Please correct me if I am wrong.
Well, the basic inference rules of course handle typed terms,
so there is type checking going on there. But in these
systems there's nothing like a "proof term" that is being
type checked. (Once _can_ keep a "log" of the inference
process that one might consider to be the proof term, but
_that_ is not something that is being type checked.)
>I would say a system is based on type theory when types play
>an important role. For example, type constructions such as
>dependent products and sums of types should play an
>essential part, and there should be some relation with the
Isabelle and the other HOLs do not have have dependent
products and sums, nor are they based on
propositions-as-types. And Mizar essentially is first-order
logic with a single sort ("set"). It _does_ have dependent
types (which is a good thing), but it is even further away
from propositions-as-types as the HOL based systems.
But both the HOLs and Mizar do not having any problem
managing a large repository of formal mathematics.
More information about the FOM