Wolfram Function Repository

Instant-use add-on functions for the Wolfram Language

Function Repository Resource:

 MetamathImport

Source Notebook

Import and work with a Metamath database

Contributed by: Mario Carneiro and Nikolay Murzin

ResourceFunction["MetamathImport"][src]

imports Metamath source code from src and returns a MetamathObject with various properties.

Details and Options

The src can be a File, URL or a String.
Options for ResourceFunction["MetamathImport"] may be one of the following:
"Verify"Falsewhether to verify theorem proofs or not
Proof verification raises Assert messages if verification fails.
The resulting MetamathObject has the following properties:
"Symbols"list of symbols
"Constants"list of constants
"Variables"list of variables
"Statements"list of statements
"Axioms"list of axioms
"Definitions"list of definitions (axioms starting with "df-")
"Theorems"list of theorems
"SymbolCount"number of symbols
"ConstantCount"number of constants
"VariableCount"number of variables
"StatementCount"number of statements
"AxiomCount"number of axioms
"DefinitionCount"number of definitions
"TheoremCount"number of theorems
"DependencyGraph"theorem proof dependency graph
"Proof", thmproof of a theorem as a list of steps
"ProofTree", thmproof tree of a theorem
"ExpandedProofTree", thmproof tree expanded down to axioms
"ProofGraph", thmproof graph of a theorem
"ExpandedProofGraph", thmproof graph expanded down to axioms
"TokenEventGraph", thmtoken event proof graph of a theorem
"ExpandedTokenEventGraph", thmtoken event proof graph expanded down to axioms
"SyntaxTree", stmtsyntax breakdown tree of a statement
"SyntaxDependencyTree", stmtsyntax dependency tree of a statement
"SimpleSyntaxTree", stmtsimplified syntax tree
"Import", srcparse and append new Metamath statements
ResourceFunction["MetamathImport"] special inputs:
"SetMM"set.mm database
"iSetMM"intuitionistic logic and set theory isetmm database
"Peano"Peano arithmetic peano.mm database
"NormMegillWolframAxioms"Norm Megill's proofs of Sheffer axioms (AxiomaticTheory["ShefferAxioms"]) from the Wolfram Axiom (AxiomaticTheory["WolframAxioms"])
"ASCIITable"ASCII replacement rules

Examples

Basic Examples (8) 

Import Metamath source code with a bunch of constants and a simple axiom:

In[1]:=
ResourceFunction["MetamathImport"][" $c = 0 S 1 $. wp $a = 0 S 1 $. "]
Out[1]=

Import a basic Metamath source code sample with 4 constants, 5 variables, 5 floating hypotheses, 1 axiom and 2 proved theorems:

In[2]:=
ResourceFunction["MetamathImport"][" $c ( ) -> wff $. $v p q r s t $. wp $f wff p $. wq $f wff q $. wr $f wff r $. ws $f wff s $. wt $f wff t $. w-> $a wff ( p -> q ) $. w->(->) $p wff ( r -> ( s -> t ) ) $= wr ws wt w-> w-> $. w(->)-> $p wff ( ( r -> s ) -> t ) $= wr ws w-> wt w-> $. "]
Out[2]=

Extract a proof of a theorem:

In[3]:=
ResourceFunction["MetamathImport"][ "\n$c ( ) -> wff $.\n$v p q r s t $.\nwp $f wff p $.\nwq $f wff q $.\nwr $f wff r $.\nws $f wff s $.\nwt $f wff t $.\nw-> $a wff ( p -> q ) $.\nw->(->) $p wff ( r -> ( s -> t ) ) $= wr ws wt w-> w-> $.\nw(->)-> $p wff ( ( r -> s ) -> t ) $= wr ws w-> wt w-> $.\n"]["Proof", "w(->)->"]
Out[3]=

Construct a proof tree:

