I would like to read a proof on the validity of natural deduction rules for first-order logic.
The papers I have found:
https://www.cs.cmu.edu/~fp/courses/atp/handouts/ch2-natded.pdf
and
https://homepage.univie.ac.at/christian.damboeck/ps06/clemente_nat_ded.pdf
introduce natural deduction and rely on intuition to understand these rules.
Is there a good account with a proof of the validity of natural deduction rules for first-order logic?
As I understand it is not possible to prove completeness of these rules for first-order logic since Gödel's non-completeness theorem. Am I right here?