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

References:

- 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 - Matthias Baaz, Christian G. Fermüller, Gernot Salzer, Richard Zach,
**Labeled calculi and finite-valued logics**,*Studia Logica***61**(1998) 7–33 - 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 - 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 - 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.
- G. Rousseau, Sequents in many-valued logic I . Fundamenta Mathematicae 60 (1966) 23-33. Errata 61 (1967), 313.
- G. Rousseau, Sequents in many-valued logic II . Fundamenta Mathematicae 67 (1970) 125-131.
- 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. - Richard Zach,
**Proof Theory of Finite-Valued Logics** - MUltlog homepage: http://www.logic.at/multlog/

- 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

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<><> <><>< HREF="http://consequently.org" REL="nofollow" TITLE="greg at consequently dot org">Greg Restall<>

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<><> <><>< HREF="http://www.ucalgary.ca/~rzach/logblog/2005/09/many-sided-sequent-calculi-and-many.html" REL="nofollow" TITLE="zamalan at netvision dot net dot il">Anna Zamansky<>

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<><> <><>< HREF="http://www.ucalgary.ca/~rzach/logblog/2005/09/many-sided-sequent-calculi-and-many.html" REL="nofollow" TITLE="eric-yin at xaut dot edu dot cn">Eric<>