Körner's criterion of relevance and analytic tableaux
type: Item
instance of: scholarly article
title: Körner's criterion of relevance and analytic tableaux
zbMATH Open document ID: 0780.03006
DOI: 10.1007/BF00248638
author: Joachim Schröder
published in: Journal of Philosophical Logic
publication date: 1992-08-03T00:00:00Z
review text: 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…
Mathematics Subject Classification ID: 03B47
Mathematics Subject Classification ID: 03F03
zbMATH DE Number: 39913
zbMATH Keywords: relevance criteria
zbMATH Keywords: analytic implication
zbMATH Keywords: relevant logics
zbMATH Keywords: proof theory
zbMATH Keywords: Körner's criterion of a relevant tautology
zbMATH Keywords: \(K\)-tautology
zbMATH Keywords: \(D\)-tautology
zbMATH Keywords: analytic tableau
reviewed by: Steve Giambrone
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/bf00248638
OpenAlex ID: W94838886
Recommended article: Q3792656
Recommended article: Intuitive Semantics for First-Degree Entailment and ‘Coupled Trees’
Recommended article: Q4268411
Recommended article: RELEVANCE FOR THE CLASSICAL LOGICIAN
Recommended article: Q3999247
Recommended article: Q5692795
Recommended article: Q3758804
Recommended article: A note on the decidability of a strong relevant logic
Recommended article: A theory of logical relevance
Recommended article: Natural deduction and sequent calculus for intuitionistic relevant logic
description: scientific article; zbMATH DE number 39913