Network Theory (Part 25)

In parts 2-24 of this network theory series, we’ve been talking about Petri nets and reaction networks. These parts are now getting turned into a book. You can see a draft here:

• John Baez and Jacob Biamonte, A course on quantum techniques for stochastic mechanics.

There’s a lot more to network theory than this. But before I dive into the next big topic, I want to mention a few more odds and ends about Petri nets and reaction networks. For example, their connection to logic and computation!

As we’ve seen, a stochastic Petri net can be used to describe a bunch of chemical reactions with certain reaction rates. We could try to use these reactions to build a ‘chemical computer’. But how powerful can such a computer be?

I don’t know the answer. But before people got interested in stochastic Petri nets, computer scientists spent quite some time studying plain old Petri nets, which don’t include the information about reaction rates. They used these as simple models of computation. And since computer scientists like to know which questions are decidable by means of an algorithm and which aren’t, they proved some interesting theorems about decidability for Petri nets.

Let me talk about: ‘reachability’: the question of which collections of molecules can turn into which other collections, given a fixed set of chemical reactions. For example, suppose you have these chemical reactions:

C + O₂ → CO₂

CO₂ + NaOH → NaHCO₃

NaHCO₃ + HCl → H₂O + NaCl + CO₂

Can you use these to turn

C + O₂ + NaOH + HCl

into

CO₂ + H₂O + NaCl ?

It’s not too hard to settle this particular question—we’ll do it soon. But settling all possible such questions turns out to be very hard

Reachability

Remember:

Definition. A Petri net consists of a set of species and a set of transitions, together with a function

saying how many copies of each state shows up as input for each transition, and a function

saying how many times it shows up as output.

Today we’ll assume both and are finite.

Jacob and I like to draw the species as yellow circles and the transitions as aqua boxes, in a charmingly garish color scheme chosen by Dave Tweed. So, the chemical reactions I mentioned before:

C + O₂ → CO₂

CO₂ + NaOH → NaHCO₃

NaHCO₃ + HCl → H₂O + NaCl + CO₂

give this Petri net:

A ‘complex’ is, roughly, a way of putting dots in the yellow circles. In chemistry this says how many molecules we have of each kind. Here’s an example:

This complex happens to have just zero or one dot in each circle, but that’s not required: we could have any number of dots in each circle. So, mathematically, a complex is a finite linear combination of species, with natural numbers as coefficients. In other words, it’s an element of In this particular example it’s

C + O₂ + NaOH + HCl

Given two complexes, we say one is reachable from another if, loosely speaking, we can get to it from the other by a finite sequence of transitions. For example, earlier on I asked if we can get from the complex I just mentioned to the complex

CO₂ + H₂O + NaCl

which we can draw like this:

And the answer is yes, we can do it with this sequence of transitions:

 

 

 

This settles the question I asked earlier.

So in chemistry, reachability is all about whether it’s possible to use certain chemical reactions to turn one collection of molecules into another using a certain set of reactions. I hope this is clear enough; I could formalize it further but it seems unnecessary. If you have questions, ask me or read this:

• Petri net: execution semantics, Wikipedia.

The reachability problem

Now the reachability problem asks: given a Petri net and two complexes, is one reachable from the other?

If the answer is ‘yes’, of course you can show that by an exhaustive search of all possibilities. But if the answer is ‘no’, how can you be sure? It’s not obvious, in general. Back in the 1970’s, computer scientists felt this problem should be decidable by some algorithm… but they had a lot of trouble finding such an algorithm.

In 1976, Richard J. Lipton showed that if such an algorithm existed, it would need to take at least an exponential amount of memory space and an exponential amount of time to run:

• Richard J. Lipton, The reachability problem requires exponential space, Technical Report 62, Yale University, 1976.

This means that most computer scientists would consider any algorithm to solve the reachability problem ‘infeasible’, since they like polynomial time algorithms.

On the bright side, it means that Petri nets might be fairly powerful when viewed as computers themselves! After all, for a universal Turing machine, the analogue of the reachability problem is undecidable. So if the reachability problem for Petri nets were decidable, they couldn’t be universal computers. But if it were decidable but hard, Petri nets might be fairly powerful—though still not universal—computers.

In 1977, at the ACM Symposium on the Theory of Computing, two researchers presented a proof that reachability problem was decidable:

• S. Sacerdote and R. Tenney, The decidability of the reachability problem for vector addition systems, Conference Record of the Ninth Annual ACM Symposium on Theory of Computing, 2-4 May 1977, Boulder, Colorado, USA, ACM, 1977, pp. 61–76.

However, it turned out to be flawed! I read about this episode here:

• James L. Peterson, Petri Net Theory and the Modeling of Systems, Prentice–Hall, New Jersey, 1981.

This is a very nice introduction to early work on Petri nets and decidability. Peterson had an interesting idea, too:

There would seem to be a very useful connection between Petri nets and Presburger arithmetic.

He gave some evidence, and suggested using this to settle the decidability of the reachability problem. I found that intriguing! Let me explain why.

Presburger arithmetic is a simple set of axioms for the arithmetic of natural numbers, much weaker than Peano arithmetic or even Robinson arithmetic. Unlike those other systems, Presburger arithmetic doesn’t mention multiplication. And unlike those other systems, you can write an algorithm that decides whether any given statement in Presburger arithmetic is provable.

However, any such algorithm must be very slow! In 1974, Fischer and Rabin showed that any decision algorithm for Presburger arithmetic has a worst-case runtime of at least

for some constant where is the length of the statement. So we say the complexity is at least doubly exponential. That’s much worse than exponential! On the other hand, an algorithm with a triply exponential run time was found by Oppen in 1978.

I hope you see why this is intriguing. Provability is a lot like reachability, since in a proof you’re trying to reach the conclusion starting from the assumptions using certain rules. Like Presburger arithmetic, Petri nets are all about addition, since they consists of transitions going between linear combinations like this:

6 CO₂ + 6 H₂O → C₆H₁₂O₆ + 6 O₂

