Sunday, December 24, 2006

Naturally deducing

I worked through most of Prawitz's Natural Deduction. I was aided in this by two things: (1) the book is short and (2) a lot of the material is very similar to stuff I worked through in proof theory last term. I was surprised at how straightforward the proof of the normal proof theorem was given that Gentzen devised the sequent calculus in order to make meta-proofs like that simpler. I'm not complaining though. I thoroughly like natural deduction systems. He didn't talk about the inference rules as much as I thought he would. He talked about them some. I should rephrase: he didn't talk about them much in the way I was hoping he would although he explained the technical ideas behind them. He's trying to show how the natural deduction inference rules can constitute the meaning of the connectives (and quantification, modality, and abstraction?). One thing that was neat was the separation of some of the rules into inference rules and deduction rules. The rules for &, v-intro, exists-intro, forall-elim, ->-elim, and ex falso are proper inference rules. The v-elim, exists-elim, ->-intro, and forall-intro (I'm pretty sure forall-intro was in there, although it escapes me why) are deduction rules. This is because they all require additional deductions in order to be used. For example, the v-elim rule requires deductions from assumptions of each disjunct, so eliminating v in AvB would require deriving C from assumption A and deriving C from assumption B. Then you can infer to C. This seemed like a good distinction to make since it is a natural way of splitting the rules. I imagine that this distinction would get a little more action in the more general proof-theoretic semantics of, say, Brandom since there would just be more rules.

Another thing that I found interesting was the final chapters on the proof theories of second-order logic and modal logics. The main thing I'll note is how the intro and elim rules for the modalities mirrored the rules for quantifiers. I've heard this before in my modal logic classes, and I've seen this in the translation from modal logic to FOL, but the structure of the intro and elim rules for the quantifiers was the same (with a small caveat on the necessity intro rule) as that of the respective modalities. I was wondering how that would play out in the natural deduction proof theory of modal logic since I had only seen the axiom systems for the various modal logics.

No comments: