What does "formal" mean?

Solution 1:

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.

Solution 2:

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.

Solution 3:

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

Solution 4:

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

Solution 5:

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).