Hm, that WP ludics page doesn’t seem to be all that helpful to me. It would be wonderful if someone here could distill the essence of ludics. (I don’t know either that I have the stomach to plow through 192 pages of Girard in Locus Solum.)

]]>I’ve not looked at Girard’s “Ludics”, but I wouldn’t mind having a Reader’s Digest version of it (what it’s about, main results, etc.). The word “ludics” suggests games (Latin *ludus* means “game”), and there is a long tradition in Linear Logic (broadly conceived, not necessarily classical MLL) of game semantics which has many incarnations, due variously to Conway, Joyal, Blass, Abramsky, Hyland, Ong, Jagadeesan, and there are a few others whom I’m shamefully forgetting. (Of course, things like Ehrenfeucht-Fraisse games play an important role in model theory as well, and games have long been used in set theory.)

A project that I had with Gerry Brady some time back was to develop a kind of game semantics based on the results of my thesis, and then somehow use this to address an old problem of Mac Lane, which is whether coherence problems (like the one for MILL or smc categories) could be decided in classical models like $Vect$. Soloviev has some positive results along such lines, but I think the area is ripe for further investigation, and I wondered whether some of this work of Girard (GoI or ludics) could be put to any use.

]]>~~The text ‘GoI, ludics,’ in the last paragraph seems to be a corruption, and I can't tell what it's supposed to be.~~

Never mind, GoI is geometry of interaction, and ludics I've heard of.

]]>I see, thanks for the quote!

]]>'Prawitz’s symmetry corresponds to negation (exchange left/right, hypothesis/conclusion), and really makes sense in a symmetric format like like linearlogic. In that case, negation is the format. In other terms, to negate A is not to refute it, but to recuse it... This remark is essential to vindicate one of the greatest philosophers, Hegel, and his contradictory foundations. From a fregean viewpoint, founding A on its negation is stupid, since A and ¬A cannot coexist by consistency! The fact is that GoI, ludics, rest upon contradictory foundations without the slightest problem.' ]]>

No, I just found it yesterday. I was going to begin listening driving in, but had a glitch. There’s a book from the lectures.

]]>Ah, thanks for the link! I wasn’t aware of that. Did you listen to it all?

]]>Anyone with 30 free hours can listen to Richard Dien Winfield’s Lecture Course in Hegel’s Science of Logic.

]]>Your Hegel-fu is clearly still better than mine, I would have to dig out the statements that you are alluding to, again.

But I’d think it should go like this:

In an ambient modal type theory (objective logic) we find axioms for physics (nature) and hence, in principle, for observers (mind). They speak in some language about what they observe (the subjective logic) and if they succeed they will recover the modal type theory as an object language in their metalanguage, hence then describe nature and finally themselves, which promotes them from observers to scientists.

Incidentally, Roger Penrose has been writing about this, too, in

- R. Penrose, Section 8.7. of “Shadows of the mind”, Oxford University Press, New York, 1994,

This is sometimes called Penrose’s maths-matter-mind-triangle, usually depicted as

$\array{ && Math \\ & \swarrow && \nwarrow \\ Matter && \longrightarrow && Mind } \,.$With Hegel I would label that equivalently

$\array{ && Logic \\ & {}^{\mathllap{objective\;logic}}\swarrow && \nwarrow^{\mathrlap{subjective\;logic}} \\ Nature && \longrightarrow && Mind }$or something like this.

]]>There’s something to your interpretation of Hegel’s objective/subjective distinction, but does it account for why ’Logic’ is just the first part of a three-fold division, followed by Nature and Mind?

Logic is the thought of the mind of God before creation.

Logic ends with a certain inadequacy of Geist, which require a created universe in which Logic can work itself out, right up to there being a part of the creation which is capable of understanding the Logic.

Even in the Logic itself, why does the third book, the subjective logic, divide into subjectivity (which does seem to concern itself with judgement and inference), objectivity (about mechanism, chemism and teleology) and the Idea (about life, cognition and the absolute idea)?

]]>Perhaps we might call the latter “that there is a path”.

Good point, I have changed it to “that there is a path” on p. 23. Thanks.

Regarding (-1)-truncation as the formalization of the step from “objective” to “subjective”: I see what you mean and I suppose that’s a general aspect of constructivism, that one regards as true only that which can be constructed and hence, to some extent, objectified.

But if you’d ask me which aspects of type theory would best serve as formal incarnation of Hegelian objective/subjective duality, then I would say:

Hegel’s “objective logic” corresponds to the

*object language*, hence the type theory itself (this is what we have been talking about at some length in fact, and it’s a happy coincidence of terms, too)Hegel’s “subjective logic” corresponds to the metalanguage, the ambient natural deduction system.

