I'm looking for a strict book/pdf about logic which discusses formal systems in great detail. I only know basic stuff. It should cover:
definitions (like $(\exists x \varphi\leftrightarrow\lnot\forall x\lnot\varphi))$ inside the formal system (what to take care of when making definitions in a formal system)
distinct variables (and that we can make a formal system without the concept of "free" variables)
substitutions (would be nice if most would be taken care of "inside" the formal system)
using classes in zfc in a way, that they can always be eliminated (with proof)
defining ordinal addition etc. "inside" the formal system and working with the definition "inside" the formal system.