Proof Theory of Finite-Valued Logics

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.

Table of contents

Prefaceii
1 Basic Concepts1

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 Resolution24

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 Calculus42

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 Deduction77

4.1 Introduction

77

4.2 Natural Deduction Systems

78

4.3 Normal Derivations

84
5 Approximating Propositional Logics88

5.1 Introduction

88

5.2 Propositional Logics

89

5.3 Singular Approximations

90

5.4 Sequential Approximations

96
Bibliography102

3 thoughts on “Proof Theory of Finite-Valued Logics

Leave a Reply

Your email address will not be published. Required fields are marked *