Tuesday, January 16, 2007

A note on my inference project

Earlier today I was at the library trying to find Structural Proof Theory, a book that Ole recommended, and I came across a book that looks like it will be useful for my side project on inference. It is Admissibility of Logical Inference Rules by Rybakov. It is not aimed at philosophers; not enough prose. (That was a joke.) It looks like it is a very technical discussion of the logic and math behind admissible inference rules. It has long sections on various flavors of propositional and modal logics as well as some stuff on first-order logics I didn't get to look at yet. I think it will flesh out some of the logical background on inference rules that I've been looking for.

Admissible and derivable rules were very briefly mentioned in my proof theory class last semester; no details. Last week in modal logic, Belnap pointed out that the connection between derivable rules and conditionals. With a derivable rule, you can always prove the conditional consisting of the conjunction of the premises as the antecedent and the conclusion as consequent. (This is for natural deduction style rules and propositional logic.) For admissible, non-derivable rules this is not the case. This is clear from the definition of admissible and derivable rules. For formulas A_i, the inference rule A_1,...,A_n/B is admissible iff all instances of the rule with substitutions of formulas for atomic propositions in the A_i,B are such that if the substituted in A_i hold, then the substituted in B holds too. A rule A_1,...,A_n/B is derivable if A_1,...,A_n|-B. Applying the deduction theorem gets the conditional in question.

To praise the book with faint damning, it has three problems. There are a fair few typos (based on my brief skimming; I've found a few so I'm guessing there are more), the index is awful, and it is too expensive to buy. That being said, it looks pretty useful.


Richard Zach said...

I'm not sure I understand your definition of derivable rule, or I don't see for what systems this is supposed to hold. In modal logic, A/[]A is usually a rule that's in the calculus, so it's presumably derivable (trivially). But A -> []A is not provable. But you said "natural deduction" so this kind of rule is probably excluded.

For classical logic, it seems to me, a rule is admissible iff A_1, ..., A_n |= B (if is obvious; only if: consider substitution instances of A_1, ..., A_n, B where the atoms are replaced by all combinations of TRUE and FALSE). And since classical propositional logic is strongly complete, the rule is admissible iff A_1, ..., A_n |- B, ie, the rule is derivable.

Shawn said...

Professor Zach,
I was trying to cut a few corners in writing up the definition. If it was unclear then I think I cut too many. The definition for derivable rule that I cited seems to be for any non-modal propositional logic (the book uses the phrase "superintuitionistic logic", although I confess I don't know what exactly that is). There looks to be a few differences when dealing with modal logics. I think Belnap's point was similarly restricted, although I will double check. He was talking about cut in natural deduction being admissible but not derivable, so there is some further information I need to get.

I was also mistaken in labelling the definition I was using as being for natural deduction. It is in an axiomatic framework with the single inference rule of modus ponens. (The inference rules were written like natural deduction rules, so I was slightly confused.) Belnap's discussion in terms of natural deduction and the book's presentation in terms of Hilbert style axiom systems "crossed beams," so to speak (and reference Ghostbusters).

The necessitation rule, A/[]A, you cited is not a derivable rule since you can't prove the conditional A->[]A.

You are probably right that for classical propositional logic with modus ponens all admissible rules are derivable. I will check on that later. Later chapters in the book deal with admissible rules for non-classical logics and general characterizations of non-derivable, admissible logics. Admisisble and derivable rules will not be equivalent for many of them, I imagine. Further posts fleshing that out will go up when (if?) I get through that material.

Ole Thomassen Hjortland said...

Sounds like an interesting book, Shawn. Haven't heard about it before, but definitely worth checking out.