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.