That’s why the old literature calls Petri nets vector addition systems. And finally, the difficulty of deciding provability in Presburger arithmetic smells a bit like the difficulty of deciding reachability in Petri nets.

So, I was eager to learn what happened after Peterson wrote his book.

For starters, in 1981, the very year Peterson’s book came out, Ernst Mayr showed that the reachability problem for Petri nets is decidable:

• Ernst Mayr, Persistence of vector replacement systems is decidable, Acta Informatica 15 (1981), 309–318.

As you can see from the title, Mayr actually proved some other property was decidable. However, it follows that reachability is decidable, and Mayr pointed this out in his paper. In fact the decidability of reachability for Petri nets is equivalent to lots of other interesting questions. You can see a bunch here:

• Javier Esparza and Mogens Nielsen, Decidability issues for Petri nets—a survey, Bulletin of the European Association for Theoretical Computer Science 52 (1994), 245–262.

Mayr’s algorithm was complicated. Worse still, it seems to take a hugely long time to run. It seems nobody knows an explicit bound on its runtime. The runtim might even grow faster than any primitive recursive function. The Ackermann function and the closely related Ackermann numbers are famous examples of functions that grow more rapidly than any primitive recursive function. If you don’t know about these, now is the time to learn!

Remember that we can define multiplication by iterating addition:

where add to itself times. Then we can define exponentiation by iterating multiplication:

where we multiply by itself times. Here I’m using Knuth’s up-arrow notation. Then we can define tetration by iterating exponentiation:

Then we can define an operation by iterating tetration, and so on. All these functions are primitive recursive. But the th Ackermann number is not; it’s defined to be

This grows at an insanely rapid rate:

where we have a stack of threes—or in other words, threes! When we get to my mind boggles. I wish it didn’t, but it does.

In 1998 someone came up with a faster algorithm:

• Zakaria Bouziane, A primitive recursive algorithm for the general Petri net reachability problem, in 39th Annual Symposium on Foundations of Computer Science, IEEE, 1998, pp. 130-136.

Bouziane claimed this algorithm is doubly exponential in space and time. That’s very slow, but not insanely slow.

However, it seems that Bouziane made a mistake:

• Petr Jančar, Bouziane’s transformation of the Petri net reachability problem and incorrectness of the related algorithm, Information and Computation, 206 (2008), 1259–1263.

So: if I tell you some chemicals and a bunch of reactions involving these chemicals, you can decide when some combination of these chemicals can turn into another combination. But it may take a long time to decide this. And we don’t know exactly how long: just more than ‘exponentially long’!

What about the connection to Presburger arithmetic? This title suggests that it exists:

• Jérôme Leroux, The general vector addition system reachability problem by Presburger inductive separators, 2008.

But I don’t understand the paper well enough to be sure. Can someone say more?

Also, does anyone know more about the computational power of Petri nets? They’re not universal computers, but is there a good way to say how powerful they are? Does the fact that it takes a long time to settle the reachability question really imply that they have a lot of computational power?

Symmetric monoidal categories

Next let me explain the secret reason I’m so fascinated by this. This section is mainly for people who like category theory.

As I mentioned once before, a Petri net is actually nothing but a presentation of a symmetric monoidal category that’s free on some set of objects and some set of morphisms going between tensor products of those objects:

• Vladimiro Sassone, On the category of Petri net computations, 6th International Conference on Theory and Practice of Software Development, Proceedings of TAPSOFT ’95, Lecture Notes in Computer Science 915, Springer, Berlin, pp. 334-348.

In chemistry we write the tensor product additively, but we could also write it as . Then the reachability problem consists of questions of this general type:

Suppose we have a symmetric monoidal category freely generated by objects and morphisms

Is there a morphism from to ?

This is reminiscent of the word problem for groups and other problems where we are given a presentation of an algebraic structure and have to decide if two elements are equal… but now, instead of asking whether two elements are equal we are asking if there is a morphism from one object to another. So, it is fascinating that this problem is decidable—unlike the word problem for groups—but still very hard to decide.

Just in case you want to see a more formal statement, let me finish off by giving you that:

Reachability problem. Given a symmetric monoidal category freely generated by a finite set of objects and a finite set of morphisms between tensor products of these objects, and given two objects is there a morphism ?

Theorem (Lipton, Mayr). There is an algorithm that decides the reachability problem. However, for any such algorithm, for any the worst-case run-time exceeds where is the size of the problem: the sum of the number of generating objects, the number of factors in the sources and targets of all the generating morphisms, and the number of factors in the objects for which the reachability problem is posed.

The Mathematics of Planet Earth

Here’s a public lecture I gave yesterday, via videoconferencing, at the 55th annual meeting of the South African Mathematical Society:

Abstract: The International Mathematical Union has declared 2013 to be the year of The Mathematics of Planet Earth. The global warming crisis is part of a bigger transformation in which humanity realizes that the Earth is a finite system and that our population, energy usage, and the like cannot continue to grow exponentially. If civilization survives this transformation, it will affect mathematics—and be affected by it—just as dramatically as the agricultural revolution or industrial revolution. We cannot know for sure what the effect will be, but we can already make some guesses.

To watch the talk, click on the video above. To see slides of the talk, click here. To see the source of any piece of information in these slides, just click on it!

My host Bruce Bartlett, an expert on topological quantum field theory, was crucial in planning the event. He was the one who edited the video, and put it on YouTube. He also made this cute poster:

I was planning to fly there using my superpowers to avoid taking a plane and burning a ton of carbon. But it was early in the morning and I was feeling a bit tired, so I used Skype.

By the way: if you’re interested in science, energy and the environment, check out the Azimuth Project, which is a collaboration to create a focal point for scientists and engineers interested in saving the planet. We’ve got some interesting projects going. If you join the Azimuth Forum, you can talk to us, learn more, and help out as much or as little as you want. The only hard part about joining the Azimuth Forum is reading the instructions well enough that you choose your whole real name, with spaces between words, as your username.

John Harte

Earlier this week I gave a talk on the Mathematics of Planet Earth at the University of Southern California, and someone there recommended that I look into John Harte’s work on maximum entropy methods in ecology. He works at U.C. Berkeley.

