Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
created an entry modal type theory; tried to collect pointers I could find to articles which discuss the interpretation of modalities in terms of (co)monads. I was expecting to find much less, but there are a whole lot of articles discussing this. Also cross-linked with monad (in computer science).
added paragraph Examples - Geometric modality: Grothendieck topology. (deserves being re-written already, but I am too tired now, feel free if you have the energy). Linked to Goldblatt's article. Does anyone have a copy of that article? I only saw the first page. Also cross-linked with Lawvere-Tierney operator
Thanks!
I feel unable to read that second reference right now. Is it possible to quickly summarize the coalgebraic formulation of modality?
Since, as we discussed at some length not long ago, an algebra over an endofunctor is equivalently an algebra over the corresponding free monad, a kind of direct relation between the two algebraizations immediately suggests itself. But I don’t know.
If you look at Moggi’s original article in def. 4.7, he immediately identifies a modal operator with an algebra over the given operad.
Another possible link is to here. The paper gives an interpretation of the proof theory of Intuitionistic S4 in terms of homotopy theory! I don’t see where to put the link.
There is a lovely survey article by Goldblatt on algebraic semantics of modal logics. (see algebraic model for modal logics).
There is a considerable literature on comonads, streams, see Alexander Kurz’s homepage. I have created Alexander Kurz.
Another possible link is to here.
Thanks, I have added that to the list at modal type theory.
The paper gives an interpretation of the proof theory of Intuitionistic S4 in terms of homotopy theory!
Is that true? I just see that it uses (augmented) simplicial sets, but not the homotopy theory of simplicial sets.
By the way, it seems to me that the simplicial set which they assign to a type in Definition 20 is the bar construction of the modality, regarded as a (co)monad. In as far as we follow Moggi, Kobayashi, de Paiva et al and identify modal operators with monads (in computer science) such bar constructions are available always.
However without some genuie homotopy theory in the game, these bar constructions are not resolutions of anything. So I’d be careful with saying that this is homotopy theoretic.
Thanks. I didn’t even know that this entry existed. It wasn’t linked to from modal logic. (There was a broken linked that probably meant to point there. I have fixed that and did a bunch of further formatting on these and related entries.)
There was a very recent meeting at Dagstuhl. Its webpage has a good motivation section.
I think that in that Intuitionistic S4 paper , Eric and Jean do not exploit any homotopy theoretic aspect, except to think of proofs as being homotopies in some sense. It is some time since I studied that paper so I am not sure. They used the decalage I think.
There is a page on logic which lists a lot of those pages. I have added a link to modal type theory.
I think the link was under algebraic semantics.
Is it possible to quickly summarize the coalgebraic formulation of modality?
I think this paper gives quickest access. But briefly, in the propositional case, on the syntactic side we have Boolean algebras. There’s an endofunctor corresponding to the addition of a modal operator, such that algebras for the endofunctor are modal algebras. Across the syntactic-semantic divide via Stone duality, we have categories of models. The composition of the dualising passage to syntax, the modal endofunctor, and the dualising return to semantics is an endofunctor on models. Coalgebras for this endofunctor provide the semantics for modal theories. E.g., maybe the introduction of an accessibility relation between worlds.
@David #9: Boolean algebras are the syntactic side? I usually think of a Boolean algebra as the semantics of classical propositional logic.
There’s an endofunctor corresponding to the addition of a modal operator, such that algebras for the endofunctor are modal algebras.
I see. Thanks. That doesn’t seem to be on the $n$Lab, or is it? Maybe you could paste your summary to the Idea-section of a suitbale entry?
I edited the page some, trying to clarify where “modality” means something acting on propositions and where it means something acting on more general types.
@Mike #10, but any Boolean algebra is the Lindenbaum-Tarski algebra (classes of logically equivalent propositional sentences) of a propositional theory. Shouldn’t I see that as syntactic? Then maps into $2$ effectively give us the lines of its truth table, i.e., the models.
But then is it straightforward to distinguish syntactic and semantic anyway? I get confused by this. For one thing, there are term models. But then when $2$ and then $Set$ play their dualising roles between syntax and semantics, I should consider the dualising objects as both syntactic and semantic?
Thanks, Mike.
So suppose somebody sees this list and feels like deducing a simple general statement:
Modal type theory is type theory equipped with (co)monads.
I imagine many modalists would complain when seeing such a statement. What would such complaints be? To which extent am I entitled to make the identification between modal type theory and the simple notion of type theory with (co)monads? Which subtleties would such an identification be missing? Are any of these subtleties “essential”?
As I said on another thread:
In case this helps for the semantics vs. syntax discussion, there is an entry on the Lindenbaum-Tarski algebra of a normal modal logic.
There is also a coalgebraic canonical model. This has the set of Λ-maximal consistent formulae as its set of states. (see that entry). Both the algebra and the coalgebra are considered as giving the semantics of the logic. Note that in maximal consistent, the link with ultrafilters is mentioned, and of course they come in quite naturally from the context.
Modal type theory is type theory equipped with (co)monads.
I imagine many modalists would complain when seeing such a statement. What would such complaints be?
I started reading
which concerns this question. With Moggi the author amplifies that strong monads on the type system have some defect when it comes to regarding them as an interpretation of modalites (and then he discusses that neverteless “$\mathcal{L}$-strong monads” work nicely in this respect ).
What is it that makes these authors reject a type system with a strong monad as a modal logic? It seems to me that there are two separate issues:
Type systems with strong monads on them don’t have a “natural modal logic” that is “like S4”. (see e.g. beginning of Kobyashi’s section 4)
Type systems with strong monads on them violate some aspect of “proofs-as-programs”. (this Kobayashi fixes in his section 7 by introducing $\mathcal{L}$-strong monads instead)
My impression is that the first point is purely a matter of taste, while the crux is in the second point. For over at modal logic we cite modal textbooks that admit that nobody has a global definiton of what modal logic is and what it is not. So if something is almost but not quite like S4 modal logic, then how would we know that we definitely don’t want to call it another flavor of modal logic?
The second point seems to contain the actual technical content. I haven’t absorbed Kobayashi’s section 7 yet (dinner was over before I got through, now I need to do something else). Is this somehow related to whether or not we can find a “computationally effective” implementation, or decidable etc.?
@David 13: I guess I use the word “syntactic” more narrowly than some people. To me, syntax is about symbols written on a page. The moment you scoop up a bunch of those symbols, mod them out by some equivalence relation and put some structure on the resulting set, then you have a model, i.e. semantics, even if it’s a semantics “built out of syntax”. The term model is the “initial semantics” but it is itself already semantics.
@Urs: My view is that a “pluralistic” view of modal logic does not restrict it to considering modalties which behave like the most classical “necessity” and “possibility” modalities. From that point of view, type theory with (co)monads is most definitely a modal type theory. I guess this is what you mean by saying that Kobayashi’s first point is a matter of taste. On the other hand, I would certainly shy away from claiming that everything one might call a “modality” is either a comonad or a monad.
I think it’s good that the coalgebra community tries to make contact with historical understanding of modality as ways of describing the status of certain propositions. See, e.g., Modal Logics are Coalgebraic
…the vast and growing family of modal logics, which are characterised by having operators that qualify formulas as holding in a certain way, e.g. ’necessarily’, ’in the future’, ’everywhere’, ’probably’, ’as everyone knows’, or ’normally’.
And
In a seemingly simple piece of knowledge such as ’Normally, the likelihood of road congestion is smaller on weekends’, one implicitly makes use of default logics (’normally’), probabilistic reasoning (’the likelihood’) and temporal knowledge (’weekends’) under a quantitative regime (’smaller’).
@Urs: As for your second point, what I got out of Kobayashi’s paper was different: it seemed to me that he was saying that strong monads don’t match the traditional meaning of “possibility”-like modalities (your first point) and that therefore Moggi thought that “modal logic” — meaning S4-like logics rather than the more pluralistic view I would favor — doesn’t have a good categorical semantics and thus can’t have a good proofs-as-programs interpretation. In other words, it sounded to me as though the entire paper was predicated on the idea that “modal logic” means specifically S4-like things, and if we take a more pluralistic point of view on the meaning of “modal logic” then all problems disappear.
@David, thanks for the reference, I put that into the relevant entries now!
@Mike:
type theory with (co)monads is most definitely a modal type theory
Okay, good.
if we take a more pluralistic point of view on the meaning of “modal logic” then all problems disappear.
Okay, good.
I would certainly shy away from claiming that everything one might call a “modality” is either a comonad or a monad.
I had this hope that we could say “modal type theory is type theory with (co)monads” because it would make the situation nicely systematic. Because otherwise, it’s disconcerting to have a concept in foundations without a definition. So I tend to wonder now which examples of “modal” type theories are not (co)monadic, and whether they might maybe all have a “fix” that makes them (co)monadic after all. It’s not so important, but that’s what I’d naturally wonder about now…
Consider a modality like “Joe believes that …”. Unless Joe is omniscient, we don’t have $A \Rightarrow$ “Joe believes that $A$” for all $A$. And unless Joe is infallible, we don’t have “Joe believes that $A$” $\Rightarrow A$ for all $A$ either. So this modality has no unit or counit, hence seemingly can’t be a monad or a comonad.
Epistemic modalities appear to be very weak. E.g., reasonable versions of belief or knowledge don’t even satisfy distribution
$\Box (p \to q) \to (\Box p \to \Box q)$.
So I may know $p \to q$ and $p$, but have not put them together to deduce $q$. Same goes for belief. I remember as a child the shock of putting together ’if mammalian mother, then lactates’ and ’mother whale is mammalian’.
The thing is, to me it is not even clear why FOL + “Joe believes”-operator deserves to be called a “modal logic”. Unless we call every operator on a plain logic a “modal logic”. Is that what we do?
Can we have a term for those modalities that are indeed (co)monadic? Of course “monadic modality” could work, but maybe we can better characterize in terms of modality itself what it means to be ‘monadic?
Maybe “faithful modality” (since it respects at least part of the notion of truth)?
Is there any established term for this?
$S4$ is the modal logic for which
This strength makes it just right for topological, and in the first order case, sheaf-theoretic treatment.
There’s a good list of modal axioms and their frame counterparts here.
The thing is, to me it is not even clear why FOL + “Joe believes”-operator deserves to be called a “modal logic”.
I think the meaning of the word “modality” demands it. Along with scads of stuff written by modal logicians. Don’t they get to decide what “modal logic” means?
Don’t they get to decide what “modal logic” means?
But did they?
I doubt you’ll find any very neat definition of what a modal logic is. Along with necessity and possibility, we find
tense logic: henceforth, eventually, hitherto, previously, now, tomorrow, yesterday, since, until, inevitably, finally, ultimately, endlessly, it will have been, it is being …
deontic logic: it is obligatory/forbidden/permitted/unlawful that
epistemic logic: it is known to X that, it is common knowledge that
doxastic logic: it is believed that
dynamic logic: after the program/computation/action finishes, the program enables, throughout the computation
geometric logic: it is locally the case that
metalogic: it is valid/satisfiable/provable/consistent that (Goldblatt, Mathematical Modal Logic: a View of its Evolution).
The metalogical version was important in the history of modern modal logic. Gödel played an important role there.
As is common with such matters, the linking of a philosophical pursuit to something more practical tends to focus minds. Computer scientists have explored modal logics extensively, as with model checking.
David. Can you adapt that to give a bit more info on modal logics somewhere on a relevant page? Complete with sources. Perhaps a new page linked to the old one would work well.
David,
can you put this kind of information into the entry on modal logic?
I understand that in the broad sense every operator that I might think of might be thought of as inducing a modal logic. Nevertheless, when I look at the mathematical literature on modal logics it is only very specific ones that are studied and hence apparently only very specific ones that are considered interesting. I haven’t yet seen a disucssion of the mathematical aspects of the “Joe believes”-logic (though of course that need not mean much, feel invited to give me such a reference).
The modal logics that I see discussed in the literature are monadic. So therefore I am wondering (still): what do we actually lose (concerning mathematical logic) if we restrict to these? I’d just like to get a feeling for how much the liberty of considering non-monadic modal logic buys us.
What are major mathematical articles on non-monadic modal logics? What are central structures of interest here? Do you have any pointers?
@Urs: There is quite an extensive literature in the AI and CS communities on belief logics. These are highly mathematical in nature BUT not in motivation. (BTW monadic has two meanings in that area. The other one refers to single ’variable’ operators.) The ‘monad’ axiom is called 4 which gives a ’multiplication’.
Johan van Benthem has written on these for instance here. These logics often have a common knowledge operator.
Another source is work by Baltag on Belief revision.
Thanks for the links. I have put them into epistemic logic. But let’s further discuss modal logic in the thread on modal logic
Concerning modal type theory: I have added the pointers
UF-IAS-2012, Modal type theory
Mike Shulman, Higher modalities (pdf)
and a pit more to Modal type theory - References.
I have done some changes mentioned on the modal logic thread.
Hey Mike,
now that I have actually read your note Higher modalities I am both happy and confused:
happy, because you say there precisely what in #14 and #23 above I was wondering if we’d be entitled to say: that a modality is a (co)monad on the type system (in the note you go even further and demand it to be an idempotent monad).
confused, because in #21 and #25 you seemed to be expressing the view that this is not a justifyable terminology.
And from this side remark in your note:
Andrej has suggested that conversely, any “logic” in which implication and universal quanti cation are “natural” ought to come from a modality
I gather that people like Andrej Bauer have a similar same stance towards modalities as under point “happy” above.
I also made a little survey among type theorists near me, if they like to consider modalities that are non-monadic. The answers were: no.
So all that makes me quite happy. I am just confused then about what happened in this discussion here. Maybe there was some misunderstanding?
I think for me it’s an issue of local terminology vs. global terminology. In a particular context where all I care about are monadic modalities, I’m happy to say plain “modality” and mean only monadic ones, just in doing commutative algebra one might say “ring” to mean only commutative ones. But in the context of a wiki page on “modality” in general, I feel obligated to point out that not all modalities are monadic.
In modal type theory are two references broken: #Goldblatt 2006, Lawvere [9]
Fixed now:
And Goldblatt2006 is just Goldblatt as cited there (apparently the online version of that article is dated 2006, so that’s what Google tends to produce.)
have added to the top of the references at modal type theory a pointer to
since this is one of the rare articles that rather explicitly talks about modal type theory (“computational type theory”) as type theory with a monad on the type system, and what it’s good for.
(I feel with much of the literature this simple basis is somehow never stated very clearly, but I may have been looking at the wrong literature all along, of course.)
It is not so clear to me yet how these modal type theories connect to the ones we use in homotopy type theory. The latter are idempotent, for one.
So in the Fairtlough-Mendler paper (p. 5), $[K, L)$ is idempotent, but conjunctions of these need not be?
Is there a reason HoTT should be committed to idempotent modalities?
Curry’s proposal was to take $\bigcirc \phi$ as the statement “in some stronger (outer) theory, $\phi$ holds”. As examples of such nested systems of reasoning (with two levels) he suggested Mathematics as the inner and Physics as the outer system, or Physics as the inner system and Biology as the Outer. In both examples the outer system is more encompassing than the inner system where reasoning follows a more rigid notion of truth and deduction. The modality $\bigcirc$, which Curry conceived of as a modality of possibility, is a way of reflecting the relaxed, outer notion of truth within the inner system.
A fun idea, but what does it mean? It’s surely not the idea that physicists’ notions of proof are weaker than mathematicians, as in that Jaffe-Quinn criticism of the sloppy habits of physics invading maths. If I recall correctly, they were after some kind of warning sign to show that a result had only been reached to a lesser standard. Maybe $\bigcirc \phi$ could mean ’we have a physicist’s proof of $\phi$’.
(Then idempotency fails since ’we have a weak proof that we have a weak proof of $\phi$’ is not the same as ’we have a weak proof of $\phi$’?)
Curry’s idea seems in line with Neel’s here:
In the judgmental approach to modal type theory, we view modal types $\Diamond A$ as internalizations of categories of judgment.
That is, in Martin-Löf’s judgmental methodology, we take the assertion “$P$ is true”, and then introduce a judgement of “$P$ is true”, which explains what constitutes evidence for $P$ (the introduction rules), and how to use a $P$ (the elimination rules). We can extend this to modalities by introducing new judgements to represent new categories of assertion. So in addition to “$P$ is true”, we might also have categories of judgment such as “$P$ is known to $X$”, “$P$ will eventually be true”, “$P$ is possible”, and so on. Then, a modal type like $\Diamond A$ is an internalization of a judgement. That is, we can say that the introduction rule for the judgement “$\Diamond A$ is true”, is actually evidence for the judgement “$A$ is possible”.
In categorical proof theory, we typically take a judgement to be a category $\mathbb{C}$, with the types represented by the objects of $\mathbb{C}$, derivations of judgements given by morphisms $f : \Gamma \to A$ (with the context $\Gamma$ represented by some kind of tensor product), and type constructors interpreted by (possibly $n$-ary and contravariant) endofunctors $T : \mathbb{C} \to \mathbb{C}$.
To extend this to judgmental modal type theory, we can introduce categories $\mathbb{C}, \mathbb{D}$ and so on for each category of judgment, and then take type constructors to be functors between these different categories. This makes the appearance of monads and comonads in modal type theory very natural. In some sense, adjoint functors give an “optimal” way of relating different categories, and composing a pair of adjoint functors gives you a comonad or monad, depending on which way around you go.
As a concrete example, take $\mathbb{C}$ to be the category of predomains and continuous functions, and $\mathbb{D}$ to be the category of pointed domains and strict continuous functions. Then, we can interpret morphisms of $\mathbb{C}$ as proofs that a proposition is true, and $\mathbb{D}$ as “possible proofs”. That is, $\mathbb{D}$ supports unrestricted recursion (has a natural transformation $\mathbb{fix}_A : (A \Rightarrow A) \to A$), and so non-normalizing terms can be defined, by taking fixed points that don’t decrease along a well-order.
If you move back to model theory, all this is is a way of saying that models are lattices, and modal operators come via monotone functions between lattices and Galois connections. This all makes me feel that some variant of the Stone representation theorem should enable you to produce worlds and Kripke models from this “point-free” account of modal logic.
David, Idempotent modalities are used to obtain a well-behaved dependent eliminator see Mike’s note.
Bas,
It may be harder to specify the syntax for non-idempotent modalities, but that seems no reason to not consider them. In fact HITs are going to be defined via non-idempotent monads.
Urs, I mentioned how idempotency was used. It may be possible to generalize this, but I don’t think it has been done yet.
I keep having this perspective that we have the syntax/semantics equivalence of relation between type theory and category theory. In this sense we certainly know precisely what the semantics of modal type theory with non-idempotent monads is. Maybe somebody still has to write out the syntax for this (not sure, this is the issue we are discussing over at computational type theory, too, some type theorists at least behave as if this exists), but this seems to be a matter of sitting down and doing it, not of principle.
In the introduction of the 95 article by Valeria de Paiva et al there is a nice comment on why monads on a type system fit well with the original idea of modal logic (and they consider not-necessarily idempotent monads). I have recorded that in the entry as follows:
Following (Moggi91, Benton-Bierman-de Paiva 95, Kobayashi 97) modal type theory is specifically understood as being a type theory equipped with a monad on its type system, representing the intended modality. Since monads in computer science embody a notion of computation, some authors also speak also of computational type theory here (Benton-Bierman-de Paiva 95, Fairtlough-Mendler 02).
According to (Benton-Bierman-de Paiva 95, p. 1-2) this matches well with the default interpretation of (S4) modal logic as being about the modality $T$ of “possibility”:
The starting point for Moggi’s work is an explicit semantic distinction between computations and values. If $A$ is an object which interprets the values of a particular type, then $T(A)$ is the object which models computation of that type $A$. $[...]$ For a wide variety of notions of computation, the unary operator $T(-)$ turns out to have the categorical structure of a strong monad on an underlying cartesian closed category of values. $[...]$ On a purely intuitive level and particularly if one thinks about non-termination, there is certainly something appealing about the idea that a computation of type $A$ represents the possibility of a value of type $A$.
Urs, you keep having that perspective, and we keep telling you that the problem of finding syntax that has these semantics is really hard and not “just a matter of sitting down and doing it”.
Sorry, but I am still not getting the complaint. For instance we have an entry internal logic that does just this, assert that every category comes with its internal logic. By just the same reasoning every category comes with its internal type theory. I don’t see why one should not be allowed to talk about this.
Moreover, in the present case at hand there are plenty of type theory articles on non-idempotent modalities in type theory. Are these somehow objectionable?
Let’s see at which point precisely the issue is.
Take Seely’s functor from suitable categories to type theories
$Lang \;\colon\; LCCCategories \longrightarrow MLTypeTheories$refined to a 2-functor by Clairambault-Dybjer (references just for completeness, I know that you know this well).
This 2-functor is an equivalence and takes monads to monads. The image of a monad under $Lan$ we may hence call a “modal type theory”.
So is the issue maybe that there is a more formal notion of type theory than appears in these articles by Seely and Clairambault-Dybjer, one defined in terms of some sequent calculus (these authors don’t talk about natural deduction)? Is it maybe indicated to distinguish different “levels of formality” of “type theory”?
I thought you were talking about homotopy type theory and $(\infty,1)$-categories. It’s the $\infty$-monad part that’s difficult. Ordinary 1-monads in extensional type theory are, as far as I know, not problematic.
The statement “every category comes with its internal logic” does not have a precise meaning. It’s a heuristic which guides us to discovering an appropriate internal logic for each given kind of category.
Mike, when you have a second, could you maybe react to the last part of the question:
What Seely’s article and in particular what Clairambault-Dybjer’s article calls a “type theory”, isn’t that something that deserves to be called “type theory” but is less formalized, in a sense, than those things that you implement on computers? Doesn’t it make sense to speak of this “type theory” and of “fully formalized type theory”, where the latter is what is given by symbol rewriting rules, whereas the former is given more at the usual level of mathematics?
At the usual level of formality in mathematics it seems to me we easily assign an internal logic to any category, and my impression is (or at least was) that this is what everybody always meant who edited the entry on internal logic: it’s the logic whose propositions are the subobjects, whose implications are the morphisms between them, whose conjunctives are product and coproduct in the slice, if they exist, and so on. This seems to be more than heuristics, while of course it is less than having a computer implementation of this logic.
The word “logic” here is being abused somewhat, perhaps. To me, a logic necessarily has an associated deductive system – after all, it is supposed to be a mathematical model of reasoning. It makes no sense to talk about logic at “the usual level of mathematics”. The so-called “internal logic” is just a language and an associated semantics – it does not come with a deductive system. If we are to take the stance that every category has an internal logic in the fashion you describe, then the implicit deductive system we get is useless: not even the basic structural rules of sequent calculus – the kind that people like to forget about but use all the time – will be valid.
I am not familiar with either paper, but it appears to me that Clairambault and Dybjer are honest and (except for the title) do not conflate type theories with related structures (e.g. categories with families). I do not accept your claim that the latter deserve the name “type theory”.
This is not something that I dreamed up. If there is something to be objected to here, than various $n$Lab entries need to be re-written or at least equipped with more qualification, notably relation between category theory and type theory.
That quotes Clairambault-Dybjer as completing the proof of the equivalence between dependent type theories and locally cartesian closed categories. I seem to remember that this was pointed out by Mike in the first place, but in any case this nLab entry has been discussed widely among people who should know, and there was never an objection.
But it is good that we finally maybe discuss this issue, it seems to have been implicitly behind various unfruitful exchanges elsewhere.
I’d be inclined to come back to my suggestion in #48 that we should have two terms to distinguish between two shades of “type theory”. Or something.
But I’d really like to hear Mike’s comment on this.
Re #51: it might make more sense however to refer to the “logic” associated with a doctrine (which here might mean a 2-monad on $Cat$, at least as a first approximation). For example, there is a logic of symmetric monoidal categories, a logic of finite limit categories, a logic of exact categories, and so on. The basic idea being that the free structured categories of some type capture the appropriate notion of equivalence classes of deductions. The further point being that the mode of deductive system (sequent calculus, natural deductions, Hilbert-style proofs, or whatever) is not necessarily the most important thing, but what is important is that differing modes of presentation agree on the appropriate equivalence classes of deduction, two deductions being equivalent if their interpretations as morphisms in free structures agree. These are the invariants of the “logic”.
Re #53:
The point I was trying to make is that syntactic categories are not themselves logics (or even logical theories). In my view it is perfectly reasonable to distinguish between Morita-equivalent theories (e.g. vector spaces over a field $k$ and modules over the matrix ring $M_n (k)$).
Re #55:
Yes, I agree: we should only speak of, say, “the internal logic of $\mathsf{D}$-categories” for some doctrine $\mathsf{D}$. But I insist that there must be at least one reasonable deductive system associated with that “logic”, which is hopefully computable in an appropriate sense. Recall the story of the Mickey Mouse proof system [Miller, p.57], which is sound and complete but utterly useless…
So what do you like to call the something that is associated to a specific category. The “internal language”? “internal logical language”? “internal type language”? “internal type theoretic language”?
Generally, how would you suggest to restate all the statements at relation between category theory and type theory?
Also for instance syntactic category would need to be re-written, if these complaints here are to be reflected. Various related entries probably too.
How do we deal with this? (And why did this issue not come up before?)
There are three components to the “internal logic” of a category (or indeed any structure whatsoever): a language $\mathsf{L}$ in the appropriate formal system, an interpretation $M$ of $\mathsf{L}$, and the collection $\mathsf{T}$ of all sentences that are true under that interpretation. I have no objections to calling $\mathsf{L}$ the “internal language”, but as Paul Taylor points out, this language is in fact an entity at the meta level, i.e. external. $M$ could be called the “canonical interpretation” or, tongue in cheek, “intended semantics”. Model theorists call $\mathsf{T}$ the “$\mathsf{L}$-theory of $M$” (or perhaps $\{ M \}$). The ideal theorem would say that $M$ is a universal model of $\mathsf{T}$.
I can’t think of a good name for the triple $(\mathsf{L}, M, \mathsf{T})$. But maybe we shouldn’t give it a name – these three things are different, and not realising that they are different caused me some confusion when I was learning this stuff…
Re #57: the phrase “internal language” seems alright to me (internal language of a topos, of a cartesian closed category, etc.). Typically this has a type-theoretic flavor (with basic types being objects, and with terms coming from morphisms). Notice that the sense of internal language is relative to a doctrine (so that the internal language of a topos $E$ is not the same as the internal language of $E$ considered as a ccc): the rules of type and term formation in these cases differ and are dictated by the doctrine $\mathbf{D}$. Actually, the language would correspond to the free $\mathbf{D}$-object $F(E)$ generated by the given structured category or $\mathbf{D}$-object $E$. There is then an interpretation $F(E) \to E$ given by the doctrinal counit. The internal theory would be $F(E)$ coupled with a description of when two terms in $F(E)$ have the same interpretation in $E$; it corresponds to the canonical presentation
$F F(E) \stackrel{\to}{\to} F(E) \to E$and $E$ could be considered the universal model of that theory.
But what do you mean “all the statements at relation between category theory and type theory” [need to be corrected]? What I saw at the article looked pretty good (I didn’t read all the way through), and actually was in accord with this doctrinal point of view. Are there particular statements there you could point to that you now think need revision?
Todd, thanks,
over at relation between category theory and type theory it seems that “type theory” (following at least Seely) is used for what here is being argued should not be called such, but should just be called “internal language”.
In particular the main statements there concern equivalences between , notably, the 2-category of locally Cartesian closed catgeories and 2-categories “of dependent type theories”. But by what you are saying here instead it should say “dependent type theory is the theory of the doctrine of locally Cartesian closed categories” or something, while the equivalence in the entry is between the 2-category of lcc categories and that of their internal languages.
Well, I am not arguing myself that the entry needs to be changed this way, I am just saying that given what you say, it would have to be changed.
No?
I’m still back on #50. There is, I guess, a difference between a fully formalized and implemented type theory and a less formal one, but that is not what’s going on here. I also don’t think that Zhen’s point about deductive systems is what is going on.
Consider basic MLTT. This is a formal system, with deductive rules, which can be interpreted into any LCCC. Moreover, if you add some “undefined” types and terms to it as axioms, then you get a new type theory, say $T$, which can be interpreted into any LCCC $C$ as soon as you specify the interpretation of those types and terms as objects and morphisms in $C$. In particular, if you start with the LCCC $C$, then you can construct the type theory $T$ whose axioms are precisely the objects and morphisms of $C$. This is the “internal logic” or “internal language” of $C$.
The theorem of Seely-Clairambault-Dybjer is that LCCCs are biequivalent to a 2-category whose objects are type theories of this form: MLTT augmented by some type-and-term axioms. This is most evident in Seely’s paper; it’s hidden a bit in the Clairambault-Dybjer paper because they reformulate the latter notion in terms of categories-with-families, I think to make it into a 2-category more easily.
However, when we say “modal type theory”, we mean an augmentation of the basic system of rules of MLTT, not an adding of axioms. The intent is then that if we consider this type theory with added rules, and consider the 2-category of type theories obtained by adding axioms, that would be equivalent to the 2-category of LCCCs-with-monads, or something of that sort. I think this is what Todd is getting at by talking about the “doctrine”. When you fix a doctrine of a kind of category, then that is supposed to determine (although there is no algorithm for this) a basic type theory with rules; then the “internal language” of any particular category in that doctrine is an augmentation of that basic type theory by axioms that represent the objects and morphisms of that category.
I think #62 hits the nail on its head perfectly and says what I was trying to say much more clearly. The deductive system / language / theory distinction is not as clear in type theory as it is in traditional logic, but what I would say that the difference Mike pointed out is precisely that. In my view, Martin-Löf type theory is a deductive system, a language with respect to that deductive system is a list of constant type and term symbols, and a theory with respect to a language is a deductively closed collection of judgements in that language.
Thanks, Mike!
I follow that. Please bear with me now when I ask yet another question (I am not trying to be obnoxious, I just would like to have this sorted out for myself and for communication with you and others):
By what you say, there are two things which we’d rather like to distinguish, but which are both called “type theories”, only with different qualifiers.
There is what you call “basic type theory”/”basic system of rules” and then there are “new type theories” obtained from this by adding “types and terms to it as axioms”. Indeed, you confirm now that an internal language is a “type theory”:
you can construct the type theory T whose axioms are precisely the objects and morphisms of C. This is the “internal logic” or “internal language” of C.
Good, that’s a relief. If this is so then we don’t need to change a bunch of $n$Lab entries (as would be the case if we adopted Zhen Lin’s standpoint).
I suppose this also refines your complaint above that the entry internal logic is “just a heuristic”. If I understand you correctly all that this entry is missing is some global statement at the beginning of the form “Fix a doctrine once and for all, and let $C$ be a category in this doctrine. Then the internal logic of $C$ is…”
But now here is finally my remaining question: if the “internal language” of some specific LCCC is “a type theory” by your above statement (albeit not a “basic” one) then the internal languag of some specific LCCC with a monad on it should be “a modal type theory, albeit not THE basic modal type theory”.
Right? I suppose what I am asking for is a clear terminology to distinguish between those “basic type theories”/”basic rules” and the “new type theories” which are “internal languages”, as you say.
I guess the ’theory’ of ’type theory’ doesn’t help. One talks of a first-order theory meaning something couched in first-order logic, with some specified predicate, relations, constants and axioms. Had it been, say, ’type calculus’, then ’a type theory’ would have been clearer.
I wouldn’t use “modal type theory” to mean a type theory with a monad on it, but rather a type theory with rules that model a monad on the semantics.
Unfortunately, I don’t think a clear terminology on the type-theoretic side exists to distinguish between “theories” and “doctrines”. You just have to get used to it. )-:
Hm, well, I wouldn’t have any problem getting used to the fact that the terminology is ambiguous were it not for the fact that I nevertheless hear not to use it this way or that way. But, yeah, I suppose that I have to get used to.
So is the lesson to draw from this discussion that nobody has devised a type theory with rules that model a monad on the semantics (#46), while it has been done in the case where the monad is idempotent?
Type theory with deduction rules for non-idempotent monads has been considered, see for instance section 2 of de Paiva et al..
What has not been done is the analog for $\infty$-monads in homotopy type theory.
To recall: the discussion above comes from me saying that since we know what the semantics of these is, and since whatever syntax for it one comes up it’s supposed to be equivalent to that semantics, analogous to the Seely-Clairambault-Dybjer equivalence, that it doesn’t hurt to speak about it. Mike feels that doing so doesn’t sufficiently highlight the trouble of actually writing down the syntax (which I assume he is working on, at least in part, for formulating HITs). Then I asked which words I could be excused to use for expressing the evident statement that does have a right to be expressed here. And it seems the answer is that such words have not been agreed on.
Yes, I dropped the $\infty$.
I wonder why the $\infty$ case is harder. Doesn’t truncation often make things more complicated?
Because of the coherences. Therefore I suppose, as we discussed in the other thread, that for $\infty$-monads which are explicitly given as the endomorphism monads of an $\infty$-adjunction it is much easier. While this is naturally the situation in the applications that I am currently considering, it is probably of little use for the discussion of HITs.
which I assume he is working on, at least in part, for formulating HITs
No, actually, the nice thing about HITs is that you can describe the initial algebras for a presented monad in terms of the presentation only, without having to make any sense of the monad itself.
Added pointer to Licata-Shulman-Riley 17 and Licata 18 also here at modal type theory, where it seems to more properly belong than at adjoint logic.
I posed the issue of the best way to record this work over here. I think when Mike’s $n$-theories ideas are settled (perhaps they are already) that would provide the ideal framework.
added pointer to the video recordings of Licata-Wellen 18
Added
It is informally understood that the purpose of modal type constructors in programming calculi is to control the flow of information between types. In order to lend rigorous support to this idea, we study the category of classified sets, a variant of a denotational semantics for information flow proposed by Abadi et al. We use classified sets to prove multiple noninterference theorems for modalities of a monadic and comonadic flavour. The common machinery behind our theorems stems from the the fact that classified sets are a (weak) model of Lawvere’s theory of axiomatic cohesion. In the process, we show how cohesion can be used for reasoning about multi-modal settings. This leads to the conclusion that cohesion is a particularly useful setting for the study of both information flow, but also modalities in type theory and programming languages at large.
added pointer to
Is the eagerly anticipated
appearing very soon? I’d like to mention it.
added the following pointers:
Felix Wellen, Geometry in Modal HoTT, talk at Geometry in Modal HoTT (2019) (video recording)
Egbert Rijke, Reflective subuniverses and modalities, talk at Geometry in Modal HoTT (2019) (video recording)
Egbert Rijke, Modal descent, talk at Geometry in Modal HoTT (2019) (video recording)
@David do you mean
A Fibrational Framework for Substructural and Modal Logics
Re #79 I hope so; the details are very fiddly and we keep having to change it around. Plus some of us had some personal issues that delayed things. But Dan is talking about it this week at HoTTEST if you want to hear the latest and the greatest.
Re #82, I look forward to it.
Re #81, no it’s the next instalment: modal unary type theory; modal simple type theory; modal dependent type theory, as explained here.
Added pointer also to the implentation on github.com/jozefg/blott
added pointer to
1 to 87 of 87