I added to logical framework some more description of the universe levels and some mention of the adequacy theorem.

]]>I un-hyperlinked “syntactic category” at logical framework, since the meaning here is different from that described at syntactic category.

]]>It seems to me that an “analytic presentation” of a dependent type theory (*sans* universes, for simplicity) inside a logical framework is rather similar to a pure type system with two sorts $\ast$ (for object-theory-types) and $\Box$ (for LF-types), with axiom $\ast:\Box$, rules $(\ast,\Box)$ and/or $(\Box,\Box)$, and perhaps augmented with a cumulativity $\ast\prec \Box$. Does this make any sense?

Ok, thanks! I clarified a bit.

]]>Okay, I removed that paragraph and added a simple example about the natural numbers which I hope clarifies things. (There’s also a similar point to be made about equality, which I went ahead and added to the section “Analytic presentation”.)

]]>Ok, I don’t quite understand what that means or how it solves the problem of comparing variables, but feel free to edit the page!

]]>Hello,

I was reading this article and one paragraph struck me as odd:

It’s worth noting that this design choice essentially renders LF incapable of representing object-theory variables in any other way than with HOAS. For ordinary usage of variables requires the ability to compare “variables” for equality and disequality, and since LF has no inductive types, we cannot define therein any type that could function as “variables” in this way.

It definitely *is* possible to represent variables/contexts via first-order encodings in LF, and this is not uncommon. The point is that the substitution operation is not defined as a function (which would require an induction principle) but rather as a relation (i.e., an LF-type family).

Hey, these recent edits are very nice. I think that I now have an idea of what a logical framework is. I even have an inkling that the concept just might be awesome.

]]>Thanks. I clarified the first one a bit; you are right on the other two.

]]>Thanks!

some basic questions:

after the item list of 3 kinds of LF types the statement

this turns out to be enough for everything we need

refers to the collection of all three items, not just the last one, right? So I have moved it out of the item context.

after the sentence starting with

Once we have set up

the next one started with “See there”. I have made that read “See (Harper)” — hopefully that’s what was meant.

In the section “Synthetic presentation” it starts saying “LF-type” for what previously was called “type” equipped with a warning. So I have changed these previous “types” also to “LF-types”. Okay?

I expanded a bunch at logical framework, based largely on Bob Harper’s talk at IAS and the notes from it (to which I also linked).

]]>added pointer to

]]>