Sequents for S4
Many of the best-known modal logics have sequent proof systems, but far from all. Devising natural extensions of the machinery is common, and we now have hypersequents, nested sequents, and labeled sequents, among others.
Fortunately, S4 is a logic that does have a sequent calculus, and a simple one at that. We now add ? to the formal language of Section 5.1, with the usual formation rule.Definition 5.6 (S4 Sequent Calculus GS4) First some notation.
We add to the axioms and rules of Definition 5.3 the following modal rules:
A GS4 proof uses the axioms and rules of Definition 5.3 and the Modal rules listed earlier.
proof is defined in the same way, but Cut is not allowed.
Theorem 5.5 extends to S4 quite easily.
Theorem 5.8 Each theorem of
can be derived in
with atomic axioms only.
Proof The proof of Theorem 5.5 needs one more case added to it. If A is I
and
is derived, then
?
5.4
More on the topic Sequents for S4:
-
Contemporary philosophical research -
Fundamentals of philosophy -
Logic -
Philosophy of Science and Technology -
Political philosophy -
Social philosophy -
-
Conflictology -
Ecology -
Economy -
Finance -
History -
Law -
Medicine -
Philosophy -
Religious studies -