Mathematical logic book that uses a proof assistant?

Question

I'm looking for an introductory book on mathematical logic that also discusses an implementation of its logic in a proof assistant. It seems to me this would be a great way to learn mathematical logic, since many concepts would become very clear and concrete when implemented in a computer program. But I have never seen such a book.

Preferably, the book would introduce the language of the proof assistant assuming no prior knowledge, and encourage the reader to use it at various points.

EDIT

I like the answers posted so far, and want to keep this open for a while to collect other recommendations in one place. However, after opening it, I also found the following excellent resources linked in this question, namely this list of resources and this book/compilation of notes by Jeremy Avigad. These resources seem like the type of thing I was looking for, and might be helpful to others who stumble on this post.

EDIT 2

One feature I would really like to see, which I haven't seen in the suggestions so far, is a book that also formalizes its meta-logic within a proof assistant. For example, I would love a book that proves (for example) a soundness theorem, and shows how such a proof could be implemented with a proof assistant.

Then again, I'd be surprised if such a resource exists, since no mathematical logic books (that I've seen) even mention the idea of formalizing meta-logic.

Answer 1

Try fundamental proof methods in computer science.it uses Athena as a proof assistant.It teaches both logic with language.

If you find that complex here a simple one- https://staff.washington.edu/jon/flip/www/userguide-nd.html It works with Python 2.7.

Answer 2

I would strongly recommend John Harrison's Handbook of Practical Logic and Automated Reasoning. The programming examples are more to do with how to implement proof assistants and decision procedures rather than how to use a proof assistant, but I think they meet your desire for implementations that clarify the key concepts. The examples are all given in the functional programming language OCaml.

Concerning the second edit: I think it is implicit in most texts on mathematical logic that the subject can be formalised in a suitable foundation system such as ZF. In the mathematical logic literature this becomes important and is made explicit in work on independence, In the world of proof assistants, self-formalisation with a view to increased assurance and understanding has been of intererest for many years. E.g., see this paper on self-verification of HOL and the references therein. I think the overall principles of a formalised meta-logic are probably more instructive than the fine details of the formalisation.

Answer 3

Books having an accompanying proof assistant for their logic is one way to look at it, but it also works the other way around: Most proof assistants implement some particular (usually constructive) logic and therefore books about the proof assistant are already books about this logic.

Here are some resources about Coq:

• Coq'Art [Bertot]

• Sofware Foundations Series [Pierce] In particular book 1 introduces constructive logic inside of Coq.

• Certified Programming with Dependent Types [Chlipala]

• Modeling and Proving in Computational Type Theory Using Coq [Smolka] is a still evolving draft of a book, which is the basis of a lecture and has accompanying Coq files on github. It's talking about the proof assistant in a less direct way.

The Lean Community site has a page on recommended learning resources.

And let's not forget the HoTT stuff:

• Homotopy Type Theory: Univalent Foundations of Mathematics There are libraries for several proof assistants (e.g. Coq) which allow you to work in HoTT.