Tableau-based decision procedure for non-Fregean logic of sentential identity

TL;DR

This paper introduces a novel tableau-based decision procedure for the non-Fregean logic of sentential identity (SCI), achieving NP complexity and providing the first implementation with proven termination and efficiency.

Contribution

It presents the first sound, complete, and NP-complexity decision algorithm for SCI, with an implementation and potential extensions to other non-Fregean logics.

Findings

Algorithm is NP-complete and terminates correctly.

Implementation compares favorably with other SCI calculi.

Potential for extending the approach to broader non-Fregean logics.

Abstract

Sentential Calculus with Identity (SCI) is an extension of classical propositional logic, featuring a new connective of identity between formulas. In SCI two formulas are said to be identical if they share the same denotation. In the semantics of the logic, truth values are distinguished from denotations, hence the identity connective is strictly stronger than classical equivalence. In this paper we present a sound, complete, and terminating algorithm deciding the satisfiability of SCI-formulas, based on labelled tableaux. To the best of our knowledge, it is the first implemented decision procedure for SCI which runs in NP, i.e., is complexity-optimal. The obtained complexity bound is a result of dividing derivation rules in the algorithm into two sets: decomposition and equality rules, whose interplay yields derivation trees with branches of polynomial length with respect to the size of the investigated formula. We describe an implementation of the procedure and compare its performance with implementations of other calculi for SCI (for which, however, the termination results were not established). We show possible refinements of our algorithm and discuss the possibility of extending it to other non-Fregean logics.