Rubrication

As you might know, I like logics. Notice that logic is in the plural. This might seem a bit strange to you. It certainly seems a bit strange to me. How can it be that there is more than one? There are quite a number of logics at this point. We pretty much started out with Aristotelian logic, ie. the logic of syllogism which you were probably forced to study in school. Aristotelian logic was formalised and generalised during the early part of last century and this formalism has come to be called Classical Logic or often just CL. This formalisation caused some to view with suspicion the outcome of various formal arguments. It gave rise to a more conservative 'constructive' logic which we will call Intuisionistic (or IL) whose informal interpretation is known as the Brouwer-Heyting-Kalmagorov interpretation or BHK. Basically in Classical logic you can make proofs about things for which you can not provide examples. This also happens however in Intuisionistic logi...

Thanks to my brother I got a really cool book on proof theory called "Basic Proof Theory". It has a bunch of nice features including a from the ground up presentation of proof theory that should be relatively accesible to anyone with a background in mathematics. It demonstrates some of the connections provided by the Curry-Howard correspondance (which is my favourite part of the book) . It also describe Second order logic, which is great because I've had very little formal exposure to this. Second order logic is really beautiful since you can define all the connectives in terms of ∀, ∀ 2 and →. If you pun ∀ and ∀ 2 you have a really compact notation. The book also forced me to learn some things I hadn't wrapped my head around. One of those was Gentzen style sequent calculus. This really turns out to be pretty easy when you have a good book describing it. I've even wrote a little sequent solver (in lisp) since I found the proofs so much fun. ...