Talk:Natural deduction

From Wikipedia, the free encyclopedia

I once took a course in proof theory, and no real mention of "evident" or of the "judgment" vs. "statement" distinction(that I tought was from the Begriffsschrift) was made. I know the stroke for judgment evolved into the turnstyle, but I haven't (outside this article) heard any logicians of our time make this distinction. I also thought that the inductive characterization of formulas was rather universally accepted, and don't understand what it has specifically to do with natural deduction or why it should be repeated here. One can write it that way, at the cost of writing "phi true" instead of "phi" everywhere in one's deductions, but I don't understand what that buys us. I thought natural deduction was just the deductive calculus apparatus. Can someone explain to me why the "judgment," "evident," and the rules for constructing formulas are here? Vivacissamamente

Plead read Per Martin-Löf's Siena Lectures, linked right below. — Kaustuv 07:06, 2005 Apr 9 (UTC)
I will, but for the moment I was hoping for a much briefer explanation... please? Vivacissamamente 00:01, 4 May 2005 (UTC)
A short answer is that distinguishing judgments from propositions allows you to talk about judgements other than "phi true", like for example "phi false", useful in formulating classical logic; or "phi valid", used in Pfenning and Davies's formulation of modal logic (see References below). William Lovas 19:32, 11 May 2005 (UTC)

Sorry to be harsh, but this is a terrible article on natural deduction, peddling outdated philosophical gobbledygook. A much better and still accessible article would be along the lines of Martin-Löf's Siena Lectures. — Kaustuv 12:26, 2004 Aug 12 (UTC)

I agree. The current revision doesn't even mention Prawitz or Gentzen. At the very least, some reference to proof theory should be there and some discussion on how ND is different from sequent-type proofs. The ND rules for classical propositional logic (while present) should be presented in ND style as introduction and elimination rules. But that's just my opinion.
On the technical side, does anyone have any suggestions how to best format proofs in this wiki? Forget about showing trees, just simple line-by-line format with some scope indicators (perhaps indentation). Is there a simpler solution than using a table? MarkSweep 16:48, 12 Aug 2004 (UTC)
I've had limited success with <math> and \frac; see structural rule for some examples. Unfortunately I've never managed to use it for multi-line proof trees. Ideally Wikipedia would support certain LaTeX packages, like Paul Taylor's proof-trees package. Worst comes to worst one can always upload images, or use some proof linearization a-la Mizar or TPS — Kaustuv 20:38, 2004 Aug 12 (UTC)

I've taken a first shot at rewriting this article. I couldn't coax Wikipedia's feeble maths support into drawing good proof trees (it doesn't understand \displaystyle?!), so I've had to improvise with tables and preformatted text. — Kaustuv 20:23, 2004 Aug 14 (UTC)

