(apologies for the wild ramble. I'll probably regret this in the future)
I like the core concept at work here, with this idea that there is a manifest difference between various philosophies of mathematics that sees itself play out in the realm of mathematical practice. Certainly, the identification of Platonism with Ante Rem realism over the domain of (higher) set theory seems to be a very common understanding (consider the foundational role of Representation Theorems in many subdomains), and the view of Formalism as a more algebraic concept of mathematical practice (building upon finite methods) echoes Hilbert’s concept of the multiple realizability of ideal mathematical objects.
For Hilbert’s view (neatly introduced in https://plato.stanford.edu/entries/frege-hilbert/#HilbFounGeom ), the grounding foundation of mathematics is in the structures formed by the concepts outlined in axioms. One comes across new kinds of mathematical structure by showing that consistent sets of axioms can be worked provably independently of one another, relative to some familiar background theory.
Far from “axioms” representing an ideal Truth of the matter, as is taken as read by the realists, axiom systems are general technologies. Such systems have at least to be able to demonstrate that they do not collapse into classical trivialism, but that consistency relative to other areas of practice should be enough to prove their viability and potential usefulness, even if we don’t have a specific interpretation for them in mind.
For the realist, like the intuitionist, a demonstration of consistency shouldn’t itself give rise to a substantial existence claim (just like the intuitionist’s concerns about the indeterminate existence proofs by contradiction). For the formalist, the nature of such existence claims does not manifest in something like abstract objects, but is instead understood simply with reference to the axiomatic theory.
If phrased in terms of a simple first order theory, there is nothing more mysterious to mathematical objects than any other kind of object, in that those things that realize the axioms can be things in the positions indicated by the theory – that “Love, Law and Chimney-sweep” might be the placeholders of the existence claims of geometry, in the sense the Platonist thinks of an abstract object domain of points and lines.
So, in some general way, the formalist is not talking about the same domain of objects as the realist – if for a formalist it suffices to talk about the relative consistency of geometric systems interpreted in the algebra of the real number field, then there is no question of a distinct abstract sphere of geometry in the sense in which the real numbers are set-theoretic objects to the realist. For the Ante rem set theoretic realist, this can only pass muster if the objects of geometry are also shown to be definable as sets, where the formalist is content merely that the theory is represented using an algebraic proof/model structure, whatever one might take as the ontic structure of the models about which theorems are proven.
For working mathematicians, this distinction rarely comes into focus. While Godel’s point about the limitations of consistency as an idiom is far-reaching, in actual fact most abstract algebra are well understood as having the legitimacy of concrete set theory with reference to the proof of Representation theorems.
To make some headway into your question, if we want to try to come up with an understanding of what it means to understand relative interpretation of axiomatic theories, some metamathematical structure is probably useful to introduce. (This is an issue posed by Frege, as mentioned in Alan Weir’s SEP article around a challenge for the Game formalist: https://plato.stanford.edu/entries/formalism-mathematics/#GamTerFor. For the sake of your question, let’s take this metatheory to be category theory)
So let’s propose that we might want to try to come up with some sort of Category-theoretic distinction between these two ways of looking at the construction of models over an algebra. Perhaps the morphisms of our category might represent consistent model-theoretic interpretation, with the objects of our category being the “domains” of our proposed theories. Our realist thinks that every category must terminate in Set, while our formalist is happy to disregard the actual objects of the model theory as long as the morphisms are structure-preserving in the key model theoretic sense. (This should indicate to us that we are in some way dealing with a functor category)
Any attempt to demonstrate that there is something specifically distinct about the naïve formalist view, particularly of Hilbert’s initial finitist aspirations, is dashed against the rocks of the Yoneda Lemma (https://en.wikipedia.org/wiki/Yoneda_lemma). By accepting the category-theoretic interpretation of a grounding metatheory to describe the structure of locally small categories, we fall prey to the inevitable realization that we could, without any loss of generality, do this all in the category of sets anyway.
It’s only in the domain of Large Categories, where we start to look at Proper Classes that outstrip the resources of set theory, that this distinction starts to play a factor. For obvious reasons, a proper class cannot be a set. But, we might ask, does this mean that the Class of all Sets/All Ordinals cannot exist? Is there a collection of all algebraic structures of a given type? The Set-theoretic realist seems compelled to say no, even if they can force their way to a set-theoretic model in which one can say that there is.
If we take this seriously, then the exact way Formalism can pull itself apart in a principled way from the Ante-rem set theoretic realist is by countenancing the existence of large categories. To me, this is a fantastic way of understanding just how weird it is to accept the commitment to the complete openness of ontology of mathematics: to the formalist, given a commitment to say that the things of maths are just its terms or the principles of symbol manipulation operating over its theories, there is absolutely nothing wrong with the existence of proper classes.
And why not? Class-theoretic Comprehension can be written down in a sensible way without collapsing into inconsistency (the separation of Set theory has helped with that in the NBG sense), so shouldn’t this be totally reasonable? And in a world where the alternative seems to be a multiverse of set theories to countenance the unanswered questions of the consistency of large cardinal principles, ironically reversing the very worry about the explosive ontologies of consistency in the first place, recognizing that one’s commitment to the stuff of maths is only as much as it represents the logical rules of the game seems like a much needed dose of reality.
