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.

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.