Regarding "tricks for constructing a corresponding natural deduction system given a set of Hilbert axioms": Constructing natural deduction systems corresponding to axiomatic propositional or first-order systems isn't too hard when most of the axioms have fairly clear 'meanings', but I think it gets a bit tricker with nonclassical logics. Pelletier & Hazen's Natural Deduction gives a good overview of some different types of natural deduction systems. See, in particular, §2.3, pp. 6–12, The Beginnings of Natural Deduction: Jaśkowski and Gentzen (and Suppes) on Representing Natural Deduction Proofs. I think that there are three types of natural deduction systems that should be considered (in order of increasing ease of translation from the natural deduction system to the axiomatic system): Gentzen-style; Fitch-style (Jaśkowski's first method); and Suppes-style (Jaśkowski's second method).
Gentzen-style Natural Deduction
Gentzen-style natural deduction use proof trees composed of instances of inference rules. Inference rules typically look like this:
$$
\begin{array}{c} A \quad B \\ \hline A \land B \end{array}\land I \qquad
\begin{array}{c} A \\ \hline A \lor B \end{array}\lor I \qquad
\begin{array}{c} [A] \\ \vdots \\ B \\ \hline A \to B \end{array}\to I
$$
A significant difference between axiomatic systems and Gentzen-style natural deduction is that intermediate deductions can be cited by any later line in an axiomatic system, but can only used once in a proof tree. For instance, to prove $(P \land Q) \land P$ from $P \land Q$ requires three instances of the assumption $P \land Q$ in a proof tree:
$$
\frac{\displaystyle
\frac{\displaystyle
\frac{[P \land Q]}{Q} \quad \frac{[P \land Q]}{P}}{Q \land P}
\quad
\frac{[P \land Q]}{P} }{
(Q \land P) \land P }
$$
There's no way to reuse the intermediate deduction of $P$ from $P \land Q$. A naïve translation of a proof tree into corresponding axiomatic deductions will probably be pretty verbose with lots of repeated work (but it would be easy to check for and eliminate redundant deductions in the axiomatic proof). A very nice benefit of these systems, however, is that it is very easy to determine where a rule can be applied, and whether a formula is "in-scope" for use as a premise. Fitch-style and Suppes-style systems are more complicated in this regard.
Fitch-style Natural Deduction Systems
Fitch-style natural deduction systems for propositional logic have a type of subproof for conditional introduction. These capture "Suppose $\phi$. … $\psi$. Therefore (no longer supposing $\phi$), $\phi \to \psi$.) Even in this simplest type of subproof, the natural deduction has proof-construction rules about how lines in subproofs may be cited (e.g., a line outside of a subproof can't cite lines within the subproof). Still, unlike proof trees, some reusability is gained. For instance, in the Barwise & Etchemendy's Fitch (from Language, Proof, and Logic), would simplify the proof by reusing the deduction of $P$ from $P \land Q$:
- $P$ by conjunction elimination with 1.
- $Q$ by conjunction elimination with with 1.
- $Q \land P$ by conjunction introduction with 2 and 3.
- $(Q \land P) \land P$ by conjunction introduction with 2 and 4.
Some presentations allow for conditional introduction from any line top-level line within a subproof. In these presentations, not only can intermediate deductions be reused, but entire subproofs:
- $P$ by conjunction elimination with 1.
- $Q$ by conjunction elimination with with 1.
- $(P \land Q) \to P$ by conditional introduction with 1–3.
- $(P \land Q) \to Q$ by conditional introduction with 1–3.
In the first-order case, not only are there subproofs for conditional introduction, but there are subproofs for introducing new 'temporary' individuals (e.g., generic instances for universal introduction, or witnesses for existential elimination). These subproofs require special rules about where the individual of concern may appear.
Kenneth Konyndyk's Introductory Modal Logic gives Fitch-style natural deduction systems for T, S4, and S5. In addition to a condtional introduction, these have modal subproofs for necessity-introduction, and those subproofs require special rules for reiterating formulae into the subproof. For instance, in T, only a modal formula $\Box \phi$ can be reiterated into a subproof, and when it does, the $\Box$ is dropped. That is, when $\Box \phi$ is outside a subproof, $\phi$ can be reiterated in (but only through one 'layer' of subproof). In S4, $\Box\phi$ can still be reiterated into a modal subproof, but the $\Box$ need not be dropped. In S5 both $\Box\phi$ and $\Diamond\phi$ can be reiterated into a modal subproof, and neither modality needs to be dropped.
The point to all this is that in the propositional case, many Hilbert-style axioms correspond nicely to Fitch-style natural deduction style rules, but it seems that the nicest cases are those for boolean connectives. E.g.,
$$ A \to \left( A \lor B \right) $$
and
$$ A \to \left( B \to (A \land B)\right) $$
turn into "left disjunction introduction" and "conjunction introduction" pretty easily. However, more complicated axiom schemata (such as what would be used for universal introduction, or modal necessitation) that really require new types of subproofs for good natural deduction treatment are trickier to handle nicely.
Suppes-style Natural Deduction Systems
There are, of course, other formalizations of natural deduction than Fitch's. Some of these might make for easier translation from axiomatic systems. For instance, consider a proof of $(A \to (B \to (A \land B))) \land (B \to (A \to (A \land B)))$. In a Fitch-style proof, the left conjunct, $A \to \dots$, would have to be proved in a subproof assuming $A$ containing a subproof containing $B$:
- $A \land B$ by conjunction introduction with 1 and 2.
- $B \to (A \land B)$ by conditional introduction with 2–3.
- $A \to (B \to (A \land B))$ by conditional introduction with 1–4.
Then another five lines are needed to get $B \to (A \to (A \land B))$, and an eleventh for the final conjunction introduction. In Suppes's system, this is shorter (eight lines) because any in-scope assumption can be discharged by conditional introduction, so we can "get out of the subproofs" in different orders:
- {1} $A$ Assume.
- {2} $B$ Assume.
- {1,2} $A \land B$ $\land$-introduction with 1 and 2.
- {1} $B \to (A \land B)$ $\to$-introduction with 3.
- {} $A \to (B \to (A \land B))$ $\to$-introduction with 4.
- {2} $A \to (A \land B)$ $\to$-introduction with 3.
- {} $B \to (A \to (A \land B))$ $\to$-introduction with 4.
- {} $(A \to (B \to (A \land B))) \land (B \to (A \to (A \land B)))$ $\land$-introduction with 5 and 7.
(Note: some implementations of Fitch's system allow this for conditional introduction as well. E.g., in Fitch from Barwise and Etchemendy's Language, Proof and Logic conditional introduction can cite a subproof that starts with an assumption $A$ and contains lines $B$ and $C$ to infer both $A \to B$ and $A \to C$.)
To use this approach, each inference rule must also specify how the set of tracked assumptions for its conclusion is determined based on the premises of the rule. For most rules, the assumptions of a conclusion are just the union of the assumptions of the premises. Conditional introduction is the obvious exception. This approach also specifies that only lines with empty assumption sets are theorems.
This "tracking" approach, though, can be used for other properties too. The same considerations apply: each rule must specify how the tracked properties of the conclusion are computed from the premises, and the proof system must define which sentences are theorems.
For instance, in a system for first-order logic, the set of new individuals (for universal generalization or existential elimination) can be tracked, with most rules giving their conclusion the "union of the premises' individuals", with existential elimination and universal introduction the exceptions. Theorems are those sentences with an empty set of individuals and an empty set of assumptions.
This approach works nicely for modal logics, too. A Suppes-style proof system for K, for instance, in addition to tracking assumptions, tracks a "modal context", which is a natural number or $\infty$. The modal context indicates how many "necessitation contexts" we're in (intuitively, how many times we should be able to apply necessity introduction to a formula). In terms of Kripke semantics, the modal context is how far removed from the designated world we are. Sentences without any assumptions have context $\infty$, corresponding to the $\vdash \phi / \vdash \Box\phi$ rule. The inference rules require that their premises have compatible modal contexts (i.e., all non-$\infty$ modal contexts are the same). The default modal propagation is that the context of the conclusion is the same as the minimum context of the premises. The exceptions are that $\Box$ introduction subtracts 1, and $\Box$ elimination adds 1. Theorems are those sentences that have no assumptions and modal context $\infty$.
- {1} (0) $\Box P$ Assume.
- {2} (0) $\Box (P \to Q)$ Assume.
- {1} (1) $P$ $\Box$-elimination with 1.
- {2} (1) $P \to Q$ $\Box$-elimination with 2.
- {1,2} (1) $Q$ $\to$-elimination with 3 and 4.
- {1,2} (0) $\Box Q$ $\Box$-introduction with 5.
- {2} (0) $\Box P \to \Box Q$ $\to$-introduction with 6.
- {} ($\infty$) $\Box(P \to Q) \to (\Box P \to \Box Q)$ $\to$-introduction with 7.
In Suppes-style proof systems, the question is no longer about reiteration rules, about about property tracking and propagation rules. The purposes are similar, but in practice, certain kinds of axiomatic systems might be easier to translate into one kind or another.
Best Answer
Are you looking for a book on Hilbert axiomatic systems in particular, or just a book on proof theory more generally? There are many different kinds of proof systems, apart from the axiomatic Hilbert-style systems. In particular, proof theory benefits most from the sequent calculus presentation. If you're only interested in Hilbert systems, then I don't know of any resources that focus exclusively on that. If you're just interested in proof theory, there's an array of books that would suit most of your needs.
The thing about proof theory books is that, most of the time, they focus mostly on two logics: classical and intuitionistic. Those, it seems, have been the most influential in developing the course of proof theory. Still, to understand proof theory for other logics, you need to understand some of the basics for proof theory in classical and intuitionistic logic first. Negri and von Plato's Structural Proof Theory is a good place to start. Takeuti's Proof Theory develops proof theory from a different angle, focusing on arithmetic and consistency proofs. For something a little faster paced, look at Troelstra and Schwichtenberg's Basic Proof Theory. All of these are written post-2000.
If you've got some understanding of sequent calculi, then the book you're looking for is definitely Greg Restall's An Introduction to Substructural Logics. This is a fantastic book (one of my favorites actually), and I keep going back to it again and again. Only the first 7 chapters talk about proof theory, but he talks about proof systems with fewer connectives, nonclassical proof systems, modal proof systems, etc., and gives plenty of good examples. The cool thing about the substructural viewpoint is that it's an amazingly elegant way to characterize a lot of nonclassical and many-valued logics in one fell swoop. Again though, to fully appreciate it, you should be sure you know some sequent calculus before reading this book.