直観主義様相論理に対する補間定理の意味論的研究
项目来源
项目主持人
项目受资助机构
立项年度
立项时间
项目编号
研究期限
项目级别
受资助金额
学科
学科代码
基金类别
关键词
参与者
参与机构
1.Cut-free Sequent Calculi for Wansing's Expansions of Nelson's Logics
- 关键词:
- Cut elimination; Sequent calculus; Nelson's logic N4; Nelson's logic N3;Consistency operator; Kripke semantics
- Sano, Katsuhiko;Toyooka, Masanobu
- 《STUDIA LOGICA》
- 2025年
- 卷
- 期
- 期刊
This paper proposes cut-free sequent calculi for Wansing (1995)'s expansions of Nelson's logics N4(perpendicular to) (Odintsov 2005) and N3(perpendicular to) with the consistency operator 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 S4. 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.
...
