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/}
}
TY  - JOUR
AU  - G. V. Bokov
TI  - Undecidable iterative propositional calculus
JO  - Algebra i logika
PY  - 2016
SP  - 419
EP  - 431
VL  - 55
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/AL_2016_55_4_a1/
LA  - ru
ID  - AL_2016_55_4_a1
ER  - 
%0 Journal Article
%A G. V. Bokov
%T Undecidable iterative propositional calculus
%J Algebra i logika
%D 2016
%P 419-431
%V 55
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/AL_2016_55_4_a1/
%G ru
%F 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/