I refer to Stephen Cole Kleene, Mathematical Logic (1967 - Dover reprint : 2002). What are the "pedagogical benefits" (if any) of the presentation chosen by Kleene, mixing Natural Deduction and Hilbert-style ?
Propositional Calculus - at pag.33 he refers back to formulas 1a-10b of Th.2 pag.15, which are usual Intro- and Elimination- rules for propositional connectives "rewritten" as axiom schemata.
Predicate Calculus - at pag.107 he add two axiom schemata : $\forall x A(x) \rightarrow A(r)$ (the A-schema) and : $A(r) \rightarrow \exists x A(x)$ (the E-schema), and the two rules - the A-rule : from $C \to A(x)$ to $C \to \forall x A(x)$ and the E-rule : from $A(x) \to C$ to $\exists x A(x) \to C$ , with x not free in C.
Then (Th.21 pag.118) he proves as derived rules the four standard rules of Intro- and Elim- for quantifiers.
I think you are right to be a bit puzzled by Kleene's mode of presentation of FOL in his Mathematical Logic. He gives a Hilbert-style axiomatic proof system with an overlay of derived rules which look rather natural-deduction-like. That strikes us, now, as an odd way of proceeding.
Kleene did the same back in his wonderful 1952 Introduction to Metamathematics. Now, immense credit to him for recognizing -- relatively early, and ahead of the crowd -- that Gentzen's work on deductive systems was deeply important (and natural!). But my sense is that Kleene didn't fully appreciate the change of perspective that is involved in moving from a Hilbertian logistic system [regarding logic as a body of truths, to be systematised axiomatically] to a Gentzen deductive system [regarding logic as a body of inferential rules, so the key notion is not that of logical truth but of valid deduction]. And because he didn't fully appreciate the change of perspective, we get what now seems to be Kleene's strange device of starting with an axiomatic system and giving it a Gentzen-like superstructure.
Of course, it is all too easy to sound patronising with historical hindsight! So it is worth noting that e.g. John Corcoran can write "Three Logical Theories" as late as 1969 (Philosophy of Science, Vol. 36, No. 2 (Jun., 1969), pp. 153-177), finding it still novel and necessary to stress the distinctions between different types of logical theory. So don't get me wrong: I immensely admire Kleene 1952 in particular, which is still hugely worth reading. But yes, the way he presents FOL perhaps reflects a transitional stage in our understanding of the relations between different types of logical theory.