Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by Kunčar/Popescu

Dear Larry,

>> We are talking about the danger - almost certainly realised - of misleading people.

I don't see how severely (and artificially) lowering the standard of what we want from a logical system can help against the potential confusion. Let me restate the obvious: We want consistency not only of bare deduction (from the HOL axioms), but of deduction from the definitional theories (including constant and type definitions). This is not a complicated statement, and most users of this systems and of similar systems will agree on it.

We did not have that in Isabelle/HOL---and this was hinted to in the reference manual, but in not very clear terms and few people knew about it. Today we have achieved this goal and it is documented in quite clear terms in the same reference manual, and people should know about it. What does not help is refusing to accept what we have already accomplished, *even as a principial goal for a logical system*.

It should also be stressed, of course, that the modifications needed to achieve this goal -- a harsher check at definitions -- did not affect in any way the previous Isabelle developments, which is great, and indeed different from similar problems in other systems.

>> The various issues involving Isabelle, Coq, PVS and other systems are all complicated in their details. Outside observes are probably not going to invest the time and effort necessary to investigate precisely what is going on in case case. They will regard these "inconsistencies" as roughly the same. So we are drawing a false equivalence between

>> I. The prover incorrectly handles correct and meaningful definitions. Users, who have done nothing wrong, cannot complete their projects.

>> II. Somebody who has studied the source code has devised a definition that is not meaningful and the prover fails to detect this. Nobody has ever used or wanted such a definition, because it is overtly nonsensical.

>> It's wrong and misleading to give the impression that I and II are the same.

There is no a priori notion of 'meaningful' definition, apart from what the system accepts. So yes, from the point of view of the logical system these situations must be treated in the same way, in particular taken equally seriously. And this while ignoring the unnecessary reference to that malicious 'somebody who has studied the source code' -- who happens to be named Ondrej and happens to have been working on something else when he discovered that. But you know very well from day one the story behind this discovery and its ordeals.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.