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 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 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, 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 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.
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: Because this is a formal calculation, we can also allow ourselves to let and obtain another solution: If we have any doubts about our argument, we can always check the final solutions to confirm that they solve the equation.
