1.4. Structures of mathematical systems

The structures, interpreting each structure symbol from a given language over a list of types (or notions), form a described system by relating the objects of some given types, giving their roles to the objects of each type with respect to those of other types. According to these roles, objects may be thought of as complex objects, in spite of have otherwise no nature like urelements.
The kinds of structures (and thus the kinds of structure symbols) allowed in first-order theories, 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.

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 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 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 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 para-operator with Boolean values, and at least one argument but no Boolean argument.
As will be formalized in 2.6., any 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 symbols and axioms will be presented in 1.7,1.8, 2.1 and 2.2, in a dedicated logical framework, convertible into first-order logic by a procedure also described in 2.1. Still more primitive components will be needed and added later (2.3, 2.6, 2.7, 4.3). Optional ones, such as the axiom of choice (2.12), will open a diversity of possible set theories.

This view of set theory as described by (one-)model theory, relates the terminologies of both theories in a different way than when interpreting generic theories in 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 and 1.B 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 ∈ of belonging : 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 xE, 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.

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:

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.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.7), but its meaning will still depend on the universe where it is interpreted, far from our present concern for one-model theory.

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,..., 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. Axioms and proofs
1.10. Quantifiers
Time in model theory
Set theory as unified framework
2. Set theory (continued) - 3. Algebra - 4. Arithmetic 5. Second-order foundations
Other languages:
FR : 1.4. Structures des systèmes mathématiques