| Preface |
|
ix | |
| Introduction |
|
1 | (4) |
|
Sequent Calculi for Positive Logic |
|
|
5 | (22) |
|
Positive Rules for Deductive Situations |
|
|
5 | (3) |
|
|
|
8 | (3) |
|
|
|
11 | (8) |
|
|
|
19 | (2) |
|
|
|
21 | (6) |
|
|
|
27 | (19) |
|
Cut Elimination with Exchange Operators |
|
|
29 | (15) |
|
|
|
44 | (2) |
|
Continuous Cut Elimination |
|
|
46 | (21) |
|
Explicit Retracing as a Motivation |
|
|
46 | (5) |
|
The Reduction Operator Ro |
|
|
51 | (12) |
|
The Reduction Operator R1 and the Elimination Operator |
|
|
63 | (4) |
|
Sequent Calculi for Minimal and Intuitionistic Logic |
|
|
67 | (21) |
|
Negation in Deductive Situations |
|
|
67 | (2) |
|
The Calculi KMo of Minimal Logic and KJo of Intuitionistic Logic |
|
|
69 | (1) |
|
The Intermediary Calculi KM1, KJ1 |
|
|
70 | (5) |
|
|
|
75 | (8) |
|
K--Calculi for the Connective ⌝ |
|
|
83 | (3) |
|
|
|
86 | (2) |
|
Sequent Calculi for Classical Logic |
|
|
88 | (38) |
|
|
|
91 | (6) |
|
Cut Elimination with Inversion Rules for MK |
|
|
97 | (4) |
|
MK as a Calculus for Classical Logic |
|
|
101 | (6) |
|
The Calculi MP, MM and MJ |
|
|
107 | (2) |
|
|
|
109 | (10) |
|
|
|
119 | (7) |
|
Classes of Algebras Associated to a Calculus |
|
|
126 | (42) |
|
d--Algebras and d--Frames |
|
|
126 | (8) |
|
e--Algebras, e--Frames and RPC--Semilattices |
|
|
134 | (7) |
|
g--Algebras, g--Frames and RPC--Lattices |
|
|
141 | (4) |
|
m--Algebras, m--Frames and m--Lattices |
|
|
145 | (6) |
|
i--Algebras, i--Frames and Heyting Algebras |
|
|
151 | (6) |
|
c--Algebras, c--Frames and Boolean Algebras |
|
|
157 | (4) |
|
Translations from Classical into Intuitionistic Logic |
|
|
161 | (7) |
|
|
|
168 | (34) |
|
Modus Ponens Calculi for Positive Logic |
|
|
174 | (7) |
|
Modus Ponens Calculi for Minimal and for Intuitionistic Logic |
|
|
181 | (4) |
|
Modus Ponens Calculi for Classical Logic |
|
|
185 | (17) |
|
Historical Notes to
Chapters 1--7 |
|
|
196 | (6) |
|
Sequent Calculi for Quantifier Logic |
|
|
202 | (34) |
|
Quantifier Rules for Deductive Situations |
|
|
202 | (2) |
|
Sequent Calculi with Q--rules |
|
|
204 | (8) |
|
The Replacement Theorem and Cut Elimination for Calculi with rep |
|
|
212 | (7) |
|
The Substitution Theorem and Cut Elimination for Calculi with sub |
|
|
219 | (2) |
|
|
|
221 | (5) |
|
The Substitution Theorem Resumed |
|
|
226 | (5) |
|
|
|
231 | (2) |
|
|
|
233 | (3) |
|
Semantical Consequence Operations and Modus Ponens Calculi |
|
|
236 | (20) |
|
The Calculi cxqt and cxqs |
|
|
236 | (4) |
|
The Variants cxqto of cxqt |
|
|
240 | (3) |
|
The Variants cxqt1 and cxqt2 of cxqt |
|
|
243 | (2) |
|
|
|
245 | (3) |
|
The Deduction Theorem and Other Metarules for the Calculi ccqti |
|
|
248 | (2) |
|
Tautologies of Positive Quantifier Logic |
|
|
250 | (2) |
|
Tautologies of Minimal Quantifier Logic |
|
|
252 | (1) |
|
Tautologies of Classical Quantifier Logic |
|
|
253 | (3) |
|
Selected Topics in Sequential Quantifier Logic |
|
|
256 | (61) |
|
Translating Between Sequential and Modus Ponens Calculi |
|
|
256 | (3) |
|
Relations between Classical and Intuitionistic Derivability |
|
|
259 | (4) |
|
|
|
263 | (7) |
|
Language Extensions with Predicate Symbols |
|
|
270 | (4) |
|
Language Extensions with Function Symbols 1 |
|
|
274 | (11) |
|
Language Extensions with Function Symbols 2 |
|
|
285 | (3) |
|
|
|
288 | (10) |
|
Herbrand's Theorem for Prenex Formulas |
|
|
298 | (7) |
|
|
|
305 | (12) |
| Index of concepts and names |
|
317 | (4) |
| Index of symbolic notations |
|
321 | |
Lisainfo e-raamatute kohta