Formal calculation

In mathematical logic, a formal calculation is a calculation which is systematic, but without a rigorous justification. This means that we are manipulating the symbols in an expression using a generic substitution, without proving that the necessary conditions hold. Essentially, we are interested in the form of an expression, and not necessarily its underlying meaning. This reasoning can either serve as positive evidence that some statement is true, when it is difficult or unnecessary to provide a 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

Simple examples

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

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

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

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

By substituting q=2 into the proof of the first equation, one obtains a formal calculation that produces the last equation. But it is wrong over the real numbers, since the series does not converge. However, there are other contexts (e.g. working with 2-adic numbers, or with integers modulo a power of 2), where 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 one can still assign a value to it with an alternative methods 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 one does not require the series to converge.

Symbol manipulation

Suppose we want to solve the differential equation

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

Treating these symbols as ordinary algebraic ones, 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}}}}$

Now we take a simple antiderivative:

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

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

Because this is a formal calculation, we can also allow ourselves to let ${\displaystyle C=\infty }$ and obtain another solution:

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

If we have any doubts about our argument, we can always check the final solutions to confirm that they solve the equation.

See also

• Formal power series
• Mathematical logic

References

• Stuart S. Antman (1995). Nonlinear Problems of Elasticity, Applied Mathematical Sciences vol. 107. Springer-Verlag. ISBN 0-387-20880-1.