4.4. Development of theories : definitions

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.

The Galois connection (Mod,Tru)

For any language L, the truth relation between ground formulas and systems defines a Galois connection (Mod,Tru), where Mod gives the class of models of any set A of ground formulas taken as axioms, while Tru gives the set of true formulas which all given systems have in common. Replacing the class of all systems by the set of all L-structures on ℕ, leaves unchanged and thus gives definite sense to the closure Tru০Mod. All theorems of a theory belong to the closure Tru০Mod(A) of axioms, which is the condition for a formula to leave unchanged Mod A when it is added to A.

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 by a unary predicate symbol R which may mean the standardness predicate in a non-standard model, as A says the the induction axiom fails on R: 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)
Still, like proofs strictly preserve models, definitions can be seen as strictly preserving something else. For any isomorphism f between models E and F of T, with respective extensions as models E' and F' of a theory T' extending T by further structures and axioms, 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.
This switch from models to isomorphisms provides similarities between levels of development, not only from proofs to definitions but also from definitions to constructions, making sense to how these also essentially preserve theories, as we shall now explain.
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. Development of theories : definitions
4.5. Constructions
4.6. Second-order logic
4.7. Well-foundedness
4.8. Ordinals and cardinals
4.9. Undecidability of the axiom of choice
4.10. Second-order arithmetic
4.11. The Incompleteness Theorem