Natural Deduction and the Isabelle Proof Assistant

Natural deduction is a popular way of teaching logic. It is also important in the philosophy of logic and the foundations of mathematics, in particular for systems of intuitionistic logic and constructive type theory, and it is used in proof assistants like Coq and Isabelle. The course provides a solid understanding of the basic methods and techniques in natural deduction as well as in the proof assistant Isabelle. It is innovative and truly cross-disciplinary because a simple approach to natural deduction is formalized in Isabelle: the syntax, semantics and the inductive definition of the proof system. The soundness of the proof system with respect to the semantics is then verified in Isabelle. Along the same lines the completeness of the proof system is formulated but not verified in the present course. The accompanying online Natural Deduction Assistant (NaDeA) http://nadea.compute.dtu.dk/ allows for interactive experiments with or without the installation of Isabelle.