Zach, Richard. 1993. “Proof Theory of Finite-Valued Logics.” Diplomarbeit, Vienna, Austria: Technische Universität Wien. DOI: 10.11575/PRISM/38803
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.
Table of contents
Preface | ii |
1 Basic Concepts | 1 |
| 1 |
| 3 |
| 4 |
| 8 |
| 11 |
| 17 |
| 21 |
2 Resolution | 24 |
| 24 |
| 25 |
| 27 |
| 31 |
| 33 |
| 36 |
3 Sequent Calculus | 42 |
| 42 |
| 44 |
| 46 |
| 54 |
| 57 |
| 65 |
| 70 |
| 72 |
4 Natural Deduction | 77 |
| 77 |
| 78 |
| 84 |
5 Approximating Propositional Logics | 88 |
| 88 |
| 89 |
| 90 |
| 96 |
Bibliography | 102 |
3 thoughts on “Proof Theory of Finite-Valued Logics”