Formal calculation

In mathematical logic, a formal calculation, or formal operation, is a calculation that is systematic but without a rigorous justification. It involves manipulating symbols in an expression using a generic substitution without proving that the necessary conditions hold. Essentially, it involves the form of an expression without considering its underlying meaning. This reasoning can either serve as positive evidence that some statement is true when it is difficult or unnecessary to provide proof or as an inspiration for the creation of new (completely rigorous) definitions.

However, this interpretation of the term formal is not universally accepted, and some consider it to mean quite the opposite: a completely rigorous argument, as in formal mathematical logic.

Examples[]

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

\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

\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[]

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 $\displaystyle x^{5}}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.

Symbol manipulation[]

To solve the differential equation

{\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: