Логика проверки

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

• 1 Примеры
• 2 История
• 3 Обобщения
• 4 См. Также
• 5 Ссылки

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

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

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

И правила вывода следующие:

• Modus ponens : из p → q и p заключаем q;
• Необходимость : из $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$p заключаем $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$□ стр.

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

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

• Условия доказуемости Гильберта – Бернейса
• Логика интерпретируемости
• Семантика Крипке
• Полимодальная логика Джапаридзе
• Теорема Лёба

• Джордж Булос, Логика доказуемости. Cambridge University Press, 1993.
• Георгий Джапаридзе и Дик де Йонг, Логика доказуемости. В: Справочник по теории доказательств, С. Басс, изд. Elsevier, 1998, стр. 475–546.
• Сергей Н. Артемов и Лев Беклемишев, Логика доказуемости. В: Handbook of Philosophical Logic, D. Gabbay and F. Guenthner, eds., Vol. 13, 2-е изд., С. 189–360. Springer, 2005.
• Пер Линдстрём, Логика доказуемости - краткое введение. Theoria 62 (1996), стр. 19–61.
• Крейг Сморински, Самореференция и модальная логика . Springer, Berlin, 1985.
• Роберт М. Соловей, `` Интерпретации доказуемости модальной логики '', Израильский математический журнал, Vol. 25 (1976): 287–304.
• , Логика доказуемости, из Стэнфордской энциклопедии философии.

.