Terminating Calculi for Propositional Dummett Logic with Subformula Property

TL;DR

This paper introduces two new terminating tableau calculi for propositional Dummett logic that adhere to the subformula property, leveraging the logic's linearly ordered Kripke semantics to improve proof procedures.

Contribution

It presents novel tableau calculi for Dummett logic that are terminating and subformula-preserving, using semantic insights and a new check to replace traditional loop checks.

Findings

First calculus operates on present and next worlds

Second calculus uses object language with a new completeness-based check

Both calculi are proven to be terminating and sound

Abstract

In this paper we present two terminating tableau calculi for propositional Dummett logic obeying the subformula property. The ideas of our calculi rely on the linearly ordered Kripke semantics of Dummett logic. The first calculus works on two semantical levels: the present and the next possible world. The second calculus employs the usual object language of tableau systems and exploits a property of the construction of the completeness theorem to introduce a check which is an alternative to loop check mechanisms.