home | mathematics | toolbox ::... 1 | 2

Moreover, to be able to implement toolbox, it is necessary to introduce proof-irrelevance for propositions. Thus propositions must be kept well distinct from sets. So a key step is to give a justification of logic independently of set theory, and we do this via the principle of reflection (see Basic logic).

Keeping communication between different views alive requires the design of a common theory in which all mathematicians can believe, while leaving them free to keep their intended semantics in mind. By leaving out both the axiom of choice and the powerset axiom at the level of toolbox, one obtains a common basis which is immediately understood as it is (that is, with no translations) and believed in by any mathematician.

Thus, contrary to what is usually required on a foundational theory, our minimal theory cannot be the best possible description of a single semantics. Rather, it is designed to admit different, and actually mutually incompatible interpretations, or extensions.

In Toolbox, we show how to develop a predicative theory of subsets within type theory.
We adopt the simple idea that it is not compulsory that a subset be a set. Then one is free to define subsets in a natural way as propositional functions and then to introduce the new notion of element of a subset, in terms of which also the other standard notions, like inclusion and extensional equality, arbitrary unions and intersections, singletons and finite subsets, quantifiers and functions defined on subsets can be defined. The resulting subset theory is a sort of type-less set theory localized to a set and we have experienced that it is sufficient for instance for the development of topology.

For a complete exposition one should look at: the preface of Toolbox, the whole of Minimalist foundation and section 3.2.1 of Some points.