UofC Navigation

Friday, September 16, 2005

Many-sided Sequent Calculi and Many-valued Logics

Since Greg asked, I thought I'd give a brief survey of many-sided sequent calculi. The basic idea is simple and quite old (the first paper on it, by Kurt Schröter, is from 1955 [8]; the most detailed early papers is [6]). In the standard semantics for classical sequents, Γ ⇒ Δ means that either one of the formulas in Γ is false or one of the formulas in Δ is true. Now if you have more than the truth values true and false, say, a set of truth values V = {v1, … vn}, you can analogously introduce an n-sided sequent Γ1 | … | Γn which means "for some i between 1 and n, and some A ∈ Γi, A has value vi."

Once you've generalized the sequent notation and its semantics, you can also generalize the other usual stuff: introduction rules for connectives and quantifiers for the i-th position, n-sided axiom sequents, cut rules; based on more or less the same idea you can also get many-sided natural deduction [3] and clause transformation calculi for many-valued resolution. If you do it right, you also get soundness, completeness, cut elimination, Maehara lemma, midsequent theorem, jadda jadda jadda. The neat thing is that the process of constructing the sequent calculus can be completely automatized. In fact, the MUltlog system [5] lets you enter the truth tables for connectives and quantifiers of your n-valued logic L, and out comes a paper about sequent calculus and resolution for L (e.g., here's a paper about 3-valued Gödel logic). Exercise: try it out with Belnap's 4-valued bilattice logic (solution in [4]).

I worked out the details of this approach to proof-theory of finite-valued logics in excruciating detail in my undergraduate thesis, imaginatively entitled Proof Theory of Finite-valued Logics [9], but much if not most of the credit goes to my supervisor Matthias Baaz and colleagues at the TU Vienna, Chris Fermüller and Gernot Salzer. Gernot is mainly responsible for implementing MUltlog, and its companion MUltseq, a propositional finite-valued resolution prover (the latter jointly with Angel Gil).

The four of us also generalized the approach to sequent calculi with arbitrary labels (instead of sides) in [2]: so instead of having a label for each truth-value, e.g., you can have a label for every subset of the set of truth values. We showed that every finite-valued logic can be given a labelled sequent calculus which is sound and complete and enjoys cut elimination for certain sets of subsets of V as labels. In fact, we showed a converse to that as well: under suitable conditions, any labelled sequent calculus which enjoys cut-elimination and has all structural rules can be given a finite-valued semantics.

All these calculi have weakening and contraction, so there's still room for more work (e.g., for Greg): generalize all this to substructural logics. Chris and Matthias have a paper [1] on finite-valued intuitionistic calculi (i.e., many-sided sequents, but some sides restricted to only one formula).

  1. Matthias Baaz, Christian G. Fermüller, Intuitionistic Counterparts of Finitely-Valued Logics.
    In: 26th International Symposium on Multiple-valued Logic (IEEE Press, Los Alamitos, 1996), pp. 136–143
  2. Matthias Baaz, Christian G. Fermüller, Gernot Salzer, Richard Zach, Labeled calculi and finite-valued logics, Studia Logica 61 (1998) 7–33
  3. Matthias Baaz, Christian G. Fermüller, Richard Zach, Systematic construction of natural deduction systems for many-valued logics, 23rd International Symposium on Multiple Valued Logic. Sacramento. (IEEE Press, Los Alamitos, 1993) 208–213
  4. Matthias Baaz, Christian G. Fermüller, Richard Zach, Elimination of cuts in first-order many-valued logics, Journal of Information Processing and Cybernetics 29 (1994) 333–355
  5. Matthias Baaz, Christian G. Fermüller, Gernot Salzer, Richard Zach, MUltlog 1.0: towards an expert system for many-valued logics. International Conference on Automated Deduction (CADE'96), LNCS (LNAI) 1104, (Springer, 1996) 226-230.
  6. G. Rousseau, Sequents in many-valued logic I. Fundamenta Mathematicae 60 (1966) 23-33. Errata 61 (1967), 313.
  7. G. Rousseau, Sequents in many-valued logic II. Fundamenta Mathematicae 67 (1970) 125-131.
  8. Karl Schröter. Methoden zur Axiomatisierung beliebiger Aussagen- und
    Prädikatenkalküle. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 1 (1955) 241-251.
  9. Richard Zach, Proof Theory of Finite-Valued Logics, Diploma Thesis, Technische Universität Wien, Vienna, 1993
  10. MUltlog homepage: http://www.logic.at/multlog/


At September 19, 2005 3:25 AM , Anonymous Anonymous said...

Ooops. I feel so bad. I knew about a lot of this stuff (but not quite that many references) already, but I hadn't put two-and-two together. I was thinking rather more geometrically and less abstractly that it appeared to me at the time. Now there's more reading for me to do. Thankyou very much for the clarification and for setting me straight. 

Posted by Greg Restall

At October 30, 2005 9:55 AM , Anonymous Anonymous said...

Thank you for the extensive list of references. By the way, the work of A. Arnon and B. Konikowska on many-valued calculi for non-deterministic matrices (which are a generalization of the standard multi-valued matrix) (http://antares.math.tau.ac.il/~aa/articles/proof-nmatrices.pdf)
may also be of interest in this context. 

Posted by Anna Zamansky

At July 19, 2006 9:32 PM , Anonymous Anonymous said...

Hi, I'm now learning many-valued logic for research. I'm so confused about the conception of bifilter on bilattice, could you help me out with some simple explanation?  

Posted by Eric


Post a Comment

Links to this post:

Create a Link

<< Home