Timo Lang

This short post is a follow-up to Sonia and Anupam’s blog post on constructive modal logics; I present a quick direct proof that the constructive modal logic is conservative over on the -free fragment. This was first discussed in the comment section to the aforementioned blog post (as an open problem), and eventually obtained in…

An instance of the cut rule is called analytic if the cut formula already appears as a subformula of the lower sequent. For example, the cut is analytic because the cut formula is contained in . Analytic cut can be seen as a deep inference rule. In classical and modal logic it corresponds to a…