Geodesic
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/

[1] H. Sinaceur, “Address at the Princeton University bicentennial conference on problems of mathematics (December 17–19, 1946), by Alfred Tarski”, Bull. Symb. Log., 6:1 (2000), 1–44 | DOI | MR | Zbl

[2] S. Linial, E. L. Post, “Recursive unsolvability of the deducibility, Tarski's completeness, and independence of axioms problems of the propositional calculus”, Bull. Am. Math. Soc., 55 (1949), 50

[3] A. V. Kuznetsov, “O nerazreshimosti obschikh problem polnoty, razresheniya i ekvivalentnosti dlya ischislenii vyskazyvanii”, Algebra i logika, 2:4 (1963), 47–66 | MR | Zbl

[4] G. V. Bokov, “Undecidability of the problem of recognizing axiomatizations for propositional calculi with implication”, Log. J. IGPL, 23:2 (2015), 341–353 | DOI | MR

[5] G. V. Bokov, “Undecidable problems for propositional calculi with implication”, Log. J. IGPL, 24:5 (2016), 792–806 | DOI | MR

[6] V. B. Kudryavtsev, Funktsionalnye sistemy, Izd-vo MGU, M., 1982

[7] A. Citkin, “A mind of a non-countable set of ideas”, Log. Log. Philos., 17:1/2 (2008), 23–39 | MR | Zbl

[8] A. V. Kuznetsov, “Analogi shtrikha Sheffera v konstruktivnoi logike”, DAN SSSR, 160:2 (1965), 274–277 | Zbl

[9] A. V. Kuznetsov, “O funktsionalnoi vyrazimosti v superintuitsionistskikh logikakh”, Matem. issl., 6:4 (1971), 75–122 | MR | Zbl

[10] A. V. Kuznetsov, “O sredstvakh dlya obnaruzheniya nevyvodimosti ili nevyrazimosti”, Logicheskii vyvod, eds. E. K. Voishvillo i dr., Nauka, M., 1979, 5–33

[11] A. I. Maltsev, I. A. Maltsev, Iterativnye algebry Posta, Nauka, M., 2012

[12] G. V. Bokov, “Iterativnye propozitsionalnye ischisleniya”, Intellekt. sist. Teor. pril., 18:4 (2014), 99–106 | MR

[13] A. I. Maltsev, “Iterativnye algebry i mnogoobraziya Posta”, Algebra i logika, 5:2 (1966), 5–24 | MR | Zbl

[14] E. L. Post, “A variant of a recursively unsolvable problem”, Bull. Am. Math. Soc., 52:4 (1946), 264–268 | DOI | MR | Zbl

[15] E. L. Post, “Formal reductions of the general combinatorial decision problem”, Am. J. Math., 65 (1943), 197–215 | DOI | MR | Zbl

[16] A. I. Maltsev, Algoritmy i rekursivnye funktsii, Nauka, M., 1965 | MR