- 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*in the role of canonical injection, with 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* - 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.*

- A
**type of structures***K*of any kind defined by a fixed expression with parameters, meaning all structures defined by this expression with all values of parameters. Its structures are:- A quotient operation, from parameters to
*K* - An evaluator, interpreting
*K*as a set of structures.

- A quotient operation, from parameters to

∀

(thanks to properties of equivalence relations and quotient)

- 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. This construction is worthless if the chosen symbol is without parameter (or behaving as such: independent of parameters) which would give singleton; or without other variable, as it would give the Boolean type.
- Definitions look like axioms: a definition of a predicate is given by a formula with free variables; axioms are chosen from ground formulas. Any formula merely defining a Boolean constant, i.e. with value depending only on the model and not on variables, such as ground formulas or provable formulas (in the sense that any free variables are implicitly bound by ∀), do not play any effective role of structures of the described system (giving roles to objects). Predicates defined without using the language, are not structuring either.
- As systems using axioms, proofs are similar to contradictions. A contradiction is a kind of proof with no theorem but 0 (False), which would be a very bad axiom. We might regard contradictions as a 4th kind of component of theories after types, symbols and axioms; not only the list of given contradictions should be empty for a theory to be of interest, but the set of possible contradictions should be empty as well.

- An extension of
*f*as an isomorphism from*E'*to*F'*will have to exist if*A*suffices to "determine" (make essentially unique) the extension of the model (interpretation of*X*and*R*) 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*E'*from having any more symmetry (nontrivial automorphism) than*E*. For example if*R*is empty, if the interpretations*X*and*X'*in*E'*and*F'*are equinumerous then any bijection between them extends*f*as an isomorphism between*E'*and*F'*; this is non-unique when*X*has at least 2 elements. - The extension
*T'*of*T*is a**construction**of*X*in*T*, when it ensures both the existence and uniqueness of an extension of*f*to*X*as an isomorphism from*E'*to*F'*. This can be formally verified in the doubly extended theory*T''*= (*T*∪*X*∪*R*∪*A*∪*X*'∪*R*'∪*A*'), by defining without parameter, a function from*X*to*X'*, and proving that it is a bijection extending Id_{E}as an isomorphism*j*between both models*E'*,*E''*of*T'*obtained by restricting a model of*T''*to copies (*T*∪*X*∪*R*∪*A*) and (*T*∪*X*'∪*R*'∪*A*') of*T'*.

The automorphismWhat we can see here strictly preserved by constructions, is the class of isomorphisms as an abstract category. In particular, constructions leave unchanged the automorphism groups seen as abstract groups, providing more types on which they act.h^{−1}০gofE'extended by Id_{X'}forms an automorphism of the model (E'∪E'') ofT''. Asjis invariant, it stays equal to its imagej০(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.
Algebraic terms

4.2. Term algebras

4.3. Integers and recursion

4.4. Presburger Arithmetic

4.5. Finiteness and countability

4.6. The Completeness Theorem

4.7. Non-standard models of Arithmetic

4.8. Developing theories : definitions

4.9.**Constructions**

5. Second-order foundations 4.2. Term algebras

4.3. Integers and recursion

4.4. Presburger Arithmetic

4.5. Finiteness and countability

4.6. The Completeness Theorem

4.7. Non-standard models of Arithmetic

4.8. Developing theories : definitions

4.9.

6. Foundations of Geometry