This lecture concerns issues related to the Curry-Howard Isomorphism for predicate logic, mostly first-order logic and first-order arithmetic. We discuss the relationship between predicate logics and the corresponding propositional logics, obtained via dependency-erasing operators. Rather than showing new results, the lecture aims at explaining basic ideas and clarifying some issues which belong to the very fundamentals of the proof technology. In particular, we consider lambda calculi corresponding to predicate logic and arithmetic, an we point out the relation between strong normalization and proof extraction. These lecture notes are based in part on a joint work with Morten Heine Sørensen [23].