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, that will define a value for each possible data of a model (system interpreting the given types and structure symbols, ignoring axioms) and of an interpretation of the free variables it contains (their values in the model).
Any expression is either a term or a formula: the values of terms will be objects, while formulas will have boolean values.
A ground expression, is an expression with no free variable (all its variables are bound) so that its value only depends on the model. The axioms of a theory are chosen among its ground formulas.

Let us sketch the general description of expressions (that will be formalized in Part 3).

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 may use symbols of the following kinds. 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 the list of arguments.
The list was empty for constants, that, as roots, formed expressions alone. Other para-operators and binders need a nonempty list, which requires a choice of display convention: Parenthesis can also be used, for each expression or subexpression, to distinguish the root by separating the subexpressions, as in (x+y)n.

Variable structures

Only few objects are usually named by the constant symbols in a given language. Any other object can be named by another symbol outside this language: a fixed variable. This may be differently interpreted depending on the theory we consider to be in:

Trying to generalize this, from simple objects (identifiable with all nullary operations that may exist between interpreted types), to other structures (with nonzero arity), we get the concept of a symbol of variable structure, but this escapes the above list of symbols allowed in expressions. Thus, the status for expressions using such a symbol must now be chosen between

As a theory in first-order logic cannot handle the full range of a variable structure with nonzero arity (unless all its arguments range over finite sets), it cannot express all properties of this range. Still some properties can be known as follows: if a formula with a symbol of variable structure (not defined) is formally proven, then it is true for all structures it might mean, no matter if they «can be found» or not. This concept of provable universal truth will be used as a rule of proof for ordinary variables (principle of Universal Introduction in 1.9) and in the formulation of the set generation principle (1.11).

Structures defined by expressions

Any theory can produce structures (operators or predicates, beyond those directly named in its language), as the operations between interpreted types, defined by the following data: Nullary operators (simple objects) are «defined» this way by the term made of a variable symbol seen as parameter. In a formalization of set theory, any function f is synonymous with the functor defined by the term «f(x)» with argument x and parameter f.

We can accept as a legitimate work inside the theory, to name such a structure by a symbol of variable structure, meant as an abbreviation of the expression with its parameters. As the variability of the symbol abbreviates the one of parameters, this variable structure can be bound in the theory as ranging over all structures defined by a common expression with all possible values of its parameters : this just abbreviates the act of binding these parameters.

Let us now fix one-model theory's notion of structure, and thus those of operator and predicate, as made of all those which can be reached in this way: defined by any expression with any possible values of parameters. As this involves the infinite set of all expressions, it escapes the abilities of the studied theory (which can only use one expression at a time) and is only accessible by the framework of one-model theory with its meta-notion of expression. Still this does not mean to exhaust the range of all operations (between interpreted types) which may exist in the universe of a set theoretical framework, as there may be undefinable structures.

Invariant structures

An invariant structure for a theory, is a structure defined without parameters (thus a constant one). Any structure named by a symbol in the language of a theory, is directly defined by it without parameter, and thus invariant for this theory. This distinction of invariant structures from other structures, generalizes the distinction between constants and variables, both to cases of nonzero arity, and to what is indirectly expressible by the theory instead of directly named in its language.
Invariant structures not yet in the language can be named by new symbols to be added there, preserving the deep meaning of the theory (meta-notions of structure, invariant structure, provability...). Such rules to develop a theory will be discussed in Part 4.

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