*To*: Makarius <makarius at sketis.net>, Lawrence Paulson <lp15 at cam.ac.uk>, Ondřej Kunčar <kuncar at in.tum.de>*Subject*: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by Kunčar/Popescu*From*: Andrei Popescu <A.Popescu at mdx.ac.uk>*Date*: Tue, 23 Aug 2016 08:33:26 +0000*Accept-language*: en-GB, en-US*Authentication-results*: spf=none (sender IP is ) smtp.mailfrom=A.Popescu@mdx.ac.uk;*Cc*: Ken Kubota <mail at kenkubota.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <f6d15502-4303-1953-ecf4-ab49e4d476f3@sketis.net>*References*: <CDD6C40D-96BE-46B5-99F1-C9C35A8CE6D6@kenkubota.de> <C5CAD6F5-6760-4704-A5CF-89C0FB06F053@cam.ac.uk> <9f07313f-afdc-aeb1-a51f-52bf84a7421e@in.tum.de> <7CE7A9FB-7DF1-41D6-9305-EA1A81107E3D@cam.ac.uk> <AM3PR01MB131338D89E41C0FC70D40C1EB7E80@AM3PR01MB1313.eurprd01.prod.exchangelabs.com>, <f6d15502-4303-1953-ecf4-ab49e4d476f3@sketis.net>*Spamdiagnosticmetadata*: NSPM*Spamdiagnosticoutput*: 1:99*Thread-index*: AQHR+wAi81lsNUW2qk6xB9kUTOFQsqBTNX0AgACcoICAAA3pAIABwWc7gACKSACAAAQ6Jw==*Thread-topic*: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by Kunčar/Popescu

I find it very dangerous for the theoretical progress in our area to refuse to accept the existence of an Isabelle/HOL logical system -- namely, a system that can be described mathematically by: (A) a mechanism for constant and type definitions (B) a set of rules of deduction This system exists as a mathematical entity independently of the implementation. (All my contributions to Isabelle/HOL so far, admittedly modest, have been based on this view -- and they have led to additions to the real system.) As soon as you accept this view (regardless of how you choose to model (A) and (B) in a reasonable way), you will see the following: You have incorporated the additional check that we suggested in the paper not only for 'adding a feature in order to amend such social problems and misunderstandings', but also for transforming an inconsistent logical system into a consistent one -- or, if you take the view that type *definitions* used to come with no consistency guarantees, this was the transformation of a logical system that officially allowed inconsistency into one that does not. And I am very happy for this. A recurrent objection that you are bringing to the above view is that Isabelle/HOL is built on top of a logical framework, which, according to you, makes the situation so complex that cannot be depicted by mortals. As I wrote before, this is a matter that is settled separately, by an adequacy proof -- so that we can ignore the logical framework when making theoretical advancements. Finally, let me note that, as far as I see, Larry's point is a distinct one: He considers that the consistency of all definitions, be they constant or type definitions, are in principle entirely the user's responsibility -- although he admits that it would be nice if the system 'nitpicked' them here and there. On the way, he reveals something that had never crossed my mind: that what, in our paper, we naively call a consistency theorem is in fact an enhancement of Nitpick. :-) My last email was addressing Larry's point. And note that I was not talking about 'a different system', but about a logical system in general. Andrei ________________________________ From: Makarius <makarius at sketis.net> Sent: 23 August 2016 08:35 To: Andrei Popescu; Lawrence Paulson; Ondřej Kunčar Cc: cl-isabelle-users at lists.cam.ac.uk; Ken Kubota Subject: 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

**References**:**[isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu***From:*Ken Kubota

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

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

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

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

*From:*Makarius

- Previous by Date: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
- Next by Date: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
- Previous by Thread: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
- Next by Thread: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu
- Cl-isabelle-users August 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list