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.
   • CommentAuthorUrs
   • CommentTimeSep 29th 2012
   • (edited Sep 29th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI 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 $$ \emptyset \to Type \to * $$ and that is the [[codomain fibration]] $$ \mathbf{H}_{/Type} \to \mathbf{H} $$ with its strutcure as a _pointed_ map remembered, since the point is $$ * \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.

   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

   $$\emptyset \to Type \to *$$

   and that is the codomain fibration

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

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

   $$* \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.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeSep 29th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexOf course, the empty context is so named because it contains *no* types, which is different from containing the empty type or the unit type.

   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.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeSep 29th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexHm. 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.

   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.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeSep 29th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexYou need to learn to think syntactically as well as semantically. (-:

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

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeSep 30th 2012
   • (edited Sep 30th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI 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 "$\Gamma$s" 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.

   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 “$\Gamma$s” 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.

6. • CommentRowNumber6.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 30th 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexAs 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, \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_i$ and you might say that the other $x_j$ displayed are there as "filler", but they do seem to serve a purpose in making precise how $x_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.

   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, \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_i$ and you might say that the other $x_j$ displayed are there as “filler”, but they do seem to serve a purpose in making precise how $x_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.

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeSep 30th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItex> but they do seem to serve a purpose in making precise how $x_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".

   but they do seem to serve a purpose in making precise how $x_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”.

8. • CommentRowNumber8.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 30th 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI 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.

   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.

9. • CommentRowNumber9.
   • CommentAuthorTodd_Trimble
   • CommentTimeSep 30th 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexMaybe 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: $$\frac{\Gamma, A \vdash B}{\Gamma \vdash A \Rightarrow B}R\Rightarrow$$ and a left-hand introduction rule for implication: $$\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 $$\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 $$\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.

   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:

   $$\frac{\Gamma, A \vdash B}{\Gamma \vdash A \Rightarrow B}R\Rightarrow$$

   and a left-hand introduction rule for implication:

   $$\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

   $$\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

   $$\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.

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeSep 30th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexIt 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.

    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.

11. • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeOct 1st 2012
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexA 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.

    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.