- How do mathematical formalists account for the unreasonable effectiveness of mathematics?
Formalism is internal to the mathematical system. It does not "leak out" of mathematics and "infect" the real world.
Mathematics was designed to match up with reality in many respects. Much of early mathematics flowed directly from geometry, which is clearly modeled on (a simplified version of) reality. Similarly, Newton (or Leibniz, depending who you ask) invented calculus for the purpose of modeling the laws of physics (in the case of Newton, whereas Leibniz seems to have had a more metaphysical interpretation of it).
But there are limits to this. If you try to use general topology to describe an iron beam, you're going to get a wildly incomplete understanding of how it will actually behave. This is because topology discards many basic assumptions of geometry, and is unable to properly account for the rigidity and strength of real-world materials. Mathematics is only successful in contexts where its axioms completely and accurately characterize the real world.
The formalist interpretation of mathematics does not mean that we simply choose a bunch of arbitrary rules at random, move symbols around in accordance with those rules, and somehow learn things about the real world. We make a deliberate choice to use symbols and rules that are, in some respect, congruent with our observations of reality. So long as we start with something that is physically representative, we will end up with something that is also physically representative. It really should not be very surprising that you can take a bunch of physically-grounded assumptions, churn them through a formalized deductive process, and come out with physically-grounded theorems on the other side.
Obviously, the choice of axioms, and the physical interpretation of theorems and other results, are both external to the mathematical process. So they need not avoid semantic reasoning which is incompatible with a purely syntactic (formalist) view of mathematics proper. The engineer or physicist slips in and out of formal, mathematical thinking as suits their requirements.
In short: Mathematics works to build bridges because we deliberately choose axioms that describe how bridges are observed to behave. If you choose a different set of axioms, you won't be able to build bridges very effectively, or at all. But either way, you will be doing mathematics. So asserting that mathematics is "unreasonably effective" at building bridges is pointing to the wrong part of the process. Mathematics is only effective when it is employed in concert with other information, which cannot reasonably be accounted for by formalism itself.
- How do mathematical formalists respond to ontology of "formal systems"?
This question feels a bit opaque to me, but I'll do my best to understand it. Formalism is (for the most part) opposed to platonism, so the response will generally be some variation of "mathematical objects aren't real." I've seen variations of these positions described in SEP:
- Mathematical statements have no inherent meaning whatsoever, so there is no ontology to account for.
- Mathematical statements are contingent on their axioms, which might be true in some concrete physical setting, so you get the ontology "for free" from that concrete setting.
- Mathematics is a game of make-believe. Mathematical objects are imaginary, but if everyone imagines the same objects, they can agree on "facts" about those objects. The ontology inheres in our mental processes.
- A mathematical statement is an assertion that a proof exists or could be created. The ontology inheres in proofs, not in statements.
However, SEP also describes various problems with all of these interpretations. I'm not sure if there is a single, widely-accepted answer that can be ascribed to "formalists" generally.