Indrzejczak Natural Deduction, Hybrid Systems and Modal Logics

1. Auflage 2010
ISBN: 978-90-481-8785-0
Verlag: Springer-Verlag
Format: PDF
Kopierschutz: Adobe DRM (»Systemvoraussetzungen)

E-Book, Englisch, 492 Seiten

This book provides a detailed exposition of one of the most practical and popular methods of proving theorems in logic, called Natural Deduction. It is presented both historically and systematically. Also some combinations with other known proof methods are explored. The initial part of the book deals with Classical Logic, whereas the rest is concerned with systems for several forms of Modal Logics, one of the most important branches of modern logic, which has wide applicability.

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.

Autoren/Hrsg.

Indrzejczak, Andrzej

Inhaltsverzeichnis

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