Hmm... becoming rather longer than I'd expected. Please suggest parts to cut or merge elsewhere. — Kaustuv 15:56, 2004 Aug 16 (UTC)
I just noticed the changes you made this weekend. A lot of work, and it clearly shows. Vast improvement compared with the old version. I wouldn't split the material into different articles yet. Perhaps the comparison between ND and sequent calculus could eventually become a separate article, referenced by both the ND article and the sequent calculus article. Another item on the To Do list might be a discussion of Prawitz-style ND, since that's what's often associated with the term ND by people coming to it from outside of proof theory. MarkSweep 22:23, 16 Aug 2004 (UTC)
Interesting that you keep mentioning Dag Prawitz. I last read his book Natural Deduction (published sometime in the 60s) some ten years ago, so my memory of it is far from sharp, but I don't remember his presentation differing much from Gentzen's system NJ (from Untersuchungen ueber das logische Schliessen, 1935; incidentally, I found an excellent quote from this paper to add to the article). His main work was in applied proof theory right? Since you are more familiar with his work, you'll certainly do a better job of describing Prawitz-style natural deduction. — Kaustuv 00:05, 2004 Aug 17 (UTC)
OK, as far as I can tell now, Prawitz-style ND is basically the same as Gentzen-style ND. However, in some circles (philosophers, logicians who use ND as a tool as opposed to an object of investigation), the term Prawitz-style ND is used to refer to the use of proof trees, as opposed to Fitch-style ND, which refers to the linearized form. This might be an historical accident: Fitch's textbook on symbolic logic was published in the early 1950s, Gentzen's work might not have been well known outside of Germany, especially so close after WWII, so Prawitz's book from 1965 might have exposed a few people for the first time to tree-structured proofs. However, this is just speculation on my part. I'll add some remarks on linear vs. tree-structured proofs.
On a different subject, did you get the quote from Gentzen directly from the source? It would seem to be that it should end in "So ergab sich ein „Kalkül des natürlichen Schließens“." (note the extra s at the end to mark genitive case. MarkSweep 22:29, 18 Aug 2004 (UTC)
Ah, you are right about the missing s, of course! mea culpa — Kaustuv 22:53, 2004 Aug 18 (UTC)

Contents

[edit] History

The article would benefit from a treatment of the historical material in Prawitz's Appendix C to his "Natural Deduction": in particular it is worth mentioning that Jaskowski's version of natural deduction was presented 4 years before Gentzen's. ---- Charles Stewart 23:27, 18 Aug 2004 (UTC)

I've summarized a part of Szabo's account of the history of natural deduction from The Collected Papers of Gerhard Gentzen, North-Holland 1969 (ISBN 072042254X). Someone with a copy of Prawitz's book should cross-check and extend, as required. — Kaustuv 00:50, 2004 Aug 19 (UTC)
Another source might be Pelletier's paper on the history of ND. MarkSweep 01:14, 19 Aug 2004 (UTC)
Thanks for that link! It was very educational about the genealogy of the Fitch's marginal bar. By the way, I'm seeing strange symbols (a pound sign, a capital "I" with a diaresis, etc.) instead of the glyphs for the connectives in that paper. Is that a problem with my fonts? — Kaustuv 03:41, 2004 Aug 21 (UTC)
The Pelletier's paper (if it is the one I know), devotes also more to Jaskowski and his descendents than just a short note as here. Also, Jaskowski's system has been used in modern proof assistants (starting with Mizar, AFAIK it is now also default in Isabelle (Isar)). I may be biased though, since I work with Mizar. Josef Urban, 2004 Nov 30

[edit] Proofs and Types

I just noticed that there seem to be two articles on the Curry–Howard correspondence:

Neither of those is in good shape. Might be worth consolidating these two articles with what's already here. MarkSweep 01:29, 19 Aug 2004 (UTC)

See Talk:Curry–Howard for the story so far. My feeling is that the CH page should in time have some of the detailed development of logical calculi moved out to own pages. So for example Hilbert-style systems, which in some sense must be the precursors of natural deduction, should be ona page of their own. There is the distinct difficulty that 'Curry-Howard' means different things to different people. I don't think this is helped by a kind of 'munging' philosophy, that it's all really one idea - that tends to be how people talk about it, while they tend to learn it by following through one particular avatar in enough detail to convince themselves.

Charles Matthews 10:55, 21 Aug 2004 (UTC)

But in some sense isn't there one concept behind it all? After all there is a subtle isomorphism between natural deduction/normalisation and sequent calculus/cut-elimination and similarly a relationship between combinators and lambda calculi that looks quite deep. Girard's view is that proofs and typed term calculi are really the same object just looked at in different (and confusing) ways. That seems (roughly) right to me: proof and interaction nets seem to support that idea. Francis Davey 22:19, 18 May 2006 (UTC)

[edit] Parentheses

"π is a proof of A true", which is written symbolically as "π : A true". Where should the parentheses go in this statement: "π is a proof of (A true)", which is written symbolically as "π : (A true)", or "(π is a proof of A) true", which is written symbolically as "(π : A) true"?

"π : (A true)", of course, as "(π : A)" isn't a proposition. — Kaustuv July 3, 2005 13:38 (UTC)

[edit] Observation

This article seems to be mostly based on some particular views and ideas of Per Martin-Löf. Don't get me wrong—Martin-Löf is an excellent, well-respected logician, and I have no problem with having some of his ideas incorporated into the article. But it seems to me that the article should should not be dominated by his ideas. Rather, it should stick to the basics of natural deduction as it is generally taught in universities. It looks like some other Wikipedians have shared this concern (see above). Comments? dbtfztalk 06:11, 5 March 2006 (UTC)

Retrieved from "http://en.wikipedia.org../../../n/a/t/Talk%7ENatural_deduction_bd06.html"