What is Math Really About? part 3- computation

Whether we are looking at the theory describing a simple phenomenon, or trying to found all of mathematics, we will want to know some things about our ability to investigate the formal theory we have chosen to study. It is natural to ask what things can be proven and dis-proven (questions of computability), and if something can be proven, how long a proof will its proof take (a question of computational complexity). This is the sort of question that began computer science as a distinguishable subject in mathematics, and all systems of computation (Turing machines, grammars, the lambda calculus and its type theories, mu-recursion, etc) can be described as rewriting systems exactly because what they are intended to describe is rewriting in math. It is not possible to prove that these systems describe all things that can be computed because they are the definition of computation (in other words, that is not something to which the notion of proof applies), but in practice the systems mentioned above are accepted for two reasons: a huge number of other systems have been shown to be weaker, or at most as strong, as these systems, and stronger ones (systems of super-Turing computability) don't seem to capture the notion of computation at all.

In some sense computer science is the constructive part of math- that part concerned only with objects that can actually be constructed where truth comes from an explicit proof. This is in contrast with classical math where something can can be "true" in some ultimate sense without being able to give a proof (for example, its possible to prove the existence of an object with some property without being able to describe any particular object with that property). This bring math down to earth- we can't talk about things too large to do computations on, we can't talk about objects that we can't construct.

What is Math Really About? part 2- models

When we try to describe a situation in math, we come up with some collection of objects that give all relevant information to understand it. To describe a family tree, we might want a set of people (the family) and a set of triples (an ordered group of three things) where the first in the triple is the mother, the second the father, and the third the child. The individuals in the set of triples are from the set of people, of course. There are some other constraints, such as that a person can't be their own parent, but lets not go into too much detail. In the definition (the theory) we don't want a particular set of people, or particular set of triples, but rather the notion that a family tree consists of people and parents. There are other ways to do this, but if we chose this way then a description might be "A family tree consists of a set F (called the family), and a multi-relation FxFxF. A family is given by (F, FxFxF) such that for all (a, b, c) in the set of triple, a, b, and c are distinct.".

While studying these objects, we will look at their properties. This may include ways of ordering them, combining them, and describing parts of their structure. That one of the most important things to study is how to translate the objects into each other, especially when the transformations preserve some aspect of the structures. One of the reasons such transformations are important is because they can be used to describe properties (often by some single objects that embodies the property in some way, and then the transformation to and from that object and others). Because of this, a theory will generally have some objects it is concerned with, and some notion of transformation that is appropriate and interesting for that object. Remember that in math we take situations we find interesting and encode them as theories, so there should be theory that describe this situation of having objects and transformations and combinations of these objects. This theory would be pretty fundamental and would have far reaching consequences- recall that the theory of symbols is logic, and we are talking about the models of these theories (the objects they describe). This theory is called Category Theory. A category is exactly what we just saw- some type of object, and some appropriate way to translate or transform between objects. In Category theory we tend look not at the internal structure of the object (which is based on definition or interpretation) but at an objects relation to other objects, so we often give properties as objects and some class of transformation between them. Category theory has pretty clear place in math from this perspective- it generalizes the notion of model. This makes it less surprising (although I personally found this immensely surprising) that categories have something call an "internal language" that is the logic they describe, and logics have an associated category.

I am not a mathematician, so take my generalizations about the importance of Category Theory with a grain of salt- I'm not sure its the amazing paradise I've made it out to be. However, it does describe an important situation, it is extremely abstract, and it is a great deal of fun.

So thats all for part 2. The last thing I'm going to go over is the manipulation of symbols in math, which, as a computer scientist, is really my place in all this.

What is Math Really About?

I often find that people are confused about what math is or what its about. This is understandable- I only came to understand this late in my college education, and I was very surprised by what I learned. Notice that I am not a mathematician- I'm a computer scientist. What I want to share is my experience and knowledge having learned this myself over the last several years. I'm going to talk about what math is, what it does, and how its used. I want to express that math is not one big unified system that explains the universe, its not all about numbers, that subjects like calculus are not "higher math", and math is not even one thing.

