2016/01/28 by Mario Carneiro, Carneiro, Mario · 1 citation
Computer Science · #03B22 #03B70 (Secondary) #03C95 (Primary) #Advanced Database Systems and Queries #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #I.2.3 #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1601.07699
openalex publication_date 2016/01/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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, \textsfZFC 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 \textsfZFC has a model), developing new independence proofs, and proving a form of Gödel's completeness theorem.