Home

Natural Deduction Reading for Beginners

The most active members of LtU for the most part already have a solid foundation in logic. For the rest of us interested in language design, but who are not already logicians here is a brief reading list on logic, focusing on natural deduction, the preferred method of expressing type systems.

More experienced members of LtU may perhaps consider contributing to the discussion with comments on the suggested reading or alternative suggestions.

[Edit: removed A History of Natural Deduction and Elementary Logic Textbooks by Jeff Pelletier and added several new links as suggested by Charles Stewart and falcon.]

By cdiggins at 2006-12-07 22:28 | Theory | other blogs | 20738 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

TAPL

Pierce's Types and Programming Languages has a short and easily read tutorial section on natural deduction that should be sufficient for programming needs. And it's a great book besides.

By Per Vognsen at Fri, 2006-12-08 00:29 | login or register to post comments

On the Unusual Effectiveness of Logic in Computer Science

for those who need motivation: On the Unusual Effectiveness of Logic in Computer Science. I once found a video of Moshe Vardi delivering a lecture of the same title, the voice quality was not very good but the talk itself was great....and surprisingly funny! If someone has a link to it, please post it.

By shahbaz at Fri, 2006-12-08 04:55 | login or register to post comments

Is it this one?

I found this (Real Media): http://webcast.rice.edu/speeches/20020417vardi.html

By Florian Häglsperger at Fri, 2006-12-08 13:40 | login or register to post comments

Avoid Pelletier

Pelletier is only interested in natural deduction as a medium for philosophers to construct proofs, and entirely ignores normalisation, which is the key to all of the applications in computer science. Pelletier's survey has interest as a comparative guide to different kinds of syntax you might find being called natural deduction, but it's not much use as an intro for LtUers.

Postscript: I'd recommend the first five chapters of Proofs and Types, which has been discussed several times here at LtU, for instance in Getting started.

By Charles Stewart at Fri, 2006-12-08 09:17 | login or register to post comments

Another Good Book but no normalization

If you just want to learn natural deduction I found Forbes Modern Logic to be an extremely good way to go (was used in a course I TAed).

Of course if things like normalization or cut-freeness are important this book won't have them. It is just a long introduction to natural deduction and semantic notions of validity.

It's what I would recommend starting with if your math background is weak but I'm sure some of the other books here are much better and more appropriate for people with stronger math backgrounds who don't need to go quite so slow and want advanced topics.

By logicnazi at Tue, 2006-12-12 19:50 | login or register to post comments

Proof and Disproof in Formal Logic

Proof and Disproof in Formal Logic: An Introduction for Programmers by Richard Bornat is a great introduction to natural deduction. It does a good job explaining all those things that are implied by everyone else. It can also be used with Jape, a simple proof assistant.

Unfortunately, this book is not available online, but you can preview the Google Books page.

By Sean Leather at Wed, 2009-07-22 15:29 | login or register to post comments