<p>This paper proposes cut-free sequent calculi for Wansing (1995)’s expansions of Nelson’s logics <InlineEquation ID="IEq1"> <EquationSource Format="TEX">$\textbf{N4}^{\bot }$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="bold">N</mi> <msup> <mn mathvariant="bold">4</mn> <mi>⊥</mi> </msup> </mrow> </math></EquationSource> </InlineEquation> (Odintsov 2005) and <InlineEquation ID="IEq2"> <EquationSource Format="TEX">$\textbf{N3}^{\bot }$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="bold">N</mi> <msup> <mn mathvariant="bold">3</mn> <mi>⊥</mi> </msup> </mrow> </math></EquationSource> </InlineEquation> with the consistency operator <InlineEquation ID="IEq3"> <EquationSource Format="TEX">${{\textsf{M}}}$</EquationSource> <EquationSource Format="MATHML"><math> <mi mathvariant="sans-serif">M</mi> </math></EquationSource> </InlineEquation>, which was originally studied in Gabbay (1982). A key semantic feature of the logics is the failure of the persistency condition in the Kripke semantics, and, as a result, the deduction theorem fails. Reflecting this aspect, we formulate the right rule for intuitionistic implication simi larly to the right rule for the strict implication for modal logic <InlineEquation ID="IEq4"> <EquationSource Format="TEX">$\textbf{S4}$</EquationSource> <EquationSource Format="MATHML"><math> <mrow> <mi mathvariant="bold">S</mi> <mn mathvariant="bold">4</mn> </mrow> </math></EquationSource> </InlineEquation>. Our calculus, with the cut rule, is sound, and its cut-free calculus is complete for the intended Kripke semantics. As a corollary, the cut-elimination theorem is established semantically. We also extract a Hilbert system from the sequent calculus. Unlike Omori (2016), we do not assume the existence of a root point in a Kripke model. Therefore, our Hilbert system is also semantically complete for the class of models that may lack the root point.</p>

Cut-free Sequent Calculi for Wansing’s Expansions of Nelson’s Logics

期刊论文
发表日期：

2025年11月24日

查看全文

Katsuhiko Sano,
Masanobu Toyooka

摘要

This paper proposes cut-free sequent calculi for Wansing (1995)’s expansions of Nelson’s logics $\textbf{N4}^{\bot }$ $N 4^{⊥}$ (Odintsov 2005) and $\textbf{N3}^{\bot }$ $N 3^{⊥}$ with the consistency operator ${{\textsf{M}}}$ $M$ , which was originally studied in Gabbay (1982). A key semantic feature of the logics is the failure of the persistency condition in the Kripke semantics, and, as a result, the deduction theorem fails. Reflecting this aspect, we formulate the right rule for intuitionistic implication simi larly to the right rule for the strict implication for modal logic $\textbf{S4}$ $S 4$ . Our calculus, with the cut rule, is sound, and its cut-free calculus is complete for the intended Kripke semantics. As a corollary, the cut-elimination theorem is established semantically. We also extract a Hilbert system from the sequent calculus. Unlike Omori (2016), we do not assume the existence of a root point in a Kripke model. Therefore, our Hilbert system is also semantically complete for the class of models that may lack the root point.