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

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

Примеры

Существует ряд логик доказуемости, некоторые из которых описаны в литературе, упомянутой в § Ссылки. Базовая система обычно обозначается как GL (от Гёделя – Лёба ) или L или K4W ( W означает обоснованность ). Она может быть получена добавлением модальной версии теоремы Лёба к логике K (или K4 ).

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

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

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

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

История

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

Обобщения

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

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

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

Ссылки

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

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

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