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?
Alex Mobius (Oct 27 2026 at 17:24):Right - is there anything in Pure that interefres with your goals? Pure implements "natural deduction", which I think is probably unsuitable for linear logic as-is (although I am sure it can be adapted), but otherwise is a fairly small package: there is the meta-level modus-ponens [P ==> Q, P] ==> Q and the lambda-reduction (%x. F x) === F, and I think that's pretty much it. (Well, and the type system setup) If that is against your goals, you probably wouldn't get much use out of Isabelle anyway, since the whole Isar language is very oriented towards Pure.
Last updated: Nov 08 2026 at 20:15 UTC