Talk:Natural deduction/Archive 1

Rewriting the article (e.g. along the lines of Martin-Löf's Siena Lectures)?

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)

First shot at rewriting the article

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)

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

Proofs and Types

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

• Talk:Curry–Howard
• Talk:Curry–Howard/Alt

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)

About the mention of "evident" and of the "judgment" vs. "statement" distinction

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)

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)

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? dbtfz^talk 06:11, 5 March 2006 (UTC)

Why is there a section on "natural deductive logic"?

Why is there a section on "natural deductive logic" pasted before the Motivation section? Should not nat.deductive logic be on a separate page? Does not seem to fit here, this is about Natural Deduction a la Gentzen, Prawitz, Martin-Loef... Andreas 2007-11-12 16:26 (MET)

Digging into the logs of Wikipedia, it appeared that this section was moved from page deductive reasoning by Comicist. It is indeed connected to natural deduction but to a so specific presentation of it that I moved it again to a specific page System L (Lemmon) in the same way as Fitch-style calculus has it own page. I hope it is OK for everyone. Hugo Herbelin (talk) 09:19, 15 March 2010 (UTC)

Premiss vs. Premise

The article uses "premiss" and "premise" in similar numbers. A quick google tells me that they're both valid but I think the article should be consistent in its usage and only use one of them. But which one? — welshbyte (talk) 04:56, 18 January 2008 (UTC)

The page had at this time 9 "premise" and 8 "premiss". A poll on site:edu pages and site:ac.uk pages says that "premise" is more common (ratio 150 in US and 40 in UK, ration 40 in US if "logic" is added, ratio 10 in UK). Wiktionary also considers "premise" to be the reference. Even though "premiss" is OK, I uniformly adopted "premise" for consistency of the spelling. Hugo Herbelin (talk) 12:04, 14 March 2010 (UTC)

Intuitionistic Logic?

The article says that it provides natural deduction within intuitionistic logic first 'for simplicity.' What's the reasoning behind this? Nobody is ever taught intuitionistic logic first, and never 'for simplicity.' 68.88.237.171 (talk) 00:17, 19 October 2008 (UTC)

Please grill me

I've added a reference to the MSc thesis of a former student of mine, Stouppa (2004). Since this is the kind of thing that just about could be regarded as self-promotion (i.e. promotion of scholarly allies), or a conflict of interest (i.e., have I really chosen the best reference to illustrate the point, or just one that supports the promotion of my own academic work?), I'd like to advertise the point, and invite questions anyone might have about the soundness of this citation. — Charles Stewart (talk) 08:54, 20 April 2009 (UTC)

That policy of wikipedia may be relevant when a subjective point of view exist. But maths have formal proofs, thus I think that is not an important point, nor I can consider it a personal promotion.

However, this article is baroque, place many logics and many inference systems in one place. That makes it very hard to read. It looks as an advanced research book, not an encyclopedia source which one may look for to understand certain topic. Natural deduction had an important impact in logic and many systems derived from it. That does not justify to pack everything in one article. That evolution should be explained, i.e. why and how natural deduction systems were developed for other logics and why the other logics exist, why are they different. That material is large to fit on one article, it should be mentioned in one, but explained in detail in an specific article for each topic. — Preceding unsigned comment added by 201.124.211.115 (talk) 18:37, 9 June 2017 (UTC)

Can Sequent Calculus not go to a seperate page?

Why put Natural deduction and Sequend Calculus on the same page? I think it would be better for both if they have their own page. (like the remark about Stouppa's thesis it is all about sequent calculus :( — Preceding unsigned comment added by 188.29.60.184 (talk) 00:08, 17 November 2011 (UTC)

I agree with you. This article mixes many different inference systems making it very confusing.

I know about types, and the Curry-Howard correspondence. Even so I find this article unclear. It seems to baroque for me. Too many concepts in one article. With no explanation on how each system relates to other, nor how the logics evolved. — Preceding unsigned comment added by 201.124.211.115 (talk) 18:23, 9 June 2017 (UTC)

Correct Inference Rules?

The inference rules are all additive. Additive inference rules are usually found in backward chaining proof search. But doesn't the original calculus consist of multiplicative rules. So instead of

Γ ⊢ π1 : A    Γ ⊢ π2 : B
------------------------ ∧I
Γ ⊢ (π1, π2) : A ∧ B

The correct formulation would be:

Γ ⊢ π1 : A    Δ ⊢ π2 : B
------------------------ ∧I
Γ, Δ ⊢ (π1, π2) : A ∧ B

Gentzen himself seems inconsequent in his NJ and NK presentation. He has structural rules, and his cut rule is also multiplicative, but for example the rule for conjunction is additive. Jan Burse (talk) 12:39, 13 April 2013 (UTC)

A question which may help to make the article clearer?

Hi, I'm french, my english is not perfect and I'm sorry for that, I don't understand something at all: Why this inference rule: $\qquad {\frac {A{\hbox{ prop}}}{\neg A{\hbox{ prop}}}}\ \neg _{F}$

For me it would mean that knowing that A is true, then A is false... such a deduction rules can't be true, so why to write it in the article?

Thanks for your answers! I hope it can help.

--Nicobzz (talk) 13:33, 25 April 2013 (UTC)

Sorry I finally undestood, it doesn't mean what I said, it just mean that if A is a proposition then not A is also a proposition.

--Nicobzz (talk) 13:39, 25 April 2013 (UTC)

The expression 'natural deduction'

Who coined the expression 'natural deduction'? Before it was coined what terminology was used? After it was coined what objections were made to it? BTW,in the 1970's I had a paper rejected immediately because its title included the expression 'natural deduction'. The editor, a former Vienna Circler, declared in his one-sentence rejection letter that all deduction is conventional. Thank you for reading my TALK.Tyro13 (talk) 19:05, 2 November 2014 (UTC)

See Gerhard Gentzen (1934-5). Perhaps Frege before him? See the sequent article for citations on usage in the 20th c. Rather than specific criticism, see the reactions in Foundations_of_mathematics#Foundational_crisis. See Frege's theorem, from Hume's principle, for a notable result (due to George Boolos). --Ancheta Wis   (talk | contribs) 08:48, 3 November 2014 (UTC)

Wow!!! how complicated easy things may be

The idea of natural deduction is simple, it has an introduction and elimination rule for each logical connective.

There is no need to present this subject in the typed version.

Natural deduction should have a more simple ease to read article, then extend it to predicate calculus, but I am not sure if the intuitionist logic should be included here.

The Curry-Howard correspondence deserves another article. Martin Löf type theory also deserves a separate article.

The typography is hard to read, it expands to the right of the screen.

If this article could be simplified and separated in a logical way, that would be great!

Everybody could read it. Now it aboard many concepts making it very confusing. — Preceding unsigned comment added by 201.124.211.115 (talk) 18:13, 9 June 2017 (UTC)