4.9. Constructions

Diverse construction schemes let new types play the roles of sets defined in set theory by operations between sets named by previous types: Each of the following schemes suffices to produce both others through the use of previous ones: The last one can be obtained by composing constructions of products (to collapse bound variables as one, and the same for parameters), a definition and a type of unary relations or functions (either as particular relations, or by adapting the form of axioms, replacing ⇔ by = ).

A development scheme at each level looks like a component at the next level

Despite their differences of nature, the 3 levels of development have remarkable similarities:

How constructions preserve isomorphisms

From any theory T, consider any extension T' = TXRA where X is a type, R is a pack of structures and A is a pack of axioms. The existence of an extension of a given model of T as a model of T', is a matter of A being small enough for these X and R. Its uniquess would not make direct sense as any identical copy would also fit. But extensions may still be qualified as «essentially unique» (being all copies of each other) giving sense to how constructions preserve models, depending on the set of isomorphisms between them. For any models E' and F' of T' respective extensions of models E and F of T, and any isomorphism f : EF, Indeed in this case, any 2 isomorphisms g,h from E' to F' with the same restriction to E, will be equal because
The automorphism h−1g of E' extended by IdX' forms an automorphism of the model (E'E'') of T''. As j is invariant, it stays equal to its image j০(h−1g)−1 by this automorphism. Therefore h−1g = IdE' , i.e. g=h.
What we can see here strictly preserved by constructions, is the class of isomorphisms as an abstract category. In particular, constructions leave unchanged the automorphism groups seen as abstract groups, providing more types on which they act.
Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory (continued)
3. Algebra 1
4. Arithmetic and first-order foundations
4.1. Algebraic terms
4.2. Term algebras
4.3. Integers and recursion
4.4. Presburger Arithmetic
4.5. Finiteness and countability
4.6. The Completeness Theorem
4.7. Non-standard models of Arithmetic
4.8. Developing theories : definitions
4.9. Constructions
5. Second-order foundations
6. Foundations of Geometry