Email Gateway (Aug 18 2022 at 20:22): Email Gateway (Aug 18 2022 at 20:22):From: gottfried.barrow@gmx.com
From: Re: [isabelle] rigorous axiomatic geometry proof in Isabelle
On 5/30/2012 11:12 PM, Bill Richter wrote:
...Let me make a rudimentary FOL point:
I think writing down strict axiomatic FOL proofs would really be
tedious because e.g. you have manually substitute variables every time
you want to use an axiom.
(Preliminary Comment): In my mind, I'm doubting that the so-called
first-order language of Zermelo-Frankael set theory does in fact give
one the ability to completely state and prove set theory as a
first-order language, primarily because of the absence in the symbols
of FOL to name constants in relation to FOL formulas. This sentence,
however, should be ignored, since I'm sitting on a question about that.
Listing the books below is the purpose of this reply.
Also, as you may have observed on hol info, I know next to nothing
about HOL... Where is a good place to learn about HOL?
I am a "book collecting" step ahead of you when it comes to learning
Isabelle/HOL, which I consider necessary to use Isabelle. My primary
interest is not in HOL but in the first-order language of ZF sets.
However, it's occurred to me that Isabelle/HOL can probably be used as a
meta-language to implement any object-language that I'll be interested
in. Additionally, and maybe of more importance, is the need in
mathematics for a solid implementation of a number system. I gather that
implementing a number system that's useful in a theorem prover is a very
difficult thing to do, and it appears that the Isabelle group has put
put a whole lot of work in doing that in Isabelle/HOL. It also appears
that most of the tool support and code development is going into
Isabelle/HOL.
Anyway, no one has told me this, but it appears that to understand
Isabelle/HOL in depth, you need to understand a combination of subjects:
1) Natural deduction logic
2) Lambda calculus
3) Typed lambda calculus, some of it coming from a non-constructivist
viewpoint
4) The ML programming language
5) The meta-logic of Isabelle/Pure
As to the minimum a person needs to know to be successful with Isabelle,
I don't know what that is. Whatever the minimum is, I'm not there yet.
Below are a list of books and documents that I've found. I don't provide
links to Amazon because the Amazon URLs get long, and the list server
converts all HTML links to the actual URL.
-----NATURAL DEDUCTION LOGIC---
NOTE: You won't find much natural deduction in logic books written by
mathematicians. They primarily use truth-table based logic.
"Proof and Disproof in Formal Logic", by Richard Bornat (Amazon)
This books is what I'm working through. Some of it's written like
"An Idiot's Guide to Natural Deduction", but it's still good,
and there's
the Jape prover for doing some natural deduction exercises.
http://www.cs.ox.ac.uk/people/bernard.sufrin/personal/jape.org/
"Mathematical Logic", by Ian Chiswell & Wilfrid Hodges (Amazon)
Covers natural deduction, but it also hits on a related logic,
sequent calculus, that gets
referred to in the Isabelle literature.
"Logic for Computer Science", by Jean H. Gallier (Amazon)
More advanced. I use it to try and find unfamiliar terminology.
"Natural Deduction", by Dag Prawitz (Amazon)
One of the first books (or the first) on natural deduction. I
use it to try and find unfamiliar terminology.
"Logic for Computer Science", by Steve Reeves and Mike Clarke (Amazon)
Covers natural deduction, but also hits on "semantic tableaux",
which gets referred to in the Isabelle literature.
http://en.wikipedia.org/wiki/Method_of_analytic_tableaux
---LAMBDA CALCULUS & TYPED LAMBDA CALCULUS---
NOTE: I separated lambda calculus from typed lambda calculus because
there are books for typed lambda calculus that take a strong,
constructivist approach, and some of these books don't apply as much.
What you're looking for is simply typed lambda calculus.
"An Introduction to Functional Programming through Lambda Calculus", by
Greg Michaelson (Amazon)
Written to be "super friendly", it uses a combination of
pseudo-programming syntax and
lambda calculus syntax. It works through examples with an
obnoxious level of detail which
serve their purpose to drive the points in.
"Type Theory & Functional Programming", by Simon Thompson (Amazon)
Has intro chapters on propositional logic, first-order logic, and
lambda-calculus. It
ties together logic, lambda-calculus, and functional programming,
and it emphasizes
types as proofs, and proofs as types.
"Basic Simple Type Theory", by J. Roger Hindley (Amazon)
A more formal, mathematical treatment. Gets to typed lambda
calculus fairly fast.
"Lambda-Calculus and Combinators - an Introduction", by Hindley & Seldin
(Amazon)
Has some of the same material as Hindley's books above, but has
too much on
combinatory logic.
"Foundations of Functional Programming", by Lawrence Paulson
A quick summary of lambda calculus.
http://www.cl.cam.ac.uk/~lp15/papers/Notes/Founds-FP.pdf
"Introduction to Lambda Calculus", by Henk Barendregt & Erik Barendsen
(Amazon)
"Lambda Calculi with Types", by Henk Barendregt (Amazon)
"Types and Programming Language", by Benjamin C. Pierce (Amazon)
"Lecture Notes on Lambda Calculus", by Peter Selinger
http://www.mscs.dal.ca/~selinger/papers/lambdanotes.pdf
---ML PROGRAMING LANGUAGE---
NOTE: The great thing about learning ML is that you can do your little
code snippets in Isabelle. Just use the command "ML{* ...code... *}".
"ML for the Working Programmer", 2nd, by Larry Paulson (Amazon)
"Programming in Standard ML '97", by Stephen Gilmore
http://homepages.inf.ed.ac.uk/stg/NOTES/
"Introduction to Functional Programming", by Mike Gordon
http://www.cl.cam.ac.uk/~mjcg/Teaching/FuncProg/Notes/
"Programming in Standard ML", by Robert Harper
http://www.cs.cmu.edu/~rwh/smlbook/
"Notes on Programming Standard ML of New Jersey", by Riccardo Pucella
http://www.ccs.neu.edu/home/riccardo/research.html
"Elements of ML Programming", by Jeffrey D. Ullman (Amazon)
---META-LOGIC OF ISABELLE/PURE---
NOTE: I'll ask the list someday what documents explain the meta-logic,
but here's some docs that appear to explain the meta-logic to varying
degrees.
Paulson: http://www.cl.cam.ac.uk/~lp15/papers/refereed.html
Isabelle - The Next 700 Theorem Provers
The Foundation of a Generic Theorem Prover
Urban: http://www.inf.kcl.ac.uk/staff/urbanc/Cookbook/
The Isabelle Cookbook
Wenzel: http://www4.in.tum.de/~wenzelm/papers/
Isabelle/Isar - A Generic Framework for Human-Readable Proof
Documents
Isabelle/Isar - A versatile environment for human-readable formal
proof documents
From the Isabelle2012 release:
Old Introduction to Isabelle
The Isabelle/Isar Reference Manual
A Proof Assistant for Higher-Order Logic
---BEST BOOK I'VE FOUND SO FAR---
"Principles of Mathematical Analysis, with a Friendly Introduction to
Natural Deduction & Typed Lambda Calculus, and How to Implement
Mathematical Proof in Isabelle2012, for the Working Mathematician, 4th
Edition", by Walter Rudin (Amazon)
--GB
Email Gateway (Aug 18 2022 at 20:23):From: gottfried.barrow@gmx.com
This last part was supposed to be a joke on my part, but I forgot that
this is an international community, that Rudin's book is not a standard
textbook everywhere, that not everyone would know that it was first
published many years ago, and that not everyone would be aware that
Rudin is deceased.
--GB
Email Gateway (Aug 18 2022 at 20:25):From: Jens Doll <jd@cococo.de>
Hello Gottfried,
let me answer the subject partially: Besides of real world understanding
and learning by oneself there also some books which could help you
clarify your (an other people's) thinking. The basic ones are listed at
http://cococo.de/Context_IT_GmbH/index.jsp?content=columbo&detail=literatur
and are structured in a certain way. Sorry for missing translations ...
Jens
Last updated: Apr 20 2024 at 04:19 UTC