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.
Note: The MUltlog system will automatically construct many-sided calculi from given truth tables.
Download A4 paper version (This has the original pagination; page references to this version, please.)
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 |