Mathematical logic book that uses a proof assistant?

Solution 1:

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.

Solution 2:

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.