Is there a general notion of definability/expressibility?

88 Views Asked by At

If we want to talk about uncountable sets, then we can distinguish between objects in the set that we can actually "specify" and those that we can't. An example of objects that can be specified are $5$, $\sup_xf(x)$, and Chaitin's constant. I can't give any examples of objects that can't be specified, since I would have specified them in doing so.

This notion is formalized in some specific contexts: E.g. a definable real number, or a definable set (of natural numbers). Based on a few quick google searches I could only find these two examples. I'd just like to get a pointer to some literature that I can read about it.

Is there a general notion of "definability" of arbitrary mathematical objects?

  • In particular, in classical mathematics. In constructive mathematics the notion of definability collapses to computability afaik.

  • I'm particularly interested if it's in type-theoretic foundations.

  • I can imagine there are some difficulties related to logical paradoxes when we try to define a notion of "definability" in full generality?

1

There are 1 best solutions below

10
On BEST ANSWER

For any structure $\mathfrak{M}$ there is a general notion of (first-order) definable subset/function/relation/element of $\mathfrak{M}$, provided by the (first-order) formulas in the language of $\mathfrak{M}$. We can also talk about definability with parameters, and so on. See here for a quick summary of this.

Now note the "first-order" bit above. This refers to the specific choice of first-order logic as our framework for making and evaluating definitions. There are other logics out there - second-order logic, infinitary logic(s), etc. - and each logic gives rise to its own definability notion. If you're interested, I strongly recommend the (legally freely available online!) wonderful collection Model-theoretic logics.

As to meta-issues, for any "reasonable" logic $\mathcal{L}$ there is a general obstacle (usually phrased for first-order logic, but much more generally applicable than that) to talking about the $\mathcal{L}$-definable phenomena in a structure $\mathfrak{M}$ within that structure itself. The existence of pointwise-definable models of set theory provides a particularly powerful example of how strong this limitation truly is! However, this doesn't prevent us from performing this analysis from outside $\mathcal{M}$. So we just have to be careful what statement is being made where.