The type system of mathematics

Occasionally I see mathematical questions that seem “grammatically incorrect” in some sense.

Example. “Is open or closed?”
Example. “Is a group?”
Example. “What’s the Fourier series of ?”

Here are some sillier examples.

Example. “Is a rectangle prime?”
Example. “Is ?”
Example. “What’s the Fourier series of the empty set?”

What all of these examples have in common is that they are type errors: they are attempts to apply some mathematical process to a kind of mathematical object it was never intended to take as input. If you tried to write a program in some highly mathematical programming language to answer these questions, it (hopefully!) wouldn’t compile.

Mathematical objects are usually not explicitly thought of as having types in the same way that objects in a programming language with a type system has types. Ordinary mathematics is supposed to be formalizable within Zermelo-Fraenkel (ZF) set theory, possibly with the axiom of choice, and in ZF every mathematical object is constructed as a set. In that sense they all have the same type. (In particular, the question “is ?” is perfectly meaningful in ZF! This is one reason not to like ZF as a foundation of mathematics.) However, I think that in practice mathematical objects are implicitly thought of as having types, and that this is a mental habit mathematicians pick up but don’t often talk about.

Instead of thinking in terms of set theory, thinking of mathematical objects as having types allows us to import various useful concepts into mathematics, such as the notions of type safety, typecasting, subtyping, and overloading, that help us make more precise what we mean by a mathematical sentence being “grammatically incorrect.” The rest of this post will be a leisurely discussion of these and other type-based concepts as applied to mathematics in general. There are various categorical ideas here, but for the sake of accessibility we will restrict them to parenthetical remarks.

Read Full Post »

Constructions vs. specifications

What does it mean to define a mathematical object?

Roughly speaking, there are two strategies you could use. One is to construct that object from other objects. For example, can be constructed from using Cauchy sequences or Dedekind cuts.

Another is to give a list of properties that uniquely specify the object. For example, can be defined as the unique Dedekind-complete totally ordered field.

Let’s call these strategies construction and specification. Construction has the advantage of concreteness, and it also proves that the object exists. However, it has the disadvantage that constructions are not unique in general and you might not be working with the most useful construction at a given time; to prove things about an interesting mathematical object you might have to switch between various constructions (while also proving that they all construct the same object).

Relying excessively on construction also has a curious disadvantage when talking to students about the object in question: namely, they might ask you how to show that object satisfies property , and you might respond “well, it’s obvious if you use construction ,” and they might respond “but I was taught that is [construction ]!” The possibility of multiple different constructions of the same mathematical object makes construction somewhat unsatisfying in terms of describing what you even mean when you say “object .”

This is the appeal of specification. Although specification is more abstract and harder to grasp at first, it has the advantage you don’t have to use any particular construction of an object to prove things about it: instead, you should in principle be able to prove everything from the properties alone, since those uniquely specify the object. This often leads to cleaner proofs. Specifications also usually give a better motivation for looking at an object: it’s easier to make sense of the claim that we want a mathematical object with various properties than to make sense of the claim that we want a mathematical object which is constructed in some arbitrary-looking (to the uninitiated) fashion.

Below we’ll go through a few examples of mathematical objects and some constructions and specifications of them.

Read Full Post »

I don’t trust uncountable sets

I have a mathematical confession: I don’t trust uncountable sets.

Some time ago on MathOverflow somebody asked what a reasonable definition of “infinite permutation” would be. The first answer that comes to mind is a bijection . The set of all such bijections does form a group, but not only is it uncountably generated, it contains, as Darsh observes, a copy of every countably generated group (acting on itself by left multiplication). In particular it contains a copy of the free group on countably many generators. It also doesn’t seem to carry any natural kind of topology.

On the other hand, a much nicer candidate is the set of “compactly supported” permutations, i.e. those which fix all but finitely many elements. This countable group is generated by transpositions and therefore has a neat presentation given by the usual relations. I believe it’s also the largest locally finite subgroup of the full group of bijections.

I find this group much more philosophically appealing than the full group of bijections, and the reason is simple: each element of the group is computable. On the other hand, only countably many elements of the full group of bijections are computable: the rest can’t be written down by a Turing machine. And I don’t trust anything that can’t be written down by a Turing machine.

Corollary: I don’t trust the real numbers.

Instead of explaining what I mean by this, which I don’t think I have time for today, I’ll just throw a question out to the audience: how do you feel about all this?

Read Full Post »

Halmos on writing and education

John Ewing wrote up a nice collection of quotes from Paul Halmos for the Notices of the AMS; let’s meditate on his words.

For example:

The best notation is no notation; whenever possible to avoid the use of a complicated alphabetic apparatus, avoid it. A good attitude to the preparation of written mathematical exposition is to pretend that it is spoken. Pretend that you are explaining the subject to a friend on a long walk in the woods, with no paper available; fall back on symbolism only when it is really necessary.

