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): Heinrich Wansing
Series: Trends in Logic, Volume 3
Publisher: Kluwer Academic Publishers
Year: 1998
Language: English
Pages: 132
Cover......Page 1
Contents......Page 2
Preface......Page 4
1 – Introduction......Page 6
1.1. The Problem of Gentzenizing Modal Logic......Page 7
1.2. Standard Sequent Systems for Normal Modal Logics......Page 8
1.3. Rules as Meaning Assignments......Page 9
1.6. Subformula Property, Cut, and Analytic Cut......Page 11
1.7. Generality......Page 12
2.1. Modal Signs......Page 13
2.3. Higher-Dimensional Sequent Systems......Page 14
2.4. Higher-Arity Sequent Systems......Page 15
2.5. Hypersequents......Page 17
2.6. Natural Deduction Systems......Page 18
3.1. Gentzen Terms......Page 19
3.2. Residuation......Page 21
3.3. The Display Theorem......Page 23
3.4. Introduction Rules......Page 24
3.5. Completeness......Page 27
4.1. Properly Displayable Logics......Page 29
4.2. A Case Distinction and Primitive Reductions......Page 30
4.3. Strong Normalization......Page 31
4.4. Displayable Logics......Page 33
4.5. Characterization of the Properly Displayable Logics......Page 34
4.6. Scope of the Method......Page 37
5.1. The Problem of Functional Completeness......Page 38
5.2. Proof-Theoretic Semantics......Page 39
5.3. Functional Completeness for Kt and K......Page 41
6.1. The Modal Display System DKf......Page 43
6.2. A Display Calculus for PDL-......Page 44
6.3. Reduction to a Set of Clauses......Page 45
6.4. Decidability and Completeness......Page 47
6.5. In the Absence of Purity......Page 48
7 – Strong Cut-Elimination and Labelled Modal Tableaux......Page 49
7.2. Primitive Reductions......Page 50
7.3. Strong Normalization......Page 53
7.4. Extensions of Quantified K......Page 55
7.5. Equivalence with Fitting’s Tableaux......Page 56
8.1. Preliminaries......Page 57
8.2. Positive Logics......Page 58
8.3. The Higher-Level Sequent Calculus G|~+......Page 59
8.4. Positive Proof-Theoretic Semantics......Page 60
8.5. Functional Completeness for |~+......Page 62
8.7. Constructive Logics......Page 63
8.8. The Higher-Level Sequent Calculus Gc......Page 65
8.9. Constructive Proof-Theoretic Semantics......Page 66
8.10. Functional Completeness for |~c......Page 67
9 – Constructive Negation and the Modal Logic of Consistency......Page 69
9.1. Disproofs and Contrariety......Page 70
9.2. Negation as Falsity......Page 74
9.3. Negation as Inconsistency......Page 75
9.4. The Relation between Negation as Falsity and Negation as Inconsistency......Page 77
9.5. Semantics-Based Nonmonotonic Reasoning......Page 78
9.6. Choice of Parameters......Page 81
10.1. Subintuitionistic Logics......Page 83
10.3. Soundness and Completeness of DK(σ)......Page 86
Untitled......Page 88
10.6. Proof of Strong Completeness......Page 89
11.1. Hypersequential Calculi......Page 91
11.2. Display Calculi......Page 93
11.3. Mapping Hypersequents into Display Sequents......Page 98
11.5. Other Translations into DL......Page 99
12 – Predicate Logics on Display......Page 100
12.1. A Sequent Calculus for KFOL......Page 101
12.2. Display of Predicate Logics......Page 102
12.3. A Route from KFOL to FOL......Page 103
12.4. Another Route to FOL......Page 106
12.6. The Barcan Formula......Page 108
13.1. DL and Fitch-Style Natural Deduction......Page 111
13.2. A New Axiomatization of Kt......Page 119
13.3. N4 Redisplayed......Page 120
A-B......Page 123
B-C-D......Page 124
E-F-G-H......Page 125
I-J-K-L-M-N......Page 126
O-P-R-S......Page 127
T-U-V-W......Page 128
A-B-C......Page 129
D-E-F-G-H-I-K......Page 130
L-M-N-O-P-Q-R-S-T......Page 131
U-V-W......Page 132
