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, among which can be free variables and bound variables (as
explained below), and that will give (define) a value for each possible
Any expression is either a term or a formula:
the values of terms will be objects, while formulas
will have boolean values.
- a system interpreting the given types and structure symbols;
- fixed values of the free variables of the expression in this system.
An expression is ground if it has no free
variable (all its variables are bound) so that its value only depends on the system.
Let us sketch the general description of expressions (which will be formalized
as mathematical systems for the case of algebraic terms in 4.1).
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 of first-order theories or set theory may use symbols of
the following kinds.
Binders, connectives and equality are called logical symbols as
they are fixed with their meaning by the logical framework, which is why they are not
listed in the languages of individual theories.
- Variables of each type, may they be free or bound : see the use binders below and in 1.8 ;
- 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 will be introduced in 2.4.
- Binders (1.8),
letting a variable be used as free in its sub-expression, while it is seen as bound
and thus unavailable outside. First-order logic only has both quantifiers ∀ ("for all")
and ∃ ("there exists"), introduced in 1.9, but our set theory will have more.
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
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 their list of arguments.
- A distinguished choice (occurrence) of a symbol (para-operator
or binder) called the root of the expression;
- If the root is a binder: one or more variable symbols, to be bound by it;
- A list of occurrences of previously built expressions.
The list was empty for constants, which formed expressions
alone (as roots). Other para-operators and binders need a
nonempty list, which requires a choice of display convention:
Parenthesis can also be used to distinguish (separate) the
subexpressions, thus distinguish the root of each expression or subexpression
from other occurring symbols (roots of their subexpressions). For example the root of
(x+y)n is the exponentiation operator.
- Most binary para-operator symbols are displayed as one
character between 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 objects ;
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 by their special way of putting
their arguments together (multiplication xy, exponentiation
Parenthesis can be part of the notation of a
symbol (function evaluator, tuples...).
Usually, only few objects are named by the constants in a given language.
Other objects can be named by fixed variables, whose status
depends on the choice of theory to see it:
The difference vanishes in generic interpretations which turn
constant symbols into variables (whose values define different models).
- Ordinary variable symbols, usable in the theory by expressions,
which using binders can let them range over all objects of their type;
- New constant symbols, to be added to the language, forming another
theory with a richer language;
By similarity to constants which are particular structures (nullary operators,
naming a fixed object), the concept of variable (naming possible objects) can
be generalized to that of variable structure, naming possible structures.
But those beyond nullary operations (= ordinary variables) escape the above
list of allowed symbols in expressions in first-order theories or set theory. Still,
the use of variable structure symbols can find justifications in specific contexts
by development of this logical framework itself, as abbreviations
(indirect descriptions) of the use of legitimate expressions. The main case of
this is explained below; more possible uses will be discussed in 1.9.
Structures defined by expressions
In any theory, one can legitimately introduce a symbol meant either as a variable structure
(operator or predicate, beyond those directly named in its language) or a Boolean variable
(which is the remaining kind of para-operator without Boolean arguments, other than structures),
as abbreviation of, thus defined by, the following data :
The variability of this structure
is the abbreviation of the variability of all its parameters. So it can be bound by
the theory to range over all structures defined by a common expression with all
possible values of its parameters, as an abbreviation of the act of binding
- An expression (operators are defined by terms, while
predicates are defined by formulas);
- Among its free variables (maybe not all used), 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.
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).
Now let us consider (the range of) the meta-notion of structure, 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 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 (of types interpreted by) finite sets with given size
limits, can be reached by one expression whose size depends on these limits.
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.
An invariant structure for a given interpreted language, is a structure
defined from it 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 deep meaning of the theory,
are the meta-notions of structure, invariant structure, and the range of theorems
expressible with the previous language.
The role of axioms
The axioms list of a theory is a set of ground formulas, meant as stating the truth of these
formulas 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 systems selected
as those where all axioms are true (from the range of all possible systems
structured by the given language), rejecting others where some axiom is false.