metamath-data

Data base files for metamath

This package contains Metamath data base files for several formal theories. * set.mm– Logic and set theory database (see Ch. 3 of the Metamath book). * nf.mm – Logic and set theory database for Quine's New Foundations set theory. * hol.mm – Higher order logic (simple type theory) database. * iset.mm – Intuitionistic logic database. * ql.mm – Quantum logic database. * demo0.mm – Demo of simple formal system (see Ch. 2 of the Metamath book). * miu.mm – Hofstadter's MIU-system (see Appendix D of the Metamath book). * big-unifier.mm – A unification stress test (see comments in the file). * peano.mm – A presentation of Peano arithmetic by Robert Solovay.

cloud_download Downloads