Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

August 30, 2012

Urs Schreiber in The Reasoner

Posted by David Corfield

In December 2008, I interviewed Tom Leinster for Kent’s in-house journal – The Reasoner. The latest version, September 2012, sees me do the same to Urs.

I’m posting this here so that any regulars, or anyone who comes here via The Reasoner, can discuss whatever strikes them in what Urs says.

The abrupt transition in The Reasoner from interview to succeeding article had people last time imagining Tom had decided to talk about ‘The Paradox of Omniscience’. Likewise, you need to guard against thinking Urs goes on to talk of ‘Personal taste ascriptions and the Sententiality assumption’.

Something I’d like to develop is the idea that transformations in the past in the relationships between logic, mathematics and physics were brought about by, and led to, a rethinking of the concepts of language, observation, world, knowledge, God (once upon a time), etc. Think Newton and the Leibniz-Clarke correspondence, or the transformations of, say, 1880-1930.

Regarding the latter, to quote a small passage from an article I’m reading at the moment, Logic, Mathematical Science, and Twentieth Century Philosophy: Mark Wilson and the Analytic Tradition, Michael Friedman characterises the thinking of early analytic philosophers as follows:

Just as Cantor, Weierstrass, Dedekind, and Peano had finally uncovered the “true” logical forms of the concepts of infinity and continuity, Frege and his followers could now embark on an analogous project of uncovering the “true” logical forms of all the concepts found in the mathematical-physical sciences–including, especially, the radically new science of space, time, motion, and matter emerging in the context of Einstein’s general theory of relativity. The crucial point, as I have emphasized, is that what we call modern set theory was not conceived as simply the most general purely mathematical theory comprising all possible purely mathematical structures; it was rather conceived as part of the most general framework for logic itself, and it was this, above all, that made it an appropriate general platform, in turn, for all properly philosophical conceptual analysis.

Should there not be an ongoing comparable, explicitly philosophical conversation taking place right now? I hope this interview can spark off such a thing.

A couple of possible starting points:

1) Is there anything in Per Martin-Löf’s philosophical background, perhaps his reading of Husserl and Frege, that gives rise to his type theory being taken up homotopy theoretically, in particular his constructive approach to identity judgements?

2) We can follow a line of thought which notes that physicists have been interested in certain kinds of theory, so that we ought in turn to be interested by a framework that’s able to capture important aspects of those theories. Cohesive homotopy type theory is such a framework. But is there not a way to run things in the other direction? Any interesting universe involves a dynamics. Dynamics must be encoded via a notion of the cohesion of adjacent elements of space. Cohesion is best encoded by the concept of a cohesive ∞\infty-topos. Most suitably structured examples of cohesive ∞\infty-toposes relate to smooth forms of cohesion. We could then be led to think that some parts of the form of current physics can be explained. What, though, if radically different kinds of cohesion were found?

Posted at August 30, 2012 3:05 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2551



33 Comments & 0 Trackbacks

Re: Urs Schreiber in The Reasoner

Thanks, David.

You write:

Is there anything in Per Martin-Löf’s philosophical background, perhaps his reading of Husserl and Frege, that gives rise to his type theory being taken up homotopy theoretically, in particular his constructive approach to identity judgements?

The way I have heard the story it’s rather the opposite, and in a quite interesting way:

apparently Martin-Löf had first made public a version of his type theory that had an extra axiom forcing identity types to have unique terms. Apparently within days, if I remember correctly, a colleague of his pointed out that including this axiom ruins one of the most precious properties of type theory: it makes “type checking undecidable”. Accordingly that axiom was dropped, and there was an uncertainly left ever since as to what to make of the resulting intensional type theory, which was so very beautiful, but in which one could’t prove that there is a unique way in which two terms are equal.

It was not before the beginning of our millenium that suddenly people realized that this apparent bug was a major feature. Not imposing this extra axiom makes the theory be homotopy type theory.

This is where much of this feeling of excitement comes from: if one just follows the spirit of the purest formal logic available, then the result is automatically and naturally homotopy theoretic. One has to go against the grain to force it not to be. In a way it is maybe more fortunate than unfortunate that Martin-Löf did not anticipate this. It makes all the more forceful the lesson to be learnd here.

We can follow a line of thought which notes that physicists have been interested in certain kinds of theory, so that we ought in turn to be interested by a framework that’s able to capture important aspects of those theories. Cohesive homotopy type theory is such a framework.

A propos: unfortunately the interview went to “print” shortly before Mike and myself wrote that little piece:

