Not signed in (Sign In)

Start a new discussion

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.
    • CommentAuthorUrs
    • CommentTimeSep 29th 2012
    • (edited Sep 29th 2012)

    I came to wonder about the words “empty context” in type theory, for what is really the context of the unit type. For there is also the context of the empty type.‘ That that might also seem to be called the “empty context”.

    I suppose nobody probably bothers to call the context of the empty type anything, because type theory over the empty type is the empty theory. :-)

    But still, it feel terminologogically unsatisfactory. Any suggestions?

    Would it not be better to speak of the unit context instead of the empty context for the context of the unit type?

    Also, I keep thinking that type theory in the context of the empty type is not entirely without use. For instance it appears in the type-theoretic version of what topos-theoretically is the base change maps over

    Type* \emptyset \to Type \to *

    and that is the codomain fibration

    H /TypeH \mathbf{H}_{/Type} \to \mathbf{H}

    with its strutcure as a pointed map remembered, since the point is

    *H /. * \simeq \mathbf{H}_{/\emptyset} \,.

    I don’t know yet if this is super-relevant for anything, but it seems non-irrlelevant enough not to preclude it from being speakable.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeSep 29th 2012

    Of course, the empty context is so named because it contains no types, which is different from containing the empty type or the unit type.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeSep 29th 2012

    Hm. It’s equivalent to the context of the unit type. In categorical semantics there is no distinction between the empty context and the context of the unit type. Both are interpreted as the slice over the terminal object.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeSep 29th 2012

    You need to learn to think syntactically as well as semantically. (-:

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeSep 30th 2012
    • (edited Sep 30th 2012)

    I don’t think I am misunderstanding something. I am suggesting that some standard terminology may be suboptimal.

    I think it is related to another standard but bad move, namely to write dummy Γ\Gamma-contexts

    ΓΓ \frac{ \Gamma \;\vdash\; \cdots }{ \Gamma \;\vdash \; \cdots }

    when working in a generic context. The appareance of the Γ\Gamma here serves no purpose except that it is a means to indicate that the context need not be the empty context.

    But maybe if we realized that this “empty context” is never actually empty but is the “unit context”, that there is always something in the context, we could drop those superfluous “Γ\Gammas” and just realize that

    \vdash \; \cdots

    means that we are working in some base context which might be however complicated. It just happens to be what we chose to be the base = unit = reference point.

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 30th 2012

    As for the Γ\Gamma’s, I would say that in sequent calculus they serve a purpose which is much like notations elsewhere in mathematics. Take for example some definition of a simplicial set where we write something like s i:(x 0,,x i,,x n)(x 0,,x i,x i,,x n)s_i: (x_0, \ldots, x_i, \ldots, x_n) \mapsto (x_0, \ldots, x_i, x_i, \ldots, x_n). The only component being acted on is x ix_i and you might say that the other x jx_j displayed are there as “filler”, but they do seem to serve a purpose in making precise how x ix_i is situated.

    It’s a common complaint that sequent calculus notation is heavy, and deductions therein cumbersome, but if the notation is suboptimal, the challenge is to come up with another notation that can achieve the same goals. One of the (if not the) biggest goals in sequent calculus is to establish a cut-elimination theorem, which involves consideration of various cases depending on the placement of the last connective introduced in each of the premises of an application of cut. Various manipulations will have to be performed where the ways formulas are situated need to be made precise.

    I heard somewhere recently – it might have been here at the forum – that the reason sequent calculus notation was invented was the difficulty in establishing cut elimination in other deductive systems and their notations. Now there are other alternatives to sequent calculus notation where the heaviness of the Γ\Gamma’s is no longer apparent and one can establish a cut-elimination or normalization algorithm (I am thinking for example of proof nets in linear logic, and one might imagine other similar string-diagram notations), but that alternative is more involved than keeping the sequent notation overall but deciding to abandon the Γ\Gamma’s in the description of rules.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeSep 30th 2012

    but they do seem to serve a purpose in making precise how x ix_i is situated.

    But do the dummy-“\Gamma”s serve any similar purpose?

    My impression is that the only purpose they serve is to indicate to the reader that “the context need not be empty”.

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 30th 2012

    I just tried to indicate that they do serve a similar purpose in sequent calculus, referring specifically to things like how one is to formulate the cut-elimination algorithm.

    • CommentRowNumber9.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 30th 2012

    Maybe I could illustrate this use in sequent calculus by writing down one of the cases for cut-elimination. Let’s see, we have a right-hand introduction rule for implication:

    Γ,ABΓABR\frac{\Gamma, A \vdash B}{\Gamma \vdash A \Rightarrow B}R\Rightarrow

    and a left-hand introduction rule for implication:

    Δ,B,ΩCΣAΔ,AB,Σ,ΩCL\frac{\Delta, B, \Omega \vdash C \qquad \Sigma \vdash A}{\Delta, A \Rightarrow B, \Sigma, \Omega \vdash C}L\Rightarrow

    and now one of the cases for cut-elimination is where we push the cut applications upward toward the axioms in a deduction tree, in the following manner: replace this application

    Δ,B,ΩCΣAΔ,AB,Σ,ΩCLΓ,ABΓABRΔ,Γ,Σ,ΩCcut\frac{\frac{\Delta, B, \Omega \vdash C \qquad \Sigma \vdash A}{\Delta, A \Rightarrow B, \Sigma, \Omega \vdash C}L\Rightarrow \qquad \frac{\Gamma, A \vdash B}{\Gamma \vdash A \Rightarrow B}R\Rightarrow}{\Delta, \Gamma, \Sigma, \Omega \vdash C}cut

    by these two

    Γ,ABΔ,B,ΩCΔ,Γ,A,ΩCcutΣAΔ,Γ,Σ,ΩCcut\frac{\frac{\Gamma, A \vdash B \qquad \Delta, B, \Omega \vdash C}{\Delta, \Gamma, A, \Omega \vdash C}cut \qquad \Sigma \vdash A}{\Delta, \Gamma, \Sigma, \Omega \vdash C}cut

    Don’t know whether this is really helpful to you. I mean, I think it’s good to be asking questions like this, but there are at least related contexts where lists of formulae Γ\Gamma serve as important placeholders.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeSep 30th 2012

    It still sounds to me like you are thinking exclusively semantically when you say that the empty context is not actually empty. Syntactically, the empty context is empty: it contains no variables. That’s definitely different from having a single variable of type unit. Moreover, the notion of context is logically prior to, and necessary for, the subsequent definition of any particular type forming operation, including the unit type.

    Type theorists do, however, frequently abuse notation by leaving out the unchanging ambient context Γ\Gamma. I don’t see anything wrong with that, once you’ve sufficiently internalized the fact that it is always there and you are confident that your reader has too.

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeOct 1st 2012

    A context is a list of assumptions, and the empty context is the empty such list.

    We consider the conclusions that follow from a context, which is contravariant, so naturally empty and unit are swapped.

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)