So, what do we do in math? The basic situation is that we observe something like a relation between people (a family tree for example), a physical phenomenon (gravity, electricity, and lots of other things), or something as simple as a quantity of some object. Having found something we want to understand, we construct some mathematical object that describes the situation. Instead of describing a single family tree, we would describe a general structure of all family trees. To do this, we have a large number of objects to combine from the usual practice of mathematics. Often we need many objects collected together to describe our situation that together give the information we need to describe the object we are interested in. The information we need give the "theory" of the thing ("the theory of family trees"), and the particular objects the models (your particular family tree).

This begs the question- where do all those objects we use come from? They in turn encode some intuition about the world- relations encode relations between things, numbers encode quantity and order, lattices encode complex orderings, etc. In other words, we can combine these objects to describe a new situation, but how do we arrive at the "first" objects- how do we found our system? The answer is that there are many ways to do this, and they are *not* all the same. Found math in different ways, and you get different results. The reason that this is not as much a problem as it might seem is that for the most part we work in some "ambient" system of logic with some notion of sets. While some of the more abstract and obscure (but still important) parts of math may change depending on the system, there is a large part of it that is generally (but not universally) agreed on. The usual system to found math on is called ZFC, and the usual logic to use is classical logic, but just as a writer doesn't wonder about how transistors work when they use a computer, a mathematician doesn't necessarily worry about how math is founded when doing their work.

While though there are many different foundations for math (category theory, set theory, logic, and more). there is some similarity to them. This brings us to the heart of math- writing down symbols that follow rules. Thats really it. We write down symbols, rewrite them according to rules, and interpret them as having a meaning. I said that when we see something interesting, we try to encode it as a mathematical object. Therefore, we should be able to encode the notion of encoding notions as an object, which we call a theory. Logic is the study of these systems of symbols and their rules, so logic is math. Notice that there are many systems of logic, which vary hugely in what they can describe. They can be very strong, and define all of what we think of as math, or very weak and be able to describe nothing, or anything in between. These systems usually will have some meaning to us as humans- they give a systematic way to write down and manipulate symbols, and therefore to write down and manipulate the concepts that the symbols are intended to stand for. Ideally, if two people agreed on some logic- the meanings of the symbols and what it means to combine the symbols in different ways- they would agree on anything that could be defined using that logic.

This brings me to the end of the first part in this series of posts. I still want to talk about models in general, and the mechanical process of writing and rewriting symbols, but the main point is here: math is logic, logic is writing symbols (often on chalkboards). The meaning comes from the person doing the writing, and what they believe in. You can refound math any way you want, you can construct all sorts of exotic objects, you can go into the highest abstractions, but if there is no reason or justification for your work then it is not interesting. This is why there is no "problem" with the fact that there is no number 1/0, or that are many sizes of infinity, or with the various things commonly called paradoxes. Even if you could come up with a construction that does not have these "problems" (it would be more accurate to call them properties), it is not necessary very interesting or useful. If there is some application, or even if it just help people understand something that is already well known, then it can become a part of the huge, distributed effort that we call math, even if it is a new mathematics based on different axioms (constructive math for example). The activity of math is more a way of thinking then a single unified system, and if it describes the universe as we experience it, then its because it was designed to.

Binary Operators

There is something that has bothered me for a long time in mathematics: what is up with the number 2? Why do we have "and" and "or" (conjunction and disjunction) in logic and type theory, meet and join in lattice theory, unions and intersections in topology (and set theory), Cartisian products and disjoint unions as polynomial data types (and set theory), products and sums in abstract algebra (sometimes we even have two "layers" of two operators which take two arguments, like in an algebra), and categorical products and coproducts in category theory. There are two things going on here- why are these binary operators (in the sense that they act on two objects) and why are there always two of them (why are they paired up)?

The reason this interests me is that we can easily define unary operators, or ternary, or what-ever-ary we want, so why is binary so common? Also, certainly not all structures have binary operators, and just having one doesn't always imply having the other, in general. For some, its because of their relationship with another pair of operators, like how lattice theory is historically a model theoretic view of truth-valued logic. However, the point is that there are often the two binary operators, not four ternary operators or one 5-ary operator or anything else. I don't know why this is the case, but I will take a stab at it.

One of the reasons is that its often really just one operator and its dual. This is particularly clear in category theory, where they are dual constructs, but similar duality conditions seem to hold for the others (perhaps not exactly? I don't know). This covers why two operators, but why are they binary?

The answer seems to be that they aren't, really. They can be given as binary operators, but as long as they are associative there is no ambiguity when defining them over finite lists of objects. Some can even be defined over infinite lists/sets. Giving them as binary operators is easy to define, but we can just as well define X V Y (with V the join) as the join of X and Y as we can define V{X, Y} as the join of all elements of a set (in this case X and Y).

So why two binary operators? It seems like we are really just looking at some operation, its dual, and the special case of defining it over two things instead of groups of things, which is just for convenience.

Closed Categories, Properties, Philosophy of Mathematics

Warning- this post is just my recent thoughts about math. I don't know how to make them rigorous, and they may be completely wrong.

I've been thinking about how the subfields of math each center around the theory of some object. The object is normally given as a set theoretic construction satisfying some axioms, and the field of study is concerned with the properties of these objects, what objects in other fields satisfy the axioms (and are therefore part of the field), and with transformations between the chosen objects. Category theory in some sense captures this idea by making the objects of study this situation- a category can be thought of as containing the objects of some field of study, the morphisms are the transformation between the objects. Categories can just be thought of as another object, defined like any other field's chosen object, but they can be considered the embodiment of a field of mathematics. This makes it a little less surprising (though not much, this is pretty surprising!) that categories are so intimately related to theories (the object "a theory" consisting of types, function symbols, axioms, and relation symbols). In fact, the "internal language" of a category is a theory, and the model of a theory is a category. This is an amazing thing that I'm just beginning to grasp, really.

In most theories of some object, there are important properties that we want to show that a particular object has. In group theory, for example, we want a set to have, among other things, an identity element for it to be a group. The group homomorphism from the one element group to a given group points out that identity element, and therefore the one element group embodies the property of identity. The proof that a group has an identity is then embodied in the existence of a homomorphism between the group that embodies the identity and the chosen group.

What I'm wondering is- how general is this idea? Are all properties of objects embodied in some object, and all proofs embodied in the existence of morphisms from that object? In closed categories, where the morphism are objects of the category, this means that the theory of the objects of the category contain their own proofs. This seems like Topos theory, which requires a couple more properties then just being closes, which studies categories that have enough structure to contain systems of mathematics (as I understand it). Not all categories contain their morphisms in this way, and so not all theories contain their proofs, but it looks like Topos and their associated theories do this.

Interestingly being closed appears to be fundamental to categorical notions of computation. The categories whose theories are type systems over the lambda calculus are Cartisian closed categories, although I think that can be weakened in some ways. This is a basic fact of computation it seems- Turing machines have their universal Turing machines which run encoding of other machines, lambda terms are defined over other lambda terms, and actual machines can't distinguish (in general) between data and code. The whole Howard-Curry isomorphism and proofs as propositions interpretation gives us the fact that programs encode proofs of a proposition in some system of logic (in the case of the lambda calculus, lambda terms can be read as programs to be reduced, or as proofs. It just depends on how you read them). It seems to me that in a constructive mathematics all proofs would indeed be some form of transformation which can be encoded in an object (functors, homomorphism groups, etc) meaning that objects and their proofs are the same thing. This puts a perspective on things like naive set theory- if you can describe objects that don't make sense (contradictory sets) then you have to expect contradictory proofs. It may be that the safest thing to found a system of mathematics on is something where we can construct all objects, where the transformations between objects are contained in the theory, and therefore we can construct the object embodying all proofs (if we couldn't construct it, it wouldn't be true).

I normally ignore the philosophy of constructive mathematics as my interest in it is really just as a computer scientist. I think of math as being a human activity, so classical logic isn't really "wrong" and people are welcome to do it if they want (it is certainly powerful, even if its a bit odd at times). On the other hand, it does seem that constructive math, as I understand it, is on a good foundation where it safely contains its own proofs and its lack of freedom in defining objects (as opposed to classical math where we can define some very strange things) prevents the weirdness of classical math. Type theory started as a way to prevent set theoretic paradoxes, and intuitionistic type theory may be the way to go for a system of math that constrains its objects and proofs enough to keep math down to earth.

Okay, enough ranting. Sorry for the half formed thoughts, but I wanted to record them somewhere.