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:
----------- [side conditions]
T' |- c = t
And if "c = t" allows you to prove False, then I call it an
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.
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.
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.
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.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and