I've been really getting (topically, hence the question) into formal logic and formal languages lately. I find the topic quite interesting. A lot of papers and posts that I read about formal languages are interesting (and a good amount are of computational nature), but overall revolve around the same subject -- languages, of course. My question is how are these things useful? For computational purposes, I see how the expressive power of, say, in particular, Domain Specific Languages is a good way to go about things, but this doesn't seem to contribute to the overall state of well-being of mathematics on the whole. I mean, perhaps there's something there (beyond expressiveness), but I don't see it, and it comes off more as a gimmick, than a really demanding-and-rewarding mathematical discipline. So the question is -- and for some reason I get the impression that this is somehow a burning question in many people's stomachs -- how does research in mathematical logic, say model theory and formal languages in particular, then, contribute to other, general-purpose mathematics, beyond assuring that the foundations of mathematics are rock solid?
Topology and geometry give back to logic in HoTT, so does algebra of course, on which modern logic currently rests. Banach and Tarski do give a seemingly paradoxical construction in geometry and topology, but this seems to be more so an exercise in logic itself, than a contribution to geometry right? I mean it goes something along the lines of "well, if we buy into the axiom of choice, (or alternatively, ZF, or a bunch others if I understand correctly), then here's what's possible and "a pea can be chopped up and reassembled into the Sun" ". Similarly, if we take non-standard analysis; here, again, this is, as far as I understand, an exercise in a "better" (different, if you disagree ;) ) interpretation of analysis.
So, while I completely agree that these are fascinating mathematical exercises in their own right, that mathematical logic deserves attention for it's own merits, and that mathematical logic is demanding-and-rewarding in it's own right, I am having trouble seeing how that percolates into other areas of mathematics. I.e., can logic give NEW results in algebra, geometry/topology, analysis/probability, or even cobinatorics/graph theory?
Forcing in set theory provides a powerful method to show that natural questions in algebra, topology, and analysis cannot be settled using "reasonable" arguments.
Both the role of model theory in motivic integration and the use of computability theory in studying moduli spaces leap out to me as good examples of positive applications of logic to the rest of mathematics.
You mention combinatorics as being specifically interesting. Well, there are applications there too! Even though I mentioned forcing as a method to prove independence results, there are examples of forcing used to prove theorems - even pure combinatorial statements about finite graphs (see the top answer)! And Harvey Friedman has extensively studied pure combinatorial principles which require extremely strong axioms ("large cardinals" - that is, set-theoretic axioms that assert the existence of extremely large infinite sets) to prove.
And here's a personal favorite: extremely large cardinals yield proofs of statements about finite algebraic structures! Although the large cardinal assumptions in similar theorems were removed eventually, currently it is unknown how to prove these results without large cardinals.
But I think that looking for justifications of a branch of mathematics based on applications to the rest of mathematics ignores the real point: that mathematical logic (as you say) is really interesting! For me, the intrinsic beauty of a subject on its own is a perfectly good justification.