3 ms·
Intuitionistic propositional logic and natural deduction
- burakemir 6y agoThis 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. It seems the only other HN discussion about a post on natural deduction so far was this one: https://news.ycombinator.com/item?id=22324836 https://news.ycombinator.com/item?id=22324836 There is also one on Curry Howard: https://news.ycombinator.com/item?id=17748717 https://news.ycombinator.com/item?id=17748717 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. https://wadler.blogspot.com/2014/08/howard-on-curry-howard.html https://wadler.blogspot.com/2014/08/howard-on-curry-howard.h...