NN (Jun 16 2026 at 08:18): NN (Jun 16 2026 at 08:18):Hi,
I want to build my own instance of a foundation of mathematics system. An old unpopular contestant for Principia Mathematica (Russelle and Whitehead). In this system for the foundation of mathematics, I have to stick to specific semantical categories and specific categorical grammar (brackets specify the category of the functors).
I would like to use Isabelle. starting with "import Pure", how can I "close" my system to only operate on my specific inference rules and axioms. But I can't let Isabelle bring anything into my deductive system that I don't define.
I found a package Nominal2 that does permutation instead of string-matching (or whatever the typical method is) to perform substitution. which was cool. I don't mind (yet) how substitution, for example, is performed. But it sort of has to be defined by me based on my categories.
Substitution is one of my inference rules; I also have detachment and a third that distributes variables within quantified formula/sentences.
I want a guarantee that "import Pure" would not interfere with my system. Because I have to take it pretty far to rebuild some mathematics I need later on. Is there another sort of "import" statement that might be more fundamental?
Last updated: Jun 26 2026 at 21:20 UTC