Because we have seen how that object language, hence the type theory itself, equipped with a sequence of modalities, reflects well the ontology of Hegel’s “objective logic”. But then the “subjective logic” is that which is used to reason about how we did this, and this is the metalanguage. Notice that Hegel’s use of “judgement” then nicely matches the use of judgement in the metatheory.

And isn’t Hegel’s superficially radiacal suggestion that these two aspects reflect on each other instead a familiar fact in formal logic, namely the fact that you may decide to take any metalanguage and formalize it as the object language of yet another metalanguage. There is a recent MO thread discussing just this kind of thing. The OP there mentions

Cori and Lascar’s book - for their excellent introduction concerning the vicious circle in what mathematical logic studies

and while I haven’t dug out that book yet, I suppose this “vicious circle” is effectively this objective/subjective duality.

I’d think.

]]>There something intriguing about $(-1)$-truncation. It’s easy to be taken from the objective to the subjective, e.g., from a space corresponding to a type to a type as proposition, as with the example in the paper here involving “the space of paths” and “there is a path”. Perhaps we might call the latter “that there is a path”.

]]>Thanks, Todd! That only goes to show my lack of education.

]]>The Zen/Chan saying takes many forms and is found all over the place, but one version is attributed to Ch’ing-yüan Wei-hsin (Seigen Ishin):

Before I had studied Zen for thirty years, I saw mountains as mountains, and waters as waters. When I arrived at a more intimate knowledge, I came to the point where I saw that mountains are not mountains, and waters are not waters. But now that I have got its very substance I am at rest. For it’s just that I see mountains once again as mountains, and waters once again as waters. Ascribed reference: Ch’uan Teng Lu, 22. (The Way of Zen)

I found it here.

]]>I would say these positions nicely reflect on each other rather than excluding each other.

For instance while it may seem that

Saying that quantum systems can be modelled in some kind of monoidal category seems far less radical.

under “computational trinitarianism” it is indeed equivalent! (That was the point which I tried to highlight so much in the entry quantum logic.)

So first there is a practical aspect, where we happen to find introducing certain structures useful for axiomatizing our applications. But after a while of using these axioms over and over, we may start to begin feeling more at home with the idea that rather than having found any random useful structure we are really changing the basic logic/type theory (to linear homotopy-type theory) and, while equivalent to what we have been doing all along, this may make us gain yet a different perspective and new insights.

I seem to recall the follow zen koan-like lines. Maybe I dreamed it up, because I cannot find the source anymore, but anyway I like it. It goes like this:

When you don’t understand, then a tree is a tree. When you are beginning to understand, a tree is no longer a try. After you have understood, a tree is again a tree.

It may take a long detour and in the end one comes back to where one once started. Of course what the lines don’t say explicitly but are supposed to make you feel the truth of is: there is non-trivial homotopy.

]]>So I guess there are degrees by which something being constituted as ’logic’ might affect the way we look at it. First, there’s the attempt to characterise a range of constructions in terms of axioms. Where this used to have a subjective aspect, axioms being evident fundamental truths, now axiomatisation is largely about defining interesting entities. So where once whether the parallel postulate was an evident truth was a key issue, whether to include a clause about a ring being unital or not is just a matter of defining entities for a task. The subjective element can disappear if I see myself as defining objectively good tools for a task.

Then there’s using a formalism which is similar to that used by logicians and computer scientists, who can thus bring their experience into play. But then a computer scientist doesn’t have to think about the subjective element, but rather a process on a machine.

A more radical position would hope that constituting something as logic would introduce philosophical issues, such as the concepts of judgement and truth. For example, when Jaynes develops probability theory as an extension of deductive logic, we’re to think of it as concerning inference in situations of incomplete knowledge. That similar considerations concern plausible inference and physics (up to maximum entropy and group invariance) brought into question how much of physical reasoning might be cast in terms of human inference, rather than representing the world straightforwardly. Perhaps you’ve seen Jorg Lemm’s Bayesian field theory or the work of Ariel Caticha.

That’s why quantum logic was viewed as such a radical proposal when it appeared. The very basis of our rationality was at stake in that the inference rules allowing the passage between propositions was being modified. Saying that quantum systems can be modelled in some kind of monoidal category seems far less radical.

]]>I’d like to know at some point is what might be gained by thinking about QFT from the logical corner

Oh, this I can tell you. (Then maybe I should also explain that better, or at all, in my notes.)

I am after getting a clear picture, and the connection to logic serves to make the extracted axioms become even more transparent by clearly showing what they mean abstractly, without any burden by concrete implementation

Concretely in the case at hand: I was always annoyed by how push-forward in twisted generalized cohomology seemed to be such a baroque process with some choice of embedding here, some Pontryagin-Thom isomorphism there, and then some twists sprinkled over it all for decoration. This was all the more an annoyance as it became clear that this process is at the very heart of what quantization is about.