I checked out his website and found that his goals resemble mine: save the planet and understand its ecosystems. He’s a lot further along than I am, since he comes from a long background in ecology while I’ve just recently blundered in from mathematical physics. I can’t really say what I think of his work since I’m just learning about it. But I thought I should point out its existence.

This free book is something a lot of people would find interesting:

• John and Mary Ellen Harte, Cool the Earth, Save the Economy: Solving the Climate Crisis Is EASY, 2008.

EASY? Well, it’s an acronym. Here’s the basic idea of the US-based plan described in this book:

Any proposed energy policy should include these two components:

• Technical/Behavioral: What resources and technologies are to be used to supply energy? On the demand side, what technologies and lifestyle changes are being proposed to consumers?

• Incentives/Economic Policy: How are the desired supply and demand options to be encouraged or forced? Here the options include taxes, subsidies, regulations, permits, research and development, and education.

And a successful energy policy should satisfy the AAA criteria:

• Availability. The climate crisis will rapidly become costly to society if we do not take action expeditiously. We need to adopt now those technologies that are currently available, provided they meet the following two additional criteria:

• Affordability. Because of the central role of energy in our society, its cost to consumers should not increase significantly. In fact, a successful energy policy could ultimately save consumers money.

• Acceptability. All energy strategies have environmental, land use, and health and safety implications; these must be acceptable to the public. Moreover, while some interest groups will undoubtedly oppose any particular energy policy, political acceptability at a broad scale is necessary.

Our strategy for preventing climate catastrophe and achieving energy independence includes:

• Energy Efficient Technology at home and at the workplace. Huge reductions in home energy use can be achieved with available technologies, including more efficient appliances such as refrigerators, water heaters, and light bulbs. Home retrofits and new home design features such as “smart” window coatings, lighter-colored roofs where there are hot summers, better home insulation, and passive solar designs can also reduce energy use. Together, energy efficiency in home and industry can save the U.S. up to approximately half of the energy currently consumed in those sectors, and at no net cost—just by making different choices. Sounds good, doesn’t it?

• Automobile Fuel Efficiency. Phase in higher Corporate Average Fuel Economy (CAFE) standards for automobiles, SUVs and light trucks by requiring vehicles to go 35 miles per gallon of gas (mpg) by 2015, 45 mpg by 2020, and 60 mpg by 2030. This would rapidly wipe out our dependence on foreign oil and cut emissions from the vehicle sector by two-thirds. A combination of plug-in hybrid, lighter car body materials, re-design and other innovations could readily achieve these standards. This sounds good, too!

• Solar and Wind Energy. Rooftop photovoltaic panels and solar water heating units should be phased in over the next 20 years, with the goal of solar installation on 75% of U.S. homes and commercial buildings by 2030. (Not all roofs receive sufficient sunlight to make solar panels practical for them.) Large wind farms, solar photovoltaic stations, and solar thermal stations should also be phased in so that by 2030, all U.S. electricity demand will be supplied by existing hydroelectric, existing and possibly some new nuclear, and, most importantly, new solar and wind units. This will require investment in expansion of the grid to bring the new supply to the demand, and in research and development to improve overnight storage systems. Achieving this goal would reduce our dependence on coal to practically zero. More good news!

• You are part of the answer. Voting wisely for leaders who promote the first three components is one of the most important individual actions one can make. Other actions help, too. Just as molecules make up mountains, individual actions taken collectively have huge impacts. Improved driving skills, automobile maintenance, reusing and recycling, walking and biking, wearing sweaters in winter and light clothing in summer, installing timers on thermostats and insulating houses, carpooling, paying attention to energy efficiency labels on appliances, and many other simple practices and behaviors hugely influence energy consumption. A major education campaign, both in schools for youngsters and by the media for everyone, should be mounted to promote these consumer practices.

No part of EASY can be left out; all parts are closely integrated. Some parts might create much larger changes—for example, more efficient home appliances and automobiles—but all parts are essential. If, for example, we do not achieve the decrease in electricity demand that can be brought about with the E of EASY, then it is extremely doubtful that we could meet our electricity needs with the S of EASY.

It is equally urgent that once we start implementing the plan, we aggressively export it to other major emitting nations. We can reduce our own emissions all we want, but the planet will continue to warm if we can’t convince other major global emitters to reduce their emissions substantially, too.

What EASY will achieve. If no actions are taken to reduce carbon dioxide emissions, in the year 2030 the U.S. will be emitting about 2.2 billion tons of carbon in the form of carbon dioxide. This will be an increase of 25% from today’s emission rate of about 1.75 billion tons per year of carbon. By following the EASY plan, the U.S. share in a global effort to solve the climate crisis (that is, prevent catastrophic warming) will result in U.S emissions of only about 0.4 billion tons of carbon by 2030, which represents a little less than 25% of 2007 carbon dioxide emissions.128 Stated differently, the plan provides a way to eliminate 1.8 billion tons per year of carbon by that date.

We must act urgently: in the 14 months it took us to write this book, atmospheric CO₂ levels rose by several billion tons of carbon, and more climatic consequences have been observed. Let’s assume that we conserve our forests and other natural carbon reservoirs at our current levels, as well as maintain our current nuclear and hydroelectric plants (or replace them with more solar and wind generators). Here’s what implementing EASY will achieve, as illustrated by Figure 3.1 on the next page.

Please check out this book and help me figure out if the numbers add up! I could also use help understanding his research, for example:

• John Harte, Maximum Entropy and Ecology: A Theory of Abundance, Distribution, and Energetics, Oxford University Press, Oxford, 2011.

The book is not free but the first chapter is.

This paper looks really interesting too:

• J. Harte, T. Zillio, E. Conlisk and A. B. Smith, Maximum entropy and the state-variable approach to macroecology, Ecology 89 (2008), 2700–-2711.

Again, it’s not freely available—tut tut. Ecologists should follow physicists and make their work free online; if you’re serious about saving the planet you should let everyone know what you’re doing! However, the abstract is visible to all, and of course I can use my academic superpowers to get ahold of the paper for myself:

