Marcus, re your earlier post: Thanks, sorry if I misinterpreted you!
So, my last post in here basically ignored Topos, and Fra seems to be a little confused in some of his posts trying to tackle the subject, so I would like to go back and try to say something about that. I apologize if anything I'm about to say here is just repeating things people already know.
Fra said:
About topos theory: I have absolutely no prior experience with this at all, and I tried to skim
(1) A Topos Foundation for Theories of Physics: I. Formal Languages for Physics
--
http://arxiv.org/abs/quant-ph/0703060
last night, and it is clearly having a high level of abstraction which I haven't idenfitied yet. Something is appealing with it, but I could be mistaken. I probalby need to read this again and think about it. The basic motivation as argued in the paper for coming up with a new formalism is one I share, but at least on the first reading I failed to see why topos formalism is the best solution. It seems to be strongly mathematically guided. I need to read more on this to be able to sensibly comment.
/Fredrik
I don't know if this will help, but let me take a shot:
First off, for purposes of what Smolin is talking about, the important thing is not
topos theory. It is
topos logic. So it would not surprise me that if you started looking up information on topos, you wouldn't see anything that seems specifically relevant to the point Smolin is making about kinds of logic.
What I mean by this: Topos are actually just a mathematical construct from category theory. Topos theory is all about the behavior of this construct. (Category theory is an aggressively abstract subject, and it has its own extremely insular and peculiar vocabulary, so if you look at material on Topos theory by itself you will probably be quickly overwhelmed by the sea of weird category-theory terms and the lack of any immediate connection to application...) Topos
logic, on the other hand, is one particular application for which this mathematical construct is useful (although it may not always be called "topos logic" specifically). As far as I know logic is one of the main uses, if not the main use, of topos; but it is not guaranteed that material on topos will be particularly useful to understanding Topos logic.
Okay, so what's Topos logic and why do we care about it in the Physics context? Well, let's look at the place where Topos first shows up in Three Roads:
The mathematicians, it seems, were not aware that they were inventing the right form of logic for cosmology, so they called it other names. In its first forms it was called 'intuitionalistic logic'. More sophisticated versions which have been studied more recently are known collectively as 'topos theory'.
This, and the reference to topos in "Trouble with Physics", show up only very briefly and mostly consist of references to other people's work, so I am going to conclude Smolin himself is not very involved with Topos and he is just trying to call attention to work by Fotini, Isham etc. in this area which he considered important. But let's look for a moment at the thing that Smolin seems to consider important here about Topos: Its link to intuitionistic logic.
Intuitionistic logic is one of a series of nonstandard "formal logics" from the last century. When we are doing "formal logic" we say that is not enough to just write a proof that can be read by humans. Instead, we define a little symbolic "language", we define construction rules for creating sentences in this language, and we define rules for transforming sentences in that language into other sentences which are somehow equivalent. We then say that a logical statement is a sentence in the little language we've defined; and a "proof" is a series of transformations that transforms our premise sentence into our theorem sentence. The general idea is that a proof should be a completely mechanical thing, such that something like a computer could understand it and check its validity, with no room for human imagination or error.
It turns out that almost all of everyday mathematics, and almost any proof you can easily think to describe, actually reduces to "first-order logic", which is a formal logic of this sort. First order logic has symbols for things like "and" and "or" or "for every" or "there exists", and it has transformation rules that-- despite just being transformations on symbolic strings-- neatly encapsulate familiar logical principles like tautology or inference.
The interesting thing here is that you have other choices as to what to work with besides first order logic. You can create systems which are more expressive than first-order logic and contain first-order logic within them. You can also create systems where the rules are simply
different. One of these is intuitionistic logic, which is distinguished by the absence of the "law of the excluded middle". The law of the excluded middle is an axiom of logic so basic that usually one would not even think to think of it as an assumption:
If not true, then false. If you throw this assumption out, you can't do things like proof by contradiction-- you can prove something is "not false", but this does not prove that it is true!
So the idea here, as best I understand, is that when people started studying Topos-- a Topos is a special kind of Category-- they found that Topos work really well with intuitionistic logics. Basically Topos define a generalization of set theory ("Set", the category that encapsulates set theory,
is a Topos, in the same way that grade-school arithmetic is a group.) and there is some sense in which topos "go with" intuitionistic logic the same way sets "go with" first-order logic. A better way of putting it might be that each different Topos prescribes a collection of objects with certain behavior, and each of these collections give rise to a different formal logic. By default, these formal logics are intuitionistic, but depending on which Topos you pick you can get logics with all kinds of different interesting and unusual rules.
This second bit-- about having a free choice of Topos-- is why Topos turn out to be
really valuable to Isham&co who wrote that paper you link, because in doing quantum gravity they find themselves wanting to describe certain systems with unusual rules. Worse, they're not quite sure what rules it is they want. They
think, for example, that quantum physics needs to be described using the complex numbers, but maybe at some point they'll have to revise that. So what they do is decide that whatever rules they pick, they will demand those rules have some specific Topos which they spring from. They assert that if you just pick Set for your topos you get classical field theory (which is actually kind of cool, since it seems to reify the idea that classical field theory is the most fundamental thing and more modern concepts of physics are generalizations of that fundamental basis). They also have a specified Topos which they claim produces quantum physics; and they seem to be claiming that if you have a description of a physical system which anyone of these topos-based-theories acts on, you can just switch out one topos for another and compare directly how different theories would act on that single system.
One interesting thing is though that it looks like they are not promoting Topos as a practical tool but rather as a sort of foundation. It seems slightly unlikely that, were these Topos guys to have a breakthrough, you would actually wind up using the Topos directly in whatever theory that results; rather, someone would use Topos to define the axiomatic basis of the mathematical constructs that some theory uses, and then once the theory was defined everybody else would just learn to use the constructs that the Topos burped out. I think-- I could be wrong about this, maybe if you had a fully Topos-grounded theory then you'd be using Category-theoretic ideas directly to reason within the theory. But it seems like the main reason they are pushing Topos is as a tool for
initially defining physical theories-- for specifying them, giving them a rigorous basis, and comparing them to other theories. This is why there is such a high level of abstraction-- because creating abstractions is precisely their goal. Of course, initially defining things is exactly what is missing in Quantum Gravity right now!
On that note there is something about this Topos stuff which is important to keep in mind:
Careful said:
Therefore, starting by throwing away the queen of science - that is logic - does not appear very fruitful to me.
The thing to remember here is that *topos logic is still a kind of logic*, and any topos-derived logic is a valid formal logic. It may be in some way different from the logic you are intuitively used to, but this is okay. We created formal logic to
mimic what we might call "intuitive logic" (the name "intuitionistic logic" itself derives from a flamewar from the 1920s or so between Hilbert and some other people, over the question over whether it is more, or less intuitive to consider the law of the excluded middle a basic logic), but it can't be
precisely equivalent to intuitive logic-- and really, we don't
want them to be, since the entire point of formal logic in the first place was to
restrict logic in such a way as to exclude the ambiguities and errors of human thought. So as long as you stick to the formalism, exotic logical systems are as trustworthy as the ones you would normally be using in physics, because even exotic logics correspond to some rigorous mode of thinking. Topos-based logic is not about "throwing away" standard logic but about expanding and enriching the ways in which we
describe the logic we are using.
However, there is a cost here, and that is that
because here we have divorced "intuitive logic" from our mathematics you cannot quite rely on intuition the same way you normally might. This is the important thing to remember-- formal logics like the ones we get out of Topos are pure math, they are formalisms, and so you can only say you are using these logics if you're
actually doing the math. For example if you study a Topos-based logic you might be able to honestly say that truth values within the logic are in some meaningful sense "subjective" or "observer-dependent". For example in the quantum-alike topos Isham&co define in the second paper you can only extract notions of "true" or "false" by the use of a particular "truth object":
In the present paper, we use L(S) to study ‘truth objects’ in the topos. These are objects in the topos that play the role of states: a necessary development as the spectral presheaf has no global elements, and hence there are no microstates in the sense of classical physics. Truth objects therefore play a crucial role in our formalism.
There is a very clear sense in which 'truth objects' are analogous to observers; and since the truth values you extract will vary depending on the choice of truth object, we have just defined a mathematically rigorous system in which it is meaningfully the case that the truth of any given proposition is "subjective". However we have to remember that the word "subjective" here is really just a
metaphor for some more complicated mechanical rule of interpreting truth values out of sentences. The metaphors can be very useful but they can also deceive-- this is always a little bit the case in mathematical physics, I think, but it will be even more of a danger with topos, because anytime Categories crop up you have REALLY diven into the deep end of the abstraction pool. So I think it may be important if one is to work with Topos-based logics to try to always try to keep a clear link between how you're thinking about the problem versus what the formalism says, and not let the metaphors and "intuitive" language take over your thinking.
Again, don't know if this is any help or not. I may go back and try to read the Isham papers in more detail, my understanding of category theory is very poor but I do know something about logic/formal languages so maybe I actually have a chance at understanding this one. :)