Displaying modal logic / Heinrich Wansing.

Format:

Book

Author/Creator:

Wansing, H. (Heinrich)

Contributor:

Class of 1939 Fund.

Series:

Trends in logic ; v. 3.

Trends in logic ; v. 3

Language:

English

Subjects (All):

Modality (Logic).

Physical Description:

xi, 252 pages : illustrations ; 25 cm.

Place of Publication:

Dordrecht [Netherlands] ; Boston : Kluwer Academic, [1998]

Contents:

1.1 The problem of Gentzenizing modal logic 2

1.2 Standard sequent systems for normal modal logics 4

1.3 Rules as meaning assignments 7

1.4 Uniqueness 10

1.5 Modularity and the Dosen Principle 10

1.6 Subformula property, cut, and analytic cut 11

Chapter 2 Sequents Generalized 15

2.1 Modal signs 15

2.2 Higher-level sequent systems 16

2.3 Higher-dimensional sequent systems 17

2.4 Higher-arity sequent systems 18

2.5 Hypersequents 22

2.6 Natural deduction systems 24

Chapter 3 Display logic 27

3.1 Gentzen terms 27

3.2 Residuation 30

3.3 The Display Theorem 34

3.4 Introduction rules 37

3.5 Completeness 43

Chapter 4 Properly Displayable Logics, Displayable Logics and Strong Cut-Elimination 47

4.1 Properly displayable logics 47

4.2 A case distinction and primitive reductions 48

4.3 Strong normalization 51

4.4 Displayable logics 55

4.5 Characterization of the properly displayable logics 57

4.6 Scope of the method 62

Chapter 5 A Proof-Theoretic Proof of Functional Completeness for Many Modal and Tense Logics 65

5.1 The problem of functional completeness 65

5.2 Proof-theoretic semantics 67

5.3 Functional completeness for Kt and K 71

Chapter 6 Modal Tableaux Based on Residuation 75

6.1 The modal display system DKf 75

6.2 A display calculus for PDL 77

6.3 Reduction to a set of clauses 79

6.4 Decidability and completeness 82

6.5 In the absence of purity 85

Chapter 7 Strong Cut-Elimination and Labelled Modal Tableaux 87

7.1 The tableau calculus TQS5 88

7.2 Primitive reductions 89

7.3 Strong normalization 94

7.4 Extensions of quantified K 98

7.5 Equivalence with Fitting's tableaux 100

Chapter 8 Tarskian Structured Consequence Relations and Functional Completeness 103

8.1 Preliminaries 103

8.2 Positive logics 105

8.3 The higher-level sequent calculus G 107

8.4 Positive proof-theoretic semantics 108

8.5 Functional completeness for 112

8.6 Negation as refutation 115

8.7 Constructive logics 115

8.8 The higher-level sequent calculus G 119

8.9 Constructive proof-theoretic semantics 120

8.10 Functional completeness for 122

Chapter 9 Constructive Negation and the Modal Logic of Consistency 127

9.1 Disproofs and contrariety 128

9.2 Negation as falsity 136

9.3 Negation as inconsistency 139

9.4 The relation between negation as falsity and negation as inconsistency 142

9.5 Semantics-based nonmonotonic reasoning 144

9.6 Choice of parameters 150

9.7 Modal logic of consistency over N4 154

Chapter 10 Displaying as Temporalizing 155

10.1 Subintuitionistic logics 155

10.2 Sequent systems for subintuitionistic logics 160

10.3 Soundness and completeness of DK ([sigma]) 161

10.4 The connection with temporalization 164

10.5 Extensions of K ([sigma]) and Kt(K([sigma]))' 165

10.6 Proof of strong completeness 167

Chapter 11 Translation of Hypersequents Into Display Sequents 171

11.1 Hypersequential calculi 171

11.2 Display calculi 174

11.3 Mapping hypersequents into display sequents 184

11.5 Other translations into DL 187

Chapter 12 Predicate Logics on Display 189

12.1 A sequent calculus for KFOL 191

12.2 Display of predicate logics 193

12.3 A route from KFOL to FOL 195

12.4 Another route to FOL 201

12.5 Strong cut-elimination 204

12.6 The Barcan formula 205

12.7 Remaining proofs 207

13.1 DL and Fitch-style natural deduction 211

13.2 A new axiomatization of Kt 226

13.3 N4 redisplayed 229

13.4 Future work 234.

Notes:

Includes bibliographical references (pages 235-246) and index.

Local Notes:

Acquired for the Penn Libraries with assistance from the Class of 1939 Fund.

ISBN:

079235205X

OCLC:

39391122