Email Gateway (Aug 23 2022 at 08:49): Email Gateway (Aug 23 2022 at 08:49):From: Georgy Dunaev <georgedunaev@gmail.com>
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
Email Gateway (Aug 23 2022 at 09:05):From: Lawrence Paulson <lp15@cam.ac.uk>
Thank you for your email. I think you are right that a uniqueness quantifier is useful to have, for Isabelle/HOL as well as for FOL. We are likely to introduce such a thing. While we welcome contributions, they should normally take the form of small snippets of new material as opposed to entire revised files.
Larry Paulson
Last updated: Apr 19 2024 at 20:15 UTC