@@ -15,4 +15,4 @@ Rather than continuing with the Agda course, I have begun to brush up on fundame ### Next Up -I'm in the middle of chapter 2 right now, which is on [intuitionistic logic](http://en.wikipedia.org/wiki/Intuitionistic_logic). My plan is to finish this chapter as well as chapters 3 and 4 on the *simply typed lambda-calculus* and the *Curry-Howard Isomorphism* respectively. As I'm reading this I'm taking notes that will be used for a post that clarifies the relationship between axioms, judgments, and implication that I mentioned earlier. In particular, chapter 2's [natural deduction](http://en.wikipedia.org/wiki/Natural_deduction) explanation as a formal version of the [BHK intepretation] of logical connectives in intuitionistic logic includes a simple definition of implication in terms of judgments (in the *introduction* and *elimination* rules). With chapters 1-4 done I think I'll be able to write the aforementioned post and be able to sleep soundly about the explanation. Once again, although I'm already familiar with the topics covered, the level of precision used in LCHI makes it a slow but gratifying read... highly recommended if you have the will-power =) +I'm in the middle of chapter 2 right now, which is on [intuitionistic logic](http://en.wikipedia.org/wiki/Intuitionistic_logic). My plan is to finish this chapter as well as chapters 3 and 4 on the *simply typed lambda-calculus* and the *Curry-Howard Isomorphism* respectively. As I'm reading this I'm taking notes that will be used for a post that clarifies the relationship between axioms, judgments, and implication that I mentioned earlier. In particular, chapter 2's [natural deduction](http://en.wikipedia.org/wiki/Natural_deduction) explanation as a formal version of the [BHK intepretation](http://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation) of logical connectives in intuitionistic logic includes a simple definition of implication in terms of judgments (in the *introduction* and *elimination* rules). With chapters 1-4 done I think I'll be able to write the aforementioned post and be able to sleep soundly about the explanation. Once again, although I'm already familiar with the topics covered, the level of precision used in LCHI makes it a slow but gratifying read... highly recommended if you have the will-power =) _posts/2009-11-02-progress-report-and-lchi.markdown a1694bbdbdbf1226fb24adf5c82b433a64a9fe56 Larry Diehl larrytheliquid@netbooktheliquid.(none) http://github.com/larrytheliquid/larrytheliquid.github.com/commit/15f1e0b1b61170b434de7b1f7191842387042ce6 15f1e0b1b61170b434de7b1f7191842387042ce6 2009-11-03T06:49:43-08:00 2009-11-03T06:49:43-08:00 A BHK link 1a34cc18b03ed8e4b2bda73073b2c6ab69d8be19 Larry Diehl larrytheliquid@netbooktheliquid.(none)