4.10. Developing theories : definitions

Given a theory T (with types, structures and axioms), a development of T is a extension of T into a 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:

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, let Thm be the transformation of ℘(X) where X is the set of all ground formulas with language L, giving the set of theorems provable from any set of formulas taken as axioms. It is a closure. 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).

This closure actually coincides with the one Tru⚬Mod of the Galois connection (Mod,Tru), where Mod gives the class of models of any set of ground formulas taken as axioms, while Tru gives the set of true formulas which all given systems have in common. While it is not a priori well defined as Mod gives a class, we can still see it a posteriori definite as follows (for countable L).

The truth relation RX×Y between X and the set Y of all L-structures on ℕ and or any subset of it, defines the Galois connection (Mod,Tru) where Mod gives a set of representatives of all finite or countable models of given axioms. Then Tru⚬Mod = Tru⚬Mod = Thm because

Mod ≤ Mod ∴ Thm ≤ Tru⚬Mod ≤ Tru⚬Mod ≤ Thm

the last inequality given by the completeness theorem. So, theorems of AX are the ground formulas leaving unchanged Mod A when added to A.

Schemes of definitions

We have 3 schemes of definitions:

Extending models by undefined structures

Again by 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 :

Definitions extend 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

Definitions preserve sets of isomorphisms

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 stay an isomorphism whenever the additional axiom(s) form a definition, determining the new structure(s), thus qualified as invariant by isomorphisms. Thus, adding a defined structure to a theory preserves the sets of isomorphisms between its models.
In particular, any relation defined by an expression with language LR without parameters is invariant by automorphisms, so is in its closure Inv(AutL E). This means that adding it to L preserves AutL E.
As we saw how the switch from models to isomorphisms provides similarities between development levels from proofs to definitions, we shall now see it also providing similarities from definitions to constructions, giving sense to how constructions also "essentially preserve" theories.

Rebuilding structures in a concrete category

In a small concrete category, the preserved families of relations are precisely all choices of unions of trajectories of tuples : each predicate symbol s interpreted as relations preserved through the category, coincides with the union of those so defined with t ranging over s through all objects K.

However, the class of relational systems obtained by even giving in this way "all possible structures" to the objects of an otherwise given concrete category, such as topology, may still admit more morphisms than those we started with (this construction behaves like a closure).

A monoid M acting on also acts on En by ∀aM, ∀xEn, ax = ⋅(a) ⚬ x. So, the set Inv(n) M of n-ary relations invariant by M, can be described as made of unions of trajectories of tuples xEn.
For any set of transformations LEE, the properties of Galois connections give

Inv(n) L = Inv(n)L{Id,⚬} ⊂ RelE(n)

so that closures of transformation sets by the (End, Inv) connection can be written

EndInv(n)L E = {gEE| ∀xEn, ∃f∈〈L{Id,⚬}, fx = gx}.
EndInv L E = {gEE| ∀n∈ℕ,∀xEn, ∃f∈〈L{Id,⚬}, fx = gx}.


Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory
3. Algebra 1
4. Arithmetic and first-order foundations
4.1. Algebraic terms
4.2. Quotient systems
4.3. Term algebras
4.4. Integers and recursion
4.5. Presburger Arithmetic
4.6. Finiteness and countability (draft)
4.7. The Completeness Theorem
4.8. More recursion tools
4.9. Non-standard models of Arithmetic
4.10. Developing theories : definitions
4.11. Constructions
4.A. The Berry paradox
5. Second-order foundations
6. Foundations of Geometry