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