# Constructibility

A relation R is constructible if there is a context

• with no dependence, for what statements it accepts as true or which relations it accepts as values, on any context which presumes:
• that R is a value; that R is not a value; or that whether R is a value is undecidable;
• that R is constructible; that R is not constructible; or that whether R is constructible is undecidable;
• in which it can be shown that R is equal to some relation whose sepcification S is such that
• for any relation v, regardless of whether context admits it as a value, either S precludes v from being a (left or right) value of R or context can show that v is constructible
• for every x and y that meets S's explicit requirements for being, respectively, a left and right value of R, context can show that the proposition R relates x to y is decidable.

Note that the demonstration that v is constructible, when required, is obliged to happen without reference to questions of R's being constructible or a value. In particular, no relation whose specification would make it one of its own left or right values, were it a value, can be constructible.

## Discussion

The use of specification makes it possible to write powerful definitions, that describe useful relations, often in very straightforward ways. The specification says what properties the thing has; it is, of course, necessary to show that something does have those properties, but one can then infer what other properties that thing has. However, the use of specification can run into a complication, particularly in conjunction with certain proof methods (used to show that something does have the specified properties) which allow one to assert the existence of a thing without actually exhibiting the thing in question; in extremis, this leads to such fascinatingly counter-intuitive results as the Banach-Tarski paradox, according to which it is possible to divide a three-dimensional volume into subsets, rotate and translate those subsets, then so re-assemble them as to obtain another three-dimensional volume arbitrarily larger (or smaller) than the original. Crucially, the subsets are proved to exist, yet not exhibited. They can also be proven non-exhibitable; indeed, the subsets do not have well-defined volumes, even in Lebesgue's measure theory, which can ascribe a volume to any exhibitable subset of (among other things) three-dimensional space (but, in fact, one can show that – in a quite definite sense – almost all subsets of space aren't (exhibitable or) measurable).

Given that I am providing a framework for describing mathematics, and intend that framework to be usable on top of arbitrary foundations, I have to accept that some of the things I may be able to prove exist are mere mythical beasts in the eyes of at least some foundations. To some extent, I can live with that, at least where the facts about other entities, that I show true by reference to such mythical beasts, are still admissibly proven. Context is at liberty to chose which relations (and, ultimately, everything I define is a relation) are admissible as values, that relations may relate to one another (along, at context's option, with any values other than relations that context opts to entertain as values). When I discuss a relation which context does not regard as a value (so it's a mythical beast), the things I say about what values it relates to one another can all be interpreted as showing that the values in question do meet the relation's specification; and this is often entirely sufficient. In such a case, the fact that I expressed the results in hand in terms of a relation is merely a matter of convenience; the tools I build for describing relations make it easy to express things in terms of them, that may be expressed without them, none the less, albeit possibly less neatly.

However: in other cases, I introduce entities (such as the natural numbers) that I really do care about being able to deal with as real entities, not mythical beasts. Without these entities, it is hard to do any useful (to a physicist) mathematics. I need to make clear which those entities are, so that anyone expressing my work in terms of a particular foundation knows what to check their expression, taken with their limitations on what relations are values, does in fact allow us to talk about. To that end, I use the notion of constructibility, which may equally be thought of as a variant on exhibitability.

To characterise constructibility of a relation r, it's necessary to talk about relations which: would be (left or right) values of it, if they were values, and; cannot be shown to not be values without knowledge of whether r is a value. Then r is constructible if: every such relation is constructible; and, in every context that accepts these relations as values, all questions about whether r relates x to y, for given values x and y, are decidable without knowledge of whether r is a value.

Written by Eddy.