I have recently been reading about first-order logic and set theory. I have seen standard set theory axioms (say ZFC) formally constructed in first-order logic, where first-order logic is used as an object language and English is used as a metalanguage.
I'd like to construct first-order logic and then construct an axiomatic set theory in that language. In constructing first-order logic using English, one usually includes a countably infinite number of variables. However, it seems to me that one needs a definition of countably infinite in order to define these variables. A countably infinite collection (we don't want to call it a set yet) is a collection which can be put into 1-1 correspondence with the collection of natural numbers. It seems problematic to me that one appears to be implicitly using a notion of natural numbers to define the thing which then defines natural numbers (e.g. via Von Neumann's construction). Is this a legitimate concern that I have or is there an alternate definition of "countably infinite collection" I should use? If not, could someone explain to me why not?
I think that one possible solution is to simply assume whatever set-theoretic axioms I wish using clear and precise English sentences, define the natural numbers from there, and then define first-order logic as a convenient shorthand for the clear and precise English I am using. It seems to me that first-order logic is nothing but shorthand for clear and precise English sentences anyway. What the exact ontological status of English is and whether or not we are justified in using it as above are unresolvable philosophical questions, which I am willing to acknowledge, and then ignore because they aren't really in the realm of math.
Does this seem like a viable solution and is my perception of first-order logic as shorthand for clear and precise English (or another natural language) correct?
Thank so much in advance for any help and insight!