University of Calgary
UofC Navigation

Proof Theory of Finite-Valued Logics

Source

Diploma Thesis, Technische Universität Wien, Vienna, 1993
Technical Report TUW-E185.2-Z.1-93

Abstract

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

Download PDF

Download A4 paper version

This has the original pagination; page references to this version, please.

Download PDF

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