## 4.4. 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:
• In which sense is T' «equivalent» to T :
• For any extension T' of T, any model of T' defines by restriction a unique model of T ;
• Such a T' is qualified a development of T if conversely, any model of T has a «unique extension» as a model of T', in a sense we need to specify.
• A list of developments schemes, where each is the data of a pair (X,Y) of theoretical components (a sub-theory X of a theory Y) so that any morphism from X to a theory T allows to add to T a copy of the rest of Y beyond its sub-theory X identified as its image in T. A list of developments schemes is sufficient when any legitimate development is producible by a succession of steps each described by one of these schemes.
• On the formal side: how, for each such scheme, the use of extra components in works (expressions, proofs...) with T' can be translated into (usually longer) works with T, and thus be seen as abbreviations of them.
There are 3 levels of development with their respective schemes:
• A proof only adds one ground formula to the axioms, as this formula is shown to be a theorem (deduced from some of the previous axioms).
• A definition adds both a new structure symbol and a new axiom.
• A construction adds altogether a new type, new structure symbol(s) and new axiom(s).

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:
• A formula φ defines a new relation symbol R with arguments the free variables of φ, with the new axiom ∀(variables), R(variables)⇔φ(variables). The use of R can be replaced by the use of φ as a sub-formula of other formulas (replacing the free variables of φ by the terms used as arguments of R).
• A term t defines an operation symbol S, with the axiom ∀(variables), S(variables)=t(variables). This S abbreviates, and can be replaced by, its defining term t.
• Given a formula φ(variables, x), if we have (∀(variables),∃!x, φ(variables, x)) then it defines a new operation symbol S, with the new axiom
∀(variables), φ(variables, S(variables)). This 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 φ. This case 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:
• If T' only has a new axiom A then E may stay or not as a model of T', depending whether A is true or false in E; it always does if A is provable from previous axioms;
• If T' only has a new symbol then E may have several extensions as models of T' by giving this symbol arbitrary interpretations, except for special cases
• Definitions precisely combine a new symbol R and a new axiom A, so that any model of T has a unique extension to an interpretation of R that satisfies A, forming a model of the extended theory (T∪{R,A}).
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 :
• T is any arithmetic and T' expresses non-standardness by letting R be a constant (number), and A the axiom schema making it non-standard.
• The other expression of non-standardness: R is a unary predicate symbol, and A makes it an exception to the induction axiom: R(0) ∧ (∀x, R(x) ⇒ R(S(x))) ∧ (∃x, ¬R(x))
• T = bare arithmetic; T' = Presburger arithmetic
• T = Presburger arithmetic; T' = full arithmetic (with addition and multiplication)

### Constructions

Diverse construction schemes let new types play the roles of sets defined in set theory by operations between sets named by previous types:
• From a type E and a unary relation φ on E we can construct a type F in the role of the subset {xE| φ(x)}, with a function symbol j:FE in the role of canonical injection, with axioms
• F x,y, j(x) = j(y) ⇒ x=y meaning that j is injective
• E x, φ(x)⇔∃F y, j(y)=x meaning that Im j = {xE| φ(x)}
• From 2 types E,F a type G is constructed in the role of the sum EF, by function symbols i:EGj:FG and axioms
• E x,y, i(x) = i(y) ⇒ x=y
• F x,y, j(x) = j(y) ⇒ x=y
• G x, (∃E y, i(y) = x)⇎(∃F y, j(y)=x)
• A type Kn of n constants (for any integer n) can be constructed ex-nihilo, with n constant symbols k1, ... kn, the axiom (∀K x, x=k1 ∨ ... ∨ x=kn) and for every 0<i<j≤n the axiom kikj.
• From 2 types E,F, a type G is constructed in the role of the product E×F, by function symbols i:GE , j:GF, a binary operation symbol *:E×FG and the axiom
E x, ∀F y, ∀G z, z = x*y ⇔ (x=i(z)∧y=j(z))
A variable of type G (or argument in a structure symbol), abbreviates a copy of the given list of variables (here with types (E,F))
A structure with values of type G, abbreviates a pack of 2 structures (to be used together as arguments of another structure, in the place of an argument with type G).
Each of the following schemes suffices to produce both others through the use of previous ones:
• From a type E, a binary relation R on E and the theorem making R an equivalence relation (∀E x,y, xRy ⇔ (∀E z,xRzyRz)), we can construct a type Q in the role of the quotient E/R with a function symbol q:EQ, and axioms
• E x,y, q(x)=q(y) ⇔ xRy
• Q x, ∃E y, q(y)=x
Any structure S(u,v,...,k) with an argument k of type Q, abbreviates a structure S'(u,v,...,x), where x is of type E, with the axiom
u,v,...∀E x,y, xRyS'(u,v,...,x)=S'(u,v,...,y)
(thanks to properties of equivalence relations and quotient)
• A type of unary relations: from 2 types E,F and a relation R between them, we construct the image Q of E in ℘(F) by the curried R, by 2 new structures
• a function q:EQ
• a relation R' between Q and F,
and axioms
• Q x,∃E y, q(y)=x
• E x,∀F y, q(x)R' yxRy
• Q x,y, (∀F z, xR' zyR' z) ⇒ x=y. Or equivalently,∀E x,y,(∀zF, xRzyRz)⇒ q(x)=q(y)
The last 2 axioms are together equivalent to
• E x,∀Q y, (∀F z, yR' zxRz) ⇔ q(x) =y.
• A type of structures K of any kind defined by a fixed expression with parameters, meaning all structures defined by this expression with all values of parameters. Its structures are:
• A quotient operation, from parameters to K
• An evaluator, interpreting K as a set of structures.
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:

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).

Definitions look like axioms: 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).
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
• Without any new type, f may stay or not as an isomorphism between E' and F', i.e. preserve the interpretation of the new structure(s). It will be an isomorphism whenever the additional axiom(s) form a definition, determining the new structure(s) and thus making it invariant by isomorphisms.
• With a new type, f may be extensible to it, as an isomorphism from E' to F'. Such an extension will have to exist if the additional axioms suffice to "determine" (make essentially unique) the extension of the model (interpretation of the new type and structures) in the following sense: any two extensions are isomorphic (making unique the isomorphism class of extended models E'), by some isomorphism whose restriction to old types is the identity. Therefore in this case, any formulas in T' without free variable in the new type are provably equivalent to formulas expressed in T, may they be ground formulas (as they describe the extended model) or with some free variables in old types (as they may define structures on previous types, which the isomorphisms must preserve).
• The uniqueness of the extension of f is a matter of T' having enough structures to prevent the model from presenting any new symmetry (nontrivial automorphism). For example with no additional structure, if there is a bijection between the interpretations in E' and F' of the new type then f can be extended by any such bijection to form an isomorphism between E' and F'; this extension of f is then non-unique as soon as the interpretation of the new type has at least 2 elements.
• When the formal extension (X,R,A) of T is a construction of X in T, any isomorphism f between any models E and F is ensured to have a unique extension as an isomorphism between any given extensions E' and F' (by a bijection between interpretations of X in E' and F'). This title of "construction", is formally verifiable as follows : 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 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 f is invariant, it stays equal to its image f০(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.
Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory (continued)
3. Algebra 1
4. Model Theory
4.1. Finiteness and countability
4.2. The Completeness Theorem
4.3. Non-standard models of Arithmetic
4.4. How theories develop
4.5. Second-order logic
4.6. Well-foundedness
4.7. Ordinals and cardinals
4.8. Undecidability of the axiom of choice
4.9. Second-order arithmetic
4.10. The Incompleteness Theorem