1.5. Expressions and definable structures

Terms and formulas

Given the first two layers of a theory (a list of types and a language), an expression is a finite system of occurrences of symbols, among which can be free variables and bound variables (as explained below), and that will give (define) a value for each possible data of Any expression is either a term or a formula: the values of terms will be objects, while formulas will have boolean values.
An expression is ground if it has no free variable (all its variables are bound) so that its value only depends on the system.

Let us sketch the general description of expressions (which will be formalized as mathematical systems for the case of algebraic terms in 4.1).

An occurrence of a symbol in an expression is a place where it is written, for example «x + x» has two occurrences of x and one of +. Expressions of first-order theories or set theory may use symbols of the following kinds. Binders, connectives and equality are called logical symbols as they are fixed with their meaning by the logical framework, which is why they are not listed in the languages of individual theories.
Expressions are built successively. The first and simplest ones are made of just one symbol already having a value by itself: constants and variables are the first terms; the Boolean constants 1 and 0 are the simplest formulas.
The next expressions are then successively built as made of the following data: The root determines the type of values (thus decides if the expression is a formula or a term) and the format of the list (the number and types of entries). For para-operator symbols, this format is given by their list of arguments.
The list was empty for constants, which formed expressions alone (as roots). Other para-operators and binders need a nonempty list, which requires a choice of display convention: Parenthesis can also be used to distinguish (separate) the subexpressions, thus distinguish the root of each expression or subexpression from other occurring symbols (roots of their subexpressions). For example the root of (x+y)n is the exponentiation operator.

Variable structures

Usually, only few objects are named by the constants in a given language. Other objects can be named by fixed variables, whose status depends on the choice of theory to see it: The difference vanishes in generic interpretations which turn constant symbols into variables (whose values define different models).
By similarity to constants which are particular structures (nullary operators, naming a fixed object), the concept of variable (naming possible objects) can be generalized to that of variable structure, naming possible structures. But those beyond nullary operations (= ordinary variables) escape the above list of allowed symbols in expressions in first-order theories or set theory. Still, the use of variable structure symbols can find justifications in specific contexts by development of this logical framework itself, as abbreviations (indirect descriptions) of the use of legitimate expressions. The main case of this is explained below; more possible uses will be discussed in 1.9.

Structures defined by expressions

In any theory, one can legitimately introduce a symbol meant either as a variable structure (operator or predicate, beyond those directly named in its language) or a Boolean variable (which is the remaining kind of para-operator without Boolean arguments, other than structures), as abbreviation of, thus defined by, the following data : The variability of this structure is the abbreviation of the variability of all its parameters. So it can be bound by the theory to range over all structures defined by a common expression with all possible values of its parameters, as an abbreviation of the act of binding these parameters.

In set theory, any function f is synonymous with the functor defined by the term f(x) with argument x and parameter f (but the domain of this functor is Dom f instead of a type).
The terms without argument define simple objects (nullary operators) ; the one made of a variable of a given type seen as parameter suffices to give all objects of its type.

Now let us consider (the range of) the meta-notion of structure, and thus those of operator and predicate, as having to include at least all those reachable in this way: defined by any expression with any possible values of parameters. The minimal version of such a meta-notion can be formalized as a role given to the data of an expression with values of its parameters. As this involves the infinite set of all expressions, it is usually inaccessible by the described theory itself (no single expression can suffice). Still when interpreting this in set theory, more operations between interpreted types (undefinable ones) usually exist in the universe. Among the few exceptions, the full set theoretical range of a variable structure with all arguments ranging over (of types interpreted by) finite sets with given size limits, can be reached by one expression whose size depends on these limits.

Invariant structures

An invariant structure for a given interpreted language, is a structure defined from it without parameters (thus a constant one). This distinction of invariant structures from other structures, generalizes the distinction between constants and variables, both to cases of nonzero arity, and to what can be defined by expressions instead of directly named in the language.
Indeed any structure named by a symbol in the language is directly defined by it without parameter, and thus invariant. As will be further discussed in 4.8, theories can be developed by definitions, which consists in naming another invariant structure by a new symbol added to the language. Among aspects of the preserved deep meaning of the theory, are the meta-notions of structure, invariant structure, and the range of theorems expressible with the previous language.

The role of axioms

The axioms list of a theory is a set of ground formulas, meant as stating the truth of these formulas in intended model(s). Depending on intentions (discussed in 1.A), this may either mean to describe a presumably given model or range of models, or to define the range of accepted models as the class of systems selected as those where all axioms are true (from the range of all possible systems structured by the given language), rejecting others where some axiom is false.

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.5. Expressions et structures définissables