1.4. Structures of mathematical systems
The structures, interpreting the language of a theory, relate the objects
of diverse types, giving their roles to the objects of each type with respect to
those of other types, to form the studied system. According to these roles,
objects may be thought of as complex objects, in spite of have otherwise no
nature like pure elements.
The kinds of structures (and thus also the kinds of structure symbols) for
theories allowed by first-order logic, thus called first-order structures,
will be classified into operators and predicates. We shall
describe them as operations designated by structure symbols in a set
theoretical interpretation. More powerful structures called second-order
structures will be introduced in 5.1, coming from set theoretical tools or as
packs of an additional type with first-order structures.
Any generic theory can be interpreted (inserted, translated) in set theory
by converting its components into components of set theory. This is the usual
view of ordinary mathematics, studying many systems as «sets with relations or
operations such that...», with possible connections between these systems.
Let us introduce both the generic interpretations applicable to any generic
theory, and other ones usually preferred for particular theories.
Any interpretation converts each abstract type into a symbol (name) designating
a set called interpreted type (serving as the range of variables of that type,
whose use is otherwise left intact). This symbol is usually a fixed variable in the
generic case, but can be accepted as constant symbol of set theory in special
cases such as numbers systems (ℕ, ℝ...).
Generic interpretations will also convert structure symbols into fixed
variables (while standard ones may define these from the language of
set theory). Any choice of fixed values of all types and structure symbols,
defines a choice of model. Models become objects of set theory, owing their
multiplicity to the variability of types and structure symbols. This
integrates all needed theories into the same set theory, while
gathering all their models inside a common model of set theory. This is
why a model of set theory is called a universe.
In generic interpretations, all objects (elements of interpreted types) are
pure elements, but other kinds of interpretations called standard
by convention for specific theories may do otherwise.
For example, standard interpretations of geometry represent points by
pure elements, but represent straight lines by sets of points.
An operator is an operation between interpreted types.
On the side of the theory before interpretation, each operator
symbol comes with the data of the list of arguments (figured
as places around the symbol), the type of each argument (as this argument
will range over that interpreted type), and the unique type of all
values (results of the operation). In a theory with only one
type, this data is reduced to the arity.
The list of types is completed by the Boolean type,
interpreted as the set of two elements we shall denote 1 for «true» and 0 for
«false». A variable of this type (outside the theory) is called a Boolean
The constant symbols (or constants) of a theory
are its nullary operator symbols (having no argument).
Unary operators (that are functions) will be called here functors
A para-operator is a generalized operator allowing the
Boolean type among its types of arguments and results.
A (logical) connective is a para-operator with only Boolean arguments
A predicate is a para-operator with Boolean values, and at
least one argument but no Boolean argument.
As will be formalized in 2.4.,
an n-ary operator f may be reduced to the (n+1)-ary predicate
(y = f(x1,...,xn)), true for a
unique value of y for any
chosen values of x1,...,xn.
Structures of set theory
Formalizing set theory, means describing it as a theory with its notions,
structures and axioms. We shall admit 3 primitive notions : elements (all objects),
sets and functions. Their main primitive structures are introduced below.
Most other primitive structures and axioms will be presented in 1.8, 1.10
and 1.11, in a dedicated logical framework, convertible into first-order logic
by a procedure also described in 1.10. Still more primitive components will be
added later (2.1, 2.4, 2.5, 2.10, 4.3).
This link between set theory and (one-)model theory (viewing set theory as
based on model theory), which relates the terminologies of both theories, differs
from the one given by conversions of generic theories into set theory. As the set
theoretical notions (sets, functions...) need to keep their natural names when
defined by this formalization, it would become incorrect to keep that terminology
for their use in the sense of the previous link (where notions were "sets" and
operators were "operations"). To avoid confusion, let us here only use the model theoretical
notions as our conceptual framework, ignoring their set theoretical interpretations.
We shall describe in 1.7 how both links can be put together, and
how both ways to conceive the same theories (describing them by model
theory or using a set theoretical interpretation) can be reconciled.
One aspect of the role of sets is given by the binary predicate ∈ : for any
element x and any set E, we say that x is in E
(or x belongs to E, or x is an element of E, or
E contains x) and write x ∈ E, to mean that
x is among the values of a variable with range E.
Functions f play their role by two operators: the domain
functor Dom, and the function evaluator, binary operator
that is implicit in the notation f(x), with arguments
f and x, giving the value of any function f
at any element x of Dom f.
About ZFC axiomatic set theory
The Zermelo-Fraenkel set theory (ZF, or ZFC with the axiom of choice)
is a generic theory with only one type «set», one structure symbol ∈ ,
and axioms. It implicitly assumes that every object is a set, and thus a set
of sets and so on, built over the empty set. As a rather simply expressible
but very powerful set theory for an enlarged founding cycle, it can be a good
choice indeed for specialists of mathematical logic to conveniently prove diverse
difficult foundational theorems, such as the unprovability of some statements,
while giving them a scope that is arguably among the best conceivable ones.
But despite the habit of authors of basic courses to conceive their
presentation of set theory as a popularized or implicit version of ZF(C), it is
actually not an ideal reference for a start of mathematics for beginners:
- It cannot be self-contained as it must assume the framework of model
theory to make sense
- Its axioms, usually just admitted (as either intuitive,
obvious, necessary or just historically selected for their consistency and the
convenience of their consequences), would actually deserve more subtle and
complex justifications, which cannot find place at a starting point.
- Ordinary mathematics, using many objects usually not seen as sets,
are only inelegantly developed on this basis. As the roles of all needed
objects can anyway be indirectly played by sets, they did not require another
formalization, but remained cases of discrepancy between the
«theory» and the practice of mathematics.
The complexity and weirdness of these needed developments
do not disturb specialists just because once known possible, they
can simply be taken for granted.
Formalizing types and structures as objects of one-model theory
Now to describe one-model theory as a theory using the meta prefix,
both meta-notions of "types" and "structures" are given their roles by
meta-structures as follows.
Since one-model theory assumes a fixed model, it only needs one
meta-type of "types" to play both roles of abstracts types (in the theory)
and interpreted types (components of the model), respectively given by
two meta-functors: one from variables to types, and one from objects
to types. Indeed the more general notion of «set of objects» is not used
and can be ignored.
But the meta-notion of structure will have to remain distinct from the language,
because more structures beyond those named in the language will be involved (1.5).
Structures will get their roles (as operations between interpreted types...) by
meta-structures similar to the function evaluator (see 3.1-3.2 for clues), while the
language (set of structure symbols) will be interpreted there by a meta-functor from
structure symbols to structures. However, this mere formalization would leave
undetermined the range of this notion of structure. Trying to conceive this range as that of
«all operations between interpreted types» would leave unknown the source
of knowledge of such a totality. This idea of totality will be formalized in set
theory as the powerset (2.5), but its meaning would still depend on the
universe where it is interpreted (assumed to contain all wanted operations),
far from our present concern for one-model theory.
FR : 1.4. Structures des systèmes