Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorZhen Lin
    • CommentTimeAug 11th 2011
    • (edited Aug 11th 2011)

    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 AA are the morphisms x:1Ax : 1 \to A in EE;

    I’m not claiming to fully understand the matter, but I think this is mistaken:

    1. What if AA has no global elements? For instance, AA could be a strict subobject of 11 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 XX are to be interpreted as the identity arrow 1:XX1 : 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.

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 11th 2011
    • (edited Aug 11th 2011)

    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.

    • CommentRowNumber3.
    • CommentAuthorZhen Lin
    • CommentTimeAug 11th 2011

    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.

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 11th 2011

    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.

    • CommentRowNumber5.
    • CommentAuthorTobyBartels
    • CommentTimeAug 11th 2011

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

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeAug 11th 2011

    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.

    • CommentRowNumber7.
    • CommentAuthorZhen Lin
    • CommentTimeAug 13th 2011
    • (edited Aug 13th 2011)

    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:ABf: A \to B, and each term σ:A\sigma : A, we have the term fσ:Bf \circ \sigma : B.
    • For terms σ:A\sigma : A and τ:B\tau : B, we have the term σ,τ:A×B\langle \sigma, \tau \rangle : A \times B.
    • For terms σ:B A\sigma : B^A and τ:A\tau : A, we have the term σ(τ):B\sigma(\tau) : B.
    • For a context Γ\Gamma, if Γ;x:Aσ:B\Gamma ; x : A \vdash \sigma : B, then Γλxσ:B A\Gamma \vdash \lambda x \, \sigma : B^A.
    • For terms σ:A\sigma : A and τ:𝒫(A)\tau : \mathcal{P}(A), we have the atomic formula στ\sigma \in \tau.
    • For terms σ:A\sigma : A and τ:A\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 σ:A\sigma : A in the context x 1:U 1;;x n:U nx_1 : U_1 ; \ldots ; x_n : U_n is interpreted as an arrow [σ]:U 1××U nA[\sigma] : U_1 \times \cdots \times U_n \to A.
    • Specifically, the variable x jx_j is interpreted as the projection [x j]:U 1××U nU j[x_j] : U_1 \times \cdots \times U_n \to U_j onto the jj-th factor.
    • The term fσf \circ \sigma is interpreted as f[σ]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 ε:B A×AB\epsilon : B^A \times A \to B is the evaluation map.
    • The term λxσ\lambda x \, \sigma is interpreted as the appropriate exponential transpose of [σ][\sigma].
    • The formula στ\sigma \in \tau is interpreted as the pullback of m:VA×𝒫(A)m : V \rightarrowtail A \times \mathcal{P}(A) along [σ],[τ]:UA×𝒫(A)\langle [\sigma], [\tau] \rangle : U \to A \times \mathcal{P}(A), where mm is the subobject of A×𝒫(A)A \times \mathcal{P}(A) classified by A:A×𝒫(A)Ω\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××U nU_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?

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeAug 13th 2011
    • (edited Aug 16th 2011)

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

    • CommentRowNumber9.
    • CommentAuthorzskoda
    • CommentTimeAug 15th 2011

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

    • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeAug 15th 2011

    Corrected link: arxiv/0704.2030.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeAug 16th 2011

    Zoran: Fixed, thanks!

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeNov 8th 2011

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