Re my Peirce comment in #47, slides like 191 of Dan Licata’s HiM talk are suggestive.

]]>Yeah, I don’t really like the term “adjoint logic” either.

]]>With the development from unary (the adjoint logic of #1) to simple to the hotly anticipated dependent type 2-theories, what’s a good way to organise this material for nLab purposes? Is there any future for the term ’adjoint logic’ (something of a pleonasm if we follow Lawvere, “we may more precisely identify logic with this scheme of interlocking adjoints”)?

So the 2-category of modes for a temporal logic we developed above in this discussion can be formulated as a superposed pair of walking adjunctions, generating cross-pair monads (#8).

If one were to look to depict a type 2-theory diagrammatically, I guess you’d have a sheet for each mode, on which the types associated with the mode can be written. In the unary case, we could have the adjoint functors transferring types between sheets.

One of these days, we’ll find that Peirce was ahead of his time again, with his tinctured gamma graphs: “the tinctures enable Peirce to distinguish between different modes of modalities” (Peirce’s Search for a Graphical Modal Logic, p. 159)

]]>Here’s a recent paper.

Temporal Type Theory: A topos-theoretic approach to systems and behavior Patrick Schultz, David I. Spivak https://arxiv.org/abs/1710.10258

It is an application of Sh(Int) to hybrid systems. Int is the interval domain.

They relate it to discrete conduce fibrations, Martin-Lof has also been lecturing on such interval type theories. I am not sure whether there is a public record of the latter. In any case, I suspect Jeffrey’s work to be related to such discrete conduce fibrations.

]]>What we were doing above (in section 5 of temporal logic) seems to point in a very similar direction to

- Alan Jeffrey, LTL types FRP

Reactive types there are our $Time_0$-dependent types. Perhaps we were doing better. Jeffrey writes:

The implementation described here is based on interval types, rather than reactive types. This might be a better match to an interval temporal logic rather than LTL, which would admit the “chop” modality

That ’chopping’ of an interval is what Mike is addressing in #18.

]]>Interesting! So we’re in this neck of the woods described by Neel Krishnaswami:

Nick Benton and I have argued for programming explicitly with streams in our paper Ultrametric Semantics of Reactive Programs. Subsequently, Alan Jeffrey suggested using LTL as a type system in his paper LTL types FRP, an observation that Wolfgang Jeltsch also made in his paper Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming.

The difference between the view Nick and I take, and the one that Alan and Wolfgang take is best understood (IMO) by comparing the construction given in Birkedal et al.’s First steps in synthetic guarded domain theory: step-indexing in the topos of trees with Alan’s paper. The topos of trees (presheaves over the natural numbers ordered by size) is very similar to category of ultrametric spaces Nick and I used, but much easier to compare with Alan’s category (presheaves over a discrete category of time), since these are both presheaf categories.

If you’re interested in futures specifically for concurrency, then it might be a better idea to look at CTL rather than LTL, though. AFAIK, that’s presently unexplored territory!

Has anyone done a Curry-Howard correspondence for CTL or even CTL$^{\ast}$?

]]>There is a curry-howard correspondence between LTL and reactive programming. This is similar to the temporal semantics in the topos of trees (presheaves over omega). http://www.itu.dk/~mogel/papers/lics2011.pdf

I can try to add more references later.

]]>I began a section on ’computation tree logic’ at temporal logic. I’ll add some more detail later. It seems a good candidate for adjoint logic treatment.

]]>Like you, David, I get a strong whiff of CATS lurking in the shadows of what and how they speak.

[Oxford Handbook on the Philosophy of Time](https://global.oup.com/academic/product/the-oxford-handbook-of-philosophy-of-time-9780199298204?cc=us&lang=en&)

[(Oxford readings) The Philosophy of Time](https://global.oup.com/academic/product/the-philosophy-of-time-9780198239994?cc=us&lang=en&) ]]>

So Bergson views time as a topological point (maybe infinitesimal thickened)?

]]>In view of the Lawverian and so Hegelian roots of adjoint logic, and of our adjoint representation of time above, it’s perhaps interesting to read what R. G. Collingwood, much influenced by Hegel, has to say about time.

In *Some Perplexities about Time: With an Attempted Solution*, Proceedings of the Aristotelian Society, New Series, Vol. 26 (1925 - 1926), pp. 135-150, he is trying to find another way to think of time other than

“spatially,” as something existing

totum simul

or as

a ceaseless flow in which the present, perpetually changing, sloughs off its states into the abyss of the past and acquires new states from the abyss of the future.

His solution is as follows:

The ideal is that which is thought, but not thought as real or existing; and in this class fall the future, which is possible but not necessary, and the past, which is necessary but not possible. The real is the present, conceived not as a mathematical point between the present and the past, but as the union of present and past in a duration or permanence that is at the same time change: the possible parting with its unnecessariness and the necessary parting with its impossibility in an actuality which is at once possible

