Firstly, a natural deduction system in standard style is introduced for Nelson's para-consistent logic N4, and a normalization theorem is shown for this system. Secondly, a natural deduction system in sequent calculus style is introduced for N4, and a normalization theorem is shown for this system. Thirdly, a comparison between various natural deduction systems for N4 is given. Fourthly, a strong normalization theorem is shown for a natural deduction system for a sublogic of N4. Fifthly, a strong normalization theorem is (...) proved for a typed λ-calculus for a neighbor of N4. Finally, it is remarked that the natural deduction frameworks presented can also be adapted for Wansing's basic connexive logic C. (shrink)