University of Calgary

# Many-sided Sequent Calculi and Many-valued Logics

## This website has moved!

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

Submitted by Richard Zach on Fri, 09/16/2005 - 7:39pm

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 = {v 1 , … v n }, you can analogously introduce an n -sided sequent Γ 1 | … | Γ n which means "for some i between 1 and n , and some A in Γ i , A has value v i ."

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 [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).

References:

1. Matthias Baaz, Christian G. Fermüller,
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/