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
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.
- Variables of each type (either free, or bound by the use of a
- Structure symbols (operators and predicates, from the
- One equality symbol per type (predicate with 2 arguments of
the same type) abusively all written = and interpreted in the
standard way ;
- Logical connectives ;
(1.8.): the only ones in first-order logic are the two
quantifiers (∀ and ∃, see 1.9.), but our set theory will have
The next expressions are then successively built as made of the
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.
- A distinguished choice (occurrence) of a symbol (para-operator
or binder) called the root of the expression;
- One or more variable symbols (to bind) if the root is a
- A list of occurrences of previously built expressions.
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.
- Most binary para-operator 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.
Function-like 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...).
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
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).
- An extended logical framework accepting variable structure
symbols (such as second-order logic);
- Again, an extended theory where this symbol is added to the language.
- A special purpose : definitions of binders (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
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
- 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.
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.
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.