Here’s a more detailed summary of the paper I just mentioned, (Ciabattoni, Galatos, and Terui, From axioms to analytic rules in nonclassical logics, LICS 2008) courtesy of Agata:
The paper contains a first step towards the definition of a general procedure to turn Hilbert axioms into analytic structural rules in various formalisms. The result is based on the substructural hierarchy — a new classification (Nn, Pn) of formulas of Full Lambek calculus with exchange (FLe) which is similar to the arithmetic hierarchy except that it tracks polarity alternations instead of quantification alternations.
The paper contains an algorithm which allows for the automated generation of a) analytic sequent structural rules equivalent to axioms up to the class N2 b) analytic hypersequent structural rules equivalent to axioms up to the class P3 (modulo a technical issue about weakening)
Given any axiom up to P3, the algorithm consists of the following two steps: 1. structural rules equivalent in power with the original axiom are generated and 2. they are afterwards completed (in the sense of Knuth-Bendix) in order to preserve cut-elimination once added to (the hypersequent version of) FLe.
Examples of axioms in N2 are ¬(A ∧ ¬A) or An → Am, for arbitrary n, m, while e.g. (A → B) ∨ (B → A), ¬A ∨ ¬¬A are in P3.
In the same paper it was also shown that (single-conclusion) structural rules in sequent calculus can only capture properties (axioms) which already hold in intuitionistic logic and hence, e.g. to characterize (A → B) ∨ (B → A) hypersequents are needed.
The question of identifying the appropriate formalisms, beyond hypersequents, for dealing in a uniform way with axioms at levels higher than P3 is open.
If you know of related or similar work, please comment at the previous post.
Over lunch the other day, my friend and colleague Agata Ciabattoni told me about her paper at this year’s LICS, “From axioms to analytic rules in nonclassical logics“. In it, she and her co-authors Nikolaos Galatos and Kazushige Terui present an intriguing and very general result: Suppose you have a logic which can be axiomatized in full Lambek calculus with exchange (that’s intuitionistic logic without weakening or contraction, but with exchange) by adding axioms. If the additional axioms aren’t too complex, there’s a systematic way of generating an analytic hypersequent calculus for your logic, i.e., a systematic way of converting the additional axioms into a structural rule for a hypersequent calculus in such a way that cut is eliminable. This procedure applies to a wide range of substructural logics but also superintuitionistic logics. (UPDATE: more detail in the next post.) So that got us thinking: what other general, systematic approaches to generation of calculi are there? Agata’s approach generates calculi of a specific form (hypersequent calculi) from other calculi (Hilbert-style calculi). Then I know of two approaches that systematically generate calculi from a semantics. Arnon Avron, Beata Konikowska, and Anna Zamansky have been doing a lot of work on logics given by what they call non-deterministic matrices. I wrote a while ago about the approach I detailed in my undergraduate thesis, which goes back to work by Rousseau in the 1960s: systematic (i.e., automatic) generation of sequent, tableaux, natural deduction calculi for a logic given by finite truth tables. These are the only systematic results I know of, but that just shows my ignorance! There must be others! I’m sure there are general results in modal correspondence theory, for instance, to obtain axioms and perhaps tableaux systems, etc., for modal logics from conditions on frames. Can anyone help me (and Agata) out here?