Geodesic
Modeling arithmetic in the first-order language enriched with temporal quantifiers
Vestnik Tverskogo gosudarstvennogo universiteta. Seriâ Prikladnaâ matematika, no. 4 (2016), pp. 5-19 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

We investigate the classical first-order language with equality enriched by the modalities of the computational tree logic $\bf CTL^\ast$. As a semantics for it we consider serial Kripke frames with constant domains. We construct an embedding of the truth arithmetics into the set of all formulas that are valid in the class of such frames. Then, we obtain some corollaries concerned algorithmical, syntactical, and semantical properties for a large class of logic in the language.
Keywords: first-order logic, computational tree logic, recursive enumerability, Kripke semantics. 
@article{VTPMK_2016_4_a0,
     author = {E. A. Kotikova and M. N. Rybakov},
     title = {Modeling arithmetic in the first-order language enriched with temporal quantifiers},
     journal = {Vestnik Tverskogo gosudarstvennogo universiteta. Seri\^a Prikladna\^a matematika},
     pages = {5--19},
     year = {2016},
     number = {4},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/VTPMK_2016_4_a0/}
}
TY  - JOUR
AU  - E. A. Kotikova
AU  - M. N. Rybakov
TI  - Modeling arithmetic in the first-order language enriched with temporal quantifiers
JO  - Vestnik Tverskogo gosudarstvennogo universiteta. Seriâ Prikladnaâ matematika
PY  - 2016
SP  - 5
EP  - 19
IS  - 4
UR  - http://geodesic.mathdoc.fr/item/VTPMK_2016_4_a0/
LA  - ru
ID  - VTPMK_2016_4_a0
ER  - 
%0 Journal Article
%A E. A. Kotikova
%A M. N. Rybakov
%T Modeling arithmetic in the first-order language enriched with temporal quantifiers
%J Vestnik Tverskogo gosudarstvennogo universiteta. Seriâ Prikladnaâ matematika
%D 2016
%P 5-19
%N 4
%U http://geodesic.mathdoc.fr/item/VTPMK_2016_4_a0/
%G ru
%F VTPMK_2016_4_a0
E. A. Kotikova; M. N. Rybakov. Modeling arithmetic in the first-order language enriched with temporal quantifiers. Vestnik Tverskogo gosudarstvennogo universiteta. Seriâ Prikladnaâ matematika, no. 4 (2016), pp. 5-19. http://geodesic.mathdoc.fr/item/VTPMK_2016_4_a0/

[1] Boolos G. S., Jeffrey R. C., Computability and Logic, Third Edition, Cambrige University Press, 1989 | MR | Zbl

[2] Ershov Yu. L., Palyutin E. A., Mathematical Logic, Second Edition, Nauka, Moscow, 1987 (in Russian)

[3] Karpov Yu. G., Model Checking: Verification of Parallel and Distributive Systems, BKHV-Peterburg, Sankt-Peterburg, 2010 (in Russian)

[4] Chang C. C., Keisler H. J., Model Theory, North-Holland Publishing Company, 1973 | MR | Zbl

[5] Clarke E. M., Grumberg O., Peled D., Model Checking, MIT Press, 1999

[6] Feys R., Modal Logic, Nauka, Moscow, 1974 (in Russian)

[7] Mal'tsev A. I., Algorithms and Recursive Functions, Second Edition, Nauka, Moscow, 1986 (in Russian)

[8] Mendelson E., Introduction to Mathematical Logic, D. van Nostrand Company, Inc., 1964 | MR

[9] Novikov P. S., Elements of Mathematical Logic, Second Edition, Nauka, Moscow, 1973 (in Russian) | MR

[10] Chagrov A. V., Rybakov M. N., “Standard translations of non-classical formulas and relative decidability of logics”, Proceedings of the Research Seminar of the Logical Center of the Institute of Philosophy, RAS, v. XIV, 2000, 81–98 (in Russian) | MR

[11] Church A., “An unsolvable problem of elementary number theory”, American Journal of Mathematics, 58 (1936), 345–363 | DOI | MR

[12] Church A., “A note on the Entscheidungsproblem”, Journal of Symbolic Logic, 1 (1936), 40–41 | DOI

[13] Gabbay D. M., Skvortsov D., Shehtman V., Quantification in Nonclassical Logic, v. 153, Elsevier Science, 2009 | MR | Zbl

[14] Kotikova E. A., Rybakov M. N., “First-Order Logics of Branching Time: On Expressive Power of Temporal Operators”, Logical Investigations, 19 (2013), 68–99 | MR | Zbl

[15] Kotikova E. A., Rybakov M. N., “Kripke incompleteness of first-order calculi with temporal modalities of CTL and near logics”, Logical Investigations, 21:1 (2015), 86–99 | MR | Zbl

[16] Kripke S., “The undecidability of monadic modal quantificational theory”, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 8 (1962), 113–116 | DOI | MR | Zbl

[17] Turing A. M., “On computable numbers with an application to the Entscheidungsproblem”, Proceedings of the London Mathematical Society, 2, 42, 1936, 230–265 | MR

[18] Turing A. M., “On computable numbers, with an application to the Entscheidungsproblem. A correction”, Proceedings of the London Mathematical Society, 2, 43, 1937, 544–546 | MR

[19] Vardi M. Y., Stockmeyer L., “Improved upper and lower bounds for modal logics of programs”, Proceedings of 17th Symposium on Theory of Computing, STOC’85 (Baltimore, USA, May 1985), 240–251