Natural Deduction, Hybrid Systems and Modal Logics (eBook)

Andrzej Indrzejczak is professor of logic and Head of the Department of General Methodology at the University of Lodz, Poland. His scientific interests include the proof theory for non-classical logics, the philosophy of logic and the methodology of science. He is the author of three books and numerous papers concerned mainly with the investigation of proof techniques for non-classical logics, published e.g. in Bulletin of the Section of Logic, Logic Journal of the IGPL, Logic and Logical Philosophy, Logica Trianguli, and Studia Logica.

Contents 6
Introduction 12
1 Preliminaries 25
1.1 Classical and Free Logic 25
1.1.1 Basic Propositional Language 25
1.1.2 The Language of First-Order Logic 28
1.1.3 Some Reasons for Introducing FQL 30
1.1.4 Formalization of CQLI and FQLI 32
1.1.5 Important Derived Notions 38
1.2 Deductive Systems, Rules, Proofs 41
1.2.1 Deductive Systems 41
1.2.2 Calculus 42
1.2.3 Realization 43
1.2.4 Extensions and Simulations 46
1.2.5 Semantical Side 48
1.2.6 Types of Deductive Systems 49
2 Standard Natural Deduction 52
2.1 Origins of ND 53
2.2 Preliminary Characterization 55
2.3 Data Structures 57
2.3.1 F-Systems 57
2.3.2 S-Systems 59
2.4 Trees or Sequences? 62
2.4.1 Problems with Trees 62
2.4.2 Problems with Linear Proofs 64
2.4.3 Suppes' Format 67
2.5 System KM 69
2.5.1 Rules 69
2.5.2 Realization 71
2.5.3 Derivations 74
2.5.4 The Original Formulation of KM 77
2.6 Adequacy of KM 79
2.7 ND for First-Order Logic 81
2.7.1 Gentzen Systems 81
2.7.2 Kalish/Montague Rules for CQL 83
2.7.3 Gentzen's Variant of KM 86
2.7.4 KM for Free Logic 88
2.7.5 Introduction of Parameters 90
2.7.6 Gentzen's Variant of KMP 92
2.7.7 KM with Parameters for Free Logic 96
2.7.8 Identity 97
3 Other Deductive Systems 99
3.1 Sequent Systems and Tableaux 100
3.1.1 Sequent Calculus 100
3.1.2 Tableau Systems 106
3.2 Resolution and Davis/Putnam Procedure 109
3.2.1 Resolution 109
3.2.2 Davis/Putnam System 112
3.3 Cut and Complexity of Proof 113
4 Extended Natural Deduction 119
4.1 Analytic and Universal Versions of ND 120
4.1.1 Analyticity 122
4.1.2 KE and ND 124
4.2 System AND1 127
4.2.1 Hintikka Sets 130
4.2.2 Proof Search Procedure for AND1 133
4.2.3 Optimization 138
4.3 System AND2 139
4.4 Resolution and ND Combined 148
4.4.1 Clauses Introduced 149
4.4.2 System RND 152
4.4.3 Simulation of Resolution and DP in RND 155
4.4.4 RND for First-Order Logic 159
5 Survey of Modal Logics 161
5.1 Basic Modal and Tense Language 161
5.2 Modal Logics in General 164
5.3 Axiomatic Approach to Modal Logics 167
5.3.1 Deducibility 173
5.4 Relational Semantics 174
5.4.1 Interpretation 176
5.4.2 Normal Logics 177
5.4.3 Expressive Strength of Ordinary Modal Language 179
5.4.4 Regular Logics 183
5.4.5 Weak Logics 184
5.4.6 Entailment 186
5.5 Completeness, Decidability and Complexity 187
5.6 First-Order Modal Logics 191
5.6.1 Introductory Remarks 191
5.6.2 Identity 194
5.6.3 Semantics 197
5.6.4 Some Logics 202
6 Standard Approach to Basic Modal Logics 206
6.1 Standard Sequent Calculi and Tableau Systems 207
6.1.1 Historical Remarks 207
6.1.2 Standard SC for Basic Modal Logics 208
6.1.3 SC for Weak Basic Logics 211
6.2 Some Standard ND for Modal Basic Logics 212
6.2.1 Modal Assumptions 212
6.2.2 Modalization of Rules 216
6.3 Modalization of Reiteration Rule 219
6.4 Rules for Possibility 227
6.4.1 Original Fitch's System 227
6.4.2 Fitch's System Generalized 229
6.4.3 Modal Assumptions 233
6.5 Standard ND for Weak Logics 235
6.6 First-Order Modal Logics 241
7 Beyond Basic Logics and Standard Systems 245
7.1 Beyond Basic Normal Logics 246
7.1.1 Almost Basic Logics 247
7.1.2 Provability Logics 248
7.1.3 Logics with Branching TS Rules 248
7.1.4 Logics of Linear Frames 250
7.1.5 Temporal Logics 251
7.2 Limitations of Standard Approach 254
7.3 Redundancy of Standard Systems 260
7.3.1 Admissibility of Proof Construction Rules 260
7.3.2 Interdefinability Problem 265
7.4 RND for Modal Logics 268
7.4.1 RND Systems for M, R and K 268
7.4.2 RND for Other Modal Logics 275
7.5 Nonstandard Deductive Systems 278
7.5.1 Semantic Tableaux of Kripke 279
7.5.2 Tableaux with Boxes 280
7.5.3 Systems of Higher Level 281
8 Labelled Systems in Modal Logics 283
8.1 Kinds of Labelling 284
8.2 Weak and Strong Labelling 287
8.2.1 Some Weakly Labelled Systems 287
8.2.2 Strong Labelling 291
8.3 Medium Labelling -- Fitting's Approach 293
8.4 Labelled ND-K 297
8.4.1 LND System for K 297
8.5 Other Logics 302
8.5.1 Basic Normal Logics 302
8.5.2 Regular Basic Logics 303
8.5.3 Temporal Logics 304
8.5.4 Some Other Logics 306
8.6 LND for Weak Modal Logics 309
8.7 MRND Systems with Labels 314
8.7.1 Local Labelling 314
8.7.2 Global Labelling 317
9 Logics of Linear Frames 321
9.1 Deductive Systems for Logics of Linear Frames 322
9.1.1 Survey of Systems 322
9.1.2 A Comparison of System's Properties and Strategies of Linearization 329
9.2 LND-System for S4.3 336
9.2.1 Characteristic Rule and Its Correctness 336
9.2.2 Efficiency 339
9.3 LND for Linear Temporal Logics 341
9.3.1 Formalization of Kt4.3 341
9.3.2 Other Linear Logics 343
9.4 Analytic Version of LND for Linear Logics 344
9.5 Extensions and Limitations 350
10 Analytic Labelled ND and Proof Search 356
10.1 Analytic LND 357
10.1.1 Labelled Hintikka Sets 358
10.1.2 Basic Procedures 363
10.2 Logics K, D, T 366
10.2.1 Optimization 369
10.3 Transitive Logics and Loop-Control 372
10.4 Symmetric and Euclidean Logics 375
10.4.1 No Transitivity 375
10.4.2 Transitive Symmetric or Euclidean Logics 378
10.5 Linear Logics 380
10.5.1 Finite Chains 381
10.5.2 Proof Search Algorithm 383
10.5.3 Worst Case Analysis 385
11 Modal Hybrid Logics 387
11.1 Hybrid Logic in Nutshell 388
11.1.1 Motivation 388
11.1.2 Historical Remarks 390
11.2 Basic Hybrid Logic 391
11.2.1 Basic Hybrid Language 391
11.2.2 Hybrid Models 393
11.2.3 Logic 394
11.3 Complete Hilbert Calculi for KH@ and KH 395
11.4 General Completeness Results 398
11.5 Hybrid Tense Logic 403
11.5.1 Impact of Past Operators 403
11.5.2 Tenses 404
11.6 Language Extensions 405
11.6.1 Global Modalities 406
11.6.2 Difference Modality 407
11.6.3 Modal Binders 408
11.6.4 Axiomatization 410
11.6.5 Expressivity 411
11.7 Miscellanea 416
11.7.1 First-Order Modal Hybrid Logic QMHL 416
11.7.2 Decidability and Complexity 418
11.7.3 Interpolation and Beth Definability 419
12 Proof Methods for MHL 422
12.1 Kinds of Formalizations of MHL 423
12.2 Sequent Calculi 424
12.2.1 Seligman's SC 425
12.2.2 Sequent Sat-Calculus of Blackburn 430
12.2.3 Nonstandard Sequent Calculi 433
12.3 Tableau Systems 436
12.3.1 Mixed Calculi 436
12.3.2 Blackburn's Sat-Calculi 440
12.3.3 Hybrid Simulation of Baldoni's Strongly Labelled TS 444
12.4 Natural Deduction Systems 445
12.4.1 Standard ND-Systems for KH@ 445
12.4.2 Braüner's ND-System 452
12.5 Resolution 458
12.5.1 HyLoRes 458
12.5.2 HRND -- Hybrid RND-System 461
Bibliography 469
Index 491