Abstract: The biodiversity scaling metrics widely studied in macroecology include the species-area relationship (SAR), the scale-dependent species-abundance distribution (SAD), the distribution of masses or metabolic energies of individuals within and across species, the abundance-energy or abundance-mass relationship across species, and the species-level occupancy distributions across space. We propose a theoretical framework for predicting the scaling forms of these and other metrics based on the state-variable concept and an analytical method derived from information theory. In statistical physics, a method of inference based on information entropy results in a complete macro-scale description of classical thermodynamic systems in terms of the state variables volume, temperature, and number of molecules. In analogy, we take the state variables of an ecosystem to be its total area, the total number of species within any specified taxonomic group in that area, the total number of individuals across those species, and the summed metabolic energy rate for all those individuals. In terms solely of ratios of those state variables, and without invoking any specific ecological mechanisms, we show that realistic functional forms for the macroecological metrics listed above are inferred based on information entropy. The Fisher log series SAD emerges naturally from the theory. The SAR is predicted to have negative curvature on a log-log plot, but as the ratio of the number of species to the number of individuals decreases, the SAR becomes better and better approximated by a power law, with the predicted slope z in the range of 0.14-0.20. Using the 3/4 power mass-metabolism scaling relation to relate energy requirements and measured body sizes, the Damuth scaling rule relating mass and abundance is also predicted by the theory. We argue that the predicted forms of the macroecological metrics are in reasonable agreement with the patterns observed from plant census data across habitats and spatial scales. While this is encouraging, given the absence of adjustable fitting parameters in the theory, we further argue that even small discrepancies between data and predictions can help identify ecological mechanisms that influence macroecological patterns.

Mathematics of the Environment (Part 4)

We’ve been looking at some very simple models of the Earth’s climate. Pretty soon I want to show you one that illustrates the ice albedo effect. This effect says that when it’s colder, there’s more ice and snow, so the Earth gets lighter in color, so it reflects more sunlight and tends to get even colder. In other words, it’s a positive feedback mechanism: a reaction that strengthens the process that caused the reaction.

Since a higher temperature leads to a higher radiation and therefore to cooling, and a lower temperature leads to a lower radiation, according to the Planck distribution, there is always also a negative feedback present in the climate system of the earth. This is dubbed the Planck feedback, and this is what ultimately protects the Earth against getting arbitrarily hot or cold.

However, the ice albedo effect may be important for the ‘ice ages’ or more properly ‘glacial cycles’ that we’ve been having for the last few ten million years… and also for much earlier, much colder Snowball Earth events. In reverse, melting ice now tends to make the Earth darker and even warmer. So, this is an interesting topic for many reasons… including the math, which we’ll get to later.

Now, obviously the dinosaurs did not keep records of the temperature, so how we estimate temperatures on the ancient Earth is an important question, which deserves a long discussion—but not today! Today I’ll be fairly sketchy about that. I just want you to get a feel for the overall story, and some open questions.

The Earth’s temperature since the last glacial period

First, here’s a graph of Greenland temperatures over the last 18,000 years:

(As usual, click to enlarge and/or get more information.) This chart is based on ice cores, taken from:

• Richard B. Alley, The Two-Mile Time Machine: Ice Cores, Abrupt Climate Change, and our Future, Princeton U. Press, Princeton, 2002.

This is a good book for learning how people reconstruct the
history of temperatures in Greenland from looking at a two-mile-long ice core drilled out of the glaciers there.

As you can see, first Greenland was very cold, and then it warmed up at the end of the last ‘ice age’, or glacial period. But there are lot of other things to see in this graph. For example, there was a severe cold spell between 12.9 and 11.5 thousand years ago: the Younger Dryas event.

I love that name! It comes from the tough little Arctic flower
Dryas octopetala, whose plentiful pollen in certain ice samples gave evidence that this time period was chilly. Was there an Older Dryas? Yes: before the Younger Dryas there was a warm spell called the Allerød, and before that a cold period called the Older Dryas.

The Younger Dryas lasted about 1400 years. Temperatures dropped dramatically in Europe: about 7 °C in only 20 years! In Greenland, it was 15 °C colder during the Younger Dryas than today. In England, the average annual temperature was -5 °C, so glaciers started forming. We can see evidence of this event from oxygen isotope records and many other things.

Why the sudden chill? One popular theory is that the melting of the ice sheet on North America lowered the salinity of North Atlantic waters. This in turn blocked a current called the
Atlantic meridional overturning circulation, or AMOC for short, which normally brings warm water up the coast of Europe. Proponents of this theory argue that this current is what makes London much warmer than, say, Winnipeg in Canada or Irkutsk in Russia. Turn it off and—wham!—you’ll get glaciers forming in England.

Anyway, whatever caused it, the Younger Dryas ended as suddenly at it began, with temperatures jumping 7 °C. Since then, the Earth continued warming up until about 6 thousand years ago—the mid-Holocene thermal maximum. The earth was about 1° or 2° Celsius warmer than today. Since then, it’s basically been cooling off—not counting various smaller variations, like the global warming we’re experiencing in this century.

However, these smaller variations are very interesting! From 6000 to 2500 years ago things cooled down, with the coolest
stretch occurring between 4000 and 2500 years ago: the Iron Age Cold Epoch.

Then things warmed up for a while, and then they cooled down
from 500 to 1000 AD. Yes, the so-called "Dark Ages" were also chilly!

After this came the Medieval Warm Period, a period from about 1000 to 1300 AD:

From 1450 AD to 1890 there was a period of cooling, often called the Little Ice Age. This killed off the Icelandic colonies in Greenland, as described in this gripping book:

• Jane Smiley, The Greenlanders, Ballantine Books, New York, 1996.

However, the term "Little Ice Age" exaggerates the importance of a small blip in the grand scheme of things. It was nowhere near as big as the Younger Dryas: temperatures may have dropped a measly 0.2° Celsius from the Medieval optimum, and it may have happened only in Europe—though this was a subject of debate when I last checked.

