- 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 a specific format of a kind of components which*T*needs to have so that it can developed by adding related a pack of additional compoments. This list should suffice for any legitimate development to be 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) - A term
*t*defines a new operation symbol*S*, with the axiom ∀(variables),*S*(variables)=*t*(variables). - A formula φ(variables,
*x*) defines a new operation symbol*S*if we have as theorem (∀(variables),∃!*x*, φ(variables,*x*)); this comes with the new axiom

∀(variables), φ(variables,*S*(variables))

The use of

- 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

*f*may stay as an isomorphism between*E'*and*F'*if there is no new type and*f*preserves the interpretation of the new structures from*E'*to*F'*(which is ensured if the extension is a definition).*f*may be extensible to the new type, as an isomorphism from*E'*to*F'*, which is ensured if this extension is deterministic in isomorphism class (thus preserves all expressible properties) and does not break the isomorphisms on previous types (so the additional structures are not structuring on previous types). Both ideas may be expressed saying that any formulas in*T'*without free variable in the new type (respectively without and with free variables in old types), are provably equivalent to formulas in the mere language of*T*. But let us not wonder here whether this condition is exactly equivalent or not.- An extension of
*f*may be unique if*T'*does not introduce a new lack of structures either. Here are cases with multiple extensions of*f*as an isomorphism between*E'*and*F'*: *E'*=*F'*and (*T'*=*T*∪*X*∪ axiom (∃2:*X*)) where the automorphism of*E*can be extended by any permutation in the extra type, such as Id, to form an automorphism of*E'*; or- if (
*T'*=*T*∪ extra type ∪ axioms specifying a finite number of elements), ensuring the existence of a bijection between interpretations of the extra type in*E'*and*F'*, (any bijection will form an isomorphism). - In the
**construction**of a new type*X*, the isomorphism*f*has a unique extension as an isomorphism between*E'*and*F'*(by a bijection between interpretations of*X*in*E'*and*F'*).

Indeed then, any 2 isomorphisms

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. Infinity and the axiom of choice

4.4. Non-standard models of Arithmetic

4.5.How theories develop

4.6. The Incompleteness Theorem