Undecidability of the problem of recognizing axiomatizations for implicative propositional calculi

TL;DR

This paper proves that it is undecidable to determine whether a finite set of formulas forms an axiomatization or derives all theorems for certain propositional calculi, using a reduction from the halting problem for tag systems.

Contribution

It establishes the undecidability of recognizing axiomatizations and theorem derivations in implicative propositional calculi, extending the understanding of their computational complexity.

Findings

Undecidability of recognizing axiomatizations.

Undecidability of deriving all theorems from a set.

Reduction from Post's halting problem for tag systems.

Abstract

In this paper we consider propositional calculi, which are finitely axiomatizable extensions of intuitionistic implicational propositional calculus together with the rules of modus ponens and substitution. We give a proof of undecidability of the following problem for these calculi: whether a given finite set of propositional formulas constitutes an adequate axiom system for a fixed propositional calculus. Moreover, we prove the same for the following restriction of this problem: whether a given finite set of theorems of a fixed propositional calculus derives all theorems of this calculus. The proof of these results is based on a reduction of the undecidable halting problem for the tag systems introduced by Post.