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:
- For a relation : ∀k,k'∈P, (∀x1,...,xn,
(x1,...,xn)∈k
⇔ (x1,..., xn)∈k')
⇒ k = k' (axiom of extensionality)
- For an operation :
∀k,k'∈P, (∀x1,...,xn,
k(x1,...,xn)
= k'(x1,...,xn))
⇒ k = k' (axiom of effectiveness)
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
- 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 consistency of the theory is preserved (provably equivalent
to the one before extension).
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), ∀r∈PE,
∃s∈PF, f∈Mor((E,r),(F,s)) or the
same with ∀s ∃r) 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 f∈FE
preserving it in the sense that
cf[E(K)] ⊂ F(K), denoting
∀x∈EK, cf(x) = f০x.
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'
∀f∈FE, ∀u∈F',
tf(u) = u০f
Mord(E,F) = {f∈FE |
tf[F']⊂E'}
∀f∈Mord(E,F),
∀g∈Mord(F,G), t(g০f)
= tf০tg : G'→E'
∀f∈Mord(E,F), Im f = F ⇒
Inj tf.
The effectiveness of a dual E' (∀x≠y∈E,
∃u∈E', u⋅x≠u⋅y), which means the injectivity of
h = ∏E' : E →
KE'
implies that of Mord(F,E) on the dual type
(∀f≠g∈Mord(F,E), tf ≠ tg).
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
IdK∈K' ∴ ∀f∈Mord(E,K),
f = IdK০f = 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) ⇔
(∀u∈E', φK০Lu
= u০φE) ⇔ h০φE =
∏u∈E' φK০Lu
= φ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),
∀u∈F', u০f ∈ E' ∴ u০f০φE
= φK০Lu০Lf
= u০φF০Lf.
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), ∀A∈HE,
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
More philosophical notes :