Yes, these are concepts from the meta-theory, i.e. the language in which you speak about the formal logic you're defining. When you define, say, sets of formulas, or maps (i.e. functions) from atoms to truth values, these objects exist outside of the formal system (i.e logic) under discussion.
Now of course, you can ask how come we're talking about sets (and functions and other objects which are sets), when we're just defining the formal logic we'll use to axiomatize the set theory. The answer is that you have to start from somewhere; you can't start speaking if you don't already have a language. For this, you use the existing mathematics whose logical foundations are imperfectly formalized and intuitive. This trails off into deep philosophical issues, but you can look at it this way: before embarking on meta-mathematics, imperfectly formalized mathematics is the most rigorous logical tool available, and we're trying to "turn it against itself," to see what it has to say about its own foundations.
Does one need meta-theory to work from propositional logic to set theory? Can I safely ignore those parts (perhaps coming back later) if my goal is to learn do theory and not to say something about theory?
I have recently become interested in the foundations of math. I am interested in tracing the fundamentals of math in a path such as: propositional logic -> first order logic -> set theory -> measure theory. Does anyone have any resources (books, webpages, pdfs etc.) they would like to recommend?
This seems like it would be a popular activity among LWers, so I thought this would be a good place to ask for advice.
My criteria (feel free to post resources which you think others who stumble across this might be interested in):