I do not set out to provide a formal foundation for mathematics, although I do sketch what might serve as a start-point for such a foundation. My aim here is to describe a set of useful abstractions, which any foundation worth the name should support, in terms of which mathematics may generally be discussed. By this means, I hope to make the discussion viable regardless of which particular foundation any given context choses for mathematics. What I write may then be of use in more contexts than otherwise.
This approach is similar, in spirit, to the common practice in the software industry of providing a standard API (application programming interface) by which software can access certain common functionalities provided by computers. The API abstracts away the details of how any particular operating system (here taking the rôle of the foundations) may actually implement those functionalities. (Operating systems likewise abstract away the particulars of the hardware on which they run.) For each operating system, one supplies a library of software which implements those APIs. Programs written to use such an API (rather than directly accessing the operating system's idiosyncratic way of doing things) can then be made to work on diverse computers, independent of the operating system, by deferring the system-specific details to the library implementing the API.
Just so, I anticipate that the abstractions I define – principally, the relation – can be expressed in terms of the details with which any given foundation concerns itself; and can then be manipulated in ways compatible with how I use them, so that the results I derive from them are still sure to hold, regardless of the choice of foundation used.
The abstraction used by a software API, to package the idiosyncratic details of each operating system, should be designed around the concerns of software that shall use the API, with only such attention as cannot be avoided to the details of specific systems. However, such an abstraction is apt to – at least in principle – entertain the notion of being able to attempt things that, at least, some systems may be unable to do; it is thus necessary to specify some way for the library implementing the API to balk at unrealisable requests.
Likewise with a packaging of the foundations of mathematics; indeed, the
abstractions I introduce do in fact (unashamedly) permit one to specify
paradoxical entities. The mechanism by which I allow for particular foundations
to avoid consequent inconsistencies is in their specification of what entities
are to be legitimately considered values
. In particular, everything I
introduce is (ultimately encoded as) a relation, characterised by which values
it relates to one another; and it is up to the way the foundation expresses
relations to restrict which such relations are admissible as values, to be
related to one another.
Any such restriction, naturally, shall eliminate at least some of the power
of the entities I define and results I demonstrate about them; that inevitably
carries the risk of rendering the whole project useless. (Just so, an operating
system supplier can – whether by malice or incompetence – implement
standard APIs so poorly as to oblige programs, in order to work well on that
system, to use system-specific APIs, so that support for that system alongside
others with good standard APIs costs more than supporting either the standard
APIs or that one system. This may be an effective way for a vendor with strong
market share to entrench the application barrier to entry that keeps them
strong, but it is a lamentable waste of the efforts of scarce developers.) I
consequently take care to delineate certain core
entities – characterised as constructible
in contrast to relations
generally being specified – that I anticipate all foundations
should be able to allow as values.
My goal, in packaging the foundations, is to provide a general notation and language for the exposition that captures the essence without the encumbrance of the pedantic details needed by any particular foundation.
Written by Eddy.