The law of assertion and the rule of restricted permutation.

Abstract

An approach to the problem o f decidability o f propositional relevant calculi is displayed in the form of effective decision procedure for the calculus closely related to V.A.Smirnov’s «absolute» system. The procedure is presented as proof-search algorithm for the sequent calculus with indexed formulae \textbf{SIRC}. The contribution is restricted by the idea and basic techniques of decision procedure whereas a question o f strategies and heuristics is not discussed. However the method under consideration is supposed to be applicable to several relevant logics.

Известно, что тождество формул в чисто импликативном языке может рассматриваться как выводимость некоторых формул в очень слабой пропозициональной системе в том же языке. С точки зрения логики и философии представляет интерес то обстоятельство, что подстановка формул типа $B\rightarrow .C\rightarrow D$вместо подформул вида $B\rightarrow .C\rightarrow D$ в формулу $А$ может быть отождествлено с CONGR — выводимостью некоторых формул в слабой логической системе $\textbf{TRW}_\rightarrow+AP. В работе дается секвенциальная формулировка \textbf{G}f\textbf{TRW} ^+RP) системы $\textbf{TRW}_\rightarrow+AP$ и доказывается, что CONGR эквивалентна тому факту, что в \textbf{G}($\textbf{TRW}_\rightarrow+RP$) выводимость теорем вида $A\rightarrow A$ предшествует выводимости любых других теорем.