Generalization of nonexpressibility of solutions

Question

Are there any ideas/areas of math that generalize the idea of when a solution to a question can be expressed in some given formal system? Something that (at least in spirit) covers results like

• No algebraic solution to a quintic polynomial
• No closed form expression for $\int_0^{x} e^{-t^2} dt$
• No turing machine to compute solutions of diophantine equations
• No formula for "G is a connected graph" in FOL logic of graphs

Answer 1

One topic you might look into is abstract model theory. Here we take as our jumping off point results about non-definability in first-order logic. The idea of AMT here is that there are many other logics besides first-order logic; an interesting subtlety it introduces is the distinction between defining a class of structures and defining a set within a given structure.

Here are a couple examples:

• The MRDP theorem says that satisfiability of Diophantine equations is not definable over the structure $\mathbb{N}$ by the $\Pi^0_1$ fragment of $\mathsf{FOL}$. This differs from the non-$\mathsf{FOL}$-definability of connectedness in two ways: we replace $\mathsf{FOL}$ by a smaller logic, and we think about defining a subset of a fixed structure instead of carving out a class of structures. Note that a closer parallel here is with the result that we can whip up a single graph $G$ whose finite-distance relation is not $\mathsf{FOL}$-definable in $G$. It's separately worth noting that a theorem of Ash/Knight/Manasse/Slaman and Chisholm provides a further connection between computational complexity and definability, but this gets a bit niche.

• The unsolvability of the quintic is related to undefinability in equational logic. This is a very weak fragment of $\mathsf{FOL}$, and takes us into the realm of universal algebra. Again, we're looking at a specific structure here.

These examples involve sharpening the usual notion of $\mathsf{FOL}$-definability. We can also go the other way, and look at logics much stronger than $\mathsf{FOL}$ which yield much looser notions of definability (and consequently much more surprising non-definability theorems). One incredibly important result of this type is that well-foundedness is not $\mathcal{L}_{\infty,\omega}$-definable. The standard text on abstract model theory is the (freely available!) collection Model-theoretic logics, although the vast majority of this text focuses on stronger logics and so doesn't really address the examples in the OP.

Answer 2

Asking for solutions in algebraic systems is a unifying concept. Examples are the existence of functions, of numbers, of words, of languages, e.g. as solutions of equations, differential equations, integral equations, functional equations or inversion problems.
Solutions in fields are just a small part of that. For solutions in fields, see e.g. Borwein, J.; Crandall, R.: Closed forms: What they are and why we care. Notices Amer. Math. Soc. 60 (2013) 50-65.
$\ $

And last but not least, category theory is a very general unifying system. See e.g. nLab.