I think this proposition ought to be discussed here as it concerns development issues. It looks like an example of a pull request, which I know Makarius hates, and I’m starting to grasp why. I don’t like the idea of a relative newcomer wanting to make such fundamental changes in a logic definition.
But looking more closely, the specific proposal (regardless of the implementation) is excellent: it is simply an “at most one” quantifier, which we also need in Isabelle/HOL, and I’m wondering that I didn’t grasp the need for this 30 years ago. Any thoughts? Larry > Begin forwarded message: > > From: Georgy Dunaev <[email protected]> > Subject: [isabelle] Tiny minor backward-compatible changes to IFOL > Date: 26 April 2020 at 11:00:58 BST > To: [email protected] > > Hello! > > I've introduced additional quantifier and rearranged some simple theorems > in IFOL in similar fashion. > > https://github.com/georgydunaev/onlyonequantifier/blob/master/my_IFOL.thy > > I just thought that it would be elegant to have E!x.P(x) as a Ex.P(x) and > !x.P(x), wouldn't be it? :) Moreover, this kind of definition is considered > to be "safe" later.(Why?) You may ask me to make additional changes if you > find that something is worth doing. > > Kind regards, > Georgy Dunaev _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
