This piece is intended as an accessible intro; it talks about the beginnings of formal logic, how intuitionism in the debate on foundations of mathematics led to intuitionistic logic, and Gentzen's natural deduction.<p>It seems the only other HN discussion about a post on natural deduction so far was this one: <a href="https://news.ycombinator.com/item?id=22324836" rel="nofollow">https://news.ycombinator.com/item?id=22324836</a><p>There is also one on Curry Howard:
<a href="https://news.ycombinator.com/item?id=17748717" rel="nofollow">https://news.ycombinator.com/item?id=17748717</a><p>It's from there that I found "Howard on Curry Howard", a published response to a letter Phil Wadler wrote to William A. Howard. It provides an excellent hint how Martin-Löf's work on dependent types was influenced by the Curry-Howard correspondence and natural deduction.
<a href="https://wadler.blogspot.com/2014/08/howard-on-curry-howard.html" rel="nofollow">https://wadler.blogspot.com/2014/08/howard-on-curry-howard.h...</a>