Sequential Reflexive Logics with Noncontingency Operator

E. E. Zolin

Matematičeskie zametki, Tome 72 (2002) no. 6, pp. 853-868

Résumé

Hilbert systems $L^\vartriangleright$ and sequential calculi $[L^\vartriangleright]$ for the versions of logics $L=\mathbf T,\mathbf {S4},\mathbf B,\mathbf {S5}$, and $\mathbf {Grz}$ stated in a language with the single modal noncontingency operator $\vartriangleright A=\square A\vee \square \neg A$ are constructed. It is proved that cut is not eliminable in the calculi $[L^\vartriangleright]$, but we can restrict ourselves to analytic cut preserving the subformula property. Thus the calculi $[\mathbf T^\vartriangleright]$, $[\mathbf {S4}^\vartriangleright]$, $[\mathbf {S5}^\vartriangleright ]$ ($[\mathbf {Grz}^\vartriangleright]$, respectively) satisfy the (weak, respectively) subformula property; for $[\mathbf B_2^\vartriangleright]$, this question remains open. For the noncontingency logics in question, the Craig interpolation property is established.