Условные тавтологии
Чтобы охватить формулы, верные при дополнительных условиях (аксиомах), рассматриваются модели с фиксированной шкалой или набором шкал.
Формула А называется верной в модели M = (W, R, h), если она верна для всех tW. Формула А называется тавтологией относительно шкалы, если она верна для любой модели с данной шкалой. Формула А называется тавтологией относительно класса шкал С, если она является тавтологией относительной каждой шкалы из класса С.
Теорема (о рефлексии). Пусть р – атом. Формула р р является тавтологией относительно шкалы (W, R), если и только если R – рефлексивное отношение (т.е. wRw для всех w W).
Доказательство. Пусть R – рефлексивно. Пусть М – модель со шкалой (W, R), tW – произвольный мир и пусть M, t |= р р. Поскольку модель М – произвольная, то р р – тавтология относительно шкалы (W, R).
Пусть, наоборот, р р – тавтология относительно (W, R). Пусть t W. Докажем, что (t, t) R. С этой целью определим модель М = (W, R, h), полагая (при фиксированном t)
h(p) = {u W : (t, u) R}.
Ясно, что M, t |= р. Но р р верно, стало быть, M, t |= р. Отсюда t h(p). Следовательно, (t, t) R, что и требовалось доказать.
- 6. Модальная и темпоральная логикИ
- 6.1. Синтаксис модальной логики
- Дополнительные логические связки
- Приоритеты операций
- Смысловые значения модальностей
- 6.2. Семантика модальной логики
- Модели Крипке
- Упражнение 1
- Упражнение 2
- Семантика темпоральной логики
- Упражнение 3
- Тавтологии
- Упражнение 4
- Условные тавтологии
- Упражнение 5
- 6.3. Алгоритмическая логика Хоара
- Пропозициональная динамическая логика
- Семантика пропозициональной динамической логики
- Аксиомы pdl
- Правила вывода
- Логика Хоара
- Корректность и полнота систем Гильберта
- Свойства шкал Крипке
- Алгоритм Салквиста
- Пример 2
- Пример 3
- Пример 6
- 6.5. Темпоральная логика
- Система Гильберта для темпоральной логики
- Линейные потоки времени
- Стандартный перевод
- Завтра и вчера
- Выбор операторов
- 7. Алгоритмы и рекурсивные функции
- 7.1. Частично рекурсивные функции
- Простейшие функции
- Пример 1
- Оператор примитивной рекурсии
- Пример 2
- Пример 4
- Пример 5
- Пример 6
- Оператор минимизации
- Пример 7
- 7.2. Машины Тьюринга
- Пример 1
- Пример 2
- Пример 3
- Упражнение
- 7.3. Вычислительная сложность
- Труднорешаемые и np-полные задачи
- 6. Модальная и темпоральная логикИ 49
- 7. Алгоритмы и рекурсивные функции 65