for QPL 2012. This explains in a bit more detail various of the issues that we are alluding to in the interview.

What, though, if radically different kinds of cohesion were found?

Yes, indeed. There are a few interesting issues to be explored. I have now two new students starting, or about to start, working on geometric quantizaton in cohesive homotopy type theory. Maybe there is a student out there fancying a thesis that aims to further explore the space of models of cohesion? Would be quite worthwhile. I have some ideas, but don’t have the time to work them all out myself.

Posted by: Urs Schreiber on August 31, 2012 12:21 AM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

I believe the story you are refering to is
Girard pointing out the inconsistency in the impredicative system.

Posted by: Bas Spitters on August 31, 2012 8:42 AM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

But later on that page it talks about the extensional/intensional issue.

Posted by: David Corfield on August 31, 2012 9:09 AM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

I believe the story you are refering to is Girard pointing out the inconsistency in the impredicative system.

Maybe I am incorrectly pairing the story with its mathematical content:

so what I was describing above is, as David says, that extensional identity types make type checking undecidable. The nnLab has a note on this here. While this deserves to be expanded, at least it cites sources, such as Martin Hofmann’s Phd thesis, which summarizes in the abstract:

In extensional type theory the propositional equality induced by the identity types is identified with definitional equality, i.e. conversion. This renders type-checking and well-formedness of propositions undecidable and leads to non-termination in the presence of universes. In intensional type theory propositional equality is coarser than definitional equality, the latter being confined to definitional expansion and normalisation. Then type-checking and well-formedness are decidable, and this variant is therefore adopted by most implementations.

But apparently I am wrong in thinking that this is something that was pointed out to Per Martin-Löf by somebody else? If so, sorry for the confusion. (I am pretty sure sombody once told me so over a coffee, but I should have checked the facts.)

But then I also would like to know the answer to David’s question 1) in the above entry! :-)

Posted by: Urs Schreiber on August 31, 2012 9:39 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

I wrote my masters thesis back in 1992 on how category theory made sense of the two kinds of interpretation of constructive logic – proof theoretic (Martin-Löf, Dummett) and topological. Dummett had promoted the thesis that the proof-theoretic one was the ‘correct’ interpretation of distinctly philosophical notions. I was happy to think that the unification provided by toposes and LCCCs suggested that logic be seen rather as a facet of mathematics, no more specifically philosophical than the spatial facet. Logic would find its most important applications in computer science.

I had reached that position on logic from Lambek & Scott, and from reading Albert Lautman, while in Paris the year before.

But, with Dummett, one might think that, given that something important was found by Martin-Löf after years of thinking hard about Brentano, Frege, Husserl and Brouwer, as you can see from these lectures, it would pay us to continue thinking about ‘acts of judging’, ‘acts of knowing’, ‘evident’ judgment, and so on.

On the other hand, we might imagine that whatever useful there was to be found has already been mined and integrated into homotopy type theory.

Now, if we spoke Swedish, we could listen to Martin-Löf on Husserl (parts 1 and 2).

Posted by: David Corfield on August 31, 2012 9:03 AM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

I was happy to think that the unification provided by toposes and LCCCs suggested that logic be seen rather as a facet of mathematics, no more specifically philosophical than the spatial facet.

But is there maybe a case to be made that the “outermost” ambient context is more naturally regarded as logic? For a universe which we view exclusively form its “inside” the internal logic seems to be the most efficient reflection.

In this context, maybe here is the right context to mention the following question, to be handled with due care:

Is the analogy that motivated the coinage of the term universe (in mathematics) from universe (in physics) deeper than originally intended? Is it relevant that with this term the central conceptual issue for quantum cosmology is the same as that of type theory (compare e.g. Mike’s discussion here): how to grasp structures in the universe entirely internally, without the external perspective available?

But, with Dummett, one might think that, given that something important was found by Martin-Löf after years of thinking hard about Brentano, Frege, Husserl and Brouwer, as you can see from these lectures, it would pay us to continue thinking about ‘acts of judging’, ‘acts of knowing’, ‘evident’ judgment, and so on.

By the way, I find reading these lectures a curious experience. With the hindsight that I have by now I do enjoy reading them. But I believe I would have had trouble to see the wood for the trees, had I been exposed to this verbose prose before knowing about either its categorical semantics or else its fully formal version (maybe some day we’ll expand the nnLab discussion of syntax of type theory to a more comprehensive exposition), where it is clear that I may ignore all that rather lengthy philosophy behind the words “judgement” and “proposition” etc. and just concentrate on what the symbol manipulation rules are.

