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

- For any extension
- 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.

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

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.

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

Mod_{ℕ} ≤ Mod ∴ Thm ≤ Tru⚬Mod ≤ Tru⚬Mod_{ℕ} ≤ Thm

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

The converse may be wrong: a theory

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

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

∀(variables), *R*⇔*R*_{1}

In particular, any relation defined by an expression with language

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.

A monoid *M* acting on also acts on *E ^{n}* by ∀

For any set of transformations

Inv^{(n)} *L* = Inv^{(n)}
〈*L*〉_{{Id,⚬}} ⊂ Rel_{E}^{(n)}

End_{Inv(n)L} *E* =
{*g*∈*E ^{E}*| ∀

End

Set theory and foundations of mathematics

1. First foundations of mathematics

2. Set theory

3. Algebra 1

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

4.11. Constructions

4.A. The Berry paradox

6. Foundations of Geometry