Return to Answer

• Isabelle/HOL to HOL-Light: http://www.cs.cmu.edu/~seanmcl/papers/modules.pdf
• HOL-Light to Isabelle/HOL: http://www.springerlink.com/content/m7621r5258r8n711/

• Isabelle/HOL to HOL-Light: http://www.cs.cmu.edu/~seanmcl/papers/modules.pdf
• HOL-Light to Isabelle/HOL: http://www.springerlink.com/content/m7621r5258r8n711/

Is there such a "dumb" system around? If yes, do formalization projects use it? If not, do they recognize the need and put the effort into developing it? Or do they have other means to make their systems trustable?

Isabelle, and Mizar have special facilities for making proofs more "human". The system for Isabelle is called Isar. These systems aren't for dummies, sadly; one really needs a bit of special training to master them. On the other hand, they are much better than the "apply-style" proofs that are commonly employed, since they conform much better to human intuition. There's a systems for Coq called Caesar that in its infancy, but I expect it will ultimately make Coq much easier to use.

In the case of systems that express higher order logic, I assume you are aware that all complete ordered field are isomorphic to one another? Isabelle/HOL happens to construct them using Cauchy sequences, and has in its library there is another formulation using Dedekind Cuts. HOL-Light formulates the positive reals using the limiting slopes of functions $f:\mathbb{N}\to\mathbb{N}$ and then constructs the full reals using a semi-ring completion. Since algebraically all of these formulations are isomorphic, in practice the details of them are hidden from the users.

The definitions should be chosen carefully - I don't want to dig through a particular construction of the reals from rationals to make sure that this is indeed the reals that I know.

I assume you are aware that all complete ordered fields are isomorphic to one another? Isabelle/HOL happens to construct them using Cauchy sequences, and has in its library there is another formulation using Dedekind Cuts. HOL-Light formulates the positive reals using the limiting slopes of functions $f:\mathbb{N}\to\mathbb{N}$ and then constructs the full reals using a semi-ring completion. Since algebraically all of these formulations are provably isomorphic, in practice the details of their construction are hidden from the users.

Is there such a "dumb" system around? If yes, do formalization projects use it? If not, do they recognize the need and put the effort into developing it? Or do they have other means to make their systems trustable?

Isabelle, and Mizar have special facilities for making proofs more "human". The system for Isabelle is called Isar. These systems aren't for dummies, sadly; one really needs a bit of special training to master them. On the other hand, they are much better than the "apply-style" proofs that are commonly employed, since they conform much better to human intuition. There's a systems for Coq called Caesar that in its infancy, but I expect it will ultimately make Coq much easier to use.

Moreover, HOL-Light has been designed by the author to exhibit relative self-consistency proofs, just like in set theory. You may read about them here: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.97.2210&rep=rep1&type=pdf

(Here he shows HOL-Light-Infinity has a model in HOL-Light, and HOL-Light has a model in HOL-Light+Grothendiek Cardinal)

They all require training to learn. However, for LCF style systems like Coq, Isabelle, and HOL-Light, its like programming languages - once you learn one, you've learned the principles necessary to understand all of them.

Isabelle, and Mizar have special facilities for making proofs more "human". The system for Isabelle is called "Isar". These systems aren't for dummies, sadly -- one really needs a bit of special training to master these systems. On the other hand, they are much better than the "apply-style" proofs that are commonly employed, since they conform much better to human intuition. There's a systems for Coq called Caesar that its infancy, but it might make Coq better.

In the case of systems that express higher order logic, I assume you are aware that all complete ordered field are isomorphic to one another? Isabelle/HOL happens to construct them using Cauchy-Sequences, and has in its library an equivalent formulation using Dedekind Cuts. HOL-Light formulates the positive reals using the limiting slopes of functions $f:\mathbb{N}\to\mathbb{N}$ and then constructs the full reals using a semi-ring completion. Algebraically, all of these formulations equivalent, so in practice how the reals are constructed does not matter.

The answer is complicated. Not all deductive systems have the same expressive power. Sets in ZFC are a special kind of object that one cannot construct in Higher Order Logic. To formulate set theory in Isabelle/HOL and HOL-Light use, one needs to postulate that a kind of object that makes true the axioms of Zermelo Fraenkel set theory exists (this is the route that Isabelle/HOLZF takes). On the other hand, one may embed HOL into ZFC without such difficulty - here is a paper where a translation system for Isabelle/HOL into ZFC is given using the theorem prover LF: http://kwarc.info/frabe/Research/RI_isabelle_10.pdf

Chantal Keller imported HOL-Light into Coq for a MSc thesis here: http://perso.ens-lyon.fr/chantal.keller/Documents-recherche/Stage09/itp10.pdf, but again the reverse is difficult. Coq has a much more expressive type system than HOL.

One cannot convert Mizar proofs to any other system because it is closed source and not based on an LCF system like the other provers :(

Moreover, HOL-Light has been designed by it's author John Harrison to exhibit relative self-consistency proofs, just like in set theory. You may read about them here: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.97.2210&rep=rep1&type=pdf

Here Harrison shows HOL-Light$-$Infinity has a model in HOL-Light, and HOL-Light has a model in HOL-Light+Grothendiek Cardinal.

They all require training to learn. However, for LCF style systems like Coq, Isabelle, and HOL-Light, its like programming languages: once you learn one, you've learned the principles necessary to understand all of them.

Isabelle, and Mizar have special facilities for making proofs more "human". The system for Isabelle is called Isar. These systems aren't for dummies, sadly; one really needs a bit of special training to master them. On the other hand, they are much better than the "apply-style" proofs that are commonly employed, since they conform much better to human intuition. There's a systems for Coq called Caesar that in its infancy, but I expect it will ultimately make Coq much easier to use.

In the case of systems that express higher order logic, I assume you are aware that all complete ordered field are isomorphic to one another? Isabelle/HOL happens to construct them using Cauchy sequences, and has in its library there is another formulation using Dedekind Cuts. HOL-Light formulates the positive reals using the limiting slopes of functions $f:\mathbb{N}\to\mathbb{N}$ and then constructs the full reals using a semi-ring completion. Since algebraically all of these formulations are isomorphic, in practice the details of them are hidden from the users.

The short answer is YES, the long answer is YES, but it's complicated. Not all deductive systems have the same expressive power. Sets in ZFC are a special kind of object that one cannot construct in Higher Order Logic. To formulate set theory in Isabelle/HOL and HOL-Light use, one needs to postulate that a kind of object that makes true the axioms of Zermelo Fraenkel set theory exists (this is the route that Isabelle/HOLZF takes). On the other hand, one may embed HOL into ZFC without such difficulty - here is a paper where a translation system for Isabelle/HOL into ZFC is given using the theorem prover LF: http://kwarc.info/frabe/Research/RI_isabelle_10.pdf

Chantal Keller has imported HOL-Light into Coq in her MSc thesis here: http://perso.ens-lyon.fr/chantal.keller/Documents-recherche/Stage09/itp10.pdf

Importing back from Coq is difficult. Coq has a much more expressive type system than HOL.

One cannot convert Mizar proofs to any other system because it is closed source, and does not have a small kernel one can use to produce proof code readable by other engines :(