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

From a logical point of view, there is no reason to go below the HOL standard,
according to which (in proof mode) "only consistency-preserving actions
(namely valid proof) can be performed" [Gordon/Melham, 1993, p. 258 f.].

Andrei Popescu found a quite adequate formulation saying that the (consistent) logic exists
independent of a particular implementation. Hence, if Isabelle/HOL is supposed to be a
manifestation of a consistent logic, it must be consistent, too. "Nonsensical" user data
should be allowed only in the form of hypotheses, which can be refuted by the logic (and,
hence, dealt with in a reasonable way), as shown previously for R0.

If we would allow weakening logical rigor by enabling (user) definitions to make the
logical system inconsistent, we could directly step back to Cantor's naive set theory,
and accuse Russell of being the malicious "who has studied the source code" of set theory,
claiming that Russell's paradox makes use of an "overtly nonsensical" definition.
Of course it is nonsensical (in formal logic and mathematics), but therefore it
shouldn't be expressible at all in the language of mathematics. This insight resulted,
as is well known, in type theory.

My suspicion is that declarations separated from definitions generally might cause
inconsistency. In order to experiment, I would need some hint how declarations of 
constants (accompanied with a latter definition) work in Isabelle 2016, as asked for at
as I couldn't find any information in the manuals about it.


Ken Kubota
doi: 10.4444/100

> Am 24.08.2016 um 12:35 schrieb Andrei Popescu <a.popescu at>:
> Dear Larry,
>>> We are talking about the danger - almost certainly realised - of misleading people.
> I don't see how severely (and artificially) lowering the standard of what we want from a logical system can help against the potential confusion. Let me restate the obvious: We want consistency not only of bare deduction (from the HOL axioms), but of deduction from the definitional theories (including constant and type definitions). This is not a complicated statement, and most users of this systems and of similar systems will agree on it.
> We did not have that in Isabelle/HOL---and this was hinted to in the reference manual, but in not very clear terms and few people knew about it. Today we have achieved this goal and it is documented in quite clear terms in the same reference manual, and people should know about it. What does not help is refusing to accept what we have already accomplished, *even as a principial goal for a logical system*.
> It should also be stressed, of course, that the modifications needed to achieve this goal -- a harsher check at definitions -- did not affect in any way the previous Isabelle developments, which is great, and indeed different from similar problems in other systems.
>>> The various issues involving Isabelle, Coq, PVS and other systems are all complicated in their details. Outside observes are probably not going to invest the time and effort necessary to investigate precisely what is going on in case case. They will regard these "inconsistencies" as roughly the same. So we are drawing a false equivalence between
>>> I. The prover incorrectly handles correct and meaningful definitions. Users, who have done nothing wrong, cannot complete their projects.
>>> II. Somebody who has studied the source code has devised a definition that is not meaningful and the prover fails to detect this. Nobody has ever used or wanted such a definition, because it is overtly nonsensical.
>>> It's wrong and misleading to give the impression that I and II are the same.
> There is no a priori notion of 'meaningful' definition, apart from what the system accepts. So yes, from the point of view of the logical system these situations must be treated in the same way, in particular taken equally seriously. And this while ignoring the unnecessary reference to that malicious 'somebody who has studied the source code' -- who happens to be named Ondrej and happens to have been working on something else when he discovered that. But you know very well from day one the story behind this discovery and its ordeals.
> Andrei

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