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

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

Примеры

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

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

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

И правила вывода таковы:

• Метод установки : Из p → q и p заключаем q ;
• Необходимость : От $\vdash$ п сделать вывод $\vdash$ □ p .

История

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

Обобщения

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

См. также

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

Ссылки

• Джордж Булос , Логика доказуемости . Издательство Кембриджского университета, 1993.
• Георгий Джапаридзе и Дик де Йонг, Логика доказуемости . В: Справочник по теории доказательств , С. Басс, изд. Эльзевир, 1998, стр. 475–546.
• Сергей Н. Артемов и Лев Беклемишев , Логика доказуемости . В: Справочник по философской логике , Д. Габбай и Ф. Гюнтер, ред., том. 13, 2-е изд., стр. 189–360. Спрингер, 2005.
• Пер Линдстрем , Логика доказуемости — краткое введение . Теория 62 (1996), стр. 19–61.
• Крейг Смориньски, Самореференция и модальная логика . Шпрингер, Берлин, 1985 г.
• Роберт М. Соловей , «Интерпретации доказуемости модальной логики», Израильский математический журнал , Vol. 25 (1976): 287–304.
• Ринеке Вербрюгге , Логика доказуемости , из Стэнфордской энциклопедии философии .

Внешние ссылки

• «Логика доказуемости» Запись Инеке Вербрюгге в Стэнфордской энциклопедии философии.