[FOM] formal proofs

[Freek Wiedijk]

Dear Tim,

>>[...] and Flyspeck used HOL. Neither of them used ZFC [...]

I consider HOL a subsystem of ZFC.  That's not entirely
true, as the HOL systems (with the exception of IMPS?) have
a Hilbert choice operator, and ZFC hasn't.  But apart from
that, the HOL world is just the V_{omega+omega} fragment
of ZFC.  A countable tower of power sets starting from omega.

Given a choice function for that part of the ZFC world,
there is a very natural embedding of the HOL terms into ZFC.
And the existence of such a choice function is provable
in ZFC.

>Yes; perhaps I should have introduced not just a two-way
>distinction between "traditional foundations" and
>"HoTT foundations" but a three-way distinction between
>"traditional set-theoretic foundations," "traditional
>type-theoretic foundations" (including Coq and HOL) and
>"HoTT foundations"?

Despite its types, I would put HOL in the set-theoretic
division of this three-way classification.  In HOL there's
no Curry-Howard isomorphism whatsoever, everything is very
classical, and (as I already said) we're just in a subsystem
of ZFC,

John Harrison does consider HOL "type theory", though,
because of the lambda terms/types on the formula level.
But for me "type theory" implies the Curry-Howard isomorphism
and the constructivity/predicativity/intensionality that
naturally comes with that.

In that sense HoTT is very much type theory (it is
constructive/predicative/intensional, right?), and therefore
maybe formalizing a model of HoTT in ZFC and then just "doing
HoTT" in that doesn't really do it justice.  If would give
you all the nice homotopy theory, but only classically, and
in that sense would be different from working in actual HoTT.

Freek