Email Gateway (Aug 23 2022 at 09:11): Email Gateway (Aug 23 2022 at 09:11):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Joshua Chen/All,
This post is a reply to Joshua Chen’s comment in the following thread:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-May/msg00075.html.
However, I believe, it is best provided as an explicit thread, as it is
concerned exclusively with https://bitbucket.org/cezaryka/tyset/src and not
the main topic of my previous question.
Firstly, thank you for letting me know about this development. It is very
useful to know about it.
In this context, I have to mention that I have started a couple of personal
applied formalization projects around “ZFC in HOL”. However, I kept
encountering and trying to solve some of the more fundamental limitations
related to the interplay of logic/type theory/set theory and the existing
‘tools’ infrastructure for Isabelle/HOL (e.g., see
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-April/msg00071.html
and
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-April/msg00117.html,
but there are many other issues). Also, I have an ever-growing desire to be
able to consider larger and larger entities without sacrificing convenience
(e.g. in “ZFC in HOL” one needs to deal with “V set set”, “V set” and V if
one is to provide a notion similar to that of a conglomerate and operations
on conglomerates).
Having had a brief revision of the content of the repository, I am
converging on the conclusion that this development makes an attempt to
address many of the problems that I am struggling with at the moment (and
more) in a structured manner and with much support. It does feel that,
eventually, it will make my current efforts in “ZFC in HOL” redundant (in
fact, some of the theories I developed for “ZFC in HOL” are almost in 1-1
correspondence from the perspective of the content with what can be found
in https://bitbucket.org/cezaryka/tyset/src). Therefore, I have several
questions:
Would you consider contributions to the project from external entities,
such as myself? If so, what kind of workflow would you expect/prefer? Would
you agree to share your own plans for this development?
If I understand correctly, at the moment, there is no license attached
to the repository. To the best of my knowledge, this means that
non-contributors can not legally redistribute any part of the content of
the repository. Is this intended? Would you consider distributing the
content under an open-source license in the future? If so, when do you
anticipate to do so?
Regretfully, I was not able to build the content associated with either
master or dev. I tried both the latest Isabelle-dev and Isabelle2020 stable
release (the first error that appears is “exception FAIL NONE raised (line
161 of "General/scan.ML")” in String.thy in the first local_setup block).
Perhaps, I am not using the needed version of Isabelle? Otherwise, unless
the cause is apparent, I am sure I will be able to figure it out on my own:
there is no need to worry on my behalf (my time spent looking at the
content can still be measured in minutes at the time of writing this email).
Naturally, the development introduces a number of new axioms in addition
to the axioms of HOL. I am curious if anything can be said with confidence
about the consistency of the new system.
I liked the idea of the notion of an object provided in the repository.
However, it seems that there are two independent theories: Object.thy and
Object_Old.thy. Does this mean that the notion of the object, as specified
in Object_Old.thy, will be abandoned in favor of another entirely different
implementation (as opposed to extended/built upon into what is shown at the
beginning of Object.thy) that is not yet available?
Kind Regards,
Mikhail Chekhov
Last updated: Apr 16 2024 at 12:28 UTC