5. Second-order foundations

5.1. Second-order structures and invariants

Second-order constructions

A full type of structures of a kind over some given types called base types, is the set of all possible first-order structures of that kind with nonzero arity over base types. If there is only one base type X, these types are RelX(n) and OpX(n) for every n∈ℕ*. These include the powerset and exponentiation of types, which suffice to give other full types of structures once applied after a construction of product (or other ways by currying).
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 second-order constructed from base types.

Second-order structures

Over a given list of sets, a first-order structure was a relation (or operation) with domains (and target) picked from this list. Now a second-order structure, is also a relation (or operation) but using as domain of at least one variable, a full type of structures over them (while those only using a full type of structures as target are mere curried views of first-order structures; and like connectives and equality, those given as parts of first-order constructions are "non-structuring").
In practice for geometry, the only used ones are unary relations on some full type of structures Y. First-order logic cannot express the exhaustivity of Y, but can directly describe any unary relation there as a type P called a type of structures, meant as a subset of Y but never using Y nor Y\P. Its role is given by an evaluator symbol S whose type is made of the intended symbol type for the elements of P, plus one argument of type P. Indeed the role of this evaluator is understandable in curried view as that of the natural injection from P to Y.
To reflect this role, S(k, x1,...,xn) will be abbreviated as (x1,...,xn)∈k if a relation, or as k(x1,...,xn) if an operation, and the injectivity requirement is expressed by an axiom: This pack of components (a type, a structure and an axiom), to be added to a theory T, plays the role of a structure in the sense of how it modifies the category of models: it has Any theory whose types are "base types" and types of structures over these (with no claim of fullness), forms a weak second-order theory.

Second-order invariants

A type of structures P, in its role of second-order structure, is invariant by a given group G of permutations on base types when it is preserved (or stable, which is equivalent) by the action of G on the full type of structures which includes P, i.e. when elements of G are extensible to the type P (acting as permutations on it). This action can be non-trivial: elements of P (as first-order structures) need not be themselves invariant. Equivalently, elements of G act as automorphisms of the whole system with its evaluating structures.

Invariance by a concrete category has several possible formulations (such as ∀f∈Mor(E,F), ∀rPE, ∃sPF, f∈Mor((E,r),(F,s)) or the same with ∀sr) only equivalent for groupoids, thus beyond which the intended version needs to be specified. Each one implies invariance by isomorphisms (by restriction to the core), which implies invariance by Aut groups.

Like first-order invariants, all these invariants of any kind can be obtained as trajectories or orbits of undefined first-order structures. But in search for appropriate ones to formalize as systems the objects of a given concrete category (which will be called spaces in geometry), this way to get them (from undefined choices in uncountable sets) remains unsatisfactory. Methods to get specific invariant types of structures will be reviewed below.

Types constructed from a given language

Between systems with a given language, all constructed types of structures (last scheme) are invariant by isomorphisms, for the same reason as the invariance of first-order structures defined without parameter. Therefore, any type of structures defined from some invariant structures of a given concrete category, is also invariant by the core of that category.
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.

Endomorphisms

The concept of endomorphism monoid M = End E, as a type of transformations of each object E, is invariant by isomorphisms. The concept Aut of autmorphism group, as a definable subset of M, is thus also invariant by isomorphisms. If the language is finite (or if its infinity of symbols is usable as type) then they are "second-order constructible" in the sense of definable from the full type of transformations.

Parametered subspaces

For a fixed set K, giving to any set E in a class, a type of structures E(K)EK, defines a concrete category of the fFE preserving it in the sense that cf[E(K)] ⊂ F(K), denoting ∀xEK, cf(x) = fx.

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.

Following the concept of concretization, the type E(K) = Mor(K,E) of K-parametered subspaces of E is an invariant second-order structure as ∀f∈Mor(E,F), cf coincides on E(K) with Hom(K,f) : E(K)F(K).
If K has a basis B then this structure is synonymous with a structure of K-algebra seeing K as the set of all B-ary algebraic symbols relevant to this category.

Dual types

A K-dual type is a type of structures E'KE, on each space E. It defines a concrete category whose duality morphisms f∈Mord(E,F)⊂FE are the functions preserving this duality structure by acting there on the opposite side as their transpose tf : F'E'

fFE, ∀uF', tf(u) = uf
Mord(E,F) = {fFE | tf[F']⊂E'}
f∈Mord(E,F), ∀g∈Mord(F,G), t(gf) = tftg : G'E'
f∈Mord(E,F), Im f = F ⇒ Inj tf.

The effectiveness of a dual E' (∀xyE, ∃uE', uxuy), which means the injectivity of

h = ∏E' : EKE'

implies that of Mord(F,E) on the dual type (∀fg∈Mord(F,E), tftg).
In any concrete category, any choice of an object K defines a K-dual type as E' = Mor(E,K).
This is an invariant of this category (Mor(E,F) ⊂ Mord(E,F)) because ∀f∈Mor(E,F), tf|F' = HomF(f,K) : F'E'.
Moreover Mord(E,K) = E' because IdKK' ∴ ∀f∈Mord(E,K), f = IdKf = tf(IdK) ∈ E'.
When effective, the duality structure suffices to define all algebraic structures on any object E as determined by those on K: E'⊂ MorL(E,K) ⇒ E∈SubLKE' as a product of algebras:

E'⊂ MorL(E,K) ⇔ (∀uE', φKLu = u০φE) ⇔ h০φE = ∏uE' φKLu = φKE'Lh.

Naturally as they are defined from duality, algebraic structures are also preserved by duality morphisms (Mord(E,F) ⊂ MorL(E,F)): as F' is effective,

f∈Mord(E,F), ∀uF', ufE'uf০φE = φKLuLf = u০φFLf.

Subspaces, embeddings and sections

From Mor(K,E), further invariant second-order structures on E can be defined, depending on the isomorphism class of K but no more using K as a base type or a list of symbols. First is the set {Im f | f ∈ Mor(K,E)} of images of K-parametered subspaces. Invariant subsets of this come by putting conditions on f: being injective, or an embedding, or a section. As already discussed, these are successive qualities for Im f to be a space, which means (instead of structures) to give its morphisms with other spaces.

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 form HE = {Im f| f ∈ Mor(K,E)} are preserved in the sense that f∈Mor(E,F), ∀AHE, f[A]∈HF.
But 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.

Quotients

Reversing the sides on concepts of subspaces which may be images of morphisms, injective morphisms, embeddings or sections, we get diverse ranges of equivalence relations. Let us further comment the one reversing the concept of embedding which gave statuses of sub-objects to some subsets.

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) P = E/R of an object E by an equivalence relation R, receives a status of quotient object (P,π) when P exists as object in this category (or can be added by isomorphism with an existing object) with π∈ Mor(E,P) that is initial among all f∈Mor(E,F) (for any object F) such that R ⊂ ∼f.
Then any f∈Mor(E,F), can be said to give to its image Im f an image structure by transport from the quotient object E/∼f when it exists; this structure is generally lower than (or equal to) that of the sub-object Im f (when it exists) which is then the greatest of them. So, the inverse transport on the latter defines another structure on the quotient E/∼f, greater than that of the quotient object which is thus minimal among such. In some categories such as any category of algebras, all such structures on any given sub-object (and thus also on any quotient) with variable f coincide.
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. Second-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 :
Gödelian arguments against mechanism : what was wrong and how to do instead
Philosophical proof of consistency of the Zermelo-Fraenkel axiomatic system