A restructuring programme operates in three steps: First the existing materials of a discipline are liquefied, then passed through a filter, and finally allowed to settle and refreeze.
In the course of restructuring no substantive results are lost. (Some results will change their shape or their function, but none will be lost.) All “losses” – the dirt removed during filtering – lack mathematical substance. By shedding residues of idle metaphysics and obscure scholasticism we gain clarity and rigour.
At least half the work under the programme therefore consists of recycling and reframing existing results. This will substantially increase transparency in the areas processed. It will lead to new results only at a second stage, when the programme has opened up fresh vistas. Trickle down effects into other areas of mathematics are to be expected, but the main impact of the programme will be felt in the so-called foundations – in areas such as model theory, proof theory, recursion theory, and set theory.
Any restructuring programme is based on an abstract concept which acts as a solvent to liquefy the status quo. The quasi-philosophical position implicit in the status quo is opposed with an alternative position. The challenge inherent in the programme is to reconstruct the discipline on the basis of this alternative position. In the present manuscript I will not be arguing philosophically for the positions at the heart of our restructuring programme. The philosophical arguments can take place elsewhere. Here I will simply state and, where necessary, explain the underlying philosophy. Instead of arguing for it philosophically we will let the fruitfulness of its mathematical consequences, and the clarity of mathematical presentation it allows, speak for itself.
The hegemonic if not entirely unchallenged position in mathematics is still a philosophy of Platonist realism about mathematical objects and a correspondence account of mathematical truth. This we reject. Our alternative theory of truth falls largely outside the scope of this manuscript, although a few brief remarks will be made in the section on restructuring model theory. The alternative ontology is one of strict finitism – a conviction that all mathematical terms should ultimately be explicable in terms of finite operations on finite strings.