CONTENTS
Page Finder
PREFACE
1.
A NOTE ON NOTATION
Introduction
Detachment substitution and 'application'
The '
D
-notation'
2.
GROUNDWORK -- THE PROPOSITIONAL CALCULUS
Building blocks
Implicational systems -- positive implication
Deduction
Some
ICI
theses
The semisubstitutivity of implication
Classical implication
Conjunction
The full positive logic
Classical C-K-A -- the redundancy of A
Negation: the full system
IC
Relationships between
IC
connectives
Classical negation: the full system
PC
Alternative bases for
PC
3.
GROUNDWORK--PROPOSITIONAL SEQUENT-LOGIC
Introduction
Formulas, sequences, and sequents
Sequent generation
Sequent-logic and propositional calculus
The 'normal form' theorem
The rule of contraction and its elimination
Inversion of rules
Contraction elimination once again
4.
GROUNDWORK -- PROPOSITIONAL LOGIC AND TABLEAUX
Proof tableaux
Proof tableaux -- formal characterization
Semantic tableaux
5.
THE ABSOLUTELY STRICT SYSTEMS -- S1° AND S1
I
ntroduction
The system
S1°
The classical
PC
in
S1°
Further theses and rules of
S1°
The semisubstitutivity of strict implication and
S1°
The system
S1
; truth-value systems
Some work within the system
S1
6.
THE ABSOLUTELY STRICT SYSTEMS -- S2°, S2, T°, AND T
The system
S2°
Semisubstitutivity of strict implication in
S2°
Some theorems of
S2°
The system
S2
The systems
T°
and
T
Modalities in
T
and its included systems
7.
THE ABSOLUTELY STRICT SYSTEMS -- ALTERNATIVE FORMULATIONS
The 'Lemmon style' bases
Other formulations
8.
THE ABSOLUTELY STRICT SYSTEMS -- MODAL SEQUENT-LOGIC
Introduction
Sequent-logic versions of
S1°
and
S1
The normal-form theorem in
LS1°
and
LS1
Equivalence of the systems
Sequent-logic versions of
S2°
and
S2
Sequent-logic versions of
T °
and
T
Decision procedures and the rule of contraction
Modalities in
T
revisited
9.
THE ABSOLUTELY STRICT SYSTEMS -- TABLEAUX
Modal models
Tableaux for modal systems
Tableaux for
T°
and
T
Tableaux for
S2°
and
S2
Tableaux for
S1°
and
S1
10.
THE SYSTEMS OF COMPLETE MODALIZATION -- S3° AND S3
The system
S3°
Semisubstitutivity of strict implication in
S3°
More theorems of
S3°
Inclusion, containment, and independence with
S3°
and
S3
The full system
S3
S3
and complete modalization
The 'unreasonableness' of
S3
and its included systems
11.
THE SYSTEMS OF COMPLETE MODALIZATION -- S4°, S4, AND S5
The system
S4°
S4°
,
S4
, and the previously discussed systems
The full system
S4
The system
S5
Complete modalization in
S5
12.
THE SYSTEMS OF COMPLETE MODALIZATION -- ALTERNATIVE FORMULATIONS
The Lemmon-style bases
Other formulations
Finite axiomatizability
Formulations without axioms beyond those of the
PC
The deduction theorem for the systems of this chapter
13.
THE SYSTEMS OF COMPLETE MODALIZATION -- SEQUENT-LOGIC, THE BASIC SYSTEMS
Sequent-logic for
S3°
and
S4°
The normal form theorem in
LS3°
and
LS4°
The equivalence of the systems
Sequent-logics for
S3
and
S4
The normal form theorem for
LS3
and
LS4
A relationship between intuitionist logic and
S4
Sequent-logic for
S5
14.
THE SYSTEMS OF COMPLETE MODALIZATION -- BASIC SYSTEMS OF TABLEAUX
Tableaux for
S4°
and
S4
Tableaux for
S3°
and
S3
Tableaux for
S5
15.
THE SYSTEMS OF COMPLETE MODALIZATION -- THE S4-S5 SPECTRUM AND RELATED SYSTEMS
Introduction
The system
S4.3
The system
S4.2
The Diodorean system
D
S4.4
and some associated systems
Sobocinski's family
K
of 'non-Lewis modal' systems
Semantics for
S4.9
; the 'last stop' before
S5
Summary
APPENDIX: BASES FOR KEY SYSTEMS AND STRUCTURES STUDIED IN THIS BOOK
(A)
Non-Modal Propositional Calculi
(A.1)
Standard ('Hilbert-style') axiomatizations
(A.1.1)
Intuitionistic propositional calculus
(
IC
)
(A.1.2)
Classical propositional calculus (
PC
).
(A.2)
Non-modal sequent-logic
(A.3)
Semantic tableaux for PC (structure MPC)
(B)
Modal Calculi
(B.1)
'
Lewis-style' axiomatizations of
S1°-S5
(B.2)
'L
emmon-style' bases for
S1°-S5
(B.3)
Systems between
S4
and
S5,
and Sobocinski's 'non-Lewis modal' systems
(B.4)
Modal sequent-logic for S1
°
-S5
(B.5)
Sequent-logic for systems between
S4
and
S5
(B.6)
Tableaux for Modal Systems
BIBLIOGRAPHY
Page Finder