# What does “formal” mean?

I know the definition of formal power series, power series and polynomials. But what does the adjective "formal" mean? In google English dictionary, does it mean "9. Of or relating to linguistic or logical form as opposed to function or meaning" or maybe another one in the link?

Or does "formal" have some mathematical meaning which is other than usual dictionary meaning?

-

I see formal used in at least two senses in mathematics.

• Rigorous, i.e. "here is a formal proof" as opposed to "here is an informal demonstration."
• "Formal manipulation," that is, manipulating expressions according to certain rules without caring about convergence, etc.

Confusingly they can mean opposite things in certain contexts, although "formal manipulations" can be made rigorous in many cases.

-
Isn't there a notion of "formal" in algebraic geometry? – Damien Jul 27 '11 at 1:44
You mean en.wikipedia.org/wiki/Formal_scheme ? Well, "formal" here seems to mean something like "including infinitesimal information." Morally the etymology comes from making formal manipulations with infinitesimals rigorous. – Qiaochu Yuan Jul 27 '11 at 1:54
I think the etymology of the word shows how the senses are related. ‘Formal’ comes from ‘form’; the association with rigour is via Hilbert's formalist school. By ‘rigour’ what is really meant is formal manipulations of logical propositions in accordance to the rules of inference, rather than following ‘intuition’. – Zhen Lin Jul 27 '11 at 2:00
It should be noted that the first sense includes a really vast spectrum of degrees of formality. The way I see it, it includes usual textbook proofs (e.g. Folland's proof of Radon-Nikodým theorem is 'formal'), and 'logically' formal proofs, as in en.wikipedia.org/wiki/Formal_proof , which also serves as input for automated proof checking. – lentic catachresis Jul 27 '11 at 3:17
I've always thought of the latter meaning as the meaning "of or related to form" — a formal power series is something that has the form of a power series, formal manipulations are those that work on the form directly (without caring about what the expression may "mean" in the analysis sense), etc. – ShreevatsaR Jul 27 '11 at 4:42

As an example, formal power series is analyzed without regard to convergence. Really, what is of interest is the sequence of coefficients.

-

And don't forget the notion of formal space arising in rational homotopy theory.

-

The word "formal" in "formal power series" is indicating that you are considering all objects that are algebraically "like a power series". This is opposed to its use in analysis where you spend a lot of time figuring out for which $x$ the series converges.

Basic analysis goes like this:

"$\displaystyle\sum_{n=1}^{\infty} x^n$ is a series which converges for $|x|<1$ and therefore the function $f(x) = \displaystyle\sum_{n=1}^{\infty} x^n$ has the domain $|x| < 1$".

You then proceed to use the function and talk about derivatives and integrals on the restricted domain. If the series has very few points of convergence such as $\displaystyle\sum_{n=1}^{\infty} n!x^n$ which converges only for $x=0$, then casting it as the function $g(x) = \displaystyle\sum_{n=1}^{\infty} n!x^n$ can only have domain $x=0$ and its value is $g(0)=0$. Pretty boring function when it comes to derivatives and integrals!

When you study formal power series, you ignore the consideration of convergence and use the series as it is presented as an algebraic entity, so even though $g$ only converges at $x=0$, you ignore that and focus on other properties of the series.

Another common use of the word "formal" is with a "formal system" which is basically a big rulebook for an artificial language comprised of an alphabet (a list of symbols), a grammar (a way of arranging those symbols), and axioms (initial lists of symbols to start from). The word "formal" here is needed because it is very prim and proper and only allows manipulations according to the grammar and axioms; you can't combine symbols in any way like you can in English (for example this ee cummings poem is an "acceptable" combination of the symbols of English, but is also seemingly "wrong" according to our standard grammar).

-
The first series certainly converges for $|x| < 1$; why wouldn't you consider it a power series with a finite radius of convergence? (I would have chosen an example with zero radius of convergence, such as $\sum n! x^n$.) – Qiaochu Yuan Jul 27 '11 at 1:39
Yes, @Qiaochu's series is an excellent example; even with the zero radius of convergence, it can be manipulated formally to produce... interesting and useful identities. – J. M. Jul 27 '11 at 2:23
Thank you for the suggestion! – tomcuchta Jul 27 '11 at 4:39
"not considered as a power series in analysis since it does not converge for any $x\in \mathbf R$" - actually, it does... if $x=0$ that is. – J. M. Jul 27 '11 at 4:45

When I was learning about logic as an undergraduate, I recall being told that the word "formal", with respect to "formal languages" meant that the "form" of expressions written in that language had primacy.

In other words, rules for manipulating expressions in a formal language could be given in terms of the form of the expression only, without needing to know to what values the variables in the expression were bound.

So a formal language permits us to use relatively simple pattern-matching algorithms to decide which transformations of an expression are valid at any given time.

In this context, formality is linked to the simplicity of the rules that define the set of valid transformations of an expression.

-