Thanks to Samara, the Open Logic Text now includes a chapter covering proofs in a natural deduction system. The chapter, found in first-order-logic/natural-deduction, parallels the chapter on the sequent calculus closely. Two new tags have been introduced, prfSC and prfND, both are on by default. If on, the relevant chapter is included in the first-order logic part. The completeness proof refers to both or either, depending on these tags. I’ve also added a section in the incompleteness/arithmetization-syntax chapter which shows how to code and deal primitive recursively with natural deduction derivations. The upshot is that you now have a choice of which proof system to use, simply by setting tags. Add \tagfalse{prfSC} to only have natural deduction, and \tagfalse{prfND} to only include the sequent calculus as before. Please file an issue on GitHub if anything got broken, or if you find mistakes in the new material.