# What is Formal Logic and How do Formal Languages Come in Useful

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?

• So ... you "find the topic quite interesting" but also think "it comes off as a gimmick"? That sounds like a not entirely consistent worldview ... – Henning Makholm Oct 13 '16 at 14:22
• To clarify, the gimmick is mostly research into programming languages on the computational side. – Joe Shmo Oct 13 '16 at 14:23

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.

• @MauroALLEGRANZA What did I write that suggested otherwise? What part do you disagree with? – Noah Schweber Oct 13 '16 at 14:40
• @MauroALLEGRANZA . . . Yes, it does. I never said it's the only such one, did I? It does indeed, however, leap out to me as a good example. Especially because it really uses the more abstract part of computability theory, rather than the definitions of computers and complexity classes. Unless you're saying you think that the application I mention isn't a good example of a positive application, I don't see what you're disagreeing with. (Or are you arguing that the study of non-computable sets isn't part of logic?) – Noah Schweber Oct 13 '16 at 14:42

This started out as a comment but it turned out to be too long for a comment so that I decided to make it in to an answer:

You might be interested in:

2) Shelah proved that Whitehead's problem was independent of set theory: https://en.wikipedia.org/wiki/Whitehead_problem

and last but not least:

Also, just to point out: Most mathematicians use the axiom of choice, Zorn's lemma is an essential tool in algebra. It is also required to show that every vector space has a basis. The Tychnoff theorem in topology is equivalent to the axiom of choice. So opting out of the axiom of choice causes a lot of problems. Also, depending on how you want to interpret it, Godel's incompleteness theorem tells us that the foundations of mathematics are anything but rock solid.

Modern logic, via automated reasoning programs which use/simulate first-order logic, has made several contributions to abstract algebra by finding new postulate sets for some algebras. Here lies some other examples.

It also enabled the solving of the Robbins problem.

There exists an old paper by Lukasiewicz, who worked by hand, entitled Formalization of Mathematical Theories. It has some theorems in arithmetic, which Lukasiewicz says were not known. The paper ends saying:

"I do not think that it would be possible to derive the theorems proved in this contribution without the powerful instrument of symbolic logic and without the formalization of proofs."

Modern logic, or equivalently symbolic logic, has even enabled a different sort of study of geometry and no doubt theorems have gotten found not previously known in previous studies (automated reasoning programs can often generate soo many theorems that probably no one could remember all of them).

Ken Kunen has also used a first-order automated program to study the theory of finite sets, and there does exist more to this.

• Can you say a bit about why finding new axiomatizations for algebras (e.g. the Robbins problem) is interesting outside logic? – Noah Schweber Oct 13 '16 at 14:56
• @NoahSchweber The Robbins problem consisted of a question that had stood open in Boolean Algebra for more than fifty years. A new axiom set for say, a fragment of geometry, might make it easier to prove certain results or to even produce results that no one knew before. – Doug Spoonwood Oct 13 '16 at 15:00
• Sorry, I wasn't clear. I know what the Robbins problem is, and I personally care a lot about new axiomatizations of structures; but I'm a logician :). I think the OP would be interested to here how new axiomatizations of algebras have led to new results about those algebras themselves - e.g. have new theorems about Boolean algebras been proved, following the solution to the Robbins problem? (Or similarly for geometries.) When you say "or to even produce results that no one knew before," that's really what I'm getting at, and what I think the OP is asking about. – Noah Schweber Oct 13 '16 at 15:32
• @NoahSchweber I'm not sure I understand what you're saying, because my response seems too simple as follows: A new axiomization of an algebra indicates that the new axiom set suffices to produce all of the other theorems that people already knew about. The new theorem about the structure would be that this new axiom set, or axiom, can produce all of the same theorems as other known axiom sets. When I said "new results" that no one knew before I meant new theorems in the theory. That's harder to demonstrate, because it requires an example, and knowledge of all previously known theorems. – Doug Spoonwood Oct 13 '16 at 17:18