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.

DOI: 10.11575/PRISM/38803

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

Zach-1993-Proof-theory-of-finite-valued-logics

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