Re: [TYPES] Localizing Hypotheses?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I suspect you've been reading too much into the chosen name. I simply
understand it as making local (to each step of inference rule) something
that was global to the whole derivation -- the annoying upward dots
describing hypothetical judgments, first presented page 4 of the PDF you
link, and sometimes described as bracketing of hypotheses. It is clearly
explained as such in the lecture notes. "Localization" is a fine name in
this regard, and I would be surprised if it was related to the other uses
you mention in other ways than coincidence.

On Tue, Mar 3, 2015 at 12:06 AM, Gershom B <[email protected]> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> In the course notes for Automated Theorem Proving (2004) [1], Pfenning
> describes the introduction of contexts in a Natural Deduction system as
> "Localizing Hypotheses" (see section 2.3). I cannot find many other
> examples of this terminology. Is this just a felicitous turn of phrase, or
> is there literature that makes the connection explicit to familiar notions
> of localization in, for example, algebraic, category-theoretic, or
> topos-theoretic settings?
>
> [1] http://www.cs.cmu.edu/~fp/courses/atp/handouts/ch2-natded.pdf
>
> Thanks,
> Gershom
>