Email Gateway (Aug 18 2022 at 14:43): Email Gateway (Aug 18 2022 at 14:43):From: fctk <fctk86@gmail.com>
Hello,
I'd like to use a proof assistant in order to formalize elementary
theorems from set theory. I think I just need some tool that
understands the rules of inference of natural deduction for
first-order logic.
Is Isabelle the right tool for me?
Thanks.
Email Gateway (Aug 18 2022 at 14:43):From: Makarius <makarius@sketis.net>
Yes, see Isabelle/ZF. This page by one of our users provides a nice
intro, and additional libraries: http://www.nongnu.org/isarmathlib
Makarius
Email Gateway (Aug 18 2022 at 14:44):From: Lawrence Paulson <lp15@cam.ac.uk>
Isabelle is certainly one of the best tools you could adopt for this purpose. Isabelle supports a number of different logics, including higher order logic (Isabelle/HOL) and axiomatic set theory (Isabelle/ZF).
It isn't immediately clear from your message whether by "set theory" you are referring to heavy-duty set theoretic concepts such as ordinals and cardinals, or only simpler ones like unions and power sets. The other crucial question is whether you want your set theory to be typed or not. Higher order logic is essentially first order logic extended with functions and a simple typed set theory. For untyped, heavy-duty set theory, choose Isabelle/ZF; otherwise, choose Isabelle/HOL.
Larry Paulson
Email Gateway (Aug 18 2022 at 14:44):From: Makarius <makarius@sketis.net>
On Mon, 15 Feb 2010, fctk wrote:
Thanks for your answer. Anyway I have a problem at installing
Isabelle/ZF in that, after having unpacked the bundle and ZF under
/usr/local, I can't run isabelle tty. It says:/usr/local/Isabelle2009-1/bin$ ./isabelle tty
Unknown logic "ZF" -- no heap file found in:
/home/francesco/.isabelle/heaps/Isabelle2009-1/polyml_x86-linux
/usr/local/Isabelle2009-1/heaps/polyml_x86-linuxIt tries to find ZF instead of HOL because I edited ISABELLE_LOGIC
variable in etc/settings.
Try "/usr/local/Isabelle2009-1/build ZF" first.
Also, why do I need an already built set theory? My goal is to write set
theory from scratch. I'd like to use only the rules of inference of
first order logic (natural deduction).
Depends what you want to do with it. Using existing formalizations will
help to get off the ground more quickly -- these things usually take a
couple of years to develop.
Makarius
Email Gateway (Aug 18 2022 at 14:44):From: fctk <fctk86@gmail.com>
Thanks for your answer. Anyway I have a problem at installing
Isabelle/ZF in that, after having unpacked the bundle and ZF under
/usr/local, I can't run isabelle tty. It says:
/usr/local/Isabelle2009-1/bin$ ./isabelle tty
Unknown logic "ZF" -- no heap file found in:
/home/francesco/.isabelle/heaps/Isabelle2009-1/polyml_x86-linux
/usr/local/Isabelle2009-1/heaps/polyml_x86-linux
It tries to find ZF instead of HOL because I edited ISABELLE_LOGIC
variable in etc/settings.
Also, why do I need an already built set theory? My goal is to write
set theory from scratch. I'd like to use only the rules of inference
of first order logic (natural deduction).
Last updated: Nov 21 2024 at 12:39 UTC