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(x1,..., xn)), true for a unique value of y for any chosen values of x1,..., xn.

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 xE, 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.

Set theory and Foundations of mathematics
1. First foundations of mathematics
1.1. Introduction to the foundations of mathematics
1.2. Variables, sets, functions and operations
1.3. Form of theories: notions, objects, meta-objects
1.4. Structures of mathematical systems
1.5. Expressions and definable structures
1.6. Logical connectives
1.7. Classes in set theory
1.8. Binders in set theory
1.9. Quantifiers
1.10. Formalization of set theory
1.11. Set generation principle
Philosophical aspects
Time in model theory
Time in set theory
Interpretation of classes
Concepts of truth in mathematics
2. Set theory (continued) 3. Algebra 4. Model theory
Other languages:
FR : 1.4. Structures des systèmes mathématiques