Қамсыздандыру логикасы - Provability logic

Қамсыздандыру логикасы Бұл модальді логика, онда қораптың операторы (немесе «қажеттілік») «бұл дәлелденетін» деп түсіндіріледі. Мәселе ақылға қонымды байдың дәлелді предикаты туралы ұғымды қабылдау формальды теория, сияқты Пеано арифметикасы.

Мысалдар

Бірқатар дәлелдеу логикасы бар, олардың кейбіреулері сілтемелер бөлімінде аталған әдебиеттерде қамтылған. Негізгі жүйе әдетте GL деп аталады (үшін Годель -Лоб ) немесе L немесе K4W. Оны модальды нұсқасын қосу арқылы алуға болады Лоб теоремасы дейін логика К. (немесе K4).

Атап айтқанда аксиомалар GL - классикалық пропозициялық логиканың таутологиялары және келесі формалардың біреуінің барлық формулалары:

• Тарату аксиомасы: □(б → q) → (□б → □q);
• Лёб аксиомасы: □(□б → б) → □б.

Және қорытынды жасау ережелері мыналар:

• Поненс режимі: Бастап б → q және б қорытындылау q;
• Қажеттілік: Бастап ${ displaystyle vdash}$ б қорытындылау ${ displaystyle vdash}$ □б.

Тарих

GL моделінің бастамашысы болды Роберт М. Соловай 1976 ж. Содан бері 1996 ж. қайтыс болғанға дейін өрістің басты шабыттандырушысы болды Джордж Булос. Бұл салаға айтарлықтай үлес қосты Артемов Сергей, Лев Беклемишев, Джорджи Джапаридзе, Дик де Джонх, Франко Монтанья, Джованни Самбин, Владимир Шавруков, Альберт Виссер және басқалар.

Жалпылау

Түсіндірмелік логика және Джапаридзенің полимодалдық логикасы дәлелдеу логикасының табиғи кеңеюін ұсыну.

Сондай-ақ қараңыз

• Гильберт-Бернейстің тұрақтылық шарттары
• Түсіндірілу логикасы
• Крипке семантикасы
• Джапаридзенің полимодалдық логикасы
• Лоб теоремасы

Әдебиеттер тізімі

• Джордж Булос, Жетімділіктің логикасы. Кембридж университетінің баспасы, 1993 ж.
• Джорджи Джапаридзе және Дик де Джонг, Дәлелділіктің логикасы. In: Дәлелдеу теориясының анықтамалығы, С.Бусс, ред. Elsevier, 1998, 475–546 бб.
• Артемов Сергей және Лев Беклемишев, Қамсыздандыру логикасы. In: Философиялық логиканың анықтамалығы, Д.Габбай және Ф. Гюнтнер, баспа, т. 13, 2-басылым, 189-360 бб. Springer, 2005 ж.
• Линдстрем, Проверативтілік логикасы - қысқаша кіріспе. Теория 62 (1996), 19-61 бет.
• Крейг Сморински, Өзіне сілтеме және модальды логика. Шпрингер, Берлин, 1985.
• Роберт М. Соловай, «Модальды логиканың провизиялық түсіндірмелері», Израиль Математика журналы, т. 25 (1976): 287-304.
• Rineke Verbrugge, Қамсыздандыру логикасы, бастап Стэнфорд энциклопедиясы философия.

Бұл логика - қатысты мақала а бұта. Сіз Уикипедияға көмектесе аласыз оны кеңейту.