In addition one may observe that the composite

$State = \prod_W W^\ast \sum_W W^\ast$is the state monad, for $W$ the type of possible internal states of the computer. The standard way in Haskell to implement random numbers is to consider a type $W = StdGen Int$ “of random integers” (say) and then work with $State StdGen Int$. This allows to read random numbers (which are the “current state”, the “currently realized world”) and then update them to the next one.

If we don’t care about “updating to the next possible world” but are happy with the one we have, then we may reduce this to $Reader = \prod_W W^\ast$.

]]>One piece of magic is that where *randomness* $\prod_W W^\ast$ is used in formalization of quantum physics, it is to be forced to act essentially equivalently to $\sum_W W^\ast$ – see at *dependent linear type theory* the section *on fundamental classes*. That’s the “ambidexterity” of Hopkins-Lurie.

Hence we find that for purposes of modelling reality in the the objective logic, the base change adjoint triple to a space of possible worlds/possible field configurations induces *three* modalities

Of course that was noticed before.

]]>If $W^\ast \sum_W$ and $W^\ast \prod_W$ are both important enough to have names, and so is $\prod_W W^\ast$, shouldn’t we give a name to $\sum_W W^\ast$? Admittedly it doesn’t seem too interesting

$\sum_W W^\ast (-) \equiv W \times (-).$ ]]>addendum to #155:

I now see that Toronto-McCarthy 10 also say it in explicit prose, in the tiny side note text on slide 35:

you could interpret this by regarding random variables as reader monad computations.

There must be a published article that goes with these talk slides, but I am not sure yet if I have found it.

[edit: ah, of course it’s here: (pdf). In 2.2 they call $\prod_W W^\ast$ the “random variable idiom” ]

]]>What I’m saying is that by choosing a particular formalization of an informal notion, you of course determine the answers to lots of questions; but someone else might prefer a different choice of formalization of the same informal notion, leading to different answers to the same questions. So formalization is an excellent tool for clarifying the exact points of disagreement, but it can’t always be relied on to eliminate the disagreement even if everyone involved is completely rational.

]]>The whole point that I am making is that after what used to be just opinions has been formalized, then there is no more room for disagreement anymore than there is generally in mathematics.

That’s why analytic philosophers are eager to use formal modal logic for their arguments and dismissive of those collegues who don’t reason formally. While that is the right idea, unfortunately most analytic philosophers forget to specify their boxes and circles and might confuse them with a flat or a sharp. If we add in that missing specification, by recognizing $\Box_W = W^\ast \prod_W$ etc., then their program of turning philosophy into mathematics actually works.

]]>once we fix that these are formalized by $W^\ast \sum_W$ and by $W^\ast \prod_W$, then answers to all the traditional questions may systematically be worked out

…but not everyone may agree that the answers thereby obtained are the right ones. (-:

]]>For what it’s worth, I have found two references that express the suggestion that I am making:

Notice that the monad in question, the one I am suggesting should be called *Zufälligkeit*, $\prod_W W^\ast$, is what computer scientists call the *reader monad*.

Verdier 14 is so kind to agree with what I wrote above:

The intuition behind the Reader monad, for a mathematician, is perhaps stochastic variables. A stochastic variable is a function from a probability space to some other space. So we see a stochastic variable as a monadic value.

The same point, not in a prose sentence but by way of an item list, is made in Toronto-McCarthy 10, slide 24.

Notice that in the line before, slide 23, these authors are even so kind as to agree that a probability space deserves to be addresses as a space of “possible worlds”.

]]>That’s part of my motivation for finding good formalization of natural language: once we have it, then quandaries as you quote will find resolution.

We have seen this in the above discussion for the example of discusison of necessity and possibility: once we fix that these are formalized by $W^\ast \sum_W$ and by $W^\ast \prod_W$, then answers to all the traditional questions may systematically be worked out.

Regarding randomness; the mathematical concept of *random variables* is perfectly well established. The space of random variables is a suitable space of functions on the given space of possible worlds. Luckily, this concept is sensible and useful independently of any questions of physics that Jaynes raises; it’s a concept of pure thought, a topic of the doctrine of essence, not of nature. (*Zufälligkeit* translates both to *randomness* as well as to *contingency*. Fewer people would come up with the second translation, though, I’d think) Once we agree on a good modalic formalization of this, then it is time to see how this will work itself out in nature, by following the formalism.

Maybe I’ve developed a certain nervousness around the term ’random’ from reading Edwin Jaynes. He generally writes it in scare quotes, and attributes much said about randomness to the so-called ’mind projection fallacy’, projecting our ignorance into ideas of chance in the world.

Those factors which vary in an uncontrolled way are often called

