Sequent calculus for the subintuitionistic logic ${\sf WF_{N_{2}}} $

TL;DR

This paper introduces a cut-free sequent calculus GWFN2 for the subintuitionistic logic WFN2, extending to Corsis logic F and embedding into classical modal logic MNec, advancing proof theory in non-classical logics.

Contribution

It presents a new G3-style sequent calculus for WFN2, extends it to Corsis logic F, and provides a syntactic embedding into classical modal logic MNec.

Findings

GWFN2 is cut-free and G3-style.

Extension to Corsis logic F is natural.

Embedding into classical modal logic MNec is syntactic.

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.