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:
----------- [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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and