Undecidable problems for propositional calculi with implication

TL;DR

This paper proves that key recognition problems like extensions, axiomatizations, and completeness are undecidable for propositional calculi with implication, highlighting fundamental limits in automated reasoning within these logical systems.

Contribution

It establishes the undecidability of recognizing extensions, axiomatizations, and completeness for propositional calculi with implication, extending prior results and providing a comprehensive survey.

Findings

Recognizing extensions is undecidable for all propositional calculi.

Recognizing axiomatizations and completeness is undecidable for calculi with the formula x → ( y → x ).

Derivability of any fixed formula is undecidable in these systems.

Abstract

In this article, we deal with propositional calculi over a signature containing the classical implication $\to$ with the rules of modus ponens and substitution. For these calculi we consider few recognizing problems such as recognizing derivations, extensions, completeness, and axiomatizations. The main result of this paper is to prove that the problem of recognizing extensions is undecidable for every propositional calculus, and the problems of recognizing axiomatizations and completeness are undecidable for propositional calculi containing the formula $x \to ( y \to x )$. As a corollary, the problem of derivability of a fixed formula $A$ is also undecidable for all $A$. Moreover, we give a historical survey of related results.