1.4. Structures of mathematical systems
The structures, interpreting the language of a theory
(values of structure symbols in a set theoretical interpretation), relate
the objects of diverse types to form the studied system. These
structures give their roles to the objects of each type with
respect to those of other types, for them to form a system.
According to these roles, objects may be interpreted as
complex objects, in spite of their basic nature of pure elements.
Generic theories admit 2 kinds of structures (and thus of structure
symbols): operators and predicates.
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 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
(this should not be confused with the concept of functor in category theory).
The list of types is completed by the Boolean type,
interpreted as the pair of elements 1 («true») and 0 («false»). A
variable of this type (outside the theory) is called a Boolean
variable.
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
and values.
A predicate is a relation between interpreted types, i.e.
a para-operator with Boolean result («true»
or «false») and at
least one argument but no Boolean argument.
As will be formalized in 2.4.,
an n-ary operation or operator f may be reduced to the (n+1)-ary
relation or predicate (y = f(x_{1},...,
x_{n})), true
for a unique value of y for any chosen values of
x_{1},..., x_{n}.
Structures of set theory
Let us start formalizing set theory with 3 primitive notions
(sorts of objects) : elements (all objects), sets and functions.
This formalization will be progressively developed as needed, with
other notions that may be seen either as primitive or derived from
the former, and other symbols contributing to give their roles to
all kinds of objects. But this formalization work requires to
ignore the above set theoretical interpretation of theories, as
both links between formalized generic theories and set theory
should not be confused (the set theoretical translation of
theories is not yet applied to set theory itself, this will be discussed
in 1.7).
One way for set theory to give sets their role is by the binary
predicate ∈ : for any element x and any set E, we
say that x is in E (or belongs to E, or is
an element of E, or that 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 in Dom f.
About ZFC axiomatic set theory
The Zermelo-Fraenkel axiomatic 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.
Specialists of mathematical logic chose it for their need of a
powerful theory in an enlarged founding cycle, by which they can
prove many difficult formulas or their unprovability. Then, authors
of basic courses usually present set theory as a popularized or
implicit version of the ZFC theory, admitted as the standard
reference, as if this was necessary or obvious (as an intuititively
motivated axiomatic system, historically selected for its consistency and the
convenience of its results).
But for a start of mathematics, ZF(C) is not an ideal reference. Its
axioms (descriptions of the universe that must assume the framework
of model theory to make sense) would deserve more subtle and complex
justifications than usually assumed. Ordinary mathematics, using
many objects usually not seen as sets, are only inelegantly
formalized 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.
Types in one-model theory
As one-model theory ignores the diversity of possible models, its notion of type
can be formalized ignoring the more general (set theoretical) notion of
«set of objects» (of which the interpreted types are particular cases), as
just one meta-notion playing both roles of abstract types (in the theory)
and of interpreted types (components of the model) : these roles are
given by meta-functors, one from variables to types, and one from objects to
types. A larger range of notions, the classes, will be introduced in 1.7.
Structures in one-model theory
Similarly, the role of «structures» (that is an operation between
interpreted types, with Boolean values if a predicate) can be
formalized by meta-structures (similar to the function evaluator).
Unlike interpreted types (all named by abstract types), our notion
of structure in one-model theory will be larger than that of values
of the symbols in the given language. For this, structures will be
another meta-type with a meta-functor from symbols to structures.
However, this mere formalization would leave the exact extension of
this notion of structure undetermined.
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.
Instead, we will fix in 1.5 the notion of structure as given by those
definable by expressions.
Other languages:
FR : 1.4. Structures des systèmes
mathématiques