Körner's criterion of relevance and analytic tableaux (Q1187981)

The author provides a proof theory for the propositional logic (set of \(K\)-tautologies) corresponding to Körner's criterion of a relevant tautology as presented (most accessibly) in \textit{S. Körner}'s paper in [Philosophy 54, 377--379 (1979)]. (A formula is a \(K\)-tautology iff 1) it is a classical tautology and 2) there is no occurrence of any subformula such that the result of replacing it by an occurrence of its negation is also a classical tautology.) It is shown that the set of \(K\)-tautologies is equivalent to the set of \(D\)-tautologies, i.e., classical tautologies that satisfy the relevance criterion of \textit{M. R. Diaz} [Topics in the logic of relevance. München: Philosophia Verlag (1981; Zbl 0471.03004)]. (A formula is a \(D\)-tautology iff 1) it is a classical tautology and 2) there is no occurrence of any variable such that the result of replacing it by an occurrence of a new propositional variable is also a classical tautology.) The author then provides a proof theory for the set of \(D\)-tautologies. The proof theory is an emendation on the analytic tableau of \textit{R. M. Smullyan} [First-order logic. Berlin etc.: Springer-Verlag (1968; Zbl 0172.28901)]. The technique depends on keeping track of which occurrence of a propositional variable in the original formula is the ancestor of an occurrence of the same propositional variable in a subformula lower down on the tableau. So each occurrence of a propositional variable of the original formula is assigned a distinct occurrence number. The tableau is then completed as usual. The author shows that a formula is a \(D\)-tautology, and hence a \(K\)-tautology, iff the tableau for its negation is closed and further, each variable occurrence of the original (negated) formula is ``solely responsible for'' the closure of at least one branch of the tableau. (Cf. pp. 52--54 of \textit{J. M. Dunn's} paper in [J. Philos. Logic 9, 41--57 (1980; Zbl 0428.03011)].) This system belongs, on the one hand, within a certain school of entailment logics which attempt to capture entailment by placing some explicit restriction on classical validity as in \textit{T. J. Smiley's} paper in [Proc. Aristot. Soc., New Ser. 59, 233--254 (1959)], and in \textit{P. T. Geach}'s paper in [Philos. Rev. 79, 237--239 (1970)]. Insofar as they are to be ``logics'', they bear comparison to relevant/relevance logics, as the name of the criterion suggests. However, criteria such as Körner's have also been treated as non-logical apparatus, as by \textit{P. Weingartner} and \textit{G. Schurz} [Logique Anal., Nouv. Sér. 29, 3--40 (1986; Zbl 0622.03007)]. For a brief discussion of this approach, see pp. 46--47 of the reviewer's paper in [Rep. Math. Logic 24, 37--47 (1990; Zbl 0759.03012)].