andnecessary, not (like the abstract mathematical present) neither. Within this present there are, as really as you like, two elements (necessity and possibility), each of which taken singly or in isolation characterizes a being which is not real but ideal—the past and future respectively. Thus the pastas pastand the futureas futuredo not exist at all, but are purely ideal; the past as living in the present and the future as germinating in the present are wholly real and indeed are just the present itself. It is because of the presence of these two elementsinthe present (not merely psychologically or illusorily, as in the doctrine of the specious present) that the present is a concrete and changing reality and not an empty mathematical point.That which is ideal is for a mind, and has no other being except to be an object of mind. But the ideal and the real are not mutually exclusive. A thing may be ideal and also real. An example of this would be a duty, which is absolutely real in spite of the fact that it only exists for mind. But some things are merely ideal, and under this head fall the past and the future; unlike a duty, which exists only for thought but, for thought, really does exist, they have being for thought, but, even for thought, have no existence. Hence, if there were no mind, there would at any given moment be no past and no future; there would only be a present in which the past survived transformed and in which the future was present in germ. The past

as pastand the futureas future, in contradistinction from their fusion in the present, have being for mind and only so. We do call the past,as such, into being by recollecting and by thinking historically; but we do this by disentangling it out of the present in which it actually exists, transformed, and re-transforming it in thought into what it was. Hence time, as succession of past, present and future, really has its beingtotum simulfor the thought of a spectator, and this justifies its “spatialized” presentation as a line of which we can see the whole at once; it also justifies, so far as they go, subjectivist views of time like that of Kant. But time, as the ceaseless change of the present, is “transcendentally real,” and the logical presupposition of any thought whatever; and this justifies the “pure flux” view of time and its treatment in philosophies like that of Bergson and Mr. Alexander.But this conception, though the only one I can discover which gives any hope of escape from my perplexities about time, is only open to a logic which conceives the real as a synthesis of opposites and a metaphysic which has abandoned the hopeless attempt to think of all objects of thought as existent. If we must regard the real as a collocation of elements each of which is real by itself and in its own right, we must give up the solution which I have attempted to sketch and find another, if we can.

Plenty of resonances there, such as adjunctions as ’synthesis of opposites’ and maybe a whiff of the kinematics/dynamics distinction of higher category theory and physics.

By the way, Bergson was supposedly instrumental in Einstein not receiving a second Nobel prize for relativity theory, the spatialization of time being evidently wrong.

]]>Added pointer to the nice slides that now go with *Licata-Shulman*.

OK, thanks for clarifying :-)

]]>Got it, thanks. Sounds like quite a menagerie!

]]>Well, it’s just saying there are box modalities

- in the strict future
- in the strict past
- in the present and future
- in the present and past
- in the past, present and future

@David, your link takes me to a page unavailable for viewing or I have reached my viewing limit for this book.

]]>Re #31, it’s just like how in modal logic, “$\phi$” unadorned means that $\phi$ is true at the current world (or, more precisely, the “truth value” of unadorned $\phi$ is the set of worlds in which it’s true), not that it’s true in all worlds.

And even in natural language, if I say just “it is 12 o’clock”, what I mean is that it’s 12 o’clock *now*, not that it’s *always* 12 o’clock.

Re #30, that route has been taken. See here in a handbook on temporal logic in AI. It’s the difference between the box and the box with plus inside.

Re #31, this is all in the context of $Time$. You can base change a timeless proposition to one which is time-dependent but constant, e.g., (1+1 = 2)(t) is always true. Timed propositions can be stated to hold now and at no other time by $\neg P \phi \wedge \phi \wedge \neg F \phi$.

]]>I don’t know if “now” is used in temporal logic, but I envisaged it to denote something that it true at a particular time, and not elsewhen. Something like “It is 12 o’clock now”. Doesn’t “$\phi$”, with no context, mean something that is “globally” true?

]]>I suppose we could always write $\phi \wedge F \phi$ if that’s what we mean. Although that might not be compatible with a constructive viewpoint on the temporal ordering. One could I guess also go crazy and have *both* the reflexive and irreflexive orderings hanging around, inducing two different families of modalities.

Does one generally have, for instance, $\phi\vdash F\phi$ in temporal logic?

Not as far as I’m aware. However, looking around some more, we find Robert Goldblatt in Logics of time and computation

]]>The most common practice in temporal logic is to regard time as an irreflexive ordering, so that “henceforth”, meaning “at all future times”, does not refer to the present moment. On the other hand, the Greek philosopher Diodorus proposed that the necessary be identified with that which is now and will always be the case. This suggests a temporal interpretation of $\Box$ that is naturally formalised by using reflexive orderings. The same interpretation is adopted in the logic of concurrent programs to be discussed in §9. (p. 44)

So if we use the $\lt$-intervals, then yes, we have only a semicategory, which in particular implies that our “modalities” are not monad/comonads since they lack units/counits. Which is maybe not a huge problem, but it means we can’t axiomatize them in type theory the way we have for all other modalities and comodalities — although we couldn’t do that anyway if we’re not propositionally truncating, since then they wouldn’t be idempotent. I guess if we encode them by breaking them down into $f^\ast$’s and $\Sigma$s and $\Pi$s using adjoint logic, that wouldn’t be a problem.

Does one generally have, for instance, $\phi\vdash F\phi$ in temporal logic?

]]>Does the adverb “now” actually mean anything in temporal logic? I mean, does “$\phi$ holds now” mean anything different from just “$\phi$”?

]]>This is the issue be dealt with here:

]]>Segal’s definition of a conformal field theory discusses “functors” for which the domain is not a category. There is an associative notion of composition for arrows, but there are no identities.