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.
Formal calculations can lead to results that are wrong in one context, but correct in another context. The equation
holds if q has absolute value less than 1. Ignoring this restriction, and substituting q = 2 to leads to
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
Suppose we want to solve the differential equation
Treating these symbols as ordinary algebraic ones, and without giving any justification regarding the validity of this step, we take reciprocals of both sides:
Now we take a simple antiderivative:
If we have any doubts about our argument, we can always check the final solutions to confirm that they solve the equation.