Decidability of Intuitionistic Sentential Logic with Identity via Sequent Calculus

TL;DR

This paper introduces a sequent calculus for an intuitionistic non-Fregean logic with identity, ISCI, and explores its decidability by addressing challenges like loops and subformula property issues.

Contribution

It develops a new sequent calculus for ISCI and analyzes its decidability, overcoming previous limitations related to loops and subformula property.

Findings

Established a proof-search procedure for ISCI

Demonstrated decidability of ISCI using Kripke semantics

Addressed subformula property limitations in the calculus

Abstract

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).