Undecidability of the problem of recognizing axiomatizations for propositional calculi with implication

DOI10.1093/JIGPAL/JZU047MaRDI QIDQ4644516zbMATH OpenOpenAlexFDO

Authors G. V. Bokov

Publication date 8 January 2019

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1407.7010

zbMATH Keywords

finite axiomatizationimplicational calculustag systemclassical and intuitionistic propositional calculi

Mathematics Subject Classification ID

Classical propositional logic (03B05) Subsystems of classical logic (including intuitionistic logic) (03B20) Decidability of theories and sets of sentences (03B25)

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.

Recommendations

• Undecidability of the problem of recognizing axiomatizations of superintuitionistic propositional calculi
• Undecidable problems for propositional calculi with implication
• Undecidable iterative propositional calculus
• Nondecidable intermediate calculus
• On the number of variables in undecidable superintuitionistic propositional calculi

Cited in

(12)

• Undecidable problems for propositional calculi with implication
• Nondecidable intermediate calculus
• Implication of clauses is undecidable
• Recursive unsolvability of a problem of expressibility in the logic of provability
• Undecidability of the problem of recognizing axiomatizations of superintuitionistic propositional calculi
• The one variable implicational calculus
• The undecidability of entailment and relevant implication
• scientific article; zbMATH DE number 1180151 (Why is no real title available?)
• Undecidable iterative propositional calculus
• Lower end of the linial-post spectrum
• Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules
• The metatheory of the classical propositional calculus is not axiomatizable

This page was built for publication: Undecidability of the problem of recognizing axiomatizations for propositional calculi with implication

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4644516)