There are several axiomatizations for number theory, group theory, and other theories represented in first order logic. Further, these theories are also representable in set theory such as $\sf ZFC$ or $\sf NBG$ and it got me thinking about reasoning about formal systems in formal systems.
Can we represent the theory (or meta-theory?) of first order logic or set theory inside first order logic or set theory the way we represent number theory inside first order logic or set theory? I assume its possible, and has been done before, but how is this usually done, and is there a good reference for using such axiomatizations? I'm interested in creating a formal system that models a formal system, so I can create formal proofs about the system that makes the formal proofs.
I'm thinking of predicates and functions that are definitions that assert that sentences that belong to the set of formulas of first order logic or set theory have certain properties or some such representation, similar to how the Peano axioms are definitions of predicates and functions that assert members belonging to the natural numbers have certain properties.