The complexity of decision procedures in relevance logic. II.

*(English)*Zbl 0945.03029Introduction: In this paper, we show that there is no primitive recursive decision procedure for the implication-conjunction fragments of the relevant logics \({\mathbf R}\), \({\mathbf E}\) and \({\mathbf T}\), as well as for a family of related logics. The lower bound on the complexity is proved by combining the techniques of an earlier paper on the same subject [the author, “The complexity of decision procedures in relevance logic”, in: J. M. Dunn and A. Gupta (eds.), Truth or consequences: Essays in honour of N. Belnap (Kluwer, Dordrecht), 61-76 (1990)] with a method used by Lincoln, Mitchell, Scedrov and Shankar in proving that propositional linear logic is undecidable.

The decision problem for the pure implicational fragements of \({\mathbf E}\) and \({\mathbf R}\) were solved by Saul Kripke in a tour de force of combinatorial reasoning, published only as an abstract [S. A. Kripke, “The problem of entailment” (Abstract), J. Symb. Log. 24, 324 (1959)]. N. D. Belnap and J. R. Wallace extended Kripke’s decision procedure to the implication-negation fragment of \({\mathbf E}\) [Z. Math. Logik Grundlagen Math. 11, 277-289 (1965; Zbl 0143.24902)]. The decision method extends immediately to the implication/negation fragment of \({\mathbf R}\). In fact, in the case of \({\mathbf R}\). In fact, in the case of \({\mathbf R}\) we can go farther; R. K. Meyer in his thesis [Topics in modal and many-valued logic, Ph. D. thesis, Univ. Pittsburgh (1966)] showed how to translate the logic \({\mathbf L}{\mathbf R}\), which results from \({\mathbf R}\) by omitting the distribution axiom, into \({\mathbf R}_{\to\wedge}\), so that the decision procedure can be extended to all of \({\mathbf L}{\mathbf R}\). This decision procedure has been implemented as a program KRIPKE by P. B. Thistlewaite, M. A. McRobbie and R. K. Meyer [Automated theorem-proving in nonclassical logics (Pitman, London) (1988; Zbl 0682.68097)]. The program is not simply a straightforward implementation of the decision procedure; finite matrices are used extensively to prune invalid nodes from the search tree.

The decision methods of Kripke, Belnap, Wallace and Meyer are of a truly marvelous complexity. In fact, they are so complex that it is not immediately clear how to compute an upper bound on the number of steps required by the procedures for an input formula of a given length. The key combinatorial lemma of Kripke that forms the basis for all these decision procedures simply asserts the finiteness of the search tree without giving an explicit bound on its size.

Here, we provide a lower bound on the complexity of these decision problems by showing that there is no primitive recursive decision procedure for them. This confirms (in fact, goes beyond) a conjecture of Saul Kripke that the decidability proof for \({\mathbf L}{\mathbf R}\) is unprovable in elementary recursive arithmetic.

In the last section of the paper, we show that the Kripke/Meyer decision procedure for \({\mathbf L}{\mathbf R}\) is primitive recursive in the Ackermann function. Since the lower bound for \({\mathbf L}{\mathbf R}\) is given in terms of a variant of the Ackermann function, the upper and lower bounds roughy match each other.

The decision problem for the pure implicational fragements of \({\mathbf E}\) and \({\mathbf R}\) were solved by Saul Kripke in a tour de force of combinatorial reasoning, published only as an abstract [S. A. Kripke, “The problem of entailment” (Abstract), J. Symb. Log. 24, 324 (1959)]. N. D. Belnap and J. R. Wallace extended Kripke’s decision procedure to the implication-negation fragment of \({\mathbf E}\) [Z. Math. Logik Grundlagen Math. 11, 277-289 (1965; Zbl 0143.24902)]. The decision method extends immediately to the implication/negation fragment of \({\mathbf R}\). In fact, in the case of \({\mathbf R}\). In fact, in the case of \({\mathbf R}\) we can go farther; R. K. Meyer in his thesis [Topics in modal and many-valued logic, Ph. D. thesis, Univ. Pittsburgh (1966)] showed how to translate the logic \({\mathbf L}{\mathbf R}\), which results from \({\mathbf R}\) by omitting the distribution axiom, into \({\mathbf R}_{\to\wedge}\), so that the decision procedure can be extended to all of \({\mathbf L}{\mathbf R}\). This decision procedure has been implemented as a program KRIPKE by P. B. Thistlewaite, M. A. McRobbie and R. K. Meyer [Automated theorem-proving in nonclassical logics (Pitman, London) (1988; Zbl 0682.68097)]. The program is not simply a straightforward implementation of the decision procedure; finite matrices are used extensively to prune invalid nodes from the search tree.

