The paper "models for metamath" (https://arxiv.org/abs/1601.07699) works out the requirements for models of metamath databases. They tend to be rather abstract as metamath is fairly logic-agnostic; you can get more useful models if you add some axioms to make it more like FOL specifically. If you are looking for just the formal definition of metamath provability, the canonical reference is Appendix C of the metamath book (on which that paper builds).
On Fri, Mar 10, 2023 at 4:59 PM Denis Carnier <[email protected]> wrote: > Hi all, > > How delightful to see our tiny project find its way onto your mailing > list! I am one of the developers for Metamathix (Arthur Correnson < > [email protected]> being the other). The project is at its > infancy, but we already have a minimal implementation of a proof checker > (without parsing/output) that we hope to prove correct with respect to a > declarative specification or formal semantics for Metamath's underlying > logic. To this end, if there already exists a reasonable model for Metamath > then we'd love to hear about it. At present, we have proposed a reference > logic and semantics, but we are rather unsure if they make sense. > > Looking forward to hearing your thoughts, > Denis > On Monday, February 27, 2023 at 10:58:04 AM UTC+1 Thierry Arnoux wrote: > >> Hi David, >> >> Feel free to add it! >> >> >> On 26/02/2023 16:20, David A. Wheeler wrote: >> >> We have a list of Metamath tools on the website pages. Will you add it? >> If not, let me know and I will add it, I just don't want to duplicate >> effort. >> >> On February 25, 2023 3:26:02 PM EST, Thierry Arnoux <[email protected]> >> wrote: >>> >>> Hi all, >>> >>> FYI, I recently found out about Metamatix >>> <https://github.com/acorrenson/metamatix>, a verified implementation of >>> a metamath proof checker, written in Coq. >>> >>> I'm not sure how far the project goes, but it's probably of interest for >>> people in this group. >>> >>> BR, >>> _ >>> Thierry >>> >> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/5DBFBC50-D236-4A71-9F55-82392C457A1A%40dwheeler.com >> <https://groups.google.com/d/msgid/metamath/5DBFBC50-D236-4A71-9F55-82392C457A1A%40dwheeler.com?utm_medium=email&utm_source=footer> >> . >> >> -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/eaea1b13-6b52-4a1f-87a1-1f2d007d08dfn%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/eaea1b13-6b52-4a1f-87a1-1f2d007d08dfn%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSt8L-Mw__wLTedsrTEcBMAjebG1qZZHxC5fhcbfx36Dmw%40mail.gmail.com.
