When/how did “formal” come to mean “informal” in mathematical contexts?

Question

A question for the mathematical etymologists in the room:

Often when I see formally used in mathematical writing, it seems to be an indicator to put the whole sentence in quotation marks - the writer is saying, "if you get my drift." Much of the time the word is used to avoid tedious rigor in a situation where it would detract from the concept. As an example of this usage, in quantum mechanics, wavefunctions of a free particle are "formally normalized to the Dirac delta function."

Call me crazy, but this seems awfully close to the meaning of informally. (Though my later question is independent of whether one agrees that this represents a synonym for the above usage.)

A related but slightly more rigorous usage of formal, as Qiaochu mentions in this answer, refers to manipulating expressions according to a set of rules without worrying too much about things like convergence. Formal power series would be an example of this.

When did "formal" take on its contemporary meaning in mathematics literature, and how did this usage develop?

Answer 1

I had a math professor define "formal" as: "In mathematics, when we say something is formal we mean that we are going to pretend we forgot what we were talking about."

I see how you could equate "formal" with "informal," but it means more like we are stripping away extraneous things like "when you write a power series obviously we are summing something" and leave behind only the symbols and basic axioms. Get rid of all the informalities, all the intuition, and consider only the simplest properties. And in math, you've probably noticed that the simpler something is, the more formal it can reasonably be.

Answer 2

In formal power series, formal means in appearance. This is different from the other meaning of serious language.

Answer 3

A penetrating question, in my opinion! The use of "formal" in contemporary (1980-2012) mathematics is very volatile and brittle, in fact, in all my experience. It is very reasonable for a cautious person to feel uneasy. :)

One unfortunate use equates "formal" with "the symbols seem to give this, but I can't justify doing it, ... but no one who cares about the outcome cares about the justification, so we'll just not worry, and no one else will, either." I know, it is possible to rationalize this, but it's not a good thing, in the same sense that I tell beginners to think carefully when they say "clearly/obviously", because either they should be able to give the one-or-two-line proof, or it's not truly sooo easy. That is, what with human foibles, we have the "it's so obvious I can't explain it" problem.

At the other end, "formal" can mean that everything is set up so well that we need merely execute some (already fully legitimized) symbol manipulation to obtain a result. Unnervingly, this usage is often mixed with the "we can't justify this, but the symbols seem to work" (=heuristic) usage.

The unfortunate example of "formal power series" adds another usage: as is well known, here "formal" means merely "not convergent", and/but this resonates with a slightly misguided sense of the "we can't justify it, but the symbols look ok". In fact, "formal power series" have a sense and meaning that does not depend on "convergence", so is not attenuated by their non-convergence. By this year, it's not "just a heuristic", but is fully legitimate, ... although 250 years ago many people (e.g., Euler) saw that the arguments gave interesting outcomes, without worrying about (being able to give?) justifications.

The further muddle seems to be that, of course, an excellent heuristic is more interesting, more productive, than many fussy proofs, so we don't object to heuristics by any means. Thus, we do not object _in_principle_ to non-rigorous interesting discussions. But our mythological commitment to "rigor" puts heuristics in an odd limbo state: with luck, a non-rigourous heuristic can conjecturally explain otherwise-unintelligible phenomena, but, also, (let's say) "unfeeling" extrapolations of otherwise-sensible ideas seem pointless.

One problem is that it is very difficult to "formally" (!?!) distinguish the two, that is, productive heuristics from superficial-and-silly heuristics.

Much more can be said... but, at least, yes, a perception of inclarity is more-than-reasonable. There is not a consistent use of "formal". Examination of contemporary use of this term is professionaly-sociologically quite interesting, but does not explain any particular case. Rather, in summary, the best contemporary use seems to be "here is a slightly vague idea, which seems to be useful, but there are missing pieces... nevertheless, I will put it into symbols for you..."

(All the more hilarious given the popular conceit that mathematics is oh-so-rigorous...)

Edit/addition: given the inhomogeneity of the audience, perhaps it is necessary to note that a "formal power series ring" $k[[x]]$ is a projective limit of quotients $k[x]/x^N$, so that it is a legitimate object... but/and while the notation for a given "formal power series" is indistinguishable from the notation for convergent power series, there is no implication that formal power series do or do not converge. Yes, there is a natural injection of convergent power series if $k$ is a valued field, etc.

Also, I would reiterate the comment that, while "rigor" is often desirable, if not too expensive given the goal, for example, it is not the only goal, surely. Further, "rigor" is surely relative. And, if we distinguish the process of learning/doing mathematics from the edifice itself, surely there is as much reason to find motivation and heuristics to discover/explain important phenomena, as there is to be as-scrupulous-as-possible about small or irrelevant or uninteresting things?

Answer 4

I think the distinction is between form and content and the language is borrowed from the humanities. For instance, when I multiply in $\mathbb{C}[[x]]$, I am performing operations on the "form" of the power series and ignoring its "content" (e.g. I am thinking of the power series as an expression, not a function on $\mathbb{C}$).

In general, when we have a sequence of events like this,

Definition: The A of a B is C.

Theorem: To compute the A of a B, represent B as a string of symbols D and manipulate it using rule R, then let C be the object corresponding to this new string of symbols.

then we can say

Definition: The formal A of a string of symbols D is what you get by manipulating D by rule R.

and this definition often pays off.