3.1. Systèmes relationnels et catégories concrètes

Formalisons le concept de système, principalement pour simplifier ceux à un seul type. Pour tout nombre n∈ℕ et tout ensemble E, notons Un langage L est un ensemble de symboles, avec la donnée de l'arité voulue ns∈ℕ pour chaque sL. Pour tout ensemble E, soit

LE = ∐sL Ens

Un langage relationnel est un langage L de symboles de relation, où chaque sL vise à être interprété dans tout ensemble E comme une relation ns-aire. Ils forment une famille appelée une L-structure sur E, élément de

sL ℘(Ens) ≅ ℘(LE)

Un système relationnel de langage L, ou L-système, est la donnée (E,E) d'un ensemble E et d'une L-structure ELE.

Le cas d'un langage algébrique, dont les symboles visent à représenter des opérations, sera étudié en 3.2.

Le plus souvent, on n'utilisera qu'une L-structure sur chaque ensemble, de sorte que E peut être vu comme implicite, déterminé par E. Précisément, imaginons donnée une classe de L-systèmes où chaque E est l'intersection de LE avec une classe fixe de (s,x), notée comme prédicat s(x) pour sa currification naturelle: chaque symbole sL s'interprète dans chaque système E comme la relation ns-aire sE en quelque sorte indépendante de E,

sE = {xEns | s(x)} = E(s)
E = {(s,x)∈LE | s(x)} = ∐sL sE.

Pour toute fonction f : EF, soit fL : LELF définie par (s,x) ↦ (s,fx).
Morphisme. Entre deux L-systèmes E,F, on définit l'ensemble MorL(E,F) ⊂ FE des L-morphismes de E vers F par ∀fFE,

f ∈ MorL(E,F) ⇔ ∀(s,x)∈E, (r,fx)∈F
⇔ (∀sL,∀xEns, s(x) ⇒ s(fx))
fL[E]⊂FEfL*F.

Catégories concrètes

Le concept de catégorie concrète est ce qui reste d'une classe de systèmes et leurs morphismes, oubliant quelles sont les structures que les morphismes préservent (cette liste de structures pouvant s'étendre sans affecter les ensembles de morphismes). Formalisons les catégories concrètes comme constituées des données suivantes (les rendant légèrement "plus concrètes" que le concept officiel de catégorie concrète d'autres auteurs)
satisfaisant les axiomes suivants:
La dernière condition se vérifie facilement pour les L-morphismes : ∀(s,x)∈E, (s,fx)∈F ∴ (s,gfx)∈G.
Un symbole relationnel s avec la donnée d'une interprétation sEEns dans chaque objet E d'une catégorie concrète donnée, est dit préservé si tous les morphismes de la catégorie sont aussi des morphismes pour ce symbole : ∀f∈Mor(E,F), ∀xsE, fxsF. Par définition, chaque symbole d'un langage L est préservé dans toute catégorie de L-systèmes.

Une catégorie est petite si sa classe d'objets est un ensemble.

Préservation de structures définissables

Dans toute catégorie de L-systèmes, ou toute catégorie concrète avec une liste L de symboles interprétés préservés, toute autre structure invariante définie par une formule n'utilise que les symboles de L et les symboles logiques ∧,∨,0,1,=,∃ est préservée.
En effet, pour tout L-morphisme f∈MorL(E,F), Donc pour tout f ∈MorL(E,F), si une formule close de langage L utilisant les seuls symboles logiques (=,∧,∨,0,1,∃), est vraie dans E, elle est alors vraie dans F. Cependant les morphismes peuvent ne plus préserver les structures définies à l'aide d'autres symboles (¬,⇒,∀).

Les cas de 0, 1, ∨ et ∧ ne sont que des cas particuliers (nullaires et binaires) de ceci:

Reconstruire les structures dans une catégorie concrète

Les relations préservées de toute catégorie concrète sont engendrables par les sortes suivantes de "plus petits blocs".

Proposition. Dans toute catégorie concrète, pour tout choix d'un uplet t d'éléments d'un objet K, la relation s définie dans chaque objet E par sE = {ft | f∈Mor(K,E)} est préservée.

Preuve : ∀g∈Mor(E,F), ∀xsE, ∃f∈Mor(K,E), (x = ftgf∈Mor(K,F)) ∴ gx = gftsF.∎
De ces définitions il pourrait résulter entre objets EF que sEsFEn mais nous n'aurons pas affaire à ce cas.

Dans une petite catégorie concrète, les familles de relations préservées sont précisément toutes les unions possibles de ceux-ci : chaque s préservé coïncide avec l'union de ceux pour t parcourant s (où K parcourt tous les objets).

Cependant la classe des systèmes relationnels obtenue même en donnant ainsi "toutes les structures possibles" aux objets d'une catégorie concrète donnée par ailleurs comme la topologie, peut encore admettre plus de morphismes que ceux dont on est partis (comme une clôture).

Catégories de systèmes typés

Ayant introduit la notion de morphisme dans le cas de systèmes avec un seul type, on peut l'étendre à des systèmes de plusieurs types. Entre les systèmes E,F avec une liste commune τ de types (et des interprétations d'une liste commune de symboles de structure), les morphismes peuvent se concevoir des 2 manière équivalentes suivantes, en plus d'avoir à conserver toutes les structures:
Set theory and foundations of mathematics
1. First foundations of mathematics
2. Set theory (continued)
3. Algebra 1
3.1. Relational systems and concrete categories
3.2. Algebras
3.3. Special morphisms
3.4. Monoids
3.5. Actions of monoids
3.6. Invertibility and groups
3.7. Categories
3.8. Algebraic terms and term algebras
3.9. Integers and recursion
3.10. Arithmetic with addition
4. Model Theory