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:
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.
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?
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