# 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. – Bruno Stonek 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.

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.

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. isn't a mathematician 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. isn't a mathematician Jul 27 '11 at 4:45

Formal proof systems

One context in which the word "formal" comes in, is that of formal proof systems.

A formal proof system is a way to write theorems and their proof in the computer, such that after it have been done the proof can be automatically verified by a computer.

In such systems, theorems are just sequences of characters (strings), and starting from your axiom strings, you use a few well defined rules to transform those strings mechanically, and obtain new true strings (thus making a proof).

The huge advantage of such systems is that since each proof step is so simple and mechanical, computers can verify proofs, which can be an extremely difficult and error prone task for humans to do!

There are also cases where the proof itself requires tedious verification of thousands of cases, and would be too time consuming for any human. One notable example of this is the four color theorem.

The downside of such systems is that they are much harder to write your proofs in, because in order to communicate with the computer you have to write everything in a very precise way.

I do believe however, that if such systems are done well enough with good tooling and standard libraries, writing a proof should be no harder than writing a computer program, and the benefits would largely outweight the greater difficulty of writing the proof.

For a concrete well presented example, a have a look at Metamath's awesome proof that 2 + 2 = 4 http://us.metamath.org/mpeuni/mmset.html#trivia

Metamath is an older proof system, and there are likely better choices today as I have mentioned at: What is the current state of formalized mathematics? but their web presentation is very nice!

Such proofs require of course defining everything in terms of things that the proof system understands. In the case of Metamath, Zermelo–Fraenkel-like set theory is used to my understanding.

A TL;DR version of the classic set theory approach would be:

The fact that mathematics can be fully formalized is surprising, and was arguably only fully realized at the end of the 19th century, in particular through the seminal Principia Mathematica, and materialized with the invention of computers.

This is in my opinion the property of mathematics that best defines it, and that which clearly separates its preciseness from other arts such as poetry.

Once we have maths formally modelled, one of the coolest results is Gödel's incompleteness theorems, which states that for any reasonable proof system, there are necessarily theorems that cannot be proven neither true nor false starting from any given set of axioms: those theorems are independent from those axioms. Therefore, there are three possible outcomes for any hypothesis: true, false or independent!

Some famous theorems have even been proven to be independent of some famous axioms. One of the most notable is that the Continuum Hypothesis is independent from ZFC! Such independence proofs rely on modelling the proof system inside another proof system, and forcing is one of the main techniques used for this.