Моделирование арифметики в языке первого порядка, обогащенном темпоральными кванторами

Рассматривается язык классической логики предикатов с равенством, обогащенный модальностями темпоральной логики $\bf CTL^\ast$. В качестве семантики для него предлагаются серийные шкалы Крипке с постоянными предметными областями. Строится погружение множества арифметических формул, истинных в стандартной модели арифметики, во множество всех модальных предикатных формул, истинных в указанном классе шкал Крипке. Извлекается ряд следствий, касающихся алгоритмических, синтаксических и семантических свойств большого класса логик в рассматриваемом языке.