Классификация пропозициональных логик доказуемости тема автореферата и диссертации по математике, 01.01.06 ВАК РФ

21 г, Ь 9 Ъ

РОССИЙСКАЯ АКАДЕМИЯ НАУК МАТЕМАТИЧЕСКИЙ ИНСТИТУТ ИМЕНИ В.А. СТЕКЛОВА

На правах рукописи УДК 510.65

БЕКЛЕМИШЕВ Лев Дмитриевич

Классификация пропозициональных логик доказуемости 01.01.06 - математическая логика, алгебра и теория чисел

Автореферат

диссертации на соискание ученой степени кандидата физико-математических наук

Москва -1992 г.

РаОота шлсшшла в Матоматическом .Институте РАН им. В. Л. Стеклова

Официальные оппоненты: доктор физико-математических

наук В. П. Оревков

кандидат физико-математических наук В. Е. Плиско

Научные руководители:

член-корреспондент РАН С. И. Адян

доктор физико-математических наук С. Н. Артемов

Водущая организация: Институт Математики СО РАН

00

Защита состоится " В " 1992 г. в 14 часов на

заседании специализированного совета Д 002.38.02 при Математическом Институте РАН им. В. А. Стеклова по адресу: Москва, ул. Вавилова 42.

С диссертацией можно ознакомиться в оиСлиотоке Математического Института км. В. А." Стеклова

Автореферат розослан " -? сг+чТ-А^-С. 1592

Учоный секретарь специализированного совета доктор физико-математических наук

М. 11. Мшшнв

ГОСУДАРСГ«сп;.А Я

БИБЛИОТЕКА _

- , Обяая характеристика.

Идея аксиоматичоского подхода к изучению доказуемости в арифметических теориях восходит к работе К. Геделя ["?]. К Гедель заметил, что многие естественные свойства доказуемости могут Сить записаны в языке исчисления высказываний, обогащенном новой одноместной связкой модальности о ( ор псншается кок "доказуемо ?>" ). Уточнение этой идеи приводит к центральному для нашей работы понятии пропозициональной логики доказуемости.

Пусть и - аксиоматизируемая арифметическая теория, т. е. порочнелшая теория 1-го порядка, сформулированная и арифметическом языке и содержащая примитивно рекурсивную арифметику рял. о Рг7(х) - построенная К.Годелем арифметическая формула. , выражающая предикат " х есть код Га1 некоторой доказуемой в теории ? формулы л Результат подстановки в модальную формулу р произвольных арифметических предложения вместо пропозициональных букв и расшифровки связки о как формулы Ргэ(х) называется э-переводом формулы р.

Совокупность всех модальных формул. г.ьСиа 5-переводи которых выводимы в некотороП арифметической теории г/, называется додалънш з-представлением яеорли и или логшеой 'доказуелости для пеории 7 оглосипелъно теории, и ( обозначаете.-! ¡/(XI) ). В частности, модальная логика 1?(ТЛ), где тл - множество всех предложении. истинных в стандартной модели арифметики, называется исгяинносшой логикой дохазуслосш.для ?.

Содержательно говоря. модальное представление описывает совокупность всех тех свойств доказуемости во ■ "внутренней" теории которые можно обосновать средствами данной 'внешней" теории и. Так. истинностная логика доказуемисти для ? определяет совокупность всех абсолютно истинных свойств доказуемости в з. а те сзоПства, которые можно обосновать средствами самой теории 7. описываются логикой ^("}). Естественно возникает вопрос об аксиоматизации модальных логик вида 1?(И) и об их разрешимости.

Диссертация посвящена классификации, т. е. описанию всевозможных логик доказуемости получашчхея при варьировании ? и и з классе арифмзтичоских тоориП. ООиая теоре!!а о классификации логик доказуемости является обьединениом результатов нескольких исследователей; завершающие результаты

ошш иолучони автором диссертации [1<]. В частности, к настоящему времени найдены естественные системы аксиом для всех логик доказуемости и полностью исследован вопрос оО их разрешимости. Остановимся Оолоо подробно на истории вопроса.

В монографии [3] Д. Гильборт и П. БерпаПс выписали нокоторыв 'условия на выводимость" в произвольной аксиоматизированноП ари^ютичоскоп теории 5. достаточною для доказательства теорем К. Годеля о ншюлното ( и фактически установленные ранее сам;«-! К. Геделем ). Условия Гильберта-Борнайса были сформулированы М. X. Лесом [в} в следу щам виде: для любых арифметических предложений дно

(нв1) ргу(глл )лРг3(гл-»в1) —. рг3;гв'}),

(нв2) РВА и- Рг3(гЛ*) —♦ рг?{ грг?г ""д"1 я }. .

(нвз) 3-а =» ).

Сам и. Х.ЛоО [в] доказал, что для любого арифметического предложения л

<ь) i- рг, ГГА* ) —• А » У-л.

