Analytic tableaux for intuitionistic First Degree Entailment

Abstract

N.D. Belnap formulated a relevant logic called $\textbf{FDE}$ (First Degree Entailment) which avoids so-called paradoxes of classical entailment: “any proposition follows from a contradiction” and “a tautology follows from any proposition”. $\textbf{FDE}$ deals with formulas which have an implication as the main connective and its antecedent as well as consequent that contain only the following connectives: negation, disjunction, and conjunction. Since intuitionistic entailment has the same paradoxes as the classical one, the problem of the presentation of an intuitionistic analogue of $\textbf{FDE}$ which avoids the paradoxes of intuitionistic entailment arises.
Y.V. Shramko solved this problem and presented the logic $\bf IE_{fde}$. $\bf IE_{fde}$ deals with both relevant and intuitionistic implications, because, in contrast to classical implication, the intuitionistic one is not expressed via negation, conjunction, and disjunction. Y.V. Shramko formulated an intuitionistic version of E.K. Voishvillo's semantics of generalized descriptions of states originally developed for $\textbf{FDE}$. In this paper we present an adequate analytic tableaux in the style of M. Fitting for $\bf IE_{fde}$, based on Y. V. Shramko's semantics for this logic. We modify M. Fitting's analytic tableaux for intuitionistic logic by adding two new types of signed formulas ($\overline{T}A$ ($A$ is not-true) and $\overline{F}A$ ($A$ is not-false)), reduction rules for them and adapting relevant definitions as well as the rules for $TA$ and $FA$. A set of signed formulas $ S $ is called closed if it contains at the same time signed formulas of types $ TA $ and $ \overline{T}A $ or $ FA $ and $ \overline{F}A $. A closed tableaux for $ \{TA, \overline{T}B\} $ is called a proof of a formula $ A\rightarrow B $. In the rules, where in intuitionistic logic signed formulas of type $FA$ are deleted, in $\bf IE_{fde}$ signed formulas of type $\overline{T}A$ are also deleted. Last, but not least, our analytic tableaux for $\bf IE_{fde}$ shows that this logic is decidable. DOI: 10.21146/2074-1472-2018-24-2-116-122