In[4]:=
ResourceFunction["MetamathImport"][ "\n$c ( ) -> wff $.\n$v p q r s t $.\nwp $f wff p $.\nwq $f wff q $.\nwr $f wff r $.\nws $f wff s $.\nwt $f wff t $.\nw-> $a wff ( p -> q ) $.\nw->(->) $p wff ( r -> ( s -> t ) ) $= wr ws wt w-> w-> $.\nw(->)-> $p wff ( ( r -> s ) -> t ) $= wr ws w-> wt w-> $.\n"]["ProofTree", "w(->)->"]
Out[4]=

Construct a proof graph:

In[5]:=
ResourceFunction["MetamathImport"][ "\n$c ( ) -> wff $.\n$v p q r s t $.\nwp $f wff p $.\nwq $f wff q $.\nwr $f wff r $.\nws $f wff s $.\nwt $f wff t $.\nw-> $a wff ( p -> q ) $.\nw->(->) $p wff ( r -> ( s -> t ) ) $= wr ws wt w-> w-> $.\nw(->)-> $p wff ( ( r -> s ) -> t ) $= wr ws w-> wt w-> $.\n"]["ProofGraph", "w(->)->"]
Out[5]=

Construct a detailed syntax tree breakdown:

In[6]:=
ResourceFunction["MetamathImport"][ "\n$c ( ) -> wff $.\n$v p q r s t $.\nwp $f wff p $.\nwq $f wff q $.\nwr $f wff r $.\nws $f wff s $.\nwt $f wff t $.\nw-> $a wff ( p -> q ) $.\nw->(->) $p wff ( r -> ( s -> t ) ) $= wr ws wt w-> w-> $.\nw(->)-> $p wff ( ( r -> s ) -> t ) $= wr ws w-> wt w-> $.\n"]["SyntaxTree", "w(->)->"]
Out[6]=

Construct a simplified syntax tree:

In[7]:=
ResourceFunction["MetamathImport"][ "\n$c ( ) -> wff $.\n$v p q r s t $.\nwp $f wff p $.\nwq $f wff q $.\nwr $f wff r $.\nws $f wff s $.\nwt $f wff t $.\nw-> $a wff ( p -> q ) $.\nw->(->) $p wff ( r -> ( s -> t ) ) $= wr ws wt w-> w-> $.\nw(->)-> $p wff ( ( r -> s ) -> t ) $= wr ws w-> wt w-> $.\n"]["SimpleSyntaxTree", "w(->)->"]
Out[7]=

Introduce a new Metamath theorem by importing a source string and verifying it:

In[8]:=
ResourceFunction["MetamathImport"][ "$( This is the Metamath database demo0.mm. $)\n\n$( Metamath is a formal language and associated computer program for\n archiving, verifying, and studying mathematical proofs, created by Norman\n Dwight Megill (1950--2021). For more information, visit\n https://us.metamath.org and\n https://github.com/metamath/set.mm, and feel free to ask questions at\n https://groups.google.com/g/metamath. $)\n\n$( The database demo0.mm was created by Norman Megill. This is the version\n of 1-Jan-2004. $)\n\n\n$( !\n#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#\n Metamath source file demo0.mm\n#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#\n\n ~~ PUBLIC DOMAIN ~~\nThis work is waived of all rights, including copyright, according to the CC0\nPublic Domain Dedication. https://creativecommons.org/publicdomain/zero/1.0/\n\nNorman Megill - https://us.metamath.org\n\n$)\n\n\n$(\n#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#\n demo0.mm: An introductory formal system example\n#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#\n\n This file is the introductory formal system example described in Chapter 2 of\n the Metamath book.\n\n$)\n\n$( Declare the constant symbols we will use. $)\n $c 0 + = -> ( ) term wff |- $.\n\n$( Declare the metavariables we will use. $)\n $v t r s P Q $.\n\n$( Specify properties of the metavariables. $)\n tt $f term t $.\n tr $f term r $.\n ts $f term s $.\n wp $f wff P $.\n wq $f wff Q $.\n\n $( Define \"term\" (part 1 of 2). $)\n tze $a term 0 $.\n\n $( Define \"term\" (part 2 of 2). $)\n tpl $a term ( t + r ) $.\n\n $( Define \"wff\" (part 1 of 2). $)\n weq $a wff t = r $.\n\n $( Define \"wff\" (part 2 of 2). $)\n wim $a wff ( P -> Q ) $.\n\n $( State Axiom ~ a1 . $)\n a1 $a |- ( t = r -> ( t = s -> r = s ) ) $.\n\n $( State Axiom ~ a2 . $)\n a2 $a |- ( t + 0 ) = t $.\n\n ${\n min $e |- P $.\n maj $e |- ( P -> Q ) $.\n $( Define the modus ponens inference rule. $)\n mp $a |- Q $.\n $}"]["Import", " th1 $p |- t = t $= tt tze tpl tt weq tt tt weq tt a2 tt tze tpl tt weq tt tze tpl tt weq tt tt weq wim tt a2 tt tze tpl tt tt a1 mp mp $. ", "Verify" -> True]["Statements"][[-1]]
Out[8]=