Как лото -видогь. утворадегшл (нв1)-снвэ). вместо с теоромэП (Ь). шоют характор пропозициональных модальных аксиом и правил ьызода. Соотвотствушое исчисление (называемое мгикой ГсОсля-ЛсСа а.) формально опроделлотся слодуюшим образом:

Аксиомы:

1) пропозициональные) жавяологии;

2) ордо(р-»<1) —» од;

3) ар —» вор.

Правила вывода: *х>аия ропепз. поОсяаиобни.

р о? —► 9

(»0 -5Г ' (ш> -9- '

(Позже било установлено, что правило (и*) можно заменить аксиомой

(1А) о (ар —» р) —♦ ар.

вырэжаюаоЯ формализованная вариант теории М. X. ЛеОа (L). )

Вопрос о полноте сг. koic системи аксиом для доказуемости привлек осоОоо внкманио исследователей по второй половине СО-х годов и бил решен положительно Р. Соловеем [Ю]. который доказал следующую теорему.

Пуст ь з - арифметическая теория, все пеордмы колорой испчнны б стпандаргмой. модели армрмсгмни (в дальнейшем ми Судом называть юпеие ncapiu корректными). Тогда

1) I? (РР.Л) - - GL.

2) 1?(ТЛ) - S s GL{ср-*р)1).

Результата Р. Содовая стимулировали дальнего интененвмоо исследование логик доказуемости (см. [5,9]). В [1,2] С.Н. Артемов предложил oOxiül подход к проблема классификации логик доказуемости. основашшл на введенном ии понятии следа модальной логики. 13 русло этого подхода Cswn полушнц слодугано результаты.

В [i] установлено, что логиками доказуемости являются все константные расширения логики gl. а в [2] доказано, что эти расширения исчерпываются логиками вида

GL = CL(F inea), аси И а п

CL~ = CL\\Jnt(f Fn), fizu И u\0 конечно, где F s on,,i —» oni.

n

В [4] йиа найдена логика доказуемости

D г СЦ-ioi, o(opvaq) —> apvoq).

и а силу результатов [2] отсюда таюха следуот. что логиками доказуемости являются логики

sp = sr'GLp 11 Dp = Dnci.^ «зси и конечно).

В [И] установлено. . что логики доказуемости, не содер-

Злесь и ниже выражение gl(. . . } означает замикание с помокьп прапия ¡nodus ponens и поястанрвки множества »се* теории gl и перечисленных в скобках аксиом.

жашнося л я.- исчерпываются логиками сь~. а логиками и ¡да 1?(1) лилпится мть си и сцо"х) для всех пей.

В (2) задача полного описания логик доказуемости для корректных теория Сила сведена к описанию логик доказуемости, лежащих между «гг. и 5.

В настоящей работе доказано, что других логик доказуемости, кроме перечисленных вше, нот, а шло! то С. стая логина Ооказуслосаи совпаваса с одной из логик

{*) С1.а, С1.~, иди Вр (а,реи. и\р конечно).

Дано олисанио истинностных логик доказуемости. а таюко всевозможных логик из списка (*), реализующихся при варьировании одной лишь вноонеП теории (для произвольной фиксированной внутренней теории).

В заключительно!! параграфо диссертации рассматривается ряд вопросов, представляющих интерес в связи с оОщеП теоремой о классификации логик доказуьмсг.ти: эффективность этоЛ классификации; разрешимость логик локазуемости; нуморнческая инвариантность логик докозуомости. то ость кх зависимость от выбора арифметической формулы РСу(х). определяющей доказуемость во внутренней теории. ?; приводятся примеры вычисления модалышх продставлошШ некоторых "остоствешшх" пар тоорий: наконец, полностью исследуется вопрос оО интерполяционном свойстве Кройга для логик доказуемости. »

Результаты диссертации докладывались на 9 и 10 Всесоюзных конференциях по математической логике (Ленинград. Г.<хЗ и Алма-Ата. 1990). нескольких международных • конференциях, семинарах кафедры математической логики механике математического факультета МГУ.