I’d have to agree. I see this as one of the strongest aspects of, for example, Terence Tao’s expository style. His latest post on relativization is a perfect example; Tao is a master at recognizing when technical details would obscure his exposition and when they are necessary. A related point:

Read Full Post »

IMO 2009 and proof systems

The problems from IMO 2009 are now available. I haven’t had much time to work on them, though.

There are two classical geometry problems, which I already know I won’t attempt. While I am well aware that classical geometry often requires a great deal of ingenuity, I am also aware of the existence of the field of automatic geometric theorem proving. On this subject I largely agree with Doron Zeilberger: it is more interesting to find an algorithm to prove classes of theorems than to prove individual theorems. The sooner we see areas like classical geometry as “low-level,” the sooner we can work on the really interesting “high-level” stuff. (Plus, I’m not very good at classical geometry.)

Zeilberger’s typical example of a type of theorem with a proof system is the addition or multiplication of very large numbers: it is more interesting to prove symbolically than it is to prove individual “theorems” such as . Zeilberger himself played a significant role in the creation of another proof system, but for the far less trivial case of hypergeometric identities (which includes binomial identities as a special case).

But so I can make my point concretely, I’d like to discuss some examples based on the types of problems most of us had to deal with in middle or high school.

Read Full Post »

Exceptional structures

Recently Isabel Lugo asked about problems that are hard for intermediate values of some parameter, and in discussing the question I got to thinking about exceptional structures in mathematics such as the sporadic groups. In 2006 David Corfield asked about how “natural” the sporadic simple groups are at the n-Category cafe. In that discussion and more generally there seem to be approximately two extremes in perspective:

• Exceptional structures represent a lack of room for asymptotic behavior to occur; thus they are distractions from the “generic” case. This seems to be the case for certain exceptional isomorphisms; there are only so many groups of a particular small order. It also seems to be a good way to think about objects that behave fine in characteristic zero or high characteristic but behave badly in low characteristic, characteristic usually being the worst offender.
• Exceptional structures represent the deepest part of a theory, and the exceptional structures in different fields are often related; thus understanding exceptional structures is crucial. This seems to be the case for the octonions, which can be thought of as an underlying cause of Bott periodicity. It also seems to be a good way to think about objects related to the number ; John Baez tells a great story about connections between the Leech lattice, the Dedekind eta function, string theory, and elliptic curves all centered around this mysterious number.

So what do you think? Are exceptional structures accidents or miracles? (Or, as a third option: am I failing to distinguish carefully enough between interesting and uninteresting exceptional structures?)

Read Full Post »

Mathematical historical fiction

Bill Gasarch is right – writing technical posts is tiring! (I’ve been trying to finish the next GILA post for days.) So I’ll share some more thoughts instead. Today’s thought was triggered by David Corfield:

In the first of the above posts I mention Leo Corry’s idea that professional historians of mathematics now write a style of history very different from older styles, and those employed by mathematicians themselves. …

To my mind a key difference is the historians’ emphasis in their histories that things could have turned out very differently [emphasis mine], while the mathematicians tend to tell a story where we learn how the present has emerged out of the past, giving the impression that things were always going to turn out not very dissimilarly to the way they have, even if in retrospect the course was quite tortuous.

This in turn reminded me of something else Rota wrote about his Walter Mitty fantasies:

Read Full Post »

I hate axioms

(A more appropriate title for this post would probably be “I hate Bourbaki,” but I like it as is.)

I spend a lot of my free time reading research papers, usually in combinatorics; those tend to require the least background. Today I decided to read everything I could find written by one of the great champions of combinatorics, Gian-Carlo Rota, and in his philosophical writings I found the explicit declaration of an opinion I’ve held for some time now.

Consider the following passage from Syntax, Semantics, and the Problem of the Identity of Mathematical Objects:

The real line has been axiomatized in at least six different ways. Mathematicians are still looking for further axiomatizations of the real line, too many to support the justification of axiomatization by the claim that we axiomatize only in order to secure the validity of the theory.

Whatever the reasons, the variety of axiomatizations confirms beyond a doubt that the mathematician thinks of one real line, that is, the identity of the object is presupposed and in fact undoubted.

The mathematician’s search for further axiomatizations presupposes the certainty of the identity of the object, but recognizes that the properties of the object can never be completely revealed. The mathematician wants to find out what else the real line can be. He wants ever more perspectives on one and the same object, and the perspectives of mathematics are precisely the various axiomatizations, which lead to a variety of syntactic systems always interpreted as presenting the same object, that is, as having the same models.

Or the following passage, from Combinatorics, representation theory, and invariant theory: The story of a ménage à trois:

Read Full Post »