Analytic tableaux for intuitionistic First Degree Entailment


Ya. I. Petrukhin


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






Бочаров В.А., Маркин В.И. Введение в логику. М.: ИД «Форум»; Инфра-М, 2013. 560 с.
Войшвилло Е.К. Философско-методологические аспекты релевантной логики. М.: Изд-во Моск. ун-та, 1988. 144 c.
Петрухин Я.И. Аналитико-табличная формализация интуиционистского варианта логики первоуровнего следования // Логикофилософские исследования. 2016. Вып. 7. С. 153–161.
Шрамко Я.В. К проблеме релевантного следования для интуиционистской логики // Логико-философские исследования. 1989. Вып. 1. С. 165–179.
Anderson A.R., Belnap N.D. Entailment: The Logic of Relevance and Necessity. Vol. I. Princeton, NJ.: Princeton University Press, 1975. 542 p.
Anderson A.R., Belnap N.D. Tautological entailments // Philosophical Studies. 1962. Vol. 13(1-2). P. 9–24.
Belnap N.D. A useful four-valued logic // Modern Uses of MultipleValued Logic / Ed. by J.M. Dunn, G. Epstein. Boston: Reidel Publishing Company, 1977. P. 7–37.
Belnap N.D. How a computer should think // Contemporary Aspects of Philosophy / Ed. by G. Rule. Stocksfield: Oriel Press, 1977. P. 30–56.
Belnap N.D. Tautological entailments // The Journal of Symbolic Logic. 1959. Vol. 24. P. 316.
D’Agostino M. Investigations into the complexity of some propositional calculi. PhD thesis, Oxford University. 1990. 135 p.
Dunn J.M. The Algebra of Intensional Logics. PhD thesis, University of Pittsburgh. 1966. 177 p.
Fitting M. Intuitionistic logic, model theory and forcing. Amsterdam, London: North-Holland Publishing Company. 1969. 191 p.