Diploma Thesis, Technische Universität Wien, Vienna, 1993
Technical Report TUW-E185.2-Z.1-93
Several people have, since the 1950’s, proposed ways to generalize proof theoretic formalisms (sequent calculus, natural deduction, resolution) from the classical to the many-valued case. One particular method for systematically obtaining calculi for all finite-valued logics was invented independently by several researchers, with slight variations in design and presentation. The main aim of this report is to develop the proof theory of finite-valued first order logics in a general way, and to present some of the more important results in this area. This report is actually a template, from which all results can be specialized to particular logics.
The main results of this report are: the use of signed formula expressions and partial normal forms to provide a unifying framework in which clause translation calculi, sequent calculi, natural deduction, and also tableaux can be represented; bounds for partial normal forms for general and induced quantifiers; and negative resolution. The cut-elimination theorems extend previous results, and the midsequent theorem, natural deduction systems for many-valued logics as well as results on approximation of axiomatizable propositional logics by many-valued logics are all new.
- The MUltlog system will automatically construct many-sided calculi from given truth tables.
- The results about the positive sequent calculus were published in Elimination of cuts in first-order finite-valued logics.
- The results about natural deduction were published in Systematic construction of natural deduction systems for many-valued logics.
- The duality between positive and negative sequent systems and their relations to tableaux calculi was discussed in Dual systems of sequents and tableaux for many-valued logics.
- The results about approximating by finite-valued logics were published in Approximating propositional calculi by finite-valued logics and in updated and extended form in Effective Finite-Valued Approximations of General Propositional Logics.