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 (that is either a term or a formula), is a finite system of occurrences
of symbols, where an occurrence of a symbol in an expression is a place where
that symbol is written (for example the term « x+x » has two occurrences
of x and one of +).
Each expression comes in the context of a given list of available free variables.
In expressions of firstorder 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) ;
 Paraoperator
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.9) are the only primitive binders of firstorder logic ;
 More binders will be introduced in set theory.
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.
In firstorder logic, let us call logical symbols the quantifiers and symbols of
paraoperators 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.
Let us sketch a more precise description (the case of expressions with only free
variables and operator symbols, called algebraic terms, will be formalized in
set theory in 4.1 for only one type).
Each expression contains a special occurrence of a symbol called its root,
while each other occurrence is the root of a unique subexpression
(another expression which we may call the subexpression of that occurrence).
The type of an expression, which will be the type of its values, is given
by the type of result of
its root. Expressions with Boolean type are formulas; others, whose type belongs
to the given types list, are terms (their values will be objects).
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 paraoperator 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
paraoperator symbol, this format is given by its list of its arguments.
Display conventions
The display of this list of subexpressions directly attached to the root requires a
choice of convention. For a paraoperator symbol other than constants :
 Most binary paraoperator 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.
 Functionlike 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
x^{n}.

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.
The role of axioms
An expression is ground if its list of available free variables is empty,
so that its value only depends on the system where it is interpreted.
In firstorder logic, a statement is a ground formula (which may be
true or false depending on the system).
The axioms list of a theory is a set of statements, meant as stating the
truth of these statements 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 all systems where all
axioms are true, so selected from the range of all possible systems structured
by the given language, (rejecting others where some axiom is false).
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 all objects of its type;
 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.9 (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 range of) the metanotion of "structure" in onemodel 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 metanotion 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 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.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 meaning of the theory,
are the metanotions of structure, invariant structure, and the range of theorems
expressible with the previous language.
Other languages:
FR : 1.5. Expressions
et structures définissables