Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorZhen Lin
   • CommentTimeAug 11th 2011
   • (edited Aug 11th 2011)
   • PermaLink
   Author: Zhen Lin
   Format: MarkdownItexThere seems to be a small mistake in the current article for the [[Mitchell-Benabou+language|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: 1. What if $A$ has no global elements? For instance, $A$ could be a strict subobject of $1$ in the topos of sheaves over a topological space. 2. But ignoring the issue of having enough global elements, this seems to be _identifying_ variables with (generalised) elements of an object. Shouldn't variables simply be formal symbols, which are interpreted as, well, varying elements? My main point is that we would like an unlimited supply of variables for each type and directly identifying variables with elements hinders this. (On the other hand, I think the quote, exactly as it stands, is a perfectly good definition of a _constant_.) 3. Finally, an appeal to authority: Mac Lane and Moerdijk [1994, p. 298] say that variables of type $X$ are to be interpreted as the identity arrow $1 : X \to X$. --- 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.

   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:

   1. What if $A$ has no global elements? For instance, $A$ could be a strict subobject of $1$ in the topos of sheaves over a topological space.
   2. But ignoring the issue of having enough global elements, this seems to be identifying variables with (generalised) elements of an object. Shouldn’t variables simply be formal symbols, which are interpreted as, well, varying elements? My main point is that we would like an unlimited supply of variables for each type and directly identifying variables with elements hinders this. (On the other hand, I think the quote, exactly as it stands, is a perfectly good definition of a constant.)
   3. Finally, an appeal to authority: Mac Lane and Moerdijk [1994, p. 298] say that variables of type $X$ are to be interpreted as the identity arrow $1 : X \to X$.

   ---

   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.

2. • CommentRowNumber2.
   • CommentAuthorTodd_Trimble
   • CommentTimeAug 11th 2011
   • (edited Aug 11th 2011)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexZhen 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.

   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.

3. • CommentRowNumber3.
   • CommentAuthorZhen Lin
   • CommentTimeAug 11th 2011
   • PermaLink
   Author: Zhen Lin
   Format: MarkdownJust ‘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.

   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.

4. • CommentRowNumber4.
   • CommentAuthorTodd_Trimble
   • CommentTimeAug 11th 2011
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexRight: 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.

   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.

5. • CommentRowNumber5.
   • CommentAuthorTobyBartels
   • CommentTimeAug 11th 2011
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexYes, it's the Right Thing to separate the language and the semantics.

   Yes, it’s the Right Thing to separate the language and the semantics.

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeAug 11th 2011
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI 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 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.

7. • CommentRowNumber7.
   • CommentAuthorZhen Lin
   • CommentTimeAug 13th 2011
   • (edited Aug 13th 2011)
   • PermaLink
   Author: Zhen Lin
   Format: MarkdownItexI 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: * **Types**: One for each object. * **Atomic terms**: An unlimited supply of variables for each type. * **Function symbols**: For each arrow $f: A \to B$, and each term $\sigma : A$, we have the term $f \circ \sigma : B$. * For terms $\sigma : A$ and $\tau : B$, we have the term $\langle \sigma, \tau \rangle : A \times B$. * For terms $\sigma : B^A$ and $\tau : A$, we have the term $\sigma(\tau) : B$. * For a context $\Gamma$, if $\Gamma ; x : A \vdash \sigma : B$, then $\Gamma \vdash \lambda x \, \sigma : B^A$. * For terms $\sigma : A$ and $\tau : \mathcal{P}(A)$, we have the atomic formula $\sigma \in \tau$. * For terms $\sigma : A$ and $\tau : A$, we have the atomic formula $\sigma = \tau$. * The rest of the usual higher-order logic formula-forming rules. Then, the canonical semantics: * A term $\sigma : A$ in the context $x_1 : U_1 ; \ldots ; x_n : U_n$ is interpreted as an arrow $[\sigma] : U_1 \times \cdots \times U_n \to A$. * Specifically, the variable $x_j$ is interpreted as the projection $[x_j] : U_1 \times \cdots \times U_n \to U_j$ onto the $j$-th factor. * The term $f \circ \sigma$ is interpreted as $f \circ [\sigma]$. * The term $\langle \sigma, \tau \rangle$ is interpreted as the arrow $\langle [\sigma], [\tau] \rangle$ obtained by the universal property of the product. * The term $\sigma(\tau)$ is interpreted as the composite $\epsilon \circ \langle [\sigma] \times [\tau] \rangle$, where $\epsilon : B^A \times A \to B$ is the evaluation map. * The term $\lambda x \, \sigma$ is interpreted as the appropriate exponential transpose of $[\sigma]$. * The formula $\sigma \in \tau$ is interpreted as the pullback of $m : V \rightarrowtail A \times \mathcal{P}(A)$ along $\langle [\sigma], [\tau] \rangle : U \to A \times \mathcal{P}(A)$, where $m$ is the subobject of $A \times \mathcal{P}(A)$ classified by $\in_A : A \times \mathcal{P}(A) \to \Omega$. * The formula $\sigma = \tau$ is interpreted as the equaliser of $[\sigma]$ and $[\tau]$. * The compound formulae are interpreted using the corresponding operations in the Heyting algebra of subobjects of $U_1 \times \cdots \times U_n$. 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?

   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:

   • Types: One for each object.
   • Atomic terms: An unlimited supply of variables for each type.
   • Function symbols: For each arrow $f: A \to B$, and each term $\sigma : A$, we have the term $f \circ \sigma : B$.
   • For terms $\sigma : A$ and $\tau : B$, we have the term $\langle \sigma, \tau \rangle : A \times B$.
   • For terms $\sigma : B^A$ and $\tau : A$, we have the term $\sigma(\tau) : B$.
   • For a context $\Gamma$, if $\Gamma ; x : A \vdash \sigma : B$, then $\Gamma \vdash \lambda x \, \sigma : B^A$.
   • For terms $\sigma : A$ and $\tau : \mathcal{P}(A)$, we have the atomic formula $\sigma \in \tau$.
   • For terms $\sigma : A$ and $\tau : A$, we have the atomic formula $\sigma = \tau$.
   • The rest of the usual higher-order logic formula-forming rules.

   Then, the canonical semantics:

   • A term $\sigma : A$ in the context $x_1 : U_1 ; \ldots ; x_n : U_n$ is interpreted as an arrow $[\sigma] : U_1 \times \cdots \times U_n \to A$.
   • Specifically, the variable $x_j$ is interpreted as the projection $[x_j] : U_1 \times \cdots \times U_n \to U_j$ onto the $j$-th factor.
   • The term $f \circ \sigma$ is interpreted as $f \circ [\sigma]$.
   • The term $\langle \sigma, \tau \rangle$ is interpreted as the arrow $\langle [\sigma], [\tau] \rangle$ obtained by the universal property of the product.
   • The term $\sigma(\tau)$ is interpreted as the composite $\epsilon \circ \langle [\sigma] \times [\tau] \rangle$, where $\epsilon : B^A \times A \to B$ is the evaluation map.
   • The term $\lambda x \, \sigma$ is interpreted as the appropriate exponential transpose of $[\sigma]$.
   • The formula $\sigma \in \tau$ is interpreted as the pullback of $m : V \rightarrowtail A \times \mathcal{P}(A)$ along $\langle [\sigma], [\tau] \rangle : U \to A \times \mathcal{P}(A)$, where $m$ is the subobject of $A \times \mathcal{P}(A)$ classified by $\in_A : A \times \mathcal{P}(A) \to \Omega$.
   • The formula $\sigma = \tau$ is interpreted as the equaliser of $[\sigma]$ and $[\tau]$.
   • The compound formulae are interpreted using the corresponding operations in the Heyting algebra of subobjects of $U_1 \times \cdots \times U_n$.

   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?

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeAug 13th 2011
   • (edited Aug 16th 2011)
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThere 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? (-:

   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? (-:

9. • CommentRowNumber9.
   • CommentAuthorzskoda
   • CommentTimeAug 15th 2011
   • PermaLink
   Author: zskoda
   Format: MarkdownItex(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](http://arxiv.org/math/abs/0704.2030)) has also a nice exposition of Kripke-Joyal seminatics.

   (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.

10. • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeAug 15th 2011
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexCorrected link: [arxiv/0704.2030](http://arxiv.org/abs/0704.2030).

    Corrected link: arxiv/0704.2030.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeAug 16th 2011
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexZoran: Fixed, thanks!

    Zoran: Fixed, thanks!

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeNov 8th 2011
    • PermaLink
    Author: Urs
    Format: MarkdownItexI have started a stub for [[Kripke-Joyal semantics]], just so that the term links to somewhere

    I have started a stub for Kripke-Joyal semantics, just so that the term links to somewhere