Teaching First-Order Logic with the Natural Deduction Assistant (NaDeA)

The natural deduction proof system 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 many proof assistants along with automatic proof methods like the tableaux procedure and the resolution calculus.

The natural deduction assistant (NaDeA) has been used for teaching first-order logic to hundreds of computer science bachelor students since 2015 [1, 2]. NaDeA runs in a standard browser and is open source software. Upon completion of a natural deduction proof the student obtains a formal proof in the interactive proof assistant Isabelle/HOL [3] of not only the correctness of the student’s natural deduction proof but also of the validity of the formula with respect to the classical semantics of formulas in first-order logic.

Our formalization of the syntax, semantics and the inductive definition of the natural deduction proof system extends work by Stefan Berghofer [4] and Melvin Fitting [5] but with a much more detailed soundness proof that can be examined and tested by the students. The corresponding completeness proof is also available but it is of course quite demanding.

We describe the main advantages and disadvantages of using an advanced e-learning tools like NaDeA for teaching logic. Furthermore we briefly survey related and future work. NaDeA can be used with or without installing Isabelle and is available online. URL Address: https://nadea.compute.dtu.dk/.