LAMP axiom/definition

[Sylvain Kerjean]

Is it possible to add an axiom or definition in lamp ? It seems in the editor, you can only edit a proof, but you can't add new definitions. Though lamp is able to read them from a database.

Did i miss something ?

[David A. Wheeler]

> On Jan 11, 2025, at 6:27 PM, Sylvain Kerjean <sylvain....@gmail.com> wrote:
>
> Is it possible to add an axiom or definition in lamp ? It seems in the editor, you can only edit a proof, but you can't add new definitions. Though lamp is able to read them from a database.

Metamath-lamp allows you to select multiple sources as input. It will then load them in order.

I usually create a small local file with additional axioms & definitions.
You can then load the "main" database up to where you want to start, then
load the other file with your additional axioms/definitions. You could also post that local file on the web,
and load it that way.

More info in the metamath-lamp guide here:
https://lamp-guide.metamath.org/#loading-source-metamath-databases-to-create-the-proof-context

--- David A. Wheeler

[Igor Ieskov]

That’s right, you cannot create axioms and definitions in mm-lamp. You can only edit/develop proofs. But that should not be a problem, because you can manually (using a usual text editor) add your new axioms and definitions to an existing database. Or, as David pointed out, it will be handy to keep new axioms in a separate file/files and load it/them together with the main database. In addition to the metamath-lamp guide, you can see an example of how you can organize files in this video https://drive.google.com/file/d/1B_hiEfuP8KE3L_6uTnfdD7wkiLP15IIp/view?usp=sharing . At 18:13 it is shown how to load two files.

If you keep your axioms in a separate file, you can include the main database with the include statement, for example [ set.mm ], at the beginning of your file. Then you will be able to validate your file with a single command in metamath.exe. You will need to pass only your file to metamath.exe. Metamath.exe will automatically load all databases specified in include statements at the beginning of your file.

A similar question was posted on GitHub https://github.com/expln/metamath-lamp/issues/200 . There is an answer which shows that you still can use mm-lamp to validate syntax of your new axioms and provides more details on this topic.

-

Igor

[Sylvain Kerjean]

Thanks for your answer. I should have better looked at the settings "+" :)

Another question : I try to follow the 'Théorie des ensembles' by J.-L. Krivine, and often he states "E(x1,...xn)" as a wff where free variables are only among x1,..,xn.

Is this notion formalizable in metamath ? It occurs really a lot on all the FOL books i read.

[Steven Nguyen]

Yes, we have a definition for (effectively) “not free” (see https://us.metamath.org/mpeuni/df-nf.html and (especially note 3) of https://us.metamath.org/mpeuni/mmset.html#distinct)

so one could negate this definition and get “free”. In practice for metamath, substitution is by default allowed, so “not free” becomes the proven thing. I don’t think I’ve ever seen a use for the negation of not free, and I’ve tried.

On Jan 14, 2025, at 10:01 AM, Sylvain Kerjean <sylvain....@gmail.com> wrote:

Thanks for your answer. I should have better looked at the settings "+" :)

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/dddccc71-655e-4c02-8761-77767a7de681n%40googlegroups.com.