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



Makarius wrote:

>> I just want to point out explicitly that I am no longer paying attention
to this very strange thread.
>> At the level of abstraction of the discussion, Isabelle is indeed
"inconsistent" and that is not going to change in the foreseeable future.


This is indeed a very strange thread -- and your backwards conclusion contributes to its strangeness. At the level of abstraction discussed here, that is, speaking of the logical system implemented in Isabelle/HOL, we are now (in 2016) talking about a logic proved to be *consistent*, not inconsistent. This level of abstraction assumes that we ignore what you call the back doors, and only focus on the purely logical mechanisms: type and constant definitions and HOL deduction.


Btw, even though they also deal with a very complex implementation, the Coq people do not have a problem speaking at this level of abstraction -- and in particular acknowledging any logic inconsistency violations arising from their definitional mechanism (as happened recently). Needless to say, they also don't have a problem reporting when these violations have been addressed. And they do use words like 'inconsistency' and 'fix'.


You show contempt for people's efforts to address such issues using proper and well-established logical concepts and terminology. And since you are speaking with the (deserved) authority of Isabelle's release manager, this is a big strategic mistake for Isabelle.



Andrei







        Makarius





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