Since then, things have been warming up:

The subject has big political implications, and is thus subject to enormous controversy. But, I think it’s quite safe to say that we’ve been seeing a rapid temperature rise since 1900, with the Northern Hemisphere average temperature rising roughly 1 °C since then. Each of the last 11 years, from 2001 to 2011, was one of the 12 warmest years since 1901. (The other one was 1998.)

All these recent variations in the Earth’s climate are very much worth trying to understand. but now let’s back off to longer time periods! We don’t have many Earth-like planets whose climate we can study in detail—at least not yet, since they’re too far away. But we do have one planet, the Earth, that’s gone through many changes. The climate since the end of the last ice age is just a tiny sliver of a long and exciting story!

The Earth’s long-term climate history

Here’s a nice old chart showing estimates of the Earth’s average temperature in the last 150 years, the last 16,000 years, the last 150,000 years and the last million years:

Here “ka” or “kilo-annum” means a thousand years. These temperatures are estimated by various methods; I got this chart from:

• Barry Saltzman, Dynamical Paleoclimatology: Generalized Theory of Global Climate Change, Academic Press, New York, 2002, fig. 3-4.

As we keep zooming in towards the present we keep seeing more detail:

• Over the last million years there have been about ten glacial periods—though trying to count them is a bit like trying to count ‘very deep valleys’ in a hilly landscape!

• From 150 to 120 thousand years ago it warmed up rather rapidly. From 120 thousand years ago to 16 thousand years ago it cooled down—that was the last glacial period. Then it warmed up rather rapidly again.

• Over the last 10 thousand years temperatures have been unusually constant.

• Over the last 150 years it’s been warming up slightly.

If we go back further, say to 5 million years, we see that temperatures have been colder but also more erratic during this period:

This figure is based on this paper:

• L. E. Lisiecki and M. E. Raymo, A Pliocene-Pleistocene stack of 57 globally distributed benthic δ¹⁸O records, Paleoceanography 20 (2005), PA1003.

Lisieki and Raymo combined measurements of oxygen isotopes in the shells of tiny sea creatures called foraminifera from 57 globally distributed deep sea sediment cores. But beware: they constructed this record by first applying a computer aided process to align the data in each sediment core. Then the resulting stacked record was tuned to make the positions of peaks and valleys match the known Milankovitch cycles in the Earth’s orbit. The temperature scale was chosen to match Vostok ice core data. So, there are a lot of theoretical assumptions built into this graph.

Going back 65 million years, we see how unusual the current glacial cycles are:

Click to make this graph bigger; it’s from:

• Robert Rohde, 65 million years of climate change, at Global Warming Art.

This graph shows the Earth’s temperature since the extinction of the dinosaurs about 65 million years ago—the end of the Mesozoic and beginning of the Cenozoic. At first the Earth warmed up, reaching its warmest 50 million years ago: the "Eocene Optimum". The spike before that labelled "PETM" is a fascinating event called the Paleocene-Eocene Thermal Maximum. At the end of the Eocene the Earth cooled rapidly and the Antarctic acquired year-round ice. After a warming spell near the end of the Oligocene, further cooling and an increasingly jittery climate led ultimately to the current age of rapid glacial cycles.

Why is the Earth’s climate so jittery nowadays? That’s a fascinating puzzle, which I’d like to discuss in the weeks to come.

Why did the Earth suddenly cool at the end of the Eocene 34 million years ago? One theory relies on the fact that this is when Antarctica first became separated from Australia and South America. After the Tasmanian Gateway between Australia and Antarctica opened, the only thing that kept water from swirling endlessly around Antarctica, getting colder and colder, was the connection between this continent and South America. South America seems to have separated from Antarctica around the end of the Eocene.

In the early Eocene, Antarctica was fringed with a warm temperate to sub-tropical rainforest. But as the Eocene progressed it became colder, and by the start of the Oligocene it had deciduous forests and vast stretches of tundra. Eventually it became almost completely covered with ice.

Thanks to the ice albedo effect, an icy Antarctic tends to keep the Earth cooler. But is that the only or even the main explanation of the overall cooling trend over the last 30 million years? Scientists argue about this.

Going back further:

Here "Ma" or "mega-annum" means "million years". This chart was drawn from many sources; I got it from:

• Barry Saltzman, Dynamical Paleoclimatology: Generalized Theory of Global Climate Change, Academic Press, New York, 2002, fig. 1-3.

Among other things on this chart, you can sort of see hints of the Snowball Earth events that may have happened early in the Earth’s history. These are thought to have occurred during the Cryogenian period 850 to 635 million years ago, and also during the Huronian glaciation 2400 to 2100 million years ago. In both these events a large portion of the Earth was frozen—much more, it seems, than in the recent glacial periods! Ice albedo feedback plays a big role in theories of these events… though also, of course, there must be some explanation of why they ended.

As you can see, there’s a lot of things a really universal climate model might seek to explain. We don’t necessarily need to understand the whole Earth’s history to model it well now, but thinking about other eras is a good way to check our understanding of the present-day Earth.

Mathematics for Sustainability (Part 1)

guest post by John Roe

This year, I want to develop a new math course. Nothing surprising in that—it is what math professors do all the time! But usually, when we dream of new courses, we are thinking of small classes of eager graduate students to whom we can explain the latest research ideas. Here, I’m after something a bit different.

The goal will be through a General Education Mathematics course, to enable students to develop the quantitative and qualitative skills needed to reason effectively about environmental and economic sustainability. That’s a lot of long words! Let me unpack a bit:

• General Education Mathematics At most universities (including Penn State University, where I teach), every student, whatever their major, has to take one or two “quantitative” courses – this is called the “general education” requirement. I want to reach out to students who are not planning to be mathematicians or scientists, students for whom this may be the last math course they ever take.

• quantitative and qualitative skills I want students to be able to work with numbers (“quantitative”)—to be able to get a feeling for scale and size, whether we’re talking about gigatonnes of carbon dioxide, kilowatts of domestic power, or picograms of radioisotopes. But I also want them to get an intuition for the behavior of systems (qualitative), so that the ideas of growth, feedback, oscillation, overshoot and so on become part of their conceptual vocabulary.

