Sequent calculus for the subintuitionistic logic $\mathsf{W}{\mathsf{F}}_{{\mathsf{N}}_2}$

Abstract

A cut-free G3-style sequent calculus GWFN2 for the subintuitionistic logic WFN2, along with its single-succedent variant GWFsN2, is introduced. The calculus GWFN2 is shown to extend naturally to a G3-style of the sequent calculus GF for Corsis logic F. Additionally, a syntactic proof of the known embedding of GWFN2 into classical modal logic MNec is presented.

arXiv admin note: text overlap with arXiv:2410.20425