I find it remarkable that these insights with their, as we are discussing here, remarkable and concrete mathematical impact, have indeed been derived from, as you say:

years of thinking hard about Brentano, Frege, Husserl and Brouwer

Posted by: Urs Schreiber on September 2, 2012 10:49 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

I see you wrote about the internal/external issue in physics at quantum cosmology

the very formulations of quantum mechanics/quantum field theory available all require, more or less explicitly and to lesser or greater extent, an external classical observer to make sense of the predictions of the theory.

Do you mean predictions involve recordings of quantities on instruments, and these instruments are large devices which through coupling produce decoherence in the quantum systems being studied?

I see we could do with expanding the quantum mechanics side of things at nLab. Nothing yet on decoherence or consistent histories.

Posted by: David Corfield on September 3, 2012 9:31 AM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

…it is clear that I may ignore all that rather lengthy philosophy behind the words “judgement” and “proposition” etc. and just concentrate on what the symbol manipulation rules are.

That raises the question of what to make of the line of thought represented in the proof-theoretic semantics of constructive logic. It was there from the first in Brouwer that we must talk in terms of a knowing subject. By the time we’ve extracted some rules of manipulation, and found that, in the case of identity, there’s a homotopic interpretation, have we left the knowing subject behind? Or all that work on Kripke frames and stages of the ideal knower in Dummett’s Elements of Intuitionism. Can’t we just talk in terms of sheaves over posets?

Even if we retain the proof-theoretic account in the context of computer science, with propositions as types or proofs as programs, hasn’t the knowing subject disappeared, rather like the way few (no-one?) follows Wigner’s reliance on consciousness in quantum mechanics.

Posted by: David Corfield on September 3, 2012 5:04 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

Even if we restrict ourselves strictly to simple types, there’s no known way to systematically give categorical semantics to type theories produced via the judgmental methodology. Going between type theories and their categorical semantics seems to require considerable insight, on a case-by-case basis. Until we can do that, I don’t think it’s reasonable to think that the mathematical potential of Martin-Lof’s ideas has been exhausted.

I recall Urs has complained that type theory is not like group theory, in that there is no axiomatic description of a type in the same way that the group axioms say what a group must be. I half-suspect/half-wonder if there is some connection….

Posted by: Neel Krishnaswami on September 4, 2012 10:58 AM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

If I recall correctly, Voevodsky has proposed to define “a type theory” to be any extension of the essentially algebraic theory of contextual categories. I don’t say I think that would be a good idea, but such a definition would at least more or less automatically carry with it some categorical semantics.

Posted by: Mike Shulman on September 6, 2012 3:08 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

Three questions:

(1) What are contextual categories? It doesn’t sound like he means the the Blute, Cockett, Seelyb definition.
(2) What is their essentially algebraic theory? (I’m especially interested in this.)
(3) What’s an extension of an essentially algebraic theory?

Posted by: Neel Krishnaswami on September 7, 2012 2:29 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

  1. No, he means Cartmell’s definition. I’m surprised that Blute-Cockett-Seely chose to re-use that term. Cartmell’s paper appears in their bibliography, but I haven’t been able to find where in the paper they mention it (if anywhere).

  2. I suppose you know what an essentially algebraic theory means in general? The notion of contextual category can be formulated as a two-sorted essentially algebraic theory, by starting with the two-sorted theory of a category (objects and arrows being the sorts, source and target and identities and composition being the operations, with composition partially defined), adding a specified “empty context” object, and a partial operation on contexts (defined on all nonempty contexts) which assigns to each context Δ\Delta the context Γ\Gamma such that Δ=Γ.A\Delta = \Gamma.A. One also needs a few operations which together assign chosen associative pullback squares, and perhaps some other stuff I’m forgetting.

  3. In this context, I think “extension” just means “adding more (partially defined) operations satisfying axioms”. These operations would correspond to type formers and their introduction and elimination rules.

Personally, I think there’s something about a type theory which this idea doesn’t capture, such as its “computational” content. I feel like there are also hard-to-define-precisely constraints on what sort of type formation rules are really allowed. (I don’t know whether Voevodsky still advocates it, either — it was a couple years ago that I heard him say this.) But it’s an interesting point of view, and might be helpful when starting to explain type theory to a mathematician.

Posted by: Mike Shulman on September 7, 2012 7:16 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

I recall Urs has complained that type theory is not like group theory, in that there is no axiomatic description of a type in the same way that the group axioms say what a group must be.

