- 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 the following pair of formats: (1) a pack of existing components from*T*, needed to allow adding there (2) a related pack of new components. 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).

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.

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

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

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

- From a type
*E*and a unary relation φ on*E*we can construct a type*F*in the**role of the subset**{*x*∈*E*| φ(*x*)}, with a function symbol*j*:*F*→*E*and 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*= {*x*∈*E*| φ(*x*)} - From 2 types
*E,F*a type*G*is constructed in the**role of the sum***E*⊔*F*, by function symbols*i*:*E*→*G*,*j*:*F*→*G*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 K**(for any integer_{n}of*n*constants*n*) can be constructed ex-nihilo, with*n*constant symbols*k*_{1}, ...*k*, the axiom (∀_{n}_{K }*x*,*x*=*k*_{1}∨ ... ∨*x*=*k*) and for every 0<_{n}*i*<*j*≤n the axiom*k*≠_{i}*k*._{j}

- From 2 types
*E,F,*a type*G*is constructed in the**role of the product***E*×*F*, by function symbols*i*:*G*→*E*,*j*:*G*→*F*, a binary operation symbol *:*E*×*F*→*G*and the axiom

∀A variable of type_{E }*x*, ∀_{F }*y*, ∀,_{G }z*z*=*x***y*⇔ (*x*=*i*(*z*)∧*y*=*j*(*z*))*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*). - From a type
*E,*a binary relation*R*on*E*and the theorem making*R*an equivalence relation (∀,_{E }x,y*xRy*⇔ (∀,_{E }z*xRz*⇔*yRz*)), we can construct a type*Q*in the**role of the quotient***E*/*R*with a function symbol*q*:*E*→*Q*, and axioms - ∀
,_{E }x,y*q*(*x*)=*q*(*y*) ⇔*xRy* - ∀
, ∃_{Q }x, q(_{E }y*y*)=*x*

∀

(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*:*E*→*Q*

- a relation
*R*' between*Q*and*F*,

- ∀
,∃_{Q }x,_{E }y*q*(*y*)=*x* - ∀
,∀_{E }x,_{F }y*q*(*x*)*R*'*y*⇔*xRy* - ∀
, (∀_{Q }x,y,_{F }z*xR' z*⇔*yR*'*z*) ⇒*x*=*y*. Or equivalently,∀,(∀_{E }x,y*z*∈*F*,*x**R**z*⇔*yRz*)⇒*q*(*x*)=*q*(*y*)

The last 2 axioms are together equivalent to

- ∀
,∀_{E }x, (∀_{Q }y,_{F }z*yR' z*⇔*xRz*) ⇔*q*(*x*) =*y.*

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

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.

Generally, for any isomorphism

- 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 have to stay an isomorphism if the additional axiom(s) suffice to form a definition of the new structure(s). - 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''*= (*T*∪*X*∪*R*∪*A*∪*X*'∪*R*'∪*A*'), one can define an invariant bijection from*X'*to*X*, and prove that it extends Id_{E}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: (*T*∪*X*∪*R*∪*A*) and (*T*∪*X*'∪*R*'∪*A*').

The automorphismWhat we can see here strictly preserved by constructions, is the class of isomorphisms as an abstract category.h^{−1}০gofE'extended by Id_{X'}forms an automorphism of the model (E'∪E'') ofT''. Asfis invariant, it stays equal to its imagef০(h^{−1}০g)^{−1}by this automorphism. Thereforeh^{−1}০g= Id_{E'}, i.e.g=h.

Set theory and foundations of mathematics

1. First foundations of mathematics

2. Set theory (continued)

3. Algebra 1

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 and ordinals

4.7. Undecidability of the axiom of choice

4.8. Second-order arithmetic

4.9. The Incompleteness Theorem