Options (2) 

Verify (2) 

Verifying theorems expands proofs with more information:

In[9]:=
Cases[ResourceFunction["MetamathImport"][ "\n$c ( ) -> wff $.\n$v p q r s t $.\nwp $f wff p $.\nwq $f wff q $.\nwr $f wff r $.\nws $f wff s $.\nwt $f wff t $.\nw-> $a wff ( p -> q ) $.\nw->(->) $p wff ( r -> ( s -> t ) ) $= wr ws wt w-> w-> $.\nw(->)-> $p wff ( ( r -> s ) -> t ) $= wr ws w-> wt w-> $.\n", "Verify" -> False]["Statements"], "Theorem"[label_, _, _, proof_] :> label -> proof]
Out[9]=
In[10]:=
Cases[ResourceFunction["MetamathImport"][ "\n$c ( ) -> wff $.\n$v p q r s t $.\nwp $f wff p $.\nwq $f wff q $.\nwr $f wff r $.\nws $f wff s $.\nwt $f wff t $.\nw-> $a wff ( p -> q ) $.\nw->(->) $p wff ( r -> ( s -> t ) ) $= wr ws wt w-> w-> $.\nw(->)-> $p wff ( ( r -> s ) -> t ) $= wr ws w-> wt w-> $.\n", "Verify" -> True]["Statements"], "Theorem"[label_, _, _, proof_] :> label -> proof]
Out[10]=

Verify Norm Megill's proofs of Sheffer axioms using the Wolfram axioms:

In[11]:=
ResourceFunction["MetamathImport"]["NormMegillWolframAxioms", "Verify" -> True]["Statements"][[{"T1", "T2", "T3"}]]
Out[11]=

Neat Examples (2) 

Import the SetMM database and explore various visualizations of its theorems:

In[12]:=
mm = ResourceFunction["MetamathImport"]["SetMM"]; // AbsoluteTiming
Out[12]=
In[13]:=
mm["ProofGraph", "pythag"]
Out[13]=
In[14]:=
mm["SimpleSyntaxTree", "pythag"]
Out[14]=
In[15]:=
mm["SyntaxDependencyTree", "pythag"]
Out[15]=
In[16]:=
mm["TokenEventGraph", "2p2e4"]
Out[16]=
In[17]:=
mm["ProofTree", "pm1.2"]
Out[17]=

Norm Megill's proofs of the Sheffer axioms from the Wolfram Axiom:

In[18]:=
nm = ResourceFunction["MetamathImport"]["NormMegillWolframAxioms"]
Out[18]=
In[19]:=
nm["SyntaxTree", "T3"]
Out[19]=
In[20]:=
nm["ProofGraph", "T3"]
Out[20]=
In[21]:=
nm["SimpleSyntaxTree", "T3"]
Out[21]=

Publisher

N. Murzin

Version History

  • 2.1.0 – 17 January 2025
  • 2.0.0 – 07 March 2022
  • 1.0.0 – 21 September 2020

Source Metadata

Related Resources

License Information