Decidability of Intuitionistic Sentential Logic with Identity via Sequent Calculus

Agata Tomczyk
(Adam Mickiewicz University)
Dorota Leszczyńska-Jasion
(Adam Mickiewicz University)

The aim of our paper is twofold: firstly we present a sequent calculus for an intuitionistic non-Fregean logic ISCI, which is based on the calculus presented in the paper by Chlebowski and Leszczynska-Jasion, 'An Investigation into Intuitionistic Logic with Identity' (Bulletin of the Section of Logic 48(4), p. 259–283, 2019) and, secondly, we discuss the problem of decidability of ISCI via the obtained system. The original calculus from the mentioned paper did not provide the decidability result for ISCI. There are two problems to be solved in order to obtain this result: the so called loops characteristic for intuitionistic logic and the lack of the subformula property due to the form of the identity-dedicated rules. We discuss possible routes to overcome these problems: we consider a weaker version of the subformula property, guarded by the complexity of formulas which can be included within it; we also present a proof-search procedure such that when it fails, then there exists a countermodel (in Kripke semantics for ISCI).

In Andrzej Indrzejczak and Michał Zawidzki: Proceedings of the 10th International Conference on Non-Classical Logics. Theory and Applications (NCL 2022), Łódź, Poland, 14-18 March 2022, Electronic Proceedings in Theoretical Computer Science 358, pp. 136–149.
Published: 14th April 2022.

ArXived at: https://dx.doi.org/10.4204/EPTCS.358.10 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org