Why do people use "formal calculation" to describe informal calculations?

Question

Many times, I see the word formal being used to describe a calculation that is not rigorous. I would think that such calculations should rather be termed informal than formal. What is the explanation of such wide-spread usage of the term formal?

Answer 1

Formal, adj. Relating to or involving outward form or structure, often in contrast to content or meaning.

In mathematics, a formal argument is one that manipulates the form of an expression without analysing the interpretation of that expression. For instance, one may formally interchange a limit and an integral (or a summation and an integral, etc.) without appealing to a theorem (e.g. Fubini's theorem, dominated convergence theorem, etc.) that could rigorously justify that interchange, or even without checking that all integrals, series, or limits actually converge. As such, formal arguments may not initially be rigorous, but if one knows what one is doing, one can often make them rigorous, perhaps after interpreting all objects involved in a suitable rigorous framework (e.g. using the theory of distributions, or of formal power series, etc.).

Informal, adj. Suitable to or characteristic of casual and familiar, but educated, speech or writing.

Informal mathematical reasoning is a different type of non-rigorous argument than formal non-rigorous mathematical reasoning, in which one does not look at the precise form of the mathematical expressions under discussion, but instead uses more casual, fuzzier terms, e.g. referring to various mathematical quantities as being "big" or "small" rather than specifying precise bounds. Imprecise adjectives such as "approximately", "roughly", "morally", "essentially", or "almost" are commonly used in informal reasoning, and there is also a heavy reliance on reasoning by analogy. Again, if one knows what one is doing, one can often convert an informal mathematical argument into a rigorous one, though often the precise definitions required to pin down a rigorous version of an informal concept can be quite technical, and an informal statement which is intuitively obvious may require quite a lengthy rigorous proof once it is made precise in this fashion.

As regards the relationship between informal reasoning, formal reasoning, and rigorous reasoning, I view the Venn diagram Euler diagram as follows:

There is some overlap between formal reasoning and rigorous reasoning, such as when one uses a formal deductive system (or software for making computer assisted proofs) to establish some mathematical statement. However, in most rigorous mathematical writing one usually does not resort to such formal systems, and uses arguments which are precise (as opposed to informal), but do not argue solely based on the form of one's expressions in order to justify the steps of the argument.

EDIT: On further thought, I would say that there is also (somewhat paradoxically) some overlap between the formal and informal modes of reasoning, in which one argues by manipulating imprecise terms in a purely formal fashion, without deeper understanding of what these terms mean even approximately. (In my experience, a homework assignment of a hopelessly confused maths undergraduate student can often produce reasoning in this category.) Needless to say, reasoning in this intersection tends to be quite far from being rigorous, to the point of being unfixably wrong. [One of my favourite examples of reasoning in this category: "Nothing is better than eternal happiness. A ham sandwich is better than nothing. Hence, a ham sandwich is better than eternal happiness."]

SECOND EDIT: The above distinctions are also related to the "pre-rigorous", "rigorous". and "post-rigorous" stages of mathematical development, as discussed on my blog here. At the pre-rigorous stage, one initially can only proceed using informal reasoning, formal reasoning, or some confused mixture of both (as discussed above). At the rigorous stage, the emphasis is naturally on rigorous modes of reasoning, with prior pre-rigorous modes of reasoning being deprecated (and in the case of unfixably "bad" modes of reasoning, discarded completely). In the post-rigorous stage, one freely utilises (the "good" types of) formal and informal reasoning in addition to rigorous reasoning, and moreover is capable of converting from one type of reasoning to another as discussed above.