Right, that was when I was trying to understand what type theory is and found it frustratingly mysterious for a while.

Now I find it delightingly self-evident and am no longer complaining. One shouldn’t really compare “type theory” with “group theory” so much. Type theory is the context, in there we want to formulate group theory. And everything else. At least Arche-type theory is ;-)

Posted by: Urs Schreiber on September 7, 2012 1:47 AM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

that was when I was trying to understand what type theory is and found it frustratingly mysterious for a while. Now I find it delightingly self-evident and am no longer complaining.

That sounds kind of like my experience learning type theory. I wish there were a way to make the learning curve easier.

Posted by: Mike Shulman on September 7, 2012 2:48 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

the very formulations of quantum mechanics/quantum field theory available all require, more or less explicitly and to lesser or greater extent, an external classical observer to make sense of the predictions of the theory.

Do you mean predictions involve recordings of quantities on instruments, and these instruments are large devices which through coupling produce decoherence in the quantum systems being studied?

I think I mean something more fundamental.

To say what I mean, let me invoke a formal description of quantum field theory, so that we have a chance of seeing more clearly, conceptually.

So I use FQFT: we formalize our nn-dimensional quantum field theory as a suitably monoidal nn-functor Z:Bord n S→nVect ℂZ : Bord_n^{S} \to n Vect_{\mathbb{C}}: what ZZ assigns to closed (n−1)(n-1)-manifold Σ n−1\Sigma_{n-1} is interpreted as the space of states of all quantum fields on Σ n−1\Sigma_{n-1} and to an nn-dimensional manifold Σ n\Sigma_n with boundary it assigns a correlator: Z(Σ n−1)→ℂZ(\Sigma_{n-1}) \to \mathbb{C}, to be thought of as assigning to every state the probability amplitude that this this state undergoes a reaction as specified by the shape of Σ n\Sigma_n.

In those cases where such nn-functors ZZ haven been matched to experiment, we look at them from the outside, as follows:

for instance when we do an experiment at LHC and compare with theory, we take ZZ above to be a 4-functor on a category of cobordisms in Minkowski space ℝ 3,1\mathbb{R}^{3,1} which is to be thought of as a neighbourhood of the accelerator ring. 4-morphism in there is not the shape of the whole universe, but just an approximation to the state of the universe around that accelerator ring. We inject some protons on one side of the accelerator and measure the correlator of the process of them propagating through and emerging in some other state at the other end. In other words, we compute some “2-point function”, Z(Σ 3×[0,1])Z(\Sigma_3 \times [0,1]). Taking the norm square of the elements of this linear map gives the probability that a certain outcome is actually measured at the LHC, and the remarkable truth is that we know a ZZ which actually reproduces the probabilities measured at LHC to high accuracy.

This is the succes story of quantum field theory as a theory of localized processes, and be they localized over kilometers.

But now let’s try to apply this kind of story to the whole universe: Even though it is not entirely clear if the full theory of quantum gravity+other forces that describes the world which we perceive is a field theory of this sort (it might be a string field theory instead, or something more similar to that than to known QFT), let’s assume now for the sake of the argument that this exists: let’s assume we have found such a 4-functor (or 10-functor ;-) ZZ which is the final model, the “theory of everything”, as physicists say. Just for the sake of argument, I just want to point out where the external/internal issue appears in this hypothetical situation.

So what then? Now a 4-cobordism Σ 4\Sigma_4 is to be interpreted as an interaction process undergone by the whole universe. We get some numbers out of this, But what does this mean? This is entirely unclear. This is the conceptual problem of quantum cosmology.

Maybe to make this more vivid, I should put it like this: Let’s consider a familiar 3-functor Z:Bord 3→3VectZ : Bord_3 \to 3 Vect, that is given by Chern-Simons theory. So it’s some topological 3d QFT. This is certainly not the “theory of everything” of the physical universe which we observe. But we could ask: since it is similar conceptually to the hypothetical such ZZ which does describe our universe: can we say what an inhabitant of the Chern-Simons 3-d universe experiences? Suppose there is some kind of observer in the hypothetical 3-dimensional world whose “theory of everything” is quantum Chern-Simons theory. What will that internal observer observe, what kind of wolrd will he experience? What is Chern-Simons theory viewed from the inside?

And the answer is: we have no idea at all. The functor ZZ gives us a way to look at this 3d universe form the outside, just as we look at a bunch of protons in the LCH accelerator ring. But we don’t even know how to ask what that 3d universe looks like for one of its inhabitants.