I think to make progress with understanding the foundations of QFT, one needs to lift such mysteries and find a way to phrase these constructions as elegantly as possible, finding their minimum axiomatic essence.

Now in the course of Joost’s thesis his prop. 4.1.27 emerged, which i really enjoyed. What I am talking about re linear logic here is just pointing out that this prop. 4.1.27 in turn can be conceptually brushed-up even a bit more.

I find the logic-speak really helpful for this, in that it is conceptually so fundamental. We have “contexts” we have “sums” and so we can talk about summing up all terms in some context and identifying this with their product. That is the conceptual essence of what is going on in push-forward in twisted generalized cohomology. That this can be modeled by Pontryagin-Thom collapse maps in stable homotopy theory is then a matter of modelling it, but is not the fundamental reason why it exists in the first place.

And among all the many advantages such streamlining of foundations has, not the least is that I can now go and explain geometric quantization, Poisson holography etc. in just a few words to any mathematician with an understanding of some formal logic. He or she need know nothing about metaplectic corrections on symplectic manifolds, of Spin^c structures and index theory of Dirac operators, nothing of the huge machinery in which this is usually phrased. Because all this machinery comes down to just being a model for a few simple logical axioms. These I can go now and explain to formal logicians.

And maybe one day one is among them who goes and starts proving theorems about geometric quantization, Poisson holography etc.

Something similar happened a few years back when the meme that TQFT is axiomatized by cobordism representations became viral among pure mathematicians. Once the axioms have been cleanly isolated, suddenly a huge amount of previously unbelievable progress is possible.

]]>I remember you touched on that in the sigma-model exposition on second quantization, sigma-model – exposition of second quantization of sigma-models.

I guess what I’d like to know at some point is what might be gained by thinking about QFT from the logical corner of the triangle of computational trinitarianism. If there’s to be some benefit from formulation as linear homotopy type theory, one might expect that it would have something to do with the heritage of ’subjective’ logic, e.g., in judgements expressing one’s commitments to what kinds of things there are, cf. Willard Quine’s ’ontological commitment’ to kinds of thing in the range of an existential quantifier.

But let’s talk about this when you have some more time.

]]>Does linear homotopy type theory know anything about these subtleties of interpretation - first quantized worldvolume, second quantized spacetime, etc.?

I find it really hard to see what it would even mean for it to “know anything about these subtleties”. That seems to be the same subtle circular-ish “coordination” issue which we discussed above/elsewhere recently: suppose you manage to formalize any sort of QFT, then how would you see from just that formalism whether it’s a QFT that inhabits observers in its parameter space, or rather a QFT which spectrally sees observers in its target space. Or maybe both! I think that’s way too deep a question to say anything much about unless maybe in a style of a gnostic mysticism.

One aspect though that one probably can and certainly should try to make formal sense of is “second quantization” as such. Given any QFT defined as a cobordism representation, one should try to formalize what it means to form the S-matrix induced by using the correlators in this QFT to build a perturbation series, and what it means to find another QFT which is described by that S-matrix.

That seems to be a really subtle issue, too, but at least it seems to be a technical subtlety and not a deep mystical riddle.

We had once talked about this before. I have this vague hunch that it will work as follows:

a local TQFT is defined by a cocycle

$\mathbf{L} \;:\; Fields \longrightarrow \mathbf{B}^n \mathbb{G}_{conn}$After quantization this is supposed to give a morphism

$Z_{\mathbf{L}} \;:\; Bord_n \longrightarrow \mathcal{C} \,.$Now one can make some plausibility arguments to the extent that what second quantization is supposed to be is a way to regard $Z_{\mathbf{L}}$ again as a cocycle on par with the original $\mathbf{L}$ (an “$n$-directed cocycle”, now, remember that we talked about this once) and so that there should be a way to just repeat the original quantization step, but now taking $Z_{\mathbf{L}}$ as input where previously we took $\mathbf{L}$ as input.

I really feel like this will be the way it should work. But there is plenty of white space to be charted in making sense of what it would mean to generalize what we do to the cocycle $\mathbf{L}$ more generally to an “$n$-directed cocycle” $Z_{\mathbf{L}}$.

]]>Thanks very much for this!

Does linear homotopy type theory know anything about these subtleties of interpretation - first quantized worldvolume, second quantized spacetime, etc.?

]]>Prompted by discussion elsewhere, I thought it would be good to have some comments on the $n$Lab on what justifies to speak of “particles” in quantum field theory. So I started at *particle*

a section What is a particle?

a section Particles and non-particles in 3d TQFT

This can clearly be exapanded and and improved a good bit further. But maybe it’s a start.

]]>