Can we prove "induction on wffs" in a non-circular way? I've always had the question of whether formal logic, number theory, or set theory "comes first" in foundations, and I've seen questions asking this. However, I recently came to what I think is the main source of my worry in the form of a specific question.
My question is, is there a way to prove that method of induction on the construction of well-formed formulas works in a non-circular way?
I am okay with taking induction on natural numbers axiomatically on the basis that saying "the natural numbers satisfy induction" is part of what we mean when we talk about natural numbers. It is easy to imagine how we could prove induction on wffs from induction on natural numbers.
However, my main question is the following: How do we know we haven't presupposed induction on wffs in the process of proving that induction on wffs follows from induction on natural numbers? Can this be done in a non-circular manner?
In order to state the axioms of natural numbers or a set theory strong enough to emulate natural numbers, we need first-order logic. In first-order logic, there are a number of results such as the unique readability theorem and the theorem of recursive definitions on wffs that rely on induction on wffs. Do we need these results to define number theory and/or set theory?
My worry is that we need unique readability or recursive definitions to define number theory / set theory containing number theory, and since unique readability & recursive definitions rely on induction on wffs, it renders the proof that
$$ \text{induction on natural numbers}\implies\text{induction on wffs} $$
circular.
 A: It seems there are at least two ways to think about this.
First Way. Just because first-order logic is a language used to express the axioms of the natural number system, doesn't mean that the natural number system doesn't exist without first-order logic. First-order logic simply provides us with the syntax to express certain concepts about the natural numbers, but the properties of the natural numbers (such as induction) do not depend on the syntax they are expressed in.
This kind of thinking does not require any sort of Platonism. All you need is to accept the fact that concepts are not the same as the syntax used to express them. In this view, there is no problem or circularity of invoking another system (the natural number system) to prove things about the initial system (the system of first-order logic).
Second Way. Perhaps in spite of the point made above, you may insist that you really want to write out some kind of textbook that proceeds as linearly as possible. To you, every single thing should be constructed from previous things you used. In this case everything turns out to be perfectly okay as well, because you don't really need universal "for all" results about first-order logic to build $\mathsf{PA}_1$.
The two results I cited that rely on induction on wffs were the unique readability theorem and the theorem of recursive definitions on wffs. Both of these are simply not needed to describe $\mathsf{PA}_1$ and induction. When you do get to a point where you formalize induction, you can go back and begin proving things about the framework you were using that were true all along but didn't need them to be explicitly stated.
