Models for Metamath

TL;DR

This paper formalizes the concept of models for Metamath systems, providing a unified framework applicable to various representations and demonstrating its utility through multiple examples and applications.

Contribution

It introduces a clear definition of models for Metamath systems, bridging the gap in formal understanding and enabling new proofs and consistency results.

Findings

Defined models for tree-based and string-based Metamath systems

Applied models to propositional calculus, ZFC set theory, and MIU system

Enabled proofs of non-provability, consistency, independence, and completeness

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, $\textsf{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 $\textsf{ZFC}$ has a model), developing new independence proofs, and proving a form of G\"odel's completeness theorem.