Inmathematical logic, aformal calculation, orformal operation, is a type of mathematical calculation, often involvingpower series, that is carried out purely algebraically while disregarding questions ofconvergence.^[1] The expressions are manipulated according to algebraic rules, without requiring that the underlying series or operations necessarily converge in the analytical sense. This approach is useful when the structure of the calculation is more important than its analytical properties.

Formal calculations can lead to results that are wrong in one context, but correct in another context. The equation

${\displaystyle \sum _{n=0}^{\mathrm{\infty }}{q}^n=\frac{1}{1-q}}$

holds ifq has an absolute value less than 1. Ignoring this restriction, and substitutingq = 2 to leads to

${\displaystyle \sum _{n=0}^{\mathrm{\infty }}{2}^n=-1.}$

Substitutingq=2 into the proof of the first equation, yields a formal calculation that produces the last equation. But it is wrong over the real numbers, since the series does not converge. However, in other contexts (e.g. working with2-adic numbers, or withintegers modulo a power of 2), the series does converge. The formal calculation implies that the last equation must be valid in those contexts.

Another example is obtained by substitutingq=-1. The resulting series1-1+1-1+... is divergent (over the real and thep-adic numbers) but a value can be assigned to it with an alternative method of summation, such asCesàro summation. The resulting value, 1/2, is the same as that obtained by the formal computation.

Formal power series is a concept that adopts the form ofpower series fromreal analysis. The word "formal" indicates that the series need not converge. In mathematics, and especially in algebra, a formal series is an infinite sum that is considered independently from any notion of convergence and can be manipulated with algebraic operations on series (addition, subtraction, multiplication, division, partial sums, etc.).

A formal power series is a special kind of formal series, which may be viewed as a generalization of a polynomial, where the number of terms is allowed to be infinite, with no requirements of convergence. Thus, the series may no longer represent a function of its variable, merely a formal sequence of coefficients, in contrast to a power series, which defines a function by taking numerical values for the variable within a radius of convergence. In a formal power series, the powers of the variable are used only as position-holders for the coefficients, so that the coefficient of${\displaystyle {\displaystyle x^5}}$ is the fifth term in the sequence. In combinatorics, the method of generating functions uses formal power series to represent numerical sequences and multisets, for instance allowing concise expressions for recursively defined sequences regardless of whether the recursion can be explicitly solved. More generally, formal power series can include series with any finite (or countable) number of variables, and with coefficients in an arbitrary ring.

Rings of formal power series are complete local rings, which supports calculus-like methods in the purely algebraic framework ofalgebraic geometry andcommutative algebra. They are analogous to p-adic integers, which can be defined as formal series of the powers of p.

To solve thedifferential equation

${\displaystyle \frac{dy}{dx}=y^2}$

these symbols can be treated as ordinary algebraic symbols, and without giving any justification regarding the validity of this step, we take reciprocals of both sides:

${\displaystyle \frac{dx}{dy}=\frac{1}{y^2}}$

A simpleantiderivative:

${\displaystyle x=\frac{-1}{y}+C}$

${\displaystyle y=\frac{1}{C-x}}$

Because this is aformal calculation, it is acceptable to let${\displaystyle C=\mathrm{\infty }}$ and obtain another solution:

${\displaystyle y=\frac{1}{\mathrm{\infty }-x}=\frac{1}{\mathrm{\infty }}=0}$

The final solutions can be checked to confirm that they solve the equation.

The cross product can be expressed as the followingdeterminant:

where${\displaystyle (\mathbf{i},\mathbf{j},\mathbf{k})}$ is a positivelyoriented orthonormal basis of a three-dimensional orientedEuclidean vector space, while${\displaystyle a_1,a_2,a_3,b_1,b_2,b_3}$ are scalars such that${\displaystyle \mathbf{a}=a_1\mathbf{i}+a_2\mathbf{j}+a_3\mathbf{k}}$, and similar for${\displaystyle \mathbf{b}}$.

• Formal power series
• Mathematical logic

• Mathematical logic