[FOM] Formalization Thesis

[Freek Wiedijk]

Andrej:

>I would prefer if my posts were not so easily branded as
>nonsense.

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
>propositions-as-types "paradigm".

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.

Freek