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

DOI10.1093/JIGPAL/JZU047zbMATH Open1405.03030arXiv1407.7010OpenAlexW3099382357MaRDI QIDQ4644516FDOQ4644516

G. V. Bokov

Publication date: 8 January 2019

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

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.

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

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

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)

Cited In (10)

• Recursive unsolvability of a problem of expressibility in the logic of provability
• Title not available (Why is that?)
• The metatheory of the classical propositional calculus is not axiomatizable
• Implication of clauses is undecidable
• Title not available (Why is that?)
• The one variable implicational calculus
• Undecidable iterative propositional calculus
• Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules
• Nondecidable intermediate calculus
• The undecidability of entailment and relevant implication

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)