For example, does every (introduction/elimination) of natural deduction encode some kind of desideratum about the proof system of natural deduction? This was suggested in this question, asking for motivation for a specific elimination rule.
In the comments of that post, it is suggested that there is a metalogical motivation for defining the inference rules of natural deduction. "Every (introduction/elimination) encodes some kind of desideratum about the proof system. E.g. ∧𝐼 encodes the desideratum that every normal proof of 𝐴∧𝐵 should consist of two proofs, one for 𝐴 and one for 𝐵. We have a ("derived") theorem, the normalization theorem, which ensures that we can normalize every proof, and hence that our system satisfies all the desiderata encoded in the rules." In my understanding this is saying that each rule is accompanied by a derived justification, in the form of a (meta-logical) theorem about the consistency or normalization of the system.
What are the metalogical desiderata for each rule of the natural deduction, and what metalogical proofs establish that each of these desires are indeed satisfied by the natural deduction.
Best Answer
Gentzen [1] kick-started the field of structural proof theory: the 1934 paper introduces natural deduction. In the paper he already noted that introduction rules essentially represent definitions of the logical symbols. Later on, Gentzen took this perspective much further in his work on the sequent calculus, where he associates to each proof of a given sentence a corresponding canonical (cut-free) proof whose last rule has predictable form, depending only on the principal connective or quantifier of the formula.
Cut-elimination allows us to prove that intuitionistic logic satisfies structural properties (what you'd call metatheoretic properties, many of them tellingly named after the connectives) such as the disjunction property (if there is a proof of $A \vee B$, there ought to be a proof of $A$ or a proof of $B$), the conjunction property (if there is a proof of $A \wedge B$, there ought to be a proof of $A$ and a proof of $B$) and consistency (there ought to be no proof of $\bot$), and corresponding to the BHK interpretation of the connectives. In Gentzen's sequent calculus, we can prove all of them the same way: by considering the last rule of a canonical proof, which has to be a right rule for the connective. E.g. to prove the conjunction property, we can consider a proof of $\vdash A \wedge B$: by cut-elimination, we can turn this proof into a canonical proof, which must then have the last rule
$$\frac{\vdash A\ \ \ \ \vdash B}{\vdash A \wedge B} \wedge\!R$$
so we indeed have proofs of $\vdash A$ and $\vdash B$ as desired. Similarly, we have consistency: if $\vdash \bot$ had a proof, it would have a cut-free proof, but it obviously has no cut-free proof (what would be its last rule?!). The rules enunciate the BHK-style desiderata: cut-elimination ensures that we indeed get the desiderata. One can play a very similar game in natural deduction, using Prawitz's [2] proof normalization technique (indeed the right rules of the former correspond to introduction rules of the latter, and left rules similarly correspond to elimination rules).
This should give you some idea about the desiderata corresponding to the rules of natural deduction, and the proofs that establish that each of these are indeed met. For a more thorough appraisal and philosophical discussion, check out Francez's book on Proof-theoretic Semantics [3], especially his discussions of inferentialism, and of Prior's tonk connective. If you're more interested in the technical details of normalization, Parwitz [2] or Chapter 4 of Dummett [4] are good starting points as well.
[1] Gerhard Gentzen, "Untersuchungen über das logische Schließen. I". Mathematische Zeitschrift 39 (2), 1934.
[2] Dag Prawitz, "Natural Deduction: A Proof-Theoretical Study", Dover Publications 1965.
[3] Nissim Francez, "Proof-theoretic Semantics", Studies in Logic 57, College Publications UK, 2015.
[4] Michael Dummett, "Elements of intuitionism", Oxford Logic Guides 39, Oxford University Press, 1977.