• to reason effectively A transition to a more sustainable society won’t come about without robust public debate—I want to help students engage effectively in this debate. Shamelessly stealing ideas from Andrew Read’s Science in Our World course, I hope to do this by using an online platform for student presentations. Engaging with this process (which includes commenting on other people’s presentations as well as devising your own) will count seriously in the grading scheme.

• environmental and economic sustainability I’d like students to get the idea that there are lots of scales on which one can ask the sustainability question – both time scales (how many years is “sustainable”) and spatial scales. We’ll think about global-scale questions (carbon dioxide emissions being an obvious example) but we’ll try to look at as many examples as possible on a local scale (a single building, the Penn State campus, local agriculture) so that we can engage more directly.

I have been thinking about this plan for a year or more but now it’s time to put it into action. I’ve been in touch with my department head and got a green light to offer this for the first time in Spring 2014. In future posts I will share some more about the structure of the course as it develops. Meanwhile, if anyone has some good suggestions, let me know!

Insanely Long Proofs

 

There are theorems whose shortest proof is insanely long. In 1936 Kurt Gödel published an abstract called “On the length of proofs”, which makes essentially this claim.

But what does ‘insanely long’ mean?

To get warmed up, let’s talk about some long proofs.

Long proofs

You’ve surely heard of the quadratic formula, which lets you solve

with the help of a square root:

There’s a similar but more complicated ‘cubic formula’ that lets you solve cubic equations, like this:

The cubic formula involves both square roots and cube roots. There’s also a ‘quartic formula’ for equations of degree 4, like this:

The quartic formula is so long that I can only show it to you if I shrink it by an absurd amount:

(Click repeatedly to enlarge.) But again, it only involves additions, subtraction, multiplication, division and taking roots.

In 1799, Paolo Ruffini proved that there was no general solution using radicals for polynomial equations of degree 5 or more. But his proof was 500 pages long! As a result, it was “mostly ignored”. I’m not sure what that means, exactly. Did most people ignore it completely? Or did everyone ignore most of it? Anyway, his argument seems to have a gap… and later Niels Abel gave a proof that was just 6 pages long, so most people give the lion’s share of credit to Abel.

Jumping ahead quite a lot, the longest proof written up in journals is the classification of finite simple groups. This was done by lots of people in lots of papers, and the total length is somewhere between 10,000 and 20,000 pages… nobody is exactly sure! People are trying to simplify it and rewrite it. The new proof will be a mere 5,000 pages long. So far six books have been written as part of this project.

Even when it’s all in one book, how can we be sure such a long proof is right? Some people want to use computers to make the argument completely rigorous, filling in all the details with the help of a program called a ‘proof assistant’.

The French are so sexy that even their proof assistant sounds dirty: it’s called Coq. Recently mathematicians led by George Gonthier have used Coq to give a completely detailed proof of a small piece of the classification of finite simple groups: the Feit–Thompson Theorem. Feit and Thompson’s original proof of this result, skipping lots of steps that are obvious to experts, took 255 pages!

What does the Feit–Thompson theorem say? Every finite group with an odd number of elements is solvable! Explaining that statement might take quite a while, depending on what you know about math. So let me just say this:

Galois invented group theory and used it to go further than Abel and Ruffini had. He showed a bunch of specific polynomial equations couldn’t be solved just using addition, subtraction, multiplication, division and taking roots. For example, those operations aren’t powerful enough to solve this equation:

while they can solve this one:

Galois showed that every polynomial equation has a group of symmetries, and you can solve the equation using addition, subtraction, multiplication, division and taking roots if its group has a certain special property. So, this property of a group got the name ‘solvability’.

Every finite group with an odd number of elements is solvable. It’s quick to say, but hard to show—so hard that making the proof fully rigorous on a computer seemed out of reach at first:

When Gonthier first suggested a formal Feit-Thompson Theorem proof, his fellow members of the Mathematical Components team at Inria could hardly believe their ears.

“The reaction of the team the first time we had a meeting and I exposed a grand plan,” he recalls ruefully, “was that I had delusions of grandeur. But the real reason of having this project was to understand how to build all these theories, how to make them fit together, and to validate all of this by carrying out a proof that was clearly deemed to be out of reach at the time we started the project.”

It took them 6 years! The completed computer proof has 170,000 lines. It involves 15,000 definitions and 4,300 lemmas. Maybe now Gonthier is dreaming of computerizing the whole classification of finite simple groups.

But there are even longer proofs of important results in math. These longer proofs all involve computer calculations. For example, Thomas Hales seems to have proved that the densest packing of spheres in 3d space is the obvious one, like this:

(There are infinitely many other equally dense packings, as I explained earlier, but none denser.)

Hales’ proof is a hundred pages of writing together with about 3 gigabytes of computer calculations. If we wrote out those calculations in a text file, they’d fill about 2 million pages!

The method is called ‘proof by exhaustion’, because it involves reducing the problem to 10,000 special cases and then settling each one with detailed calculations… thus exhausting anybody who tries to check the proof by hand. Now Hales is trying to create a fully formal proof that can be verified by automated proof checking software such as HOL. He expects that doing this will take 20 years.

These proofs are long, but they’re not what I’d call insanely long.

Insanely long proofs

What do I mean by ‘insanely’ long? Well, for example, I know a theorem that you can prove using the usual axioms of arithmetic—Peano arithmetic—but whose shortest proof using those axioms contains

symbols. This is so many symbols that you couldn’t write them all down if you wrote one symbol on each proton, neutron and electron in the observable Universe!

I also know a theorem whose shortest proof in Peano arithmetic contains

symbols. This is so many that if you tried to write down the number of symbols—not the symbols themselves—in ordinary decimal notation, you couldn’t do it if you wrote one digit on each proton, neutron and electron in the observable Universe!

I also know a theorem whose shortest proof in Peano arithmetic contains…

… well, you get the idea.

