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



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?

Of course, Makarius, you are right to remind us that Isabelle/HOL is a complex software system and its reliability has many facets. Of course, Larry, you are right to remind us that often user definitions can fail to be faithful to the intended concepts. But please let me remind you (again) that these are both different points.

Andrei


________________________________
From: Lawrence Paulson <lp15 at cam.ac.uk>
Sent: 21 August 2016 21:31
To: Ondřej Kunčar
Cc: Ken Kubota; cl-isabelle-users at lists.cam.ac.uk; Andrei Popescu
Subject: Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by Kunčar/Popescu

You can see definitions that way, but then almost everything can be codified as an inference system.

Of course I am not criticising your work, it's a positive contribution. Everything we can do to catch user errors is constructive. Note also how sledgehammer warns you if it can prove your theorem directly from an inconsistency in your assumptions. And we also have nitpick to catch user errors in theorem statements. But there is a difference between failing to catch a user error and performing incorrect deductions.

Larry

> On 21 Aug 2016, at 20:41, Ondřej Kunčar <kuncar at in.tum.de> wrote:
>
> 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:
>
>     T
> ----------- [side conditions]
> T' |- c = t
>
> And if "c = t" allows you to prove False, then I call it an inconsistency.
>




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