Содерхание работы.

Диссертация состоит из введения и основною текста, разбитого на 8' параграфов. ООшиП ооьем диссертации 101 страницы. Список литературы содержит 24 наименования. Нумерация утверждения отражает их расположении внутри нирагр>;ив. Нсклкяешш составляют теоремы, являющиеся основными результатами д!!ссерташш; для них принята однозначная нумерации.

В §1 вводятся основные понятия диссертации. Одно из самых

-э-

сатих ~ понятно ранга аксиоматизированной арифметической теории (п.1.5). Для данной теории 5 рассмотрим бесконечную последовательность теорий <7п)пЫ . определенную по правилам:

J з 1. 7 я У •> ConfJ ). о n»¿ п • п

где сол(?п> - гедвлевская формула непротиворечивости теорни з .

Рангом rk(J¡ теории J называйся наименьшее леи такое, что теория противоречива, если такое п сущоствуэт. и ш - в противном случае. Ранг теории j яоляетсЛ корой со близости к противоречивой теории. Теории бесконечного ранга мы Оудом называть сильно непрохиеоречивизи.

Сильно непротиворечивые Teopira классифицируются по степени их корректности. Как уко Сало отмечоно выше, теория и наэисаотся хорренлаюй. осли все теоремы v истинны в стандартной модели арифметики. и называется некорректной, если истинными являются аса £ -прзяложвния. доказуемые в у. в приводятся естественные примеры, показывающие. что классификация теорШ по рангу и степени коррочтности ¡шЕырохдона.

52 иосзязеи построению семантики Крипко для трех наиболее

важных (помимо логики et) логик доказуемости: s. d и cl .2 ■

U

Доказывается полнота этих логик относительно некоторих специальных классов (бесконечных) моделей Крипко. называемых соответственно s- . о- и cl^-moдолями. а такхо их разрешимость.

В §3 излагаются необходимо для дальнейшего результат!; из работ 1Ю,2]. В первой части этого параграфа приводится так называемая конструкшш Солобоя [ю]. а во в го рой дается краткое изложение техники следов модальных формул и логик 12]. Оактичоски. результаты, полученные в работе ( г j для корректных внутренних тсориП. переносятся на случай произвольных сильно непротиворечивых теория. В частности, вопрос о классификации лигик доказуемости для сильно непротиворечивых теорий сводится к описанию логик доказуемости, логоцих между clu h s. Упроааотся доказательство тооремы Внссерз [И]. описывающей логики доказуемости. но содержащихся в логико s.

В '¡i понятия простой модели Крипко и спроделяг.аоП формулы

''ляя яогики S тлквя егмлнтнк» Аыаа построена в lili и. нпплвисиыо. в I б 1 .

для такоП (.юдоли (см. (2}) распастраняются на класс cl^-ыодолой. В §5, опираясь на технику, изложенную в 64, мы показываем, что всякая непротиворечивая логика доказуемости, строго содержащая d. совпадает с логикой s. Тем cam.!. учитывая результаты §3. обцая проблема глассифпкащш логик доказуемости сводится к описанию логик доказуемости, лежащих меад glu и о.

В §6 доказывается, что люОал логика доказуемости, строго содержащая glu. содорашт и логику о. Этот результат, являющийся наиОолее содержательной частью работы, фактически завершает общую классификацию логик доказуемости.

• Основные результаты диссертации формулируются и доказываются в §7. Прежде всого. суьашруя результаты §§2-6. мы получаем следущую теорему о полноте классификации логик доказуемости.

ТЕОРЕМА 1. Всякая логина Ооказуелосяи собпадаеи с одной из слеОукших логин:

GLa, CL~, Dp, (а. Дси. u\fJ конечно). {*)

Теорема 2 показывает, что каждая логика из списка (*) фактически реализуется как логика доказуемости для любоП сильно непротиворечивой внутренней теории.

ТЕОРЕМА 2. Если аксиолояизированная теория ? сильно непротиворечива. по

' ¡У (РИА) - I?(3 ) - вь.

1?(ТЛ) - 5. о или

и всякая логика из списка (*) яЗляеися з-представлением подходящей арифметической аеории.

Теорема 3 дает описание всевозможных истинностных логик доказуемости.

ТЕОРЕМА 3. Истиююсвныхи логиками доказуеяосяи яЗхчхдса логики

в. о. ы. и СЦГ ), леи {**)

u кольно они. Причел для „vsCoû ахсиолазилзироватой пеории з

a) l'ctaj-s о (теория з >:оррс:?та);

