Undecidable iterative propositional calculus
Algebra i logika, Tome 55 (2016) no. 4, pp. 419-431
Voir la notice de l'article provenant de la source Math-Net.Ru
We consider iterative propositional calculi that are finite sets of propositional formulas together with modus ponens and an operation of superposition defined by a set of Mal'tsev operations. For such formulas, the question is studied whether the derivability problem for formulas is decidable. In the paper, we construct an undecidable iterative propositional calculus whose axioms depend on three variables. A derivation of formulas in the given calculus models the solution process for Post's correspondence problem. In particular, we prove that the general problem of expressibility for iterative propositional calculi is algorithmically undecidable.
Keywords:
iterative propositional calculus, derivability problem, expressibility problem, Post’s correspondence problem.
@article{AL_2016_55_4_a1,
author = {G. V. Bokov},
title = {Undecidable iterative propositional calculus},
journal = {Algebra i logika},
pages = {419--431},
publisher = {mathdoc},
volume = {55},
number = {4},
year = {2016},
language = {ru},
url = {http://geodesic.mathdoc.fr/item/AL_2016_55_4_a1/}
}
G. V. Bokov. Undecidable iterative propositional calculus. Algebra i logika, Tome 55 (2016) no. 4, pp. 419-431. http://geodesic.mathdoc.fr/item/AL_2016_55_4_a1/