# How to prove this sequent system is sound and complete for S4 Modal Logic?

Take LK sequent calculus without cut, but change the $$\to R$$ rule to the following:

$$\cfrac{\Gamma’, A \vdash B}{\Gamma \vdash A \to B, \Delta}$$

where $$\Gamma’=\{C \in \Gamma|C=(D \to E)\}$$ for well-formed formulas $$D,E$$.

I seek to show that this is the only rule that needs to be changed from LK to achieve Classical S4 with $$\to$$ as strict implication, provided negation and either disjunction or conjunction to get the rest.

I can get started proving this rule is sound: just replace $$\vdash$$ with $$\vDash$$ and argue via a semantics for S4.

Regarding completeness, I would like to show that this system is equivalent to other proof systems for S4. One can easily show that this system can represent all of the operators in S4. Namely, we can represent them as:

• $$\Box A:=((A \to A) \to A)$$
• $$(A \Rightarrow B):=\sim (A \land \sim B)$$ where $$\sim$$ is negation and $$\Rightarrow$$ is classical implication
• $$\Diamond A:=\sim \Box \sim A$$

Still, I don’t know how to show that this system is equivalent to another proof system for S4 without using cut.

I will be honest, I am a total novice at proof theory and meta-logic in general, so I may be in over my head. Is my general strategy correct, and in particular, is the proof strategy for soundness the best way to go?

• Typically S4 tends to be axiomatised using the $\Box$-operator, rather than the strict implication (though of course they are interdefinable). Could you clarify how you represent the operators from S4 in this system? Commented Jul 22 at 23:05
• A natural first step, from a proof-theoretic point of view, in obtaining what you want would be to check whether your system is indeed cut-free. The natural choice would be to see if the cut elimination of LK can be pushed through with adaptations to the new rule. This may fail, since if I recall correctly, cut elimination is not straightforward, and often fails, in the case of modal logics. Also if cut elimination fails, that often spells trouble for proving completeness in turn, and can be a useful tool for figuring out new rules that are necessary. Commented Jul 22 at 23:09
• @RodrigoNicolauAlmeida see my edit. Commented Jul 22 at 23:36