random, a term which we shall usually avoid, because in current English usage it carries some very wrong connotations.To many, the term ‘random’ signifies on the one hand lack of physical determination of the individual results, but, at the same time, operation of a physically real ‘propensity’ rigidly fixing long-run frequencies. Naturally, such a self-contradictory view of things gives rise to endless conceptual difficulties and confusion throughout the literature of every field that uses probability theory. We note some typical examples in Chapter 10, where we confront this idea of ‘randomness’ with the laws of physics. (Probability Theory as Logic, 271)

I find this equating probability with plausibility in the face of incomplete knowledge quite plausible in our everyday dealings with the world. As for quantum physics, I don’t know. Jaynes seems to want to push it all the way:

incomplete knowledge is the only working material a scientist has! (61)

By the way, I came across another category theoretic takes on probability theory

- Kirk Sturtz, Categorical Probability Theory, http://arxiv.org/abs/1406.6030

This takes up Tom Leinster’s and Tom Avery’s account of the Giry monad as codensity monad.

]]>David, thanks for getting back to me.

That article considers maps to $[0,1]$ as homomorphisms of effect algebras in the hope to capture aspects of quantum physics. Despite exposure to many seminar hours of effort in Nigmegen, I remain to be convinced of the effect of effect algebras. If we are asking for effect of categorical logic in general – and of the (co-)monads $\sum_W W^\ast$ and $\prod_W W^\ast$ in particular – on quantum physics, then only modesty keeps me from claiming that the only genuinely viable approach to that which I am aware of is that via secondary integral transforms in dependent linear homotopy type theory. It is due to this that I know for a fact that the dependent linear semantics of $\sum_W W^\ast$ and $\prod_W W^\ast$ captures the phenomenon of quantum randomness observed in the real world.

But what I was after here now is more elementary, more Platonistic, maybe just linguistic. I am thinking that just from an elementary observation of the basic nature of $\prod_W W^\ast$, and in view of the pronounciation of $W^\ast \prod_W$ as *necessity*, it should seem sensible to pronounce it as *randomness*.

It’s supposed to be utterly simple: you can try to feed $\prod_W W^\ast$ a proposition. But since this monad now acts on the empty context instead of on the context of possible worlds as its dual sublings do, this comes out vacuous. Either we feed it the true proposition, then it returns *true*, or we feed it the false proposition, then it returns *false*. Hence we conclude that the meaning of $\prod_W W^\ast$ is beyond first-order logic,beyond the Prop-truncation, and is genuinely type theoretic.

So we feed it any type $V$ that is not $(-1)$-truncated instead. What does it return? The type of $V$-valued functions on the space of possible worlds.

At this simplistic level, there is no normalization on these functions that would constrain them from $V$-valued “distributions” to probability distributions. But then, comparison to the case where $V = KU$ and where I fully understand how this relates to genuine real quantum physics, I see that the idea to normalize *these* functions right away is too naive anyway, that it’s rather probability *amplitudes* that matter and that in addition there is some holography in the game, etc., and that we better let the tao of mathematics lead the way than trying to force it to submit to our prejudices.

So to disregard such technicalities as normalization; I wonder: if you walk over to your colleague’s office and say: “I have here a space of possible configurations and the space of functions over it,what might that be?”; wouldn’t most people think of the space of functions on a space of configurations as a space of random variables? What else?

]]>Maps to $[0, 1]$ appear in the adjunction on p. 2 of Duality for Convexity.

]]>That’s what here we usually call “propositions as types”. But I suppose we are talking past each other now, for I am not sure what #149 is reacting to.

Try something more linear than $\Omega$ to get a better impression of randomness, such as $[0,1]$. Of course it works really fully well only for stable types.

But if my little linguistic intuition here does not resonate with you, it’s not too important. The nForum might be the wrong place to try to sort it out further.

]]>The understanding of a proposition as a set of possible worlds is commonplace. E.g., here

]]>The possible-worlds analysis of propositions identifies a proposition with the set of possible worlds where it is true.

Yes, *randomness*.

You should best think of applying it to pointed types, such as $\Omega$ or such as stable types. Then $\prod_W W^\ast$ sends this to the collection of all distributions of possible worlds where in each world either “it holds” or it doesn’t. A term of $\prod_W W^\ast \Omega$ is a random subset of all possible worlds.

]]>Is there likely to be a good name for it then?

]]>Yes!

]]>So in the ordinary nonlinear case, $\prod_W W^\ast (-)$ is just the function type $[W, -]$?

]]>On another linguistic note:

So we have, recall, that $W^\ast \prod_W$ is to be pronounced *necessity* and that $W^\ast \sum_W$ is to be pronounced *possibility*. Then: is there a good candidate for a natural language incantation for $\prod_W W^\ast$ ?

I have come to think that there is: this is *randomness* or *contingency*.