Of course people have tried to come to grips with this. Notably the idea of Bohr toposes is that these would provide a way to formalize what it means to observe a quantum system “from the inside”. This is the question that Chris Isham and Andreas Döring call their “secondary motivation” on the first page of their arXiv:quant-ph/0703060. But despite these attempts, the “quantum cosmology internal/external problem” remains a problem. At least with Joost Nuiten’s work there is now something on Bohr toposes for actual quantum field theories, not just quantum mechanics (which is wildly insufficient for the topic of quantum cosmology).

Posted by: Urs Schreiber on September 4, 2012 11:15 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

After writing that above, I was looking about for something category theoretic on consistent histories and found Chris Isham’s paper. That got me wondering if the Bohrification project was relevant to what you were saying.

But we don’t even know how to ask what that 3d universe looks like for one of its inhabitants.

Won’t the 2d creature living in the 3d universe do like us (if 2d is enough to be able to think)? Won’t they bracket off pieces of their universe and make observations, do experiments, make predictions, etc.?

I don’t see why this is harder than our relating what the universe looks like to us to our best theory.

I can see there’s an interesting issue when we take the universe as a whole, and we, and our experiments, are just part of that 4d thing.

What is the boundary of the cobordism that is our universe supposed to be? From the empty manifold to some infinitely future, infinitely expanded space?

Posted by: David Corfield on September 5, 2012 11:10 AM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

I can see there’s an interesting issue when we take the universe as a whole, and we, and our experiments, are just part of that 4d thing.

Yes, that is the issue.

I keep trying to think about a way to say it more formally, as to be more useful. But I can’t right now. And probably not for a while. But who knows, maybe there can be progress now.

What is the boundary of the cobordism that is our universe supposed to be? From the empty manifold to some infinitely future, infinitely expanded space?

That’s part of the problem that I mentioned: the very formalization of QFT as cobordism representation is an abstraction of the nature of scattering experiments: you prepare an initial state, let it evolve, interact and scatter, and check what comes out. It is not really clear what to make of that if you yourself are part of what is scattering.

Posted by: Urs Schreiber on September 7, 2012 1:39 AM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

I’m not sure I see precisely what the problem is. Presumably it’s something like that it would be wrong to take the universe as one large scattering experiment, where nothing comes in and some heat death state comes out. But why? Because the very idea of ‘comes in’ and ‘comes out’ is wrong? Is it that the application of QFT is dependent on some macroscopic device capable of measurement?

I take it this isn’t just a worry about reductionism: it’s all very well to think your QFT’s doing well when it accounts for the statistics of scattering in lots of very carefully prepared experiments, where all manner of means are used to screen that patch of the universe from external influences, and where the initial and final states can be characterised very simply in the physical theory. But we shouldn’t expect QFT to help us predict what will result when two businessmen are introduced into a room to make a deal.

If it were just this, couldn’t we take time slices either side of the presence of complex structures in the universe? But your point at quantum cosmology is that

the very formulations of quantum mechanics/quantum field theory available all require, more or less explicitly and to lesser or greater extent, an external classical observer to make sense of the predictions of the theory. This makes sense, in principle, for every subsystem of the observable universe. But a comprehensive theory of “quantum cosmology” would seem to need a notion of observables of quantum phenomena by “quantum observers” internal to the quantum system which they observe, instead of by “classical observers” external to that quantum system.

So it’s not just an issue of the initial state, but any attempt to take a time slice.

How do you characterise, say, our observation of the cosmic background radiation? It’s surely not just about the patch of the universe in the vicinity of our detectors.

Posted by: David Corfield on September 7, 2012 11:01 AM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

I’m not sure I see precisely what the problem is.

Good that you are further pushing this question.

Just a few years back there was a conference at the Perimeter Institute where one of the leaders of a certain proposal for how to do non-perturbative quantum gravity gave a talk, the slides are (or were) available online. The topic of the talk was (in my paraphrase): “In this room we all agree that we have succeded in constructing a theory of non-perturbative quantum gravity. Unfortunately, our colleagues don’t believe us. How can we convice them?”

Let’ do this as a thought experiment here: suppose I hand you a functor ZZ from 4d cobordisms: for each smooth closed 3d manifold I give you a vector space, for each 4d cobordism a linear map. Nothing else. Suppose I claim: this is the quantum field theory of gravity and the other forces that describes our observable world. The theory of everything, as they call it.

