Email Gateway (Aug 22 2022 at 21:12): Email Gateway (Aug 22 2022 at 21:12):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
Recently, I found myself spending more and more time experimenting with
"ZFC in HOL". While most of my experiments are "work in progress", I was
able to compile a certain number of further foundational results that I
found useful when reasoning about small classes (binary relations, partial
functions or correspondences, infinite Cartesian products and other
operations on indexed families, finite sequences or lists) in an
independent development that I consider to be in a reasonably mature state.
In particular, I have tried (with moderate success) to (heuristically)
train the classical reasoner and simplifier for most expected commonly
occurring patterns.
I have made the aforementioned development publicly available from my
repository: https://gitlab.com/mikhail.chekhov/zfc_hol_foundations.
Perhaps, someone else will also find it useful. Also, naturally, I always
appreciate constructive feedback on my work.
As a side note, I found it particularly enjoyable to do applied
formalization work within "V" in "ZFC in HOL". Somehow, with this approach,
all concepts can be transferred from textbooks as they are written without
the need to invent new patterns around the type theory. Of course, in this
sense, it is not too different from Isabelle/ZF, but it has all the
advantages of being (potentially) interfaced/integrated with all other
utilities developed specifically for HOL (e.g.
transfer/function/inductive/code generation/etc).
Thank you,
Mikhail Chekhov
Email Gateway (Aug 23 2022 at 08:26):From: Lawrence Paulson <lp15@cam.ac.uk>
I am very glad to hear that people are taking advantage of my AFP entry. So I had better give notice that some changes are underway, some of them already visible in the development version, which will become part of the release version later in 2020. Some of these changes are incremental, others are significant.
The main change involves generalising the notion of an order type to relations involving any type rather than simply type V. This requires generalising the notion of a small set to arbitrary types: a set counts as small if it can be injected into the extension of a ZF set. Through the type class setup, any set of reals (for example) is trivially small. All this is already in the development version.
Further developments have not yet been uploaded. These include ordinal exponentiation, Cantor normal form and the notion of indecomposable ordinals.
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC