1.4. Structures of mathematical systems
The structures, designated in each interpretation by the structure symbols forming a
given language, form a described system by relating the objects of the diverse types, giving their
roles to the objects of each type with respect to those of other types. Depending on details, the
roles so given to objects of some types may be understood as those of complex
objects, though all this can work with bare objects like urelements.
First-order structures
The kinds of structures (and thus the kinds of structure symbols) allowed in
first-order theories, thus called first-order structures, are split into operators
and predicates as described below. 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.
An operator is an operation between interpreted types.
On the side of the theory before interpretation, each operator symbol
comes with its symbol type made of
- its list of arguments (variable symbols figured as places
around the operator symbol instead of names),
- for each argument, its abstract type, whose value as a set will be the
range of this argument in any interpretation;
- its type of results: the type which will contain all results of the operation
designated by this symbol, in any interpretation with given values of its arguments.
In a theory with only one type, this data is reduced to the arity.
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
(*).
The list of types is completed by the Boolean type, interpreted as the pair of elements
(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 variable.
A para-operator is an operator in the generalized sense allowing the
Boolean type among its types of arguments and results.
A (logical) connective is a para-operator with only Boolean arguments
and values.
A predicate is a para-operator with Boolean values, and at
least one argument but no Boolean argument.
Structures of set theory
Formalizing set theory, means describing it as a theory with its notions, structures
and axioms. We shall do this in a dedicated logical framework, different from
but convertible into first-order logic by a procedure described in 2.1.
This relates the terminologies of set theory and one-model theory
in a different way than when a theory is interpreted in set theory. To keep the
natural names of set theoretical notions (sets, functions...) when defined by
this formalization, it would become incorrect to still use them 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.
Ways to put both links together, and to reconcile both conceptions of the same
theories (descriptions by model theory and interpretations in set theory) will
be described in 1.7 and 1.D.
Let us admit 3 primitive notions : elements (all objects), sets and functions. Here are
their main primitive structures.
One aspect of the role of sets is given by the binary
predicate ∈ of belonging or membership : 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 a possible value of the variables 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.
More primitive symbols
will be presented in 1.7 and 1.8, then most other primitive symbols and axioms
will be introduced in 1.A, 2.1, 2.2 and 2.7.
About ZFC 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 math 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 of mathematics.
- Ordinary mathematics, using many objects usually not seen as sets,
are only inelegantly developed from 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
To formalize one-model theory through the use of 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, from meta-structures similar to
the function evaluator (see 3.2-3.3 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.7), but its meaning will still depend on the
universe where it is interpreted, far from our present concern for one-model theory.
Other languages:
FR : 1.4. Structures des systèmes
mathématiques