[isabelle-dev] Fwd: [isabelle] Tiny minor backward-compatible changes to IFOL

[Lawrence Paulson]

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 <georgedunaev at gmail.com>
> Subject: [isabelle] Tiny minor backward-compatible changes to IFOL
> Date: 26 April 2020 at 11:00:58 BST
> To: cl-isabelle-users at lists.cam.ac.uk
> 
> 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