While these sorts of «constructions» are essentially well-determined in set theory by the powerset and exponentiation operators, they fail to be qualified as constructions in first-order logic, as they are neither essentially determined by first-order axioms, nor translatable as abbreviations in the initial theory (and the extensibility of permutations of base types is only ensured for those which belong to the given universe, not for those which don't). This failure reflects the fact that these operators are not justified by the set generation principle. Thus, full types of structures are said to be

In practice for geometry, the only used ones are unary relations on some full type of structures

To reflect this role,

- For a relation : ∀
*k*,*k*'∈*P*, (∀*x*_{1},...,*x*, (_{n}*x*_{1},...,*x*)∈_{n}*k*⇔ (*x*_{1},...,*x*)∈_{n}*k*') ⇒*k*=*k'*(axiom of extensionality) - For an operation :
∀
*k*,*k*'∈*P*, (∀*x*_{1},...,*x*,_{n}*k*(*x*_{1},...,*x*) =_{n}*k*'(*x*_{1},...,*x*)) ⇒_{n}*k*=*k'*(axiom of effectiveness)

- Enough structures to prevent any new symmetry: the above axiom
requests the evaluator to be «structuring enough» over
*P*to prevent, for any isomorphism between 2 models of*T*, any multiplicity of extensions to interpretations of*P*forming isomorphisms between extended models; - Not «enough axioms to define» (essentially determine) the extension of the
model : Id on base types (or other isomorphisms between interpretations of them) is
not always extensible to an isomorphism between any two interpretations of
*P*; - Anyway not «too much axioms», so the theory remains consistent (it has models).

Invariance by a concrete category
has several possible formulations (such as ∀*f*∈Mor(*E*,*F*), ∀*r*∈*P _{E}*,
∃

For a concrete category that is not a groupoid, for each specific concept of invariance required of the named structures (be they first or second order), each concept of invariance required of an additional type of structures involves specific conditions on the syntax of formulas which define those where its satisfaction is ensured.

As a development of any
geometry (we may call *constructions ex nihilo*), consider adding any space *K* as
a type with enough additional structures to not let endomorphisms act nontrivially on it.
This may be done by taking as set of constants, either all *K* (anyway), or any basis
of it (if one exists, which may have the advantage of being finite, or countable).
Then all elements and structures purely over *K* are invariants as well.
This role of *K* may be played by ℝ, ℝ^{n},
or any subset of ℝ^{n} which would form a space.
Actually ℝ and ℝ² will suffice as grounds to formalize geometry.

If

∀*f*∈*F ^{E}*, ∀

Mor

∀

∀

*h* = ∏*E'* : *E* →
*K*^{E'}

In any concrete category, any choice of an object

This is an invariant of this category (Mor(

Moreover Mor

When effective, the duality structure suffices to define all algebraic structures on any object

*E'*⊂ Mor_{L}(*E*,*K*) ⇔
(∀*u*∈*E'*, φ_{K}০* ^{L}u*
=

∀*f*∈Mor_{d}(*E*,*F*),
∀*u*∈*F'*, *u*০*f* ∈ *E'* ∴ *u*০*f*০φ_{E}
= φ_{K}০* ^{L}u*০

Depending on the geometry, these types may differ or not : images of non-injective morphisms may be images of sections with another domain. In topology or differential geometry, a circle and a plane are spaces, the circle has embeddings into the plane (the official concept of embedding there may be more strict than the general one) but they are not sections.

Sets of the formBut depending on the geometry, other sets of embeddings, or sections, or embedded subspaces, or section subspaces, may not be anyhow preserved by morphisms which are not embeddings or sections.

In categories of relational systems, any set may form diverse systems depending on the choice of interpretation of a given relational language, and this set of possible choices is ordered by inclusion. More generally in concrete categories, a given set may receive multiple statuses as object, defined (transferred) by bijections serving as isomorphisms with existing objects, and these form an ordered set: reflexivity and transitivity are what axioms of concrete categories give in this case of uniqueness of the requested morphism (that is Id on the set), while antisymmetry comes by definition of the equality of statuses as object.

Then a partition (quotient)Then any

Set theory and foundations of mathematics

1. First foundations of mathematics

2. Set theory (continued)

3. Algebra 1

4. Arithmetic and first-order foundations

5.1. **Second-order structures and invariants**

5.2. Second-order logic

5.3. Well-foundedness

5.4. Ordinals and cardinals

5.5. Undecidability of the axiom of choice

5.6. Second-order arithmetic

5.7. The Incompleteness Theorem

More philosophical notes :
5.2. Second-order logic

5.3. Well-foundedness

5.4. Ordinals and cardinals

5.5. Undecidability of the axiom of choice

5.6. Second-order arithmetic

5.7. The Incompleteness Theorem