By the way, if you don’t know what Peano arithmetic is, don’t worry. It’s just a list of obvious axioms about arithmetic, together with some obvious rules for reasoning, which turn out to be good enough to prove most everyday theorems about arithmetic. The main reason I mention it is that we need to pick some particular setup before we can talk about the ‘shortest proof’ of a theorem and have it be well-defined.

Also by the way, I’m assuming Peano arithmetic is consistent. If it were inconsistent, you could prove 0=1, and then everything would follow quite quickly from that. But most people feel sure it’s consistent.

If it is, then the shortest proof using Peano arithmetic of the following theorem contains at least symbols:

This statement has no proof in Peano arithmetic that contains fewer than symbols.

Huh? This doesn’t look a statement about arithmetic! But Gödel showed how you could encode the concept of ‘statement’ and ‘proof’ into arithmetic, and use this to create statements that refer to themselves. He’s most famous for this one:

This statement has no proof in Peano arithmetic.

It turns out that this statement is true… so it’s an example of a true statement about arithmetic that can’t be proved using Peano arithmetic! This is Gödel’s first incompleteness theorem.

This variation is similar:

This statement has no proof in Peano arithmetic that contains fewer than symbols.

This statement is also true. It’s provable in Peano arithmetic, but its proof contains at least symbols.

Even longer proofs

But this is just the beginning. If Peano arithmetic is consistent, there are infinitely many theorems whose shortest proof is longer than 10 to the 10 to the 10 to the 10 to the… where the stack of 10’s is as long as the statement of the theorem.

Indeed, take any computable function, say F—growing as fast as you like. Then if Peano arithmetic is consistent, there are infinitely many theorems whose shortest proof is longer than this function of the length of the theorem!

But how do we know this? Here’s how. Using Gödel’s clever ideas, we can create a statement in arithmetic that says:

This statement has no proof in Peano arithmetic that is shorter than F of the length of this statement.

Let’s call this statement P.

We’ll show that if Peano arithmetic is consistent, then P is provable in Peano arithmetic. So, according to what P itself says, P is an example of a statement whose shortest proof is insanely long!

Now, let me sketch why if Peano arithmetic is consistent then P is provable in this setup. To save time, I’ll use N to stand for ‘F of the length of P’. So, P says:

P has no proof in Peano arithmetic whose length is less than N.

Assume there were a proof of P in Peano arithmetic whose length is less than N. Then, thanks to what P actually says, P would be false.

Moreover, we could carry out the argument I just gave within Peano arithmetic. So, within Peano arithmetic, we could disprove P.

But wait a minute—this would mean that within Peano arithmetic we could both prove and disprove P! We’re assuming Peano arithmetic is consistent, so this is impossible.

So our assumption must have been wrong. P must have no proof in Peano arithmetic whose length is less than N.

But this is what P says! So P is true!

Even better, P is provable in Peano arithmetic. Why? Because we can just go through all proofs shorter than N, and check that they’re not proofs of P… we know they won’t be… and this will constitute a proof that:

P has no proof in Peano arithmetic whose length is less than N.

But this is just what P says! So this is a way to prove P. Moreover we can carry out this long-winded check within Peano arithmetic, and get a proof of P in Peano arithmetic!

Of course, this proof has length more than N.

By the way, here I’m using the fact that there are only finitely many proofs with length less than N, so we can go through them all. We have to define ‘length’ in a way that makes this true, for my argument to work. For example, we can take the length to be the number of symbols.

Also, it’s important that our function F be computable. We need to compute N to know how many proofs we need to go through.

The upshot: if Peano arithmetic is consistent, there’s a provable statement whose shortest proof in Peano arithmetic is insanely long, by any computable standard of what counts as ‘insanely long’.

Now, so far we’ve just gotten one theorem with an insanely long proof. But we can get infinitely many, one for each natural number n, as follows. Let P(n) be a statement in arithmetic that says:

This statement has no proof in Peano arithmetic whose length is less than n plus F of the length of this statement.

The same argument I just sketched shows that if Peano arithmetic is consistent then P(n) is provable, but has no proof shorter than n plus F of the length of P(n). The statements P(n) are different for different values of n. So, we get infinitely many different statements with insanely long proofs… at least if Peano arithmetic is consistent, which most people believe.

Proof speedup

But wait a minute! If we’ve proved all these statements P(n) have proofs, then we’ve basically proved them—no? And my argument, though sketchy, was quite short. So, even a completely detailed version of my argument should not be ‘insanely long’. Doesn’t that contradict my claim that the shortest proofs of these statements are insanely long?

Well, no. I only showed that the shortest proof of P(n) using Peano arithmetic is insanely long. I did provide a short proof of P(n). But I did this assuming Peano arithmetic is consistent!

So I didn’t give a short proof of P(n) using Peano arithmetic. I gave a short proof using Peano arithmetic plus the assumption that Peano arithmetic is consistent!

So, if we add to Peano arithmetic an extra axiom saying ‘Peano arithmetic is consistent’, infinitely many theorems get vastly shorter proofs!

This is often called Gödel’s speedup theorem. For more, see:

• Gödel’s speedup theorem, Wikipedia.

Connections

It’s pretty cool how just knowing Peano arithmetic was consistent would let us vastly shorten infinitely many proofs.

As an instant consequence, we get Gödel’s second incompleteness theorem: it’s impossible to use Peano arithmetic to prove its own consistency. For if we could, adding that consistency as an extra axiom couldn’t shorten proofs by an arbitrarily large amount. It could only shorten proofs by a fixed finite amount: roughly, the number of symbols in the proof that Peano arithmetic is consistent.

And while we’re at it, let’s note how the existence of insanely long proofs is related to another famous result: the Church–Turing theorem. This says it’s impossible to write a computer program that can decide in a finite time, yes or no, whether any given statement is provable in Peano arithmetic.

Suppose that in Peano arithmetic there were a computable upper bound on the length of a proof of any statement, as a function of the length of that statement. Then we could write a program that would go through all potential proofs of any statement and tell us, in a finite amount of time, whether it had a proof. So, Peano arithmetic would be decidable!

