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 - 8:31am

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?

- 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"

## Comments

Richard, on this issue I would like to recommend you and Agata to have a look at our paper <>Two's company: "The humbug of many logical values"<>, a preprint of which can be found < HREF="http://wslc.math.ist.utl.pt/ftp/pub/CaleiroC/05-CCCM-dyadic.pdf" REL="nofollow">here<>. We exhibit there a constructive procedure for reducing a 'sufficiently expressive' finite-valued into an alternative adequate (non-truth-functional) bivalued semantics, and show next how to extract 2-signed tableau systems from that. Other important papers on the issue are mentioned at the bibliography of that paper, in particular the paper by Carnielli at the JSL in 1987, where he extends the work of Rousseau that you mentioned.For an even more practical work on the automatic generation of classic-like (non-analytic) tableaux for finite-valued logics, I have delivered this year a paper at IJCAR in Sydney, where we implement the algorithm mentioned in the above paper in order to generate theory files ready to use by the <>Isabelle<> proof assistant. The corresponding paper, currently submitted for publication, is called <>Towards fully automated axiom extraction for finite-valued logics<>, and I will send a copy directly to your email and to anyone else who manifests interest on it. You might also like to have a look at < HREF="http://tinyurl.com/5cakro" REL="nofollow">this<> implementation in ML.Finally, on the extraction of axioms for modal systems, there is some nice work done by Renate Schmidt, please do have a look at her webpage.

"Superdeduction" deals with transforming certain kinds of definitional axioms into sequent calculus rules...Have a look on: http://hal.archives-ouvertes.fr/docs/00/14/67/35/PDF/superdeduction.pdfBest regards,Bruno Woltzenlogel Paleo< HREF="http://www.logic.at/people/bruno/" REL="nofollow">http://www.logic.at/people/bruno/<>