Week 8: Other databases

The Metamath databases beside set.mm: intuitionistic logic, higher-order logic, New Foundations, quantum logic, Peano arithmetic, the MIU system, Laws of Form, and the third-party ones on GitHub.

26 April 2027

set.mm is one database among many. The set.mm repository’s page on verification calls set.mm and iset.mm “the primary databases under active development” and says “All other databases’ proofs are verified by one verifier (metamath.exe).”

The explorers on metamath.org#

iset.mm, the Intuitionistic Logic Explorer, lives in the same repository as set.mm. Intuitionistic logic is constructive: “we must build and exhibit concrete examples of objects before we can accept their existence,” and the law of excluded middle, (φ ∨ ¬ φ), “doesn’t always hold.” There is no double negation elimination either. iset.mm “adds (or substitutes) intuitionistic axioms for a number of the classical logical axioms of set.mm,” dropping set.mm’s ax-3. Its home page keeps a cross reference of set.mm theorems that iset.mm lacks, with the closest replacements; Wednesday’s lab works from that table.

hol.mm, the Higher-Order Logic Explorer: “an alternative approach to predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics. It is also called simple type theory.”

nf.mm, the New Foundations Explorer, created by Scott Fenton: “an alternative set theory to the Zermelo-Fraenkel set theory presented in the regular Metamath Proof Explorer,” descended from the set theory of Principia Mathematica.

ql.mm, the Quantum Logic Explorer: three sets of axioms, “the ortholattice axioms, the orthomodular law … and stronger axioms,” for a logic the page says nobody knows to be decidable.

Smaller files#

metamath.org’s other topics page lists Robert Solovay’s peano.mm, Peano arithmetic; and miu.mm, Hofstadter’s MIU-system, alongside big-unifier.mm and demo0.mm. The same page lists Naip Moro’s Laws of Form database, derivations of G. Spencer-Brown’s boundary algebra, which its own page calls “a non-trivial example of a system that requires, indeed is based on, the empty substitution.”

Third-party databases on GitHub#

Each described by its README: sctfn/metamath-nf, “New Foundations set theory developed in metamath”; digama0/dtt.mm, “Metamath database for dependent type theory”; tirix/q0.mm, “A Metamath library for the Q0 logic”; and Sylvain78/bourbaki_in_metamath, “Bourbaki coded in metamath.”

The definition exercise is due this week.

Read#

• Intuitionistic Logic Explorer, the sections “Overview of this work” and “How to intuitionize classical proofs”: what you need before Wednesday.
• How are the databases verified?: which databases get five verifiers and which get one.
• Laws of Form in Metamath: a whole system built on the empty substitution, in a few pages.