3.10. How theories develop

Given a theory T (with types, structures and axioms), a development of T is a extended theory T' = T∪(pack of extra components) which remains «equivalent» to T.  This concept has 3 aspects:
There are 3 levels of development with their respective schemes:

The use of a theorem as an available axiom for the proofs of the next theorems, abbreviates a repetition of its proof as a part of the next proofs (with possible substitutions of variables by terms to which the theorem is applied).
When inserting theories in the set theoretical framework, constructions become set theoretical definitions, which is why the distinction between definitions and constructions is not usually clarified in the literature.

Definitions

We have 3 schemes of definitions: The last scheme may be split in 2 steps : the definition of a relation symbol R by φ (by the first scheme); then a reduced version of the last scheme directly using R instead of a formula φ.

The use of R can be replaced by the use of φ as a sub-formula of other formulas (where the free variables of φ are replaced by the terms used as arguments of R). The replacement of operation symbols by their defining term is obvious, and the case of operations defined by formulas was discussed with the uniqueness quantifiers (2.4).

How definitions preserve models

For any theory T with a model E, extensions T' of T by an additional axiom and/or structure symbol may have different effects: The uniqueness of the extension for every E, means that in the doubly extended theory (T∪{R,A,R1,A1}) where (R1,A1) is a copy of (R,A), one can prove

∀(variables), RR1

Thanks to the completeness theorem, if every model of T can be extended as a model of a T' = (T∪{R,A}) where R is a new symbol and A is a new (set of) axiom(s), then every ground formula of T provable in T', is also provable in T.
The converse may be wrong: a theory T may be extensible to a theory T' unable to prove more of its formulas, but to which not all its models are extensible. Here are some examples from non-standard models of arithmetic :

Constructions

Diverse construction schemes let new types play the roles of sets defined in set theory by operations between sets named by previous types: An alternative presentation of the quotient is the following: When coming after 2 constructions of products and a definition, the construction of a type of unary relations becomes the more general construction scheme of a type of structures of any kind defined by any fixed expression (what was seen in 1.5 as a variable structure defined by an expression with parameters). First for predicates, then for operations, either as a particular case, or by adapting the form of axioms (replacing ⇔ by = as needed).

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

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

A proof of a theorem A in a theory T looks like a contradiction in the theory (T∪ ¬A); a contradiction (4th kind of component) in a theory is a proof whose theorem is 0 (which would be a very bad axiom).

A definition of a predicate is given by a formula with free variables; axioms are chosen from ground formulas. A ground formula would only define a Boolean constant (whose value depends on the model), which do not play any effective role of structures of the described system (giving roles to objects).
A predicate defined by a provable formula (with free variables, but that can bound by ∀ to appear as theorem), would be constantly true and thus not structuring either.

A construction of a type of structures is given by a variable structure, that is a structure symbol with a selection of variables to play the role of parameters. Structures in the language are invariant, i.e. without parameter.
A type of structures constructed by what behaves as an invariant structure (not varying with the value of parameters) would be a singleton, thus worthless.

How constructions preserve isomorphisms

The sense in which constructions preserve models, is more subtle than with definitions: any model of T is extensible to a model of the extended theory T' = TXRA (where X is a type, R is a pack of structures and A is a pack of axioms), but any identical copy of this extension of interpretation would fit as well. But the extension is «essentially unique» in the sense that any 2 possible ones will be the mere copy of each other, being related by a unique isomorphism (like initial or final objects in a category).
Generally, for any isomorphism f between models E and F of T, with respective extensions as models E' and F' of extended theory T', we may have several cases This double property of existence and uniqueness of an extension of every possible isomorphism, by which a given pack of additional formal components can get the title of "construction", can be ensured by the following formal property: in the doubly extended theory T''= (TXRAX'∪R'∪A'), one can define an invariant bijection from X' to X, and prove that it extends IdE to an isomorphism f between both models E' , E'' of T' respectively obtained by restricting the model of T'' to each of both copies of T' it contains: (TXRA) and (TX'∪R'∪A').
Indeed then, 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 f is invariant, it stays equal to its image f০(h−1g)−1 by this automorphism. Therefore h−1g = IdE' , i.e. g=h.
In fact, what is strictly preserved by constructions, is the class of isomorphisms as an abstract category (a concept we only sketched but is otherwise the most common concept of category).
Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory (continued)
3. Algebra 1
3.1. Morphisms of relational systems and concrete categories
3.2. Special morphisms
3.3. Algebras
3.4. Algebraic terms and term algebras
3.5. Integers and recursion
3.6. Arithmetic with addition
4. Model Theory
4.1. Finiteness and countability
4.2. The Completeness Theorem
4.3. Infinity and the axiom of choice
4.4. Non-standard models of Arithmetic
4.5. How theories develop
4.6. The Incompleteness Theorem