This is the first comprehensive introduction to Display Logic in the context of generalized Gentzen calculi. After reviewing several standard and non-standard sequent-style proof systems for modal logics, the author carefully motivates and develops Display Logic, an important refinement of Gentzen's sequent calculus devised by N. Belnap. A general strong cut-elimination theorem is proved that covers a large class of display sequent calculi. Moreover, a proof-theoretic semantics of the modal operators is developed. Proof-theoretic characterizations are also obtained for the logical operations of systems associated with Tarskian structured consequence relations. These systems include constructive logics with strong negation. Using the embedding of intuitionistic logic in S4, display calculi are presented for certain subintuitionistic logics that may be used as monotonic base systems for semantics-based non-monotonic reasoning. Eventually, a first-order display calculus is defined. Its modal extension is general enough to avoid the provability of both the Barcan formula and its converse.
Author(s): Wansing H.
Series: Trends in Logic, Volume 3
Publisher: Kluwer
Year: 1998
Language: English
Pages: 265
Title ......Page 3
Copyright ......Page 4
Contents ......Page 5
Preface ......Page 9
CHAPTER ONE / Introduction ......Page 13
1.1 The problem of Gentzenizing modal logic ......Page 14
1.2 Standard sequent systems for normal modal logics ......Page 16
1.3 Rules as meaning assignments ......Page 19
1.5 Modularity and the Dosen Principle ......Page 22
1.6 Subformula property, cut, and analytic cut ......Page 23
1.7 Generality ......Page 25
2.1 Modal signs ......Page 27
2.2 Higher-level sequent systems ......Page 28
2.3 Higher-dimensional sequent systems ......Page 29
2.4 Higher-arity sequent systems ......Page 30
2.5 Hypersequents ......Page 34
2.6 Natural deduction systems ......Page 36
3.1 Gentzen terms ......Page 39
3.2 Residuation ......Page 42
3.3 The Display Theorem ......Page 46
3.4 Introduction rules ......Page 49
3.5 Completeness ......Page 55
4.1 Properly displayable logics ......Page 59
4.2 A case distinction and primitive reductions ......Page 60
4.3 Strong normalization ......Page 63
4.4 Displayable logics ......Page 67
4.5 Characterization of the properly displayable logics ......Page 69
4.6 Scope of the method ......Page 74
5.1 The problem of functional completeness ......Page 77
5.2 Proof-theoretic semantics ......Page 79
5.3 Functional completeness for Kt and K ......Page 83
6.1 The modal display system DKf ......Page 87
6.2 A display calculus for PDL~ ......Page 89
6.3 Reduction to a set of clauses ......Page 91
6.4 Decidability and completeness ......Page 94
6.5 In the absence of purity ......Page 97
CHAPTER SEVEN / Strong cut-elimination and labelled modal tableaux ......Page 99
7.1 The tableau calculus TQS5 ......Page 100
7.2 Primitive reductions ......Page 101
7.3 Strong normalization ......Page 106
7.4 Extensions of quantified K ......Page 110
7.5 Equivalence with Fitting's tableaux ......Page 112
8.1 Preliminaries ......Page 115
8.2 Positive logics ......Page 117
8.3 The higher-level sequent calculus G^ ......Page 119
8.4 Positive proof-theoretic semantics ......Page 120
8.5 Functional completeness for |~+ ......Page 124
8.7 Constructive logics ......Page 127
8.8 The higher-level sequent calculus Gjf ......Page 131
8.9 Constructive proof-theoretic semantics ......Page 132
8.10 Functional completeness for |~c ......Page 134
CHAPTER NINE / Constructive negation and the modal logic of consistency ......Page 139
9.1 Disproofs and contrariety ......Page 140
9.2 Negation as falsity ......Page 148
9.3 Negation as inconsistency ......Page 151
9.4 The relation between negation as falsity and negation as inconsistency ......Page 154
9.5 Semantics-based nonmonotonic reasoning ......Page 156
9.6 Choice of parameters ......Page 162
9.7 Modal logic of consistency over N4 ......Page 166
10.1 Subintuitionistic logics ......Page 167
10.2 Sequent systems for subintuitionistic logics ......Page 172
10.3 Soundness and completeness of DK(s) ......Page 173
10.4 The connection with temporalization ......Page 176
10.5 Extensions of K(s) and Kt(K(s))' ......Page 177
10.6 Proof of strong completeness ......Page 179
11.1 Hypersequential calculi ......Page 183
11.2 Display calculi ......Page 186
11.3 Mapping hypersequents into display sequents ......Page 196
11.4 Discussion ......Page 198
11.5 Other translations into DL ......Page 199
CHAPTER TWELVE / Predicate logics on display ......Page 201
12.1 A sequent calculus for KFOL ......Page 203
12.2 Display of predicate logics ......Page 205
12.3 A route from KFOL to FOL ......Page 207
12.4 Another route to FOL ......Page 213
12.5 Strong cut-elimination ......Page 216
12.6 The Barcan formula ......Page 217
12.7 Remaining proofs ......Page 219
13.1 DL and Fitch-style natural deduction ......Page 223
13.2 A new axiomatization of Kt ......Page 238
13.3 N4 redisplayed ......Page 241
13.4 Future work ......Page 246
BIBLIOGRAPHY ......Page 247
INDEX ......Page 259
