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



On 23.08.2016 01:38, Andrei Popescu wrote:

Regardless of whether we consider definitions as part of the inference kernel, the following is self-evident:

A logical system, if it takes the trouble to guarantee anything, is supposed to guarantee that False cannot be inferred via the canonical 'safe' user interaction with the system -- which consists of performing definitions plus logical deduction.

Since nobody does bare deduction without (building on top of) definitions, having the former consistent is pointless without having the latter consistent. So what are we talking about here?
I am talking about how Isabelle works. You are talking about a different system. That is very dangerous, because people might pick up wrong ideas about the system, and then produce true non-sense.

The whole "typedef is axiomatic" versus "typedef is definitional in the sense of HOL set theory" affair from last year was about adding a feature in order to amend such social problems and misunderstandings. There was little practical relevance from a logical standpoint.

In Isabelle we have yet more ways to produce a bad theory content and then derive results that look wrong.


        Makarius





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