Description of HF and Mizar theories

by Brown, Thursday, September 24, 2020, 11:12 (437 days ago)

Last month I wrote two documents describing the HF theory (built into Proofgold) and the Mizar theory. Both of these are set theories. HF is essentially at the level of Mac Lane set theory (without choice). In principle that's enough to do mathematics (because at higher types one can define the reals and sets of reals and so on), but it's significantly weaker than ZF. The Mizar theory is (higher-order) Tarski-Grothendieck set theory, with the axioms formulated following Mizar's foundation. This is much stronger than ZFC and is a better target for formalizing mathematics.

Here is the description of the HF theory:

http://grid01.ciirc.cvut.cz/~chad/pfghf.pdf

Here is the discription of the Mizar theory:

http://grid01.ciirc.cvut.cz/~chad/pfgmizar.pdf