Your task now is: check this claim. Come up with a scheme to extract information from that functor that allows you to deduce experimental information. Anything.

How would you even deduce what the broad-stroke properties of the universes are, that are described by this functor? How many fundamental forces do its inhabitants observe (on average, if you wish)? Is gravity even one of those forces? Are there nuclear, electric forces? What is their gauge group?

I don’t know how to deduce this. But suppose you can figure this out, suppose you can check that indeed the functor that I handed you describes a world with gravity and unitary Yang-Mills forces. So now here is a smooth 3-manifold Σ 3\Sigma_3, and here is a vector ψ∈Z(Σ 3)\psi \in Z(\Sigma_3). Let’s ask some questions: “What is the average energy density of the universe in state ψ\psi? What is the mean curvature of space? What is the vacuum expactation value of the Higgs field, if any?” And so forth.

Above in your comments I think you were assuming that you know what an incoming state is, observationally. Say that it has an amplitude concentrated on a “heat death”-configuration of the universe. But how do you actually know this? From just ψ∈Z(Σ 3)\psi \in Z(\Sigma_3) and functoriality of ZZ?

To answer these question, you have nothing but this vector and the information of how it transforms as you choose 4d cobordisms with Σ 3\Sigma_3 one of their boundary components. You need to device a clever boot-strap self-consistency-check kind of way to deduce from from these transformations what’s going on.

It’s like deciphering an alien script with no no context information whatsoever. All you have is the signs on the wall. You need to read a universe into them. How?

Posted by: Urs Schreiber on September 7, 2012 10:06 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

I’m feeling completely out of my depth here, but anyway.

After your last comment I’m left wondering how any physics gets done at all. Back here, you made it sound straightforward to relate QFTs as functors to what’s going on in the LHC. I think I’d have to understand that better since it seems quite miraculous to me already, before I come to see the further problems of making physics work for the whole universe.

Does one imagine there are a quadrillion or so copies of the ‘same’ cobordism, which is a space-time region neighbouring a collision, or as you had it, the accelerator ring?

Posted by: David Corfield on September 10, 2012 9:53 AM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

After your last comment I’m left wondering how any physics gets done at all.

Yes, good, and that’s what I am trying to get across: for ordinary phyics, not quantum cosmology, there are maps that provide the data which I pointed out in the above example are missing. These physical theories of phenomena in an accelerator come with identifications of what it means to “prepare a state” using macroscopic parts of the experiment, so that you do know what some vector in Z(Σ 3)Z(\Sigma_3) means.

It is this extra information to an external observer who is not itself part of the quantum system wich is needed to make sense of any formalization of quantum physics. But this is also exactly what is missing when one considers quantum cosmology.

This is an old, old issue that our ancestors at the beginning of the 20th century fought with. For instance the reason why Bohr toposes are called this way is that they are meant to formalize a perspective on this problem that Niels Bohr used to amplify, see at

  • Erhard Scheibe, The logical analysis of quantum mechanics . Oxford: Pergamon Press, 1973.

if you can get hold of it. He said something like “However weird quantum mechanics seems, it must be possible that we go and make classical observations about quantum system, that yield clear classical information which we can tell go and tell our friend about.”

On the one hand this is good, as it gives a means to handle the relation between the macroscopic classical world and the quantum system. On the other hand it is bad, because it seems to restrict attention to a formalism that cannot describe a system without outside observer, such as quantum cosmology.

Posted by: Urs Schreiber on September 11, 2012 6:21 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

Any interesting universe involves a dynamics. Dynamics must be encoded via a notion of the cohesion of adjacent elements of space.

The second sentence in the quote presupposes that any dynamics involves continuous time, or, at least, continuous transformations, doesn’t it?

Posted by: Eugene on August 31, 2012 3:00 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

Well, there’s the intriguing prospect that there may be more kinds of cohesion than one might suspect. See, e.g., this conversation and again here about analytic spaces.

Then again, I find intriguing how the reals tend to pop up unannounced. I wonder if there’s an explanation of this via some variant of the cobordism hypothesis. You require in your physics a certain kind of symmetric monoidal nn-category with duals, then you should expect the free such one on one object to appear.

Posted by: David Corfield on August 31, 2012 3:17 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

Any interesting universe involves a dynamics. Dynamics must be encoded via a notion of the cohesion of adjacent elements of space.

The second sentence in the quote presupposes that any dynamics involves continuous time, or, at least, continuous transformations, doesn’t it?

In fact it does not! There is “discrete cohesion” in that there are models whose intrinsic notion of path involves discrete steps.

