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



On 08/21/2016 12:21 PM, Lawrence Paulson wrote:
This question is a perfect example why I dislike the use of the word
âinconsistency" in connection with the work of KunÄar and Popescu.

Which word would you use then? I'm open to suggestions.

Probably most people associate that word with some sort of incorrect
logical reasoning. However, their work is concerned with Isabelle's
automatic detection and rejection of circular definitions.

I see. 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.

I don't find distinguishing between theorems stemming from axioms (and "pure" logical reasoning) and between theorems stemming from definitions particularly enlightening.

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.

Bests,
Ondrej




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