Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 9 of 9
Today I had an opportunity to speak to some type theorists about the meanings of these words. It seems that not all type theorists agree about them either. Per Martin-Lof and some other people said that natural deduction is about the general notion of “reasoning from assumptions”, perhaps not referring to a particular formal presentation but to the underlying “sort of reasoning”. But someone else said that for him, at least, natural deduction refers instead to systems built out of introduction and elimination rules, as our page natural deduction currently says. Perhaps I will edit it to mention the alternative points of view, when I am less tired.
I also learned that “logical framework” has multiple meanings. One of them is a particular style of metatheory for presenting certain classes of definitions of formal systems; this is the sense in which it is used in LF, twelf, etc. Its notable feature appears to be the unification of the meta-notion of conditional provability with the internal notion of hypothetical judgment. But apparently Martin-Lof uses the term “logical framework” in a different way, referring to some “meta” sort of -types that are used in order to describe the rest of the syntax of type theory; I didn’t get to the point yet of really understanding what that means. If and when I do, maybe I’ll record it at logical framework.
Finally, I learned another term which may be relevant for our previous discussion: a formal system. Perhaps this is the same as what was being referred to informally as a “proof system” or “deductive system”?
Thanks for asking! I thought I had heard of “deductive system” being used officially or semi-officially, and might have created a gray link for it, but when Urs asked me about “logical framework”, I assumed that was also an official term, and since it seemed to fit what we were discussing, I went ahead and linked “deductive system” to that. Which was clearly a premature thing to do.
Occasionally the nLab moves a little fast, and it’s good to slow down and really make sure we’ve got things straight. So thanks again.
I’m a little apprehensive about the name “formal system”, because that’s a phrase that I’ve become accustomed to use informally in a more inclusive way. I’m not sure how standard it is to use that phrase for this notion, but when it was used that way in an introductory lecture today, none of the type theorists present objected.
Yes, thanks for asking!
So there is apparently no semi-canonical textbook that would make a choice for all this terminology and to which one could point and say things like “…where we follow in terminology the standard textbook Smith-Jones (1985)”, is there?
I’ve made a lot of links to formal system, I think!
Well, unfortunately, after talking to some more type theorists today, I found out that “formal system” is not really a standard terminology, and that perhaps “deductive system” is at least a little more common. It sounds like there is no absolutely standard terminology, but I think we should have a page about this concept and we need to call it something, so right now I think probably “deductive system” is the best.
Anticipating (perhaps optimistically) no objections, I will now go rename the page and edit the references to it.
I am always in favor of descriptive terminology, and “deductive system” is more descriptive than “formal system”. I like that.
Since I had written “deductive system” earlier, I’m obviously in favor.
Although my grey links have been to ‘formal system’, I have no objections.
But note the cache bug, so here is a correct link: deductive system.
1 to 9 of 9