Notably the topos of simplicial sets is a cohesive 1-topos (spelled out here), and an ∞\infty-topos of simplicial object in another ∞\infty-topos H\mathbf{H} is a cohesive ∞\infty-topos over H\mathbf{H}.

In these models of cohesion, the intrinsic notion of path is: edge in a simplicial set/object. This is “discrete” in the sense that I believe you are thinking of.

And nevertheless, of course, the cohesive homotopy type theory sees this discrete model as being just as continuous as all the other models.

Mike Shulman just recently observed that such a cohesive ∞\infty-topos of simplicial objects may be the right context for formulating directed homotopy type theory, see his post here: in this interpretation the “intrinsic discrete step paths” are the morphisms in an internal ∞\infty-category.

This needs to be further fleshed out. It is interesting how geometric cohesion and categorical directedness appear on the same footing from the point of cohesive homotopy type theory (assuming, of course, that what Mike suggests there can be carried through to the end, which still needs to be done).

Posted by: Urs Schreiber on August 31, 2012 9:50 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

I see. I was confused by ”adjacent.” So here “adjacent” means connected by a path and a path is a 1-dim simplex.
Posted by: Eugene on August 31, 2012 10:41 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

So here “adjacent” means connected by a path and a path is a 1-dim simplex.

Yes, that’s right. Maybe a simpler analog and special case of this “discrete cohesion” (in one sense of “discrete”, not in another) that you might want to think of is that of finite topological spaces. As long as these are locally contractible, such as the pseudocircle, they are cohesive (see at locally contractible infinity-groupoid). But clearly all “paths” in them proceed in discrete steps, in some sense (not in another).

By the way: following public demand on the nnForum, we started an nnLab page motivation for cohesion which is supposed to collect non-technical but illuminating discussion. I should maybe add a paragraph in reply to your question there. But not tonight.

Posted by: Urs Schreiber on September 4, 2012 11:34 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

Do you have a sense of how this notion of a path is related to the notion of a path in Bisimulation from Open Maps ?
For Joyal, Nielsen, Winskel “a path represents a computation or history of a process.” What do your paths represent for you? Why a single 1-simplex?

Posted by: Eugene on September 5, 2012 3:21 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

Do you have a sense of how this notion of a path is related to the notion of a path in Bisimulation from Open Maps ?

I’d have to look at that in more detail but one thing I can say right away is that the notion of open maps used in that article is closely related to cohesion.

Just these days a student of mine is defending his thesis on this question: if we refine cohesion to infinitesimal cohesion then the infinitesimally cohesive homotopy type theory has a notion of formally étale maps. These are open maps in the sense of Joyal-Moerdijk (with some technical fine-print).

Intuitively, what happens is that in infinitesimally cohesive homotopy type theory there is not just an intrinsic notinon of path, but of infinitesimal path (its an axiomatization of D-geometry) and this provides at least part of what Lurie would call a geometry, which involves a notion of open maps (“admissible morphisms”).

For Joyal, Nielsen, Winskel “a path represents a computation or history of a process.” What do your paths represent for you?

The intrinsic paths of cohesive homotopy type theory subsume and generalize the traditional notion of paths and higher paths that form fundamental infinity-groupoids. Specifically for cohesion modeled on smooth manifolds one can prove that the intrinsic notion of path is precisely that of smooth function out of ℝ 1\mathbb{R}^1: smooth cohesion is “ℝ 1\mathbb{R}^1-homotopy theory” in the sense of A1-homotopy theory: here the functor Π\Pi is precisely “ℝ 1\mathbb{R}^1-homotopy localization”.

So the notion of path in cohesive homotopy theory subsumes the traditional notion of paths in geometry. Of trajectories, if you wish. (It subsumes also a bit more, though.)

Of course this can be re-interpreted in terms of computation, if desired – by computational trinitarianism, to use a fun term that I just picked up from Robert Harper.

Why a single 1-simplex?

That’s in the specific model provided by ∞\infty-toposes of simplicial objects. Whereas the intrinsic path in cohesion modeled on SmoothManifoldsSmoothManifolds is an ℝ 1\mathbb{R}^1-homotopy, so the intrinsic path in cohesion modeled on the simplec category Δ\Delta is a 1-simplex. In other models it is yet something else.

Posted by: Urs Schreiber on September 7, 2012 1:16 AM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

I really enjoyed reading the interview. I think it is a great service to stop and discuss these things simply and heuristically once in a while for a more general audience.

