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 letter paper version

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.1 Languages and Formulas	1
1.2 Substitutions and Unification	3
1.3 Semantics of First Order Logics	4
1.4 Signed Formula Expressions	8
1.5 Partial Normal Forms	11
1.6 Bounds for Partial Normal Forms	17
1.7 Induced Quantifiers	21
2 Resolution	24
2.1 Introduction	24
2.2 Clauses and Herbrand Semantics	25
2.3 Clause Translation Calculi	27
2.4 Semantic Trees and Herbrand’s Theorem	31
2.5 Soundness and Completeness	33
2.6 Negative Resolution	36
3 Sequent Calculus	42
3.1 Introduction	42
3.2 Semantics of Sequents	44
3.3 Construction of Sequent Calculi	46
3.4 Equivalent Formulations of Sequent Calculi	54
3.5 The Cut-elimination Theorem for PL	57
3.6 The Cut-elimination Theorem for NL	65
3.7 Analytical Properties of PL	70
3.8 Interpolation	72
4 Natural Deduction	77
4.1 Introduction	77
4.2 Natural Deduction Systems	78
4.3 Normal Derivations	84
5 Approximating Propositional Logics	88
5.1 Introduction	88
5.2 Propositional Logics	89
5.3 Singular Approximations	90
5.4 Sequential Approximations	96
Bibliography	102