(This works a bit better in German; *Notwendigkeit*, *Möglichkeit*, *Zufälligkeit*.)

For instance, fixing the argument to be the prop universe $\Omega$ and varying in the space $W$ of “possible worlds”, then $\prod_{(-)} (-)^\ast \Omega$ is the power set operation. Changing $\Omega$ to something more linear gives more linear (probability-)distributions.

And not the least, on linear dependent types, it is $\prod_W W^\ast$, not $W^\ast \prod_W$, which governs path integral quantization via secondary integral transforms.

]]>Re 142: For me, a categorical model is one as discussed in the Studia Logica paper: The fundamental idea of a categorical treatment of proof theory is that propositions should be interpreted as the objects of a category and proofs (lambda-terms) should be interpreted as morphisms. The proof rules correspond to natural transformations between appropriate hom-functors. The proof theory gives a number of reduction rules, which can be viewed as equalities between proofs. In particular these equalities should hold in the categorical model, page 19 and forward ones of On an Intuitionistic Modal Logic (with Gavin Bierman), Studia Logica (65):383-416, 2000.

Re 141 indeed, the $\Box$ fragments do agree. but to make the modalities “classical” we need to make sure that they are inter-definable i.e. that $\lozenge(A) = \neg (\Box (\neg A))$.

Your idea of a model is not proved to satisfy the equations forced on us by the proof-theory. at least it is not obvious to me that it does. the problematic cases are again the distributions that we’ve been discussing. This is what I mean by saying that categorical models for me come from the Curry-Howard correspondence. (and by the way thanks for reading the paper on CK.)

]]>Re: 141: What do you mean by making constructive modalities into classical modalities? (I’ll note that the $\Box$ fragment of $\mathrm{CK}$ does become the $\Box$ fragment of classical $\mathrm{K}$ when using a classical propositional basis)

Re: 140: I agree that you have many options when constructivizing a notion. So my argument is about a subjective sense of what seems to me the most natural intuitionistic correspondent of $\mathrm{K}$, rather than about any objective claim.

What do you consider to be a categorical model? As I’ve said, the notion of intuitionistic $\mathrm{K}$ I have in mind could be modelled by considering two models of intuitionistic logic (i.e., cartesian closed categories with coproducts) $C$ and $D$, two homomorphisms (i.e., cartesian closed functors preserving coproducts) $M$ and $N$ from $C$ to $D$, and right and left adjoints to $M$, taking $\Box$ and $\lozenge$ to be $N$ followed by the right and left adjoints to $M$, respectively. A particular case of this arises when considering a directed multigraph, with each proposition assigned some set at each node of the multigraph; the set assigned to $\Box A$ at a node is the product, over all edges out of that node, of the sets assigned to $A$ at the destination of those edges, and similarly for $\lozenge A$ replacing “product” with “sum”. (As these sets need not be subterminal, this is indeed a categorification.)

]]>Re: 139 It is indeed true and known that the system CK does not become K when you make the basis classical. This corresponds to the idea that modalities also have their own classical or not character. When you want to make a system consisting of propositional basis + modalities classical you have to make both components classical, the basis becomes classical propositional logic and the constructive modalities have to become classical modalities.

]]>Re: 138 As I said when you ‘constructivize’ a notion, you have, sometimes, many options. There are several non-equivalent Constructive Set Theories, for example.

When it comes to constructive modal logic K, I take my cues from the Curry-Howard correspondence and the the categorical semantics. They do not support the distribution of $\lozenge$ over disjunction: when you look at a ND-tree that ends up in $\lozenge(A)\vee \lozenge(B)$ there is no obvious way to see a map getting there from $\lozenge(A\vee B)$. At least none that I can see.

The $\lozenge(A\vee B) \to \lozenge(A)\vee \lozenge(B)$ distribution can, nonetheless, be considered a basic law (by fiat) and Simpson’s has a very pretty system that does it. But there is no categorical model of it, as far as I know. I will be delighted if you can provide one. Meanwhile the system without the distribution, which has been considered several times over by applications in CS – e.g Nerode’s work – does have categorical models.

]]>I’ll also note that the system $\mathrm{CK}$ (defined on page 4 of the linked paper as propositional logic + the necessitation rule + the axioms $\Box(A \to B) \to (\Box A \to \Box B)$ and $\Box(A \to B) \to (\lozenge A \to \lozenge B)$) does not have the property that, when its underlying propositional logic is made classical, it yields classical $\mathrm{K}$. This is clear by noting that, no matter what underlying logic it is taken upon, any theorem of $\mathrm{CK}$ remains a theorem when $\lozenge$ is replaced by $\Box$ throughout, but this property does not hold for classical $\mathrm{K}$.

]]>