Re: [Metamath] LAMP axiom/definition (and freeness)

[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.kerjea...@gmail.com> wrote: 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. Le lundi 13 janvier 2025 à 17:23:30 UTC, David A. Wheeler a écrit : > 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 -- 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+unsubscr...@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/metamath/dddccc71-655e-4c02-8761-77767a7de681n%40googlegroups.com. -- 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+unsubscr...@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/metamath/29EEDEFE-EDE6-4FCD-A111-244A94ED5B6D%40gmail.com.