Concerning the propositional logic, it might be worth mentioning that he gives (presumably the first) decision procedure for intuitionistic propositional logic. ]]>

Ah, I see. I went ahead and replaced the phrase simply by “for predicate logic” (since he didn’t give a separate system for propositional logic but just treated it as a fragment, and because at the time AFAIK there was no version of predicate logic to be “untyped” relative to), and slightly tweaked the ordering. Anyways, this was just a minor point – thanks to the people who have contributed to this article, which is pretty good overall.

]]>@NoamZeilberger: I agree. the quotes were actually added by me to a previous text which I bound with some additions to what in my view is an awkward phrase in need of improvement.

]]>Thanks for adding these interesting historical references. I think it’s a bit strange, though, to say that Gentzen developed natural deduction, cut-elimination, and so on “for ‘h-propositions’ in propositional logic and untyped predicate logic”. Besides being anachronistic, one could argue that these are the very concepts that made it possible to have a non-trivial theory of identity of proofs (which is why Gentzen is credited with initiating the study of “structural” proof theory). How about replacing that phrase simply by “for propositional logic and untyped predicate logic”?

]]>I’ve expanded the references at natural deduction mostly with some historical comments and done some cosmetics in the idea section.

]]>is there a reason

Not a good one, at least.

I have merged the pages.

]]>Speaking of logical frameworks, is there a reason why Elf and Edinburgh Logical Framework are separate pages?

]]>This is a great idea. I am planning to write more at logical framework which will partly answer this question, but first I need to finish asking my local type theorists about what “logical framework” means. (-:

]]>Okay, thanks. This last point I would just like to understand a little bit better.

What exactly is it that a “logical framework” achieves for a deductive system. It makes it “more formal”, is that what it is?

I am hoping that it is possible to root these notions here in “reality” by saying what each of these means in terms of somebody setting up an actual computer implementation of a type theory.

Can we maybe play through that? I think that would be worthwhile. I would like to have a dictionary where I hand you in the above order 1. a logical framework, 2. a deductive system, 3. a natural deduction systems, 4. an actual type theory, and you tell me what each of these steps means in terms of setting up a proof-checker for that type theory.

So there will be a piece of software, and we build it in stages. At the lowest stage it has a parser that reads in strings of the form

antecedent $\vdash$ succedent

and takes them apart into pairs of strings $(antecedent, succedent)$. Then in the next stage we gradually add to the software a rule for how to turn such strings into other strings (or maybe rather a rule to check if a list of such strings is a valid list of symbol manipulations).

In this kind of way of speaking, can one say what the piece of the software does that implements the “logical framework”, what the piece does that implements the “deductive system” and then the “natural deduction” specifically.

Do you see what I am after here?

]]>Yes, I think that’s basically right, except that a deductive system doesn’t *have* to be formulated in the particular kind of metatheory that goes by the name ’logical framework’.

Can I just double-check if I am now following the ambient dependency tree; is the following a correct organization of the notions it mentions:

At the beginning there is a logical framework.

Given that, we may formulate a deductive system.

One class of examples of deductive systems are systems of natural deduction.

- One subclass of examples of natural deduction are type theories.

Another class of examples of deductive systems are sequent calculi.

?

I have put it this way now into *deduction and induction - contents*. But let me know what you think.

Very nice. And, sure, I have removed the previous Examples-section.

]]>I have added a lot to the “Summary” section at natural deduction, based on what I have learned recently from Dan Licata and other type theorists. I would kind of like to remove entirely the section “Examples of type formation/introduction/elemination/computation rules”, since I felt it necessary to incorporate a couple of examples already into the “Summary” description, and then having a long list of “examples” seems like unnecessary duplication of the pages product type, sum type, etc. But I thought I should ask first before deleting; thoughts?

]]>Since the Idea section was so big, I put most of it in a Summary section instead. I also a few remarks about it along the way.

]]>