University of Calgary

# More on Ciabattoni, Galatos, and Terui

## This website has moved!

You are looking at an archived page. The website has moved to richardzach.org.

Submitted by Richard Zach on Wed, 12/17/2008 - 9:03am

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.