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



On 21.08.2016 21:41, OndÅej KunÄar wrote:

I guess the whole discrepancy boils down to the question if definitions are part of logical reasoning. For me, this is the case since you can view definitions as the following inference rule:

     T
----------- [side conditions]
T' |- c = t

And if "c = t" allows you to prove False, then I call it an inconsistency.

This is an important observation. In classic Cambridge HOL systems, adding definitions is an inference, but in Isabelle it is not: it is a certain extension of the theory with certain properties that might or might not be checked separately. That distinction of genuine inferences vs. specifications is important, because explicit theory contexts are central to Isabelle.

I don't find distinguishing between theorems stemming from axioms (and "pure" logical reasoning) and between theorems stemming from definitions particularly enlightening.
Maybe, but this is how Isabelle works. Note that Isabelle follows conventional logic text books in that respect. It was Cambridge HOL to make specifications an inference, probably due to technical reasons: there is only one big implicit theory in the ML environment that is augmented by rules of inferences.

It is always possible to discuss design decisions of existing systems, but it needs to be made clear in the text that this is done. Calling something broken (or "inconsistent"), while actually talking about a different system is leading to endless confusion.

While itâs right that they have
fixed this problem, nobody had actually exploited it, and the fix had
no effect on the millions of lines of Isabelle proofs in existence.
This is because the lack of checks was known over many years as something that is hardly relevant in practice. The feature addition of that additional check is theoretically nice, nonetheless.

You are right. As far as I know, this was the case for any problems (either implementation bugs or more substantial problems) that were found in other provers. But does this mean we should resign on inspecting and improving our kernels/logics? I hope not.
No, but here the situation was different: You started to look at the implementation for other reasons, found things that were surprising, and called them a "bug". Then I pointed to the documentation, that this "bug" was an official feature. That caused a lot of noise and confusion that still seems to be unsettled until today, even though "typedef" has been officially upgraded from an axiomatic specification to a definitional one in the implementation and documentation. (Both were consistent before and after that feature addition.)


    Makarius




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