Аналитико-табличная формализация систем временной логики... О.М. Григорьев

Logical Studies No.8 (2002)
О.М. Григорьев
Аналитико-табличная формализация систем временной логики с нестандартным отношением между прошлым и будущим
Данная статья посвящена разработке аналитико-табличной процедуры для системы временной логики с нестандартным отношениием сопряженности между прошлым и будущим, идея построения которой принадлежит российскому логику В.А.Смирнову. Главное отличие этой логики от стандартных систем Прайора заключается в том, что для интерпретации каждой из временных модальностей (G и H) используется собственное отношение достижимости, тогда как обычно обходятся лишь одним отношением для интерпретации модальностей прошлого и будущего. Наличие двух отношений достижимости (и некоторой содержательной интерпретации отношений) приводит к тому, что мы имеем дело с новым классом шкал Крипке и, соответственно, новой временной логикой. Предлагаемая аналитико-табличная формализация представляет собой вариант индексированных аналитических таблиц, в которых индексы выписываются перед формулами и ставятся в соответствие точкам шкалы Крипке. Этот хорошо известный подход модифицирован за счет введения особой элементарной структуры - R-Г-пары. Здесь R представляет собой пару множеств, каждое из которых, в свою очередь, состоит из пар индексов, а Г есть ассоциированное с R множество индексированных формул. Совокупность R-Г-пар называется конфигурацией. Аналитическая таблица есть последовательность конфигураций, где каждая конфигурация, за исключением самой первой, получается из предыдущей применением одного из правил редукции. Доказываются теоремы о полноте и непротиворечивости постренного формализма относительно соответствующего класса шкал Крипке.

по-русски