Formal calculation

This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed. Find sources: "Formal calculation" – news · newspapers · books · scholar · JSTOR (April 2026) (Learn how and when to remove this message)

In mathematical logic, a formal calculation, or formal operation, is a type of mathematical calculation, often involving power series, that is carried out purely algebraically while disregarding questions of convergence.^[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

∑ n = 0 ∞ q n = 1 1 − q {\displaystyle \sum _{n=0}^{\infty }q^{n}={\frac {1}{1-q}}}

holds if q has an absolute value less than 1. Ignoring this restriction, and substituting q = 2 to leads to

∑ n = 0 ∞ 2 n = − 1. {\displaystyle \sum _{n=0}^{\infty }2^{n}=-1.}

Substituting q=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 with 2-adic numbers, or with integers 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 substituting q=-1. The resulting series 1-1+1-1+... is divergent (over the real and the p-adic numbers) but a value can be assigned to it with an alternative method of summation, such as Cesà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 of power series from real 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 x 5 {\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 of algebraic geometry and commutative algebra. They are analogous to p-adic integers, which can be defined as formal series of the powers of p.

To solve the differential equation

d y d x = y 2 {\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:

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

A simple antiderivative:

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

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

Because this is a formal calculation, it is acceptable to let C = ∞ {\displaystyle C=\infty } and obtain another solution:

y = 1 ∞ − x = 1 ∞ = 0 {\displaystyle y={\frac {1}{\infty -x}}={\frac {1}{\infty }}=0}

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

The cross product can be expressed as the following determinant:

a × b = | i j k a 1 a 2 a 3 b 1 b 2 b 3 | {\displaystyle \mathbf {a\times b} ={\begin{vmatrix}\mathbf {i} &\mathbf {j} &\mathbf {k} \\a_{1}&a_{2}&a_{3}\\b_{1}&b_{2}&b_{3}\\\end{vmatrix}}}

where ( i , j , k ) {\displaystyle (\mathbf {i} ,\mathbf {j} ,\mathbf {k} )} is a positively oriented orthonormal basis of a three-dimensional oriented Euclidean vector space, while a 1 , a 2 , a 3 , b 1 , b 2 , b 3 {\displaystyle a_{1},a_{2},a_{3},b_{1},b_{2},b_{3}} are scalars such that a = a 1 i + a 2 j + a 3 k {\displaystyle \mathbf {a} =a_{1}\mathbf {i} +a_{2}\mathbf {j} +a_{3}\mathbf {k} } , and similar for b {\displaystyle \mathbf {b} } .

• Formal power series
• Mathematical logic