Cohesion seems like something I’d like to try to understand and I look forward to seeing what this will mean for directed homotopy type theory.

Fun stuff!

Posted by: Eric on September 1, 2012 1:31 PM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

This is great. Even though I was involved in a lot of what you’re talking about here, it’s sometimes easy to miss the forest for the trees when I’m focused on just doing some mathematics. Working on the joint paper that Urs mentioned, and reading this interview, has been great for me to get a sense for what you/we are actually trying to accomplish here. (And it is audacious! So much so that I slightly hesitate to see my name associated with it.)

Posted by: Mike Shulman on September 4, 2012 5:28 AM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

Thanks, Mike. I can return the favor: I consider myself rather lucky to be in contact with you on these matters. I have just posted something to this effect on G+, too. :-)

Concering your slight hesitation: To me, one nice aspect of having a genuine formalization of aspects of physics is that it has precisely this synergy effect: suddenly mathematicians can just grab the axioms, ignore all those fairy tales told in physics, and start to work. On physics.

One sees this more and more on conferences in the last years, ever since the formalization of quantum field theory via cobordism representations (FQFT) had matured enough to be practically interesting in some areas. Some notable examples of this synergy effect are collected in our book. It is probably no secret that some of the mathematician authors there have little traditional physics education. Nevertheless, by the force of the axiomatics, they can now go where no physicist has gone before.

Posted by: Urs Schreiber on September 5, 2012 12:28 AM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

I appreciated the discussion of statics and dynamics, which I think is a promising intuition.

I’m going to get a bit hand-wavy and speculative, but I guess that’s allowed here, within bounds. Leave aside the physics element for the moment, and just consider a computer program. CH gives us propositions as types, programs as proofs. Statics, dynamics. The dynamics of the proof process itself arguably capture the “computing” character of a computation. Normalization, evaluation, reduction, denotation… all almost the same. But what happens when we move to a dependently typed calculus, or even just start to blur the edges of proofs and propositions more gently? You lose the phase distinction between typechecking and execution. Everything starts to bleed into everything else, and everything happens at once, so to speak. Proofs and propositions become interchangeable depending on your point of view, cats lie with dogs, etc.

Actually this isn’t really true. We can apply CH locally just fine. But I do think it becomes harder to give a uniform, global interpretation of an arbitrary program.

And I think this does make it difficult to ask what the “dynamics” of a proof are, since asking what it proves is equivalent to simply running it to completion.

My sense, and this is just a hunch, is that introducing homotopy paths gives us a way to recover talking about transformation-as-such instead of accidentally interpreting it away via typechecking/evaluation.

In this rough intuition, Homotopy Types : Intuitionistic Type Theory :: Plain Old Types : Plain Old Programs, in that they let us take something thought of as intrinsic and innate in terms and recast it as something extrinsic and structuring terms. This is shades of Church vs. Curry style, except I am using the words intrinsic and extrinsic almost exactly opposite how they are typically used.

Posted by: Gershom B on September 5, 2012 4:58 AM | Permalink | Reply to this

Re: Urs Schreiber in The Reasoner

I appreciated the discussion of statics and dynamics, which I think is a promising intuition.

[…]

propositions as types, programs as proofs. Statics, dynamics.

I would just like to warn that there is a level skip involved in going from the statics/dynamics in the sense of cohesion to that in the sense of types/programs: in the latter case the paths are in the ambient category, in the former they are in the objects.

Write H\mathbf{H} for the ambient catgeory, the thing whose objects are our types and whose slices are our contexts. Then a proof of a proposition Φ\Phi is “dynamics in H\mathbf{H}”, namely a morphism *→Φ* \to \Phi in some slice of H\mathbf{H}. A path to Φ\Phi

But if H\mathbf{H} is cohesive, then there is another notion of paths: there are then also paths in Φ\Phi.

So there is a level difference. A differernce of universes:

in cohesive homotopy type theory we may form the type ΠΦ\Pi \Phi of paths in Φ\Phi. Now suppose that Mike succeeds with his project of directed homotopy type theory. Then we can regard ΠΦ\Pi \Phi as an internal category type, a category, internal to H\mathbf{H}.

Once we have this, we can of course climb inside that new internal universe, presumeable, and consider the internal type theory of Π(Φ)\Pi(\Phi). In there then, yes, what used to be paths in Φ\Phi now give rise to programs and proofs of propositions.

Posted by: Urs Schreiber on September 7, 2012 1:33 AM | Permalink | Reply to this

Post a New Comment