## 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, where, intuitively speaking, an occurrence of a symbol in an expression is a place where that symbol is written (more details later).

Each expression comes in the context of a given list of available free variables. Any expression will give (define) a value (either an object or a Boolean) for each possible data of

• A system interpreting the given types and structure symbols;
• Fixed values of available free variables in this system.
The type of an expression, determined by its syntax as described below, gives the type of all its possible values. Expressions with Boolean type are called formulas; others, whose type belongs to the given types list (their values will be objects), are called terms.

For example, « x+x » is a term with two occurrences of the variable «x», and one of the addition symbol «+».

### The diverse kinds of symbols

In expressions of first-order theories and set theory, symbols of the following kinds may occur.
• Variables of each type:
• Free variables, from the list of available ones ;
• Bound variables, whose occurrences are contained by binders (see 1.8) ;
• Para-operator symbols:
• Structure symbols from the language (operators and predicates) ;
• One equality symbol per type (predicate with 2 arguments of the same type) abusively all written = ;
• Logical connectives (1.4, listed in 1.6) ;
• The conditional operator may be introduced for abbreviation (2.4).
• Binders (1.8):
• Quantifiers ∀ and ∃ (1.10) are the only primitive binders of first-order logic ;
• More binders will be introduced in set theory.
In first-order logic, let us call logical symbols the quantifiers and symbols of para-operators outside the language (equality, connectives and conditional operator): their list and their meaning in each system are determined by the logical framework and the given types list, which is why they are not listed as components of individual theories.

### Root and sub-expressions

Each expression contains a special occurrence of a symbol called its root, while each other occurrence of a symbol there, is the root of a unique sub-expression (another expression contained in the given one, and which we may call the sub-expression of that occurrence). The type of an expression is given by the type of result of its root.

Expressions are built successively, in parallel between different lists of available free variables. The first and simplest ones are made of just one symbol (as root, 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:

• A choice of root, occurrence of either a para-operator symbol (beyond constants we already mentioned) or a binder;
• If the root is a binder: a choice of variable symbol, to be bound by it;
• A list of previously built expressions, whose format (number and types of entries) is determined by the root : for a para-operator symbol, this format is given by its list of its arguments.
An algebraic term is a term with only free variables and operator symbols ; these are the only terms in first-order logic without conditional operator. This notion for only one type, will be formalized as a kind of system in set theory in 4.1.

### Display conventions

The display of this list of sub-expressions directly attached to the root requires a choice of convention. For a para-operator symbol other than constants :
• Most binary para-operator symbols are displayed as one character between (separating) both arguments, such as in x+y
• Symbols with higher arities can be similarly displayed by several characters separating the entries, such as in the addition x+y+z of 3 numbers.
• Function-like displays, such as +(x,y) instead of x+y, are more usual for arities other than 2 ; parenthesis may be omitted when arities are known (Polish notation).
• A few symbols «appear» only implicitly by their special way of putting their arguments together : multiplication in xy, exponentiation in xn.
• Parenthesis can be part of the notation of a symbol (function evaluator, tuples...).
Parenthesis can also be used to distinguish (separate) the subexpressions, thus distinguish the root of each expression from other occurring symbols. 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. Any other objects can be named by a fixed variable, whose status depends on the choice of theory to see it:
• An ordinary variable symbol, usable by expressions which by a binder can let it range over some notion;
• A new constant symbol, to be added to the language, forming another theory with a richer language.
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), the concept of variable can be generalized to that of variable structure. But those beyond nullary operations (ordinary variables) escape the above list of allowed symbols in expressions. Still some specific kinds of use of variable structure symbols can be justified as abbreviations (indirect descriptions) of the use of legitimate expressions. The main case of this is explained below, forming a development of the theory ; more possible uses will be introduced in 1.10 (the view of a use as an abbreviation of other works amounts to using a developed version of the logical framework).

### Structures defined by expressions

In any theory, one can legitimately introduce a symbol meant either as a variable structure (operator or predicate) or a Boolean variable (nullary predicate, not a "structure"), as abbreviation of, thus defined by, the following data :
• An expression (terms define operators, while formulas define predicates and Booleans);
• Among its available free variables, a selection of those which will be bound by this definition in the role of arguments of the intended structure; the rest of them, which remain free, are called parameters;
• Each of its possible values as a structure or a Boolean comes by fixing the values of parameters.
The variability of this structure is the abbreviation of the variability of all its 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 declare the meta-notion of "structure" in one-model theory, 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 range of all combinations of an expression with fixed values of its parameters. As this involves the infinite set of all expressions, this meta-notion usually escapes (is inaccessible by) the described theory itself : no fixed expression can suffice to simulate it. 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 finite sets (as interpreted types) with given size limits, can be reached by one expression whose size depends on these limits.

### Invariant structures

An invariant structure of a given system (interpreted language), is a structure defined from its language 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.10, 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 meaning of the theory, are the meta-notions of structure, invariant structure, and the range of theorems expressible with the previous language.

 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 2. Set theory - 3. Algebra - 4. Arithmetic - 5. Second-order foundations
Other languages:
FR : 1.5. Expressions et structures définissables