0) l3(ta)-d » (авария з £ -?горрекина. но не коррекгма);

в) о (яеория 7 ко яблясася z^-коррсхпной. но

Г) LJ(TA)'Gl{->Fn) о rk(7)-n (ОСЛИ Пчо.).

Теорема 4. дсполняюцая'теорему 2. для произвольной внутренней тоории з конечного ранга-описывает совокупность всевозможных логах доказуемости для з. Оказывается, что эта совокупность однозначно определяется рангом теории т.

ТЕОРЕМА 4. Пусть 7 - аксиожаяизирсванная гсеир&я" ранга п<и. ГогОа

.¡У(ГА) - СЦлГп), l7(pra) - cl(on*'i), I?(1) - GL(ani )

и логwat доказуелосяи Оля з исчерпивахп все яьринеови расширения логики gl(o""i|. то есть логики gl~, u\az(o,... ,п).

В заключительном параграфе диссертации рассматриваются отдельные вопросы, представляющие интерес в связи с общей теоремой о классификации логик доказуемости. В п. 8.1 обсуждается эффективность классификации логик доказуемости. В п. 8.2 приводится ряд примеров вычисления модальных представлений конкротных "естественных" пар тоорий. П. 8.3 посвящен исследованию вопроса о нуморической инвариантности логик доказуемости, то ость зависюдасти. этих логик от выпора арифметической форели, определяющей доказуемость во внутренней теории. Наконец, в п. 8.4 полиостью исследуется вопрос об интерполяционном свойство Кройга для логик доказуемости. Показано, что логиками доказуемости, на удовлетворяющими этому свойству, являются лишь логики Dp (Peu, конечно).

Мне хотелось бы выразить сердечную благодарность своим

научным руководители.! за постановку задачи, внимание, проявленное к работе, и многочисленные ценные замочання.

ЛИТЕРАТУРА

1. Артемов С.Н. Арифлатачески полнио модальные теории. -Семиотика и Информатика. Ы. :ВИНИТИ. 1980. вып. 14. стр. 115-133.

2. Артемов С. К. О модальных логиках, аксиоматизирующих доказуемость. - Известия *ЛН СССР. сер. матом.. 1985. т. 49. ¡.'6, стр. 1123-1154.

3. ГильОорт Д.. БорнаПс П. Основания математики. Г.2: Теория доказательств. Ы Наука. 1982.

4. Джапаридзе Г. К. Модально-логические сродства исследования доказуемости. Канд. дасс.. 1АГУ. 1986.

5. Boolos G. The Unprovability of Consistensy; An Essay in Modal Logic.- Cambridge University Press, Cambridge, 1979.

6. Booloa G. Provability, Truth, and Modal Logic. - Journal of Philosoph. Logic, 1981, v.9, pp.1-7.

7. Gcc'el K. Eino Interpretation des intuitionistischen Aussagan-kalkuls. - Ergebnisse Math. Kolloq., 1933, Bd.4, S.39-40.

8. M.H.Lob. Solution of a problem of Laon Henkin. - Journal of Symbolic Logic, 1955, v.20, pp.115-118.

9. Smorynski C. Self-Reference and Modal Logic. Springer-Verlag, Universitext, 1985.

10. Solovay R.H. Provability interpretations of nodal logic. -Israel Journal of Mathenatic3, 1976, v.25, pp.287-304. .

11. Vicser A." The provability logics of recursively enumerable theories extending Peano arithsetic at arbitrary theories extending Peano arithmetic. - Journal of Phiiosoph. Logic, 1904, v.13, pp.97-113.

РАБОТЫ АВТОРА ПО ТИЛЕ ДИССЕРТАЦИИ

12. Нормализация выводов и интерполяция для. некоторых логик доказуемости. - Успехи War. Наук. 1987. т. 42. вып. 6 ( 268). стр. 179-180.

13. Логика доказуемости Сез интерполяционного свойства Kpellra. -Математические заметки. 1989. т. 45, W6. стр. 12-22. .

-914. О классификации пропозициональных логик доказуемости. -Известия АН СССР, 2эр. мат., 1969. т. 53. «5. стр. 915-943.

Подл. « псч. 15.06.92 г. Тмраш 100 акз. Закаа * 16175 Централизованная типография ГА "Соеастройнатермалоа"