The decision methods of Kripke, Belnap, Wallace and Meyer are of a truly marvelous complexity. In fact, they are so complex that it is not immediately clear how to compute an upper bound on the number of steps required by the procedures for an input formula of a given length. The key combinatorial lemma of Kripke that forms the basis for all these decision procedures simply asserts the finiteness of the search tree without giving an explicit bound on its size.

Here, we provide a lower bound on the complexity of these decision problems by showing that there is no primitive recursive decision procedure for them. This confirms (in fact, goes beyond) a conjecture of Saul Kripke that the decidability proof for \({\mathbf L}{\mathbf R}\) is unprovable in elementary recursive arithmetic.

In the last section of the paper, we show that the Kripke/Meyer decision procedure for \({\mathbf L}{\mathbf R}\) is primitive recursive in the Ackermann function. Since the lower bound for \({\mathbf L}{\mathbf R}\) is given in terms of a variant of the Ackermann function, the upper and lower bounds roughy match each other.

##### MSC:

03B47 | Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) |

03B25 | Decidability of theories and sets of sentences |

03F20 | Complexity of proofs |

##### Keywords:

decision procedure; implication-conjunction fragments; lower bound on the complexity; upper bound; Ackermann function##### Software:

KRIPKE
PDF
BibTeX
XML
Cite

\textit{A. Urquhart}, J. Symb. Log. 64, No. 4, 1774--1802 (1999; Zbl 0945.03029)

Full Text:
DOI

##### References:

[1] | DOI: 10.1007/978-94-009-0681-5_5 · doi:10.1007/978-94-009-0681-5_5 |

[2] | DOI: 10.1016/0168-0072(92)90075-B · Zbl 0768.03003 · doi:10.1016/0168-0072(92)90075-B |

[3] | DOI: 10.1016/S0022-0000(69)80011-5 · Zbl 0198.32603 · doi:10.1016/S0022-0000(69)80011-5 |

[4] | Introduction to automata theory, languages and computation (1979) |

[5] | Proceedings of the London Mathematical Society 2 pp 326– (1952) |

[6] | DOI: 10.1007/BF01694011 · Zbl 0165.32002 · doi:10.1007/BF01694011 |

[7] | DOI: 10.2307/2370405 · JFM 44.0220.02 · doi:10.2307/2370405 |

[8] | DOI: 10.1002/malq.19650110403 · Zbl 0143.24902 · doi:10.1002/malq.19650110403 |

[9] | Entailment 2 (1992) |

[10] | Entailment 1 (1975) · Zbl 0345.02013 |

[11] | The undecidability of entailment and relevant implication 49 pp 1059– (1984) |

[12] | Lectures on linear logic (1992) · Zbl 0942.03535 |

[13] | Automated theorem-proving in nonclassical logics (1988) |

[14] | Ordinal numbers and the Hilbert basis theorem 53 pp 961– (1988) |

[15] | Subrecursion: functions and hierarchies (1984) · Zbl 0539.03018 |

[16] | Bulletin of the Section of Logic, Polish Academy of Sciences 9 pp 30– (1980) |

[17] | DOI: 10.1016/0304-3975(84)90029-X · Zbl 0569.68046 · doi:10.1016/0304-3975(84)90029-X |

[18] | DOI: 10.1145/322261.322271 · Zbl 0462.68020 · doi:10.1145/322261.322271 |

[19] | The problem of entailment 24 pp 324– (1959) |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.