Sequent calculus for the subintuitionistic logic ${\sf WF_{N_{2}}} $
Fatemeh Shirmohammadzadeh Maleki
TL;DR
The paper tackles subintuitionistic logics, focusing on $WF_{N_{2}}$, which are weaker than intuitionistic logic and admit neighborhood-based semantics. It introduces a cut-free G3-style sequent calculus $GWF_{N_{2}}$ for $WF_{N_{2}}$ and a single-succedent variant $GWFsN_{2}$, with an extension to a G3-style calculus $GF$ for Corsis logic $F$, enabling structural rule analysis and proof-theoretic study. A syntactic embedding of $WF_{N_{2}}$ into the classical modal logic ${M_{Nec}}$ is provided, and the paper establishes admissibility of weakening, contraction, and cut, as well as equivalence with the Hilbert-style system. The work clarifies the connections between subintuitionistic semantics and modal companions, and the single-succedent system is shown to retain the same strength on $WF_{N_{2}}$-formulas, contributing to a robust proof-theoretic framework for these logics.
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.