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.
 Variables of each type (either free, or bound by the use of a
binder) ;
 Paraoperator
symbols:
 Structure symbols (operators and predicates, from the
language) ;
 One equality symbol per type (predicate with 2 arguments of
the same type) abusively all written = ;
 Logical connectives (1.6) ;
 Binders
(1.8.): the only ones in firstorder logic are the two
quantifiers (∀ and ∃, see 1.9.), but our set theory will have
more.
All binders and symbols of paraoperator outside the language, i.e. equality, connectives and quantifiers, are called
logical symbols, and are fixed with their meaning by the logical framework.
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:
 A distinguished choice (occurrence) of a symbol (paraoperator
or binder) called the root of the expression;
 One or more variable symbols (to bind) if the root is a
binder;
 A list of occurrences of previously built expressions.
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 paraoperator symbols, this format
is given by the list of arguments.
The list was empty for constants, that, as roots, formed expressions
alone. Other paraoperators and binders need a nonempty list, which
requires a choice of display convention:
 Most binary paraoperator symbols are displayed as one
character between both arguments, such as x+y
 Symbols with higher arities can be similarly displayed by
several characters delimiting the entries.

Functionlike displays, such as +(x,y), are more
usual for arities other than 2.

A few symbols «appear» only by their special way of putting
their arguments together (multiplication, exponentiation).

Parenthesis can be part of the notation of a
symbol (function evaluator, tuples...).
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:
 As a simple variable symbol (allowed in expressions though
not «in the language» of the theory): we can form an
expression in the theory about all objects of one
type, by using and binding this variable.
 As a new constant symbol, added to the language, with a
specific name for one specific value: we get a richer language,
for another theory. The different possible values are seen as
corresponding to different models.
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
 An extended logical framework accepting variable structure
symbols (such as secondorder logic);
 Again, an extended theory where this symbol is added to the language.
 A special purpose : definitions of binders (1.11)
As a theory in firstorder 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:
 An expression (operators are defined by terms, while
predicates are defined by formulas);
 A list of some of its free variables (maybe not all used) to be bound
by this definition in the role of arguments of the intended structure; other
free variables are called parameters;
 Fixed values of parameters.
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 onemodel 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 onemodel
theory with its metanotion 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 (metanotions of structure, invariant structure,
provability...). Such rules to develop a theory will be
discussed in Part 4.
Other languages:
FR : 1.5. Expressions
et structures définissables