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.
There seems to be a small mistake in the current article for the Mitchell-Bénabou language. At the moment, it states
the variables of type $A$ are the morphisms $x : 1 \to A$ in $E$;
I’m not claiming to fully understand the matter, but I think this is mistaken:
Having broached the topic, I’d like to ask for some opinions on a couple of matters:
Firstly, is it worth trying to separate the syntactic and semantic sides of the Mitchell–Bénabou language? At the moment the article, like the corresponding section of Sheaves in Geometry and Logic, develops the formal language and its ‘canonical’ semantics (if I may coin a term) simultaneously. I feel this is confusing. (The first time I read about the Mitchell–Bénabou language, I got the impression that the canonical semantics were the only way to interpret it. This led to problems when I tried to play with even the simplest of non-trivial examples.)
Secondly, where should the division between the Mitchell–Bénabou language and Kripke–Joyal semantics be? The point of Kripke–Joyal semantics, as I understand it, is that it is easier to work with than the canonical semantics but is otherwise equivalent to it. Again, I don’t quite agree with the way Mac Lane and Moerdijk treat the subject: I think that the conclusions of Theorem VI.6.1 should be presented as definitions (with additions so as to give a fully inductive definition from the atomic terms), if only so that the definition of the ‘forcing’ relation $\Vdash$ would not have to be given in terms of canonical semantics.
Zhen Lin (Zhen for short? or would it be Lin?): you are absolutely right about variables. Please feel free to make the necessary corrections, as in Mac Lane-Moerdijk. (And: thanks!)
You are probably also right that the whole article deserves a closer look, and perhaps a good going-over.
Just ‘Zhen’ is fine. (‘Lin’ is the second half of my given name.)
I'd be quite happy to rewrite the whole article (as well as start the article for Kripke–Joyal semantics), but I thought it would be better to ask what people think than risk stepping on their toes.
Right: maybe it would be a good idea to hear from Toby first. Whatever happens, it might be nice to have some references. I seem to recall that Johnstone’s Topos Theory gives a traditional syntactic description of the Mitchell-Bénabou language, but I don’t have that book in front of me.
Yes, it’s the Right Thing to separate the language and the semantics.
I agree that syntax and semantics are good to separate, and it would be great to have more extensive pages on these, making clear the connection with internal logic and type theory.
I don’t have Johnstone’s books to refer to, but this is my view of the Mitchell-Bénabou language.
First, as a formal language:
Then, the canonical semantics:
The main difference between the above and Mac Lane and Moerdijk’s description is that I am distinguishing between propositional formulae and terms of type $\Omega$. I am not sure if this is a useful distinction to make in the context of a type theory; at any rate it somewhat reduces the expressiveness of the language by banning terms like $\rho (\sigma \in \tau)$, say. I am also interpreting formulae as subobjects, rather than as classifying arrows — this seems like a more general approach that could be applied to Heyting categories. Any thoughts?
There are many different ways to express the internal language of a topos. It’s definitely true that distinguishing between propositional formulae and terms of type $\Omega$ generalizes more easily to the internal logic of categories that lack subobject classifiers. On the other hand, the current version of the page Mitchell-Benabou language asserts that it is precisely a language without this distinction that the name “Mitchell-Benabou language” refers to (as opposed to other versions of the internal language of an elementary topos). Let’s look at the literature…
In the Elephant, Johnstone distinguishes between formulae and terms of type $\Omega$, which is entirely reasonable since he spends a lot of time on categories with less structure. As far as I can tell, however, he does not use the name “Mitchell-Benabou language” there.
In Johnstone’s 1977 book “Topos Theory”, I find the following passages:
This idea was first made explicit by W. Mitchell [85]; subsequently, various “improved” descriptions of $L_{\mathcal{E}}$ have been given by J. Bénabou [24], G. Osius [94] and M. Fourman [35], among others. The version which we describe here does not correspond precisely to any of these…
(He then goes on to describe a version of the internal language in which formulae are identified with terms of type $\Omega$, and terms are interpreted by morphisms in the category, so that formulae in particular are identified with morphisms into $\Omega$.)
The principal respect in which our description of $L_{\mathcal{E}}$ differs from those of Bénabou and Osius is in the identification of formulae with terms of type $\Omega$. This seems a reasonable simplification from our point of view…
There is an alternative interpretation of the formulae of $L_{\mathcal{E}}$ (called the “external interpretation” by Osius) in which a formula $\phi$… is interpreted as a statement about generalized elements… The rules for this interpretation are commonly known as Kripke-Joyal semantics; they are a development of S. Kripke’s original semantics [173] for modelling intuitionistic logic in what was essentially a topos of presheaves….
…in Kripke’s original semantics, disjunction and existential quantification were given “on-the-spot” interpretations similar to that for conjuction. The reason is that Kripke was concerned with [a presheaf topos] and therefore restricted the objects… to be representable functors; the Yoneda Lemma easily implies that these are projective… so that the epis… are automatically split. For a general topos, the need for a “local” interpretation of existentiation… was first emphasized by A. Joyal…
(Side note: I don’t think I’ve ever encountered the word “existentiation” before!)
Johnstone’s reference [85] is Mitchell’s “Boolean topoi and the theory of sets,” which describes (the Boolean version of) an internal language in which (if I’m reading it correctly), formulas are distinguished from terms of type $\Omega$, but are nevertheless interpreted by morphisms into $\Omega$ rather than by subobjects. Mitchell also says at the beginning:
The discussion below is intended only to outline results of Lawvere and Tierney and to establish our notation. The constructions and proofs can be found in [seminar notes of Benabou and Celeyrette] or [Lawvere and Tierney, to appear].
This post was originally longer, but somehow the forum software truncated it upon submission, and I don’t have the energy to rewrite it all. Suffice it to say that Osius seems to do the same thing that Mitchell does (in a non-Boolean context), and I don’t have easy access to any of the other references.
So maybe this should be called the Lawvere-Tierney-Benabou-Celeyrette-Mitchell-Osius-Johnstone language? (-:
(ad Mike): Johnstone’s Topos theory book is more like 1977 than above mistyped 1970 (with a preprint version circulating probably a couple of years earlier, say 1975). Durov’s thesis (arxiv/0704.2030) has also a nice exposition of Kripke-Joyal seminatics.
Corrected link: arxiv/0704.2030.
Zoran: Fixed, thanks!
I have started a stub for Kripke-Joyal semantics, just so that the term links to somewhere
1 to 12 of 12