Condensed version of set.mm?

[Ishan Murphy]

I'd like to use the set theory portion of set.mm as a starting point for another theorem database. However, set.mm is several megabytes large, and I don't need most of it. Has anyone made a condensed version of it that only includes the "essential" parts of propositional logic and set theory, or should I just copy the axioms and pick out the theorems I need?

[Jim Kingdon]

Have you looked into WRITE SOURCE set.mm/SPLIT ? That might be exactly what you are looking for in terms of propositional and predicate logic, and maybe a good start for set theory (in which the axioms are spread out over a larger section of the file).

[Mario Carneiro]

An easy thing you can do is start with set.mm and just start deleting large swaths of the database until you have what you want. Obviously you can always draw a line and delete anything after a certain point, and many theorems are independent of their neighbors so you can also trim it down more selectively. (This is how iset.mm was born.) You can also be more precise about this by using the "trace axioms" command (or an external script, it's not that hard) to find all the dependents of a chosen set of theorems.

--
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 on the web visit https://groups.google.com/d/msgid/metamath/E6690107-FA12-4897-9A3C-2F05E39B9850%40panix.com.