Email Gateway (Aug 22 2022 at 15:44): Email Gateway (Aug 22 2022 at 15:44):From: Ken Kubota <mail@kenkubota.de>
In this discussion on the Isabelle mailing list, I am missing the question
of the correctness of the small logical kernel that should guarantee
the correctness of the whole system.
Currently, the arguments presented so far seem to open up a false alternative
between logically correct (reliable) but small theorem provers (e.g., HOL Zero),
and large and practical but less reliable provers (e.g., Isabelle/HOL):
The other big provers (e.g. Coq) are similar in this respect. […]
HOL-Zero is a notable exception in targeting a market of potentially
malicious (ab-)users, but it is not a "big prover".
According to this idea, any reliable prover/checker must be small,
and any practical (and hence, large) prover isn't reliable.
But the concept of a small logical kernel that guarantees
the correctness of the whole system states exactly the opposite,
i.e., no matter how large and practical the software is, it remains reliable.
This concept is given up in arguments like
We do not have to work on the basis that "X has been proved, therefore X is true", but rather "We have been given a proof of X; Is it credible?"
which even seems to rhetorically downplay a desirable must-have (correctness)
as an annoying impediment to get rid of ("do not have to work on the basis").
In particular, transferring the responsibility for providing reliability (correctness)
from (verifying) the small logical kernel to either examining specific parts of
the formalized proof or estimating the credibility of the supplying person is questionable,
as even the best mathematicians from time to time fail at complex proofs:
Then we can look at any part of this proof where we have doubts. […]
The effort we choose to invest in this would depend on how important X is and how much we distrust the person who supplied the proof.
I do not see any alternative to providing a correct small logical kernel.
Preserving logical dependencies is part of (has to be guaranteed by) the logical kernel.
For this reason, I consider the following phenomenon as highly problematic
(and even as a failure of the logical kernel):
found this originally, but you can hide the ‘taint’ of a theorem by
going through a type class instantiation:
If a conditional can be stripped off so easily, it might be possible to obtain from
different conditionals two contradictory theorems, and hence, an inconsistency.
In a related discussion about this question on the Metamath mailing list I argued
in favor of introducing all non-logical axioms as conditionals (hence, Q0 and R0 have only five axioms)
in order to make the dependency explicit:
Third, the dependency is made explicit. If "the software tracks
axiom usage, as Metamath does", the task of tracking dependencies
is moved from the logic to the software, which I already, in another
context, criticized at Kunčar/Popescu's approach (which is
nevertheless legitimate as an auxiliary approach).
[…] Andrews' exercise X5308 […] stated and
formalized on pp. 151 ff. of
http://www.owlofminerva.net/files/formulae.pdf
is taken as an example where the dependency of the theorem
is make explicit, assuming the form
AC => theorem
since the (non-logical) Axiom of Choice was
introduced as a conditional, not as an axiom.
https://groups.google.com/d/msg/metamath/WwKPkCGoZkg/VSAVebXPCQAJ
Norman Megill presented a similar example:
It is certainly possible to prefix every theorem with "ZFC ->"
https://groups.google.com/d/msg/metamath/WwKPkCGoZkg/nvmXHUffCQAJ
I agree with Norman Megill that in certain practical contexts constantly displaying
the same conditional prefix may be redundant, but this is a question of the user interface
(which could, for example, replace the default prefix – e.g., "ZFC ->" – by a star "*"), but not a
matter relevant for the logical kernel, where this dependency should be made explicit.
As mentioned earlier, the Isabelle concept of axiomatic type classes as described and discussed in
https://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf
and introduced in
Prover-powered type classes were introduced by Nipkow and Snelting [28] in Isabelle/HOL
and by Sozeau and Oury [32] in Coq—they additionally feature verifiability
of the type-class conditions upon instantiation: a type T is accepted as a member
of the semigroup class only if associativity can be proved for its + operation.
http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-itp2015.pdf (p. 3)
is considered as a preliminary solution by me, since the same fact can be expressed
very naturally with the means of type abstraction (as suggested by Mike Gordon, see first quote at
http://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/
) and as argued and demonstrated at pp. 12, 362, 420 of
http://www.owlofminerva.net/files/formulae.pdf
Here, the fact that (o,XOR) is a group, formalized as
Grp o XOR
(p. 420) can be stated only after proving the three group axioms for (o,XOR),
and only after that, a general proof on groups (Uniqueness of the Group Identity Element, pp. 362 ff.)
can be instantiated (transferred) to the specific XOR group without having to carry out the proof again
(Uniqueness of the Group Identity Element of the XOR Group, pp. 420 ff.).
Coq is not suited for a comparison. It is very expressive (e.g., it has dependent types),
but there is profound criticism raised by Freek Wiedijk and John Harrison (and Josef Urban),
see section 3 of
http://doi.org/10.4444/100.111
and for an example the rule on top of p. 54 at
http://www.cl.cam.ac.uk/~jrh13/papers/joerg.pdf
which is very far from a natural expression of formal logic and mathematics.
The Isabelle documentation is discussed quite often.
Extensive documentation is available.
http://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf (p. 3)
The problem remains open: How can true expertise about how Isabelle
really works be reconstructed? We've seen a slow and steady decline in
the past 10 years, and myself writing hundreds of pages of documentation
helped only very little.
It is always claimed that the Isabelle documentation is ample, but unfortunately,
it is not logically structured, which makes the extent of the documentation
rather a disadvantage than an advantage.
For comparison, the HOL/HOL4 documentation provides a precise and quick introduction,
which allowed me to fully comprehend the logic, install the software and
carry out proofs very quickly. It has, as one would expect, a separate logic part
(Part III: The HOL Logic [Gordon and Melham, 1993, pp. 191–232]), available online at
http://freefr.dl.sourceforge.net/project/hol/hol/kananaskis-11/kananaskis-11-logic.pdf
and a very good guidebook which allows one to inspect the details of the system:
https://hol-theorem-prover.org/guidebook/
I already made suggestions for improvements earlier:
Although of course Isabelle/HOL is a very good piece of software, this precision is currently missing in my opinion.
The extension from classical HOL to Gordon's HOL can be found in section 11.7 (p. 261), as well as the
(single) extension from Gordon's HOL to Isabelle/HOL ("Isabelle/HOL goes beyond Gordon-style HOL
by admitting overloaded constant definitions") within a document of 13 chapters and 330 pages,
which makes it practically impossible to identify and locate important features and extensions of the core logic
within a reasonable amount of time:
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/isar-ref.pdf
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-October/msg00050.html
Essential information on the logic is hidden somewhere between many technical details,
and at the first glance I can't even see a reason for why the extension of the HOL logic is
described in the Isar reference, and not in the Isabelle/HOL reference.
With the HOL/HOL4 documentation, I was able to understand the logic and study
the details of the proof technology within 24 hours (see example files attached),
but with the Isabelle/HOL documentation, even after many months the details
are obscure. Moreover, the concept of a small logical kernel should be reflected
in the documentation by a separate logic part, as in the HOL/HOL4 documentation.
The Isabelle/HOL documentation currently doesn't conform to this clear standard
established by the original HOL system.
The emails quoted are attached below.
The full discussion is available at
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-July/date.html
Ken Kubota
http://doi.org/10.4444/100
Am 08.07.2017 um 20:59 schrieb Lawrence Paulson <lp15@cam.ac.uk>:
To protect against malicious intentions would turn Isabelle into a form of security software. But the guarantees we get from the latter are quite different from what we get from a formal proof. Ultimately security claims depend upon trusting a lot of complicated mechanisms, such as certificate authorities and cryptosystems. We are not a lot better off than when a model checker comes back with nothing.
However, we work with formal proofs, which can be examined, even interactively. We do not have to work on the basis that "X has been proved, therefore X is true", but rather "We have been given a proof of X; Is it credible?" Then we can look at any part of this proof where we have doubts. A devious user has many ways to try to fool us, but it's not so easy if he has to supply the full source code and we insist on legibility throughout. The effort we choose to invest in this would depend on how important X is and how much we distrust the person who supplied the proof.
Larry Paulson
On 8 Jul 2017, at 18:12, scott constable <sdconsta@syr.edu> wrote:
Isabelle does not protect against malicious intentions. It would require
a quite different system to do that, one that you won't like to
[message truncated]
Last updated: Nov 21 2024 at 12:39 UTC