Email Gateway (Aug 18 2022 at 14:38): Email Gateway (Aug 18 2022 at 14:38):From: Bart Kastermans <Bart.Kastermans@Colorado.EDU>
I am trying to better understand how logics that come with Isabelle are
set up, and how to set up my own. Is there any good documentation on
this? Explaining the use of TrueProp, and say all the commands in the
first 150 lines of a file like IFOL.thy .
Thanks.
Best,
bart
Email Gateway (Aug 18 2022 at 14:38):From: Tobias Nipkow <nipkow@in.tum.de>
Hi Bart,
I would be interested why you feel it necessary to set up a new logic.
To get anywhere requires an enormous amount of ground work. I can
understand that as a mathematician you may not like HOL, but ZF might be
more to your taste - and although not as well developed as HOL, it is
still a lot better than nothing.
Best
Tobias
Bart Kastermans wrote:
Email Gateway (Aug 18 2022 at 14:38):From: Lawrence Paulson <lp15@cam.ac.uk>
Isabelle was of course designed for this purpose, but as nearly everybody wants to use higher-order logic, most of the development and documentation has gone in that direction.
The early papers on Isabelle might give you some useful background information; see http://www.cl.cam.ac.uk/~lp15/papers/isabelle.html
Unfortunately, the early documentation (which did devote some space to this question) is hopelessly out of date.
The file IFOL.thy begins with a lot of references to automated tools which have been made available to first-order logic. You will not need these immediately and they may not even be relevant to your logic.
IFOL.thy then introduces a type o of truth values for the formalism being defined. We do not of course identify this with the "real" type of truth values. The judgement Trueprop mediates between the two levels, and Trueprop(P) is most easily interpreted as "P == True".
Then, the logical constants are introduced. The inference rules governing them are then introduced as axioms. And that is it! You only need to do more if you want special syntax (which you can see in this file) or automation.
The discussion above presupposes that you are working in the natural deduction framework. To formalise a sequent calculus require some technical tricks, which you can see in the file Sequents.thy.
Larry Paulson
Email Gateway (Aug 18 2022 at 14:39):From: Makarius <makarius@sketis.net>
Section 2.3 of the isar-ref manual
http://isabelle.in.tum.de/dist/Isabelle/doc/isar-ref.pdf demonstrates the
"purity" of the Isar language by definining first-order logic and doing
some basic reasoning.
This is a nice example for everything, except the hairy tool setup.
Makarius
Email Gateway (Aug 18 2022 at 14:39):From: Bart Kastermans <Bart.Kastermans@Colorado.EDU>
My first priority is not to actually set up a new logic, but to understand
how this one is set up. I am working inside ZF, and am trying to
understand how the system works in the background. It seems to me that
knowing what these "incantations" really do to the system is important for
this. Also to learn to use the system more effectively. I am also
learning SML for this (and maybe to write some extensions at some point),
but I have not found a good entrance point into the code yet.
Btw, I do like HOL but the current project if formalizing a result from
set theory itself. Using ZF for this does seem more natural.
Best,
Bart
Last updated: Apr 25 2024 at 08:20 UTC