[question]: How to add an axiom?

[volisoft]

Metamath-lamp assumes using existing database. Does it support creating a new database from scratch or extending existing one with new axioms? Are there any tools available that support that? I know I can edit the database in any text editor, but it would be helpful to get a syntax check and all other advantages of a dedicated tool.

[expln]

Metamath-lamp doesn't support creating new databases from scratch, but you can use it to extend existing ones with new axioms.

As I know, other tools like mmj2 and yamma also can validate syntax. I would advise to post this question in Metamath Google Group mailing list to get more comprehensive answers for other tools.

To add new axioms to an existing database using mm-lamp do the following steps: 1) Load the existing database to mm-lamp. 2) Add new provable statements in the editor of mm-lamp. Mm-lamp will check syntax of the statements. It also will allow you to use its features for constructing and editing statements. Your statements will be marked as unproved, but you just ignore this. 3) Transfer the new statements as axioms from mm-lamp to the database (it can be done manually or automatically, see the demo below).

I made a demo video which demonstrates this process to explain it better. At the end of the video, an undocumented feature is used - "macros". It is still a work in progress. Its API may change. But hopefully I will document it soon.

https://drive.google.com/file/d/17hEdfgvX-hcA13qdAgNps_29dew065kB/view?usp=sharing

The database and JS code used in the demo:

$c |- term wff ( ) -> /\ \/ <= == < $.

$v x y z P Q $.

f1 $f term x $.
f2 $f term y $.
f3 $f term z $.
f4 $f wff P $.
f5 $f wff Q $.

s_ax1 $a wff ( P -> Q ) $.
s_ax2 $a wff ( P /\ Q ) $.
s_ax3 $a wff ( P \/ Q ) $.
s_ax4 $a wff ( x <= y ) $.
s_ax5 $a wff ( x == y ) $.
s_ax6 $a wff ( x < y ) $.

ax0 $a |- ( ( x <= y ) \/ ( y <= x ) ) $.
ax1 $a |- ( ( ( x <= y ) /\ ( y <= x ) ) -> ( x == y ) ) $.
ax2 $a |- ( ( x <= y ) -> ( ( x < y ) \/ ( x == y ) ) ) $.
ax3 $a |- ( ( ( x <= y ) /\ ( y <= z ) ) -> ( x <= z ) ) $.

temp1.stmts.map((s,i) => `ax${i} $a ${s.cont} $.`).join('\n')

async function exportStatementsAsAxioms() {
    const editorState = (await api.editor.getState()).res
    const axiomsStr = editorState.steps.map((s,i) => `ax${i} $a ${s.stmt} $.`).join('\n')
    navigator.clipboard.writeText(axiomsStr)
    api.showInfoMsg("Axioms are copied to the clipboard.")
}

const macros = [
    {
        displayName:'Export statements as axioms',
        run: exportStatementsAsAxioms
    },
]

return macros

[volisoft]

This is very helpful. Thank you so much!