Логика доказуемости - Provability logic

Логика доказуемости это модальная логика, в котором оператор окна (или «необходимость») интерпретируется как «это доказуемо». Дело в том, чтобы уловить понятие предиката доказательства достаточно богатого формальная теория, такие как Арифметика Пеано.

Примеры

Существует ряд логик доказуемости, некоторые из которых описаны в литературе, упомянутой в разделе «Ссылки». Базовая система обычно упоминается как GL (для Гёдель -Лёб ) или L или K4W. Его можно получить, добавив модальную версию Теорема Лёба к логика K (или К4).

А именно аксиомы из GL - все тавтологии классической логики высказываний плюс все формулы одной из следующих форм:

  • Аксиома распределения: □(п → q) → (□п → □q);
  • Аксиома Лёба: □(□п → п) → □п.

И правила вывода находятся:

  • Modus ponens: От п → q и п заключить q;
  • Необходимость: От п заключить □п.

История

Модель GL была изобретена Роберт М. Соловей в 1976 году. С тех пор, вплоть до своей смерти в 1996 году, главным вдохновителем этой области был Джордж Булос. Значительный вклад в эту область внесли Сергей Н. Артемов, Лев Беклемишев, Георгий Джапаридзе, Дик де Йонг, Франко Монтанья, Джованни Самбин, Владимир Шавруков, Альберт Виссер и другие.

Обобщения

Логика интерпретируемости и Полимодальная логика Джапаридзе представляют собой естественные расширения логики доказуемости.

Смотрите также

использованная литература