Home

A Topos Foundation for Theories of Physics

A Topos Foundation for Theories of Physics: I. Formal Languages for Physics. Andreas Döring and Chris Isham.

This paper is the first in a series whose goal is to develop a fundamentally new way of constructing theories of physics. The motivation comes from a desire to address certain deep issues that arise when contemplating quantum theories of space and time. Our basic contention is that constructing a theory of physics is equivalent to finding a representation in a topos of a certain formal language that is attached to the system. Classical physics arises when the topos is the category of sets. Other types of theory employ a different topos. In this paper we discuss two different types of language that can be attached to a system, S. The first is a propositional language, PL(S); the second is a higher-order, typed language L(S). Both languages provide deductive systems with an intuitionistic logic. The reason for introducing PL(S) is that, as shown in paper II of the series, it is the easiest way of understanding, and expanding on, the earlier work on topos theory and quantum physics. However, the main thrust of our programme utilises the more powerful language L(S) and its representation in an appropriate topos.

This is a little outside of our usual areas, but I think it will appeal to at least some readers. Personally, I find the approach aesthetically very, very appealing for several reasons, and I would be thrilled if an answer to quantum cosmology came from this direction, but I'm the first to admit that my grasp of the phsyics is barely enough to follow along. I was able to make it through this paper fairly easily, but things aren't too interesting in the classical case, and I sadly suspect that the application to quantum physics in parts II and III will leave me behind.

Via The n-Category Cafe, where there is also considerable discussion, much of it around the single word "peristalithic"...

By Matt Hellige at 2007-03-21 05:13 | Category Theory | Type Theory | other blogs | 10136 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Logics of Worlds

From way off in left field, the recent Logiques des mondes by the French philosopher Alain Badiou uses some basic topos theory to elaborate an account of appearance qua being-there. It's interesting in this connection that the linked article refers to "Daseinisation"...

By Dominic Fox at Wed, 2007-03-21 10:05 | login or register to post comments

A long way from home

Ouch... This is very far from PLT as known to mankind...

But the Badiou paper sounds interesting, none the less.

By Ehud Lamm at Wed, 2007-03-21 10:26 | login or register to post comments

Not that far ?

It sure is a long way from home, but maybe not that much.

What Düring and Isham are doing is try to find a way to formulate physical theories with an interface that can be separate from an implementation. That sounds familiar already, but even more familiar is that the interface language is an high-order multi-sorted intuitionistic logic, not far from the ones we use in type systems.

Also, one of the key ideas of their papers is that translation between different local languages of different toposes is central to understand physical systems. Sounds like DSL to me :)

In general, I think that, with the rise of quantum computing for example, methods and models from the computing science side (and maybe especially PLT) are going to start being used in physics. As a (somewhat weak) proof, the n-category café is publishing online a course of John Baez about Classical versus quantum computation, which integrates a huge and interesting part about lambda-calculus and its categorified models, with a lot of references and papers that are, this time, directly in our garden.

But maybe I just have a simply too broad vision of what "PLT" is :)

By renaud at Wed, 2007-03-21 11:23 | login or register to post comments

Agreed

I agree with you, which is why I decided to post it. I won't post more of this kind of stuff, probably, but I thought it ought to show up at least once. Not because of how far away it seems to be, but rather because there's some chance that it's closer than we think.

And in any case I'm glad I'm not the only one who found it relevant!

By Matt Hellige at Fri, 2007-03-23 06:19 | login or register to post comments

Please continue

I read the n-category cafe at least weekly. The relevance may be hard to see at first, but once you learn enough programming language semantics, the links are quite clear.

And if ever there really is a quantum computer that one can truly program, all this stuff is going to come back magnified a 100-fold!

By Jacques Carette at Mon, 2007-03-26 15:03 | login or register to post comments

2-categories and catastrophe theory

Thanks for that Baez link! I love that stuff.

By Frank Atanassow at Fri, 2007-03-23 11:28 | login or register to post comments

This is spam

Somebody tried very hard to write what looks like a real comment, but the last link proves otherwise. (Or it is a genuine post but "Innocent" has some kind of virus in his browser that puts links in his post data.)

By Sjoerd Visscher at Fri, 2007-07-27 11:42 | login or register to post comments