Logblog: Richard Zach's Logic Blog

University of Calgary

UofC Navigation

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 (N_{n}, P_{n}) 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 N

_{2}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 N

_{2}are ¬(A ? ¬A) or A^{n}? A^{m}, for arbitrary n, m, while e.g. (A ? B) ? (B ? A), ¬A ? ¬¬A are in P_{3}.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 P

_{3}is open.

If you know of related or similar work, please comment at the previous post.

- Richard Zach's blog
- Log in to post comments

- Open Logic Project
- The LogBlog is Moving!
- Academic Genealogy Graphed
- CfP: Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics
- In Memoriam: Grigori Mints
- Previously Unknown Turing Manuscript Going to Auction
- Carnap (and Goodman and Quine) and Linguistics (Guest post by Darin Flynn)
- Carnap on "Syntax" vs "Semantics"