An Expression is a type of LogicConcept. (For the other types, see the documentation of that class.) Expressions are mathematical statements and their sub-parts, in the usual manner of organizing into tree form what many mathematicians informally call "mathematical expressions" as trees.

For instance, $3+k=9$ and $\frac{58}{1+x}<e$ are two mathematical expressions. Their subexpressions are also expressions, including, for example, $9$, $3+k$, $1+x$, and $\frac{58}{1+x}$. Even $+$ and $=$ are subexpressions; they are functions that are being applied to arguments.

When we speak of "tree form," we refer to the idea that every expression can be organized into a tree by following the order of operations. For example, $3+k=9$ might have $=$ at the root, with right child $9$ and left child a subtree with $+$ over $3$ and $k$. Although that is one way to organize expressions into trees, we actually choose a slightly different means of applying functions/operators to arguments, which is covered in the documentation for the Application class.

Expressions are analogous to what mathematicians typically write inside $...$ or $$...$$ math mode in LaTeX. This distinguishes them from larger structures that appear in mathematical writing, such as a proof, or a section, or an axiom, or an exercise.

There are three types of Expressions:

1. Atomic expressions, also called Symbols, which can represent any mathematical symbol, such as $x$, $5$, $e$, $\pi$, $B_4$, $\in$, $\int$, etc. (Note that notation here is in math form just for the documentation; actual symbols may use a different style, such as B_4.)
2. Applications, which represent the application of a function or operator to zero or more arguments, as in the example of $3 + k$, above, which applies $+$ to the arguments $3$ and $k$.
3. Binding Expressions, which represent the use of a dummy variable in an expression. Specifically, if you have an expression such as $\exists x,(x^2=2)$ or $\int_a^b f(x);dx$, the $x$ is used as a "dummy" or "bound" variable in each case, and thus has a limited scope one cannot express with a mere function Application. See the documentation for the Binding Expression class for details on how to represent expressions like those examples.

We do not define these cases further here; see the documentation of each of the classes linked to above for details. The Expression class is an abstract base class, and every instance should be an instance of one of those three subclasses.