But since it’s not decidable, no such computable upper bound can exist. This is another way of seeing that there must be theorems with insanely long proofs.

So, the existence of insanely long proofs is tightly connected to the inability of Peano arithmetic to prove itself consistent, and also the undecidability of Peano arithmetic. And these are features not just of Peano arithmetic, but of any system of arithmetic that’s sufficiently powerful, yet simple enough that we can write a program to check to see if a purported proof really is a proof.

Buss’ speedup theorem

In fact Gödel stated his result in a more sophisticated way than I did. He never published a proof… but not because the proof is insanely long, probably just because he was a busy man with many ideas. Samuel Buss gave a proof in 1994:

• On Gödel’s theorems on lengths of proofs I: Number of lines and speedups for arithmetic, Journal of Symbolic Logic 39 (1994), 737–756.

In first-order arithmetic you can use variables like x,y,z to stand for natural numbers like 0,1,2,3,… This is the kind of arithmetic I’ve been talking about so far: Peano arithmetic is an example. In second-order arithmetic you can also use variables of a different kind to stand for sets of natural numbers. Third-order arithmetic goes further and lets you use variables for sets of sets of natural numbers, and so on.

Gödel claimed, and Buss showed, that each time you go up an order, some statements that were already provable get insanely shorter proofs. So, turning this fact around, there are theorems that have insanely long proofs in first-order arithmetic!

(And similarly for second-order arithmetic, and so on…)

For more details, explained in a fairly friendly way, try:

• Speed-up theorems, Stanford Encyclopedia of Philosophy.

By the way, this post is a kind of followup to my post on enormous integers. Insanely long proofs are related to enormous integers: if you know a quick way to describe an enormous integer, you can use the trick I described to cook up a theorem with an enormous proof.

Last time we saw the logician Harvey Friedman was a master of enormous integers. So it’s not surprising to me that Wikipedia says:

Harvey Friedman found some explicit natural examples of this phenomenon, giving some explicit statements in Peano arithmetic and other formal systems whose shortest proofs are ridiculously long.

However, I don’t know these statements. I assume they’re more natural than the weird self-referential examples I’ve described. What are they?

Elsevier: Strangling Libraries Worldwide

 

After academics worldwide began a boycott against Elsevier, this publisher claimed it would mend its ways and treat mathematicians better.

Why just mathematicians? Maybe they didn’t notice that only 17% of the researchers boycotting them are mathematicians. More likely, they’re trying a ‘divide and conquer’ strategy.

Despite their placating gestures, the overall problem persists:

Elsevier’s business model is to get very smart people to work for free, then sell their results back to them at high and ever-rising prices.

Does that sound sustainable to you? It works better than you might think, because they have control over many journals that academics want, and they sell these journals in big ‘bundles’, so you can’t stop buying just some of them. In short, they have monopoly power.

Worse, the people who actually buy the journals are not the academics, but university libraries. Librarians are very nice people. They want to keep their customers—the academics—happy. So they haven’t been very good at saying what they should:

Okay, you want to raise your prices? Fine, we’ll stop subscribing to all your journals until you lower them!

And so, libraries world-wide are slowly being strangled by Elsevier.

A while back, when the economic crisis hit here at U. C. Riverside, our library’s budget was cut. Journals eat up most of the budget, but librarians felt they couldn’t drop subscriptions to all the Elsevier journals, and Elsevier’s practice of bundling meant they couldn’t drop just some of them. The only ways to cut costs were to cut library hours, lay off staff, cut journals published by smaller—and cheaper!—publishers, and buy fewer books. Books can always be bought later… in theory… so they took the biggest hit. Our book budget was slashed to about a tenth of its original level!

The people most hurt were not mathematicians or scientists, but people working in the humanities. They’re the ones who use books the most.

And here’s a shocking story I recently got in my email. I’ll paraphrase, because the details of cases like this are kept secret thanks to Elsevier’s legal tactics:

I wanted to inform you that the University of X is negotiating our new contract with Elsevier for 2013–2015, and what effect Elsevier’s proclaimed changes have.

First of all, the university library has a 42% smaller budget in 2013 than in 2010 for books, journals, etc. So they are negotiating with many publishers, to be able to cancel more subscriptions than allowed in the existing contracts.

The Elsevier contracts for journal subscriptions ends in 2012, and for the so-called “Freedom Collection”—a bundle providing access to all non-subscribed journals—it ends in 2013. I asked the librarian whether there was a price reduction for the new contracts. He reported:

At the beginning of the negotiations he told the Elsevier sales representative, Mister Q, that the University of X has its back to the wall due to the 42% budget cut. Q offered the new contract with moderate price increase of around 5%. A price decrease was out of the question.

Our librarian asked whether he could cancel various subscriptions, many more than allowed in the expiring contract. Q agreed in principle—as long as the total price does not decrease! He was quite cooperative, and essentially offered various different knives to be stabbed with, such as:

• a price increase for the Freedom Collection

or

• an increase of the content fee: this fee, charged in addition to the subscription if one wants electronic access, could go up to 25%. This fee is charged even if one wants only the electronic access and no printed volumes.

Then our librarian asked Q what he should reply to my question about price decreases. Q sent a long reply including that:

– our national science foundation bought the Elsevier archive already some years ago. Therefore we would not benefit from the fact that the archives are now partly free.

– our university cancelled all its math subscriptions already in 2007. Therefore we do not benefit from the price decrease of math journals.

Then he explained at length that we would benefit from what they were doing “as part of our ongoing project to address the needs of the mathematics community”: “holding down 2013 prices, launching a Core Mathematics subject collection, convening an advisory Scientific Council for Mathematics – designed to meet the specific needs of the mathematics community, members of which were critical of Elsevier in the wake of the Cost of Knowledge petition.”

I hope you see why we all need to boycott Elsevier. Stop publishing our papers with them, stop refereeing papers for them, stop working as editors for them, and convince your librarian that it’s okay to unsubscribe to their journals. Please go to this website and join over 12,000 top researchers in this boycott.

For more information, click on this: