Models for Metamath

Abstract

Although some work has been done on the metamathematics of Metamath, there has not been a clear definition of a model for a Metamath formal system. We define the collection of models of an arbitrary Metamath formal system, both for tree-based and string-based representations. This definition is demonstrated with examples for propositional calculus, $\text{ZFC}$ set theory with classes, and Hofstadter's MIU system, with applications for proving that statements are not provable, showing consistency of the main Metamath database (assuming $\text{ZFC}$ has a model), developing new independence proofs, and proving a form of Gödel's completeness theorem.

15 pages, 0 figures; submitted to CICM 2016

Cited by in corpus (2)

• A Survey on Theorem Provers in Formal Methods
• Metamath Zero: The Cartesian Theorem Prover