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

ЛЕНИНГРАДСКИЙ ГССУДАРСТВЕННЬЙ "ОРДЕНА ЛЕНИНА И ОРДЕНА ' ^

ТРУДОВОГО КРАСНОГО ЗНАМЕНИ УНИВЕРСИТЕТ ИМЕНИ А.А.ДЦАНОЗА /

На правах рукописи

ЗАСЛАВСКИЙ ИГОРЬ ДОИТРИЕЭДЧ

Уда 510.6:510.25:519.712

СИМИЕШЯЕСКАЯ КОНСТРУКТИВНАЯ ЛОГИКА И НЕКОГОШЕ ЕЁ .

ч

пишсшш

01.01.06 - гате^атичаская логика,алгебра и теория чисел)

АВТОРЕФЕРАТ диссертации на соискание .ученой стервни доктора физнко-катекатических наук

Чочгл&ь»* Псрс&о^ Не Ь /к выслан 3 из п /о 3 г. Враг а н а

¡2 Сл.-\bc\Loc. оикс- По¿ъ амI-а

!

П Моак^М , !>дсчеГН(,1ц счсТ И<? мер к ИТ д И Л И. -— о I I * ,

Ленинград - 1987

Работа выполнена в Вычислительной центре Академии Наук Армянской ССР и Ереванского государственного университета

Официальные оппоненты: доктор физ.-мат, наук А.О. Слисенко доктор физ.-мат. наук А.Л. .Семенов . доктор физ.-мат. наук'Л.Л. Максимова

Ведущая организация: Московский государственный , университет имени М.В. Ломоносова

Защита состоится " "_198_

в час. на заседании специализированного совета Д 063.57.29 по защите диссертаций на соискание ученой степени доктора физико-математических наук при Ленинградском государственном университете им. А.А.Жданова (адрес совета: 198904,Ленинград, Петродворец,Библиотечная пл.,2,математико-механический факультет Защита будет проходить по адресу:I9I0II,Ленинград,Наб.р.Фонтанк; д.27',ауд.ЗП,в помещении Ленинградского отделения Математическо1 института им. В.А.Стеклова АН СССР.

С диссертацией можно ознакомиться в библиотеке им. А.М.Горького Ленинградского государственного университета

Автореферат разослан "_" ;__198_

Ученый секретарь специализированного

совета,пррфессор Ю.А. Давидов

'Актуальность т е м ы., В настоящее время постанов-га прЬблем формализации и автоматизации процессов логической цедукЦии связывается с введением и исследованием оценок досто-ей^яЪсти суждений в рамках формальных логических систем. Рассмотрение многоступенчатых оценок достоверности суждений послужило в свое время отправной идеей для построения многозначных логик. Однако, несмотря на значительное развитие, которое ныне получили многозначные логики,они рассматривались до сих пор лишь в.качестве предмета математического исследования, но не логической основы дедукции в математических теориях.Вопрос об учете многоступенчатых оценок достоверности суждений в языке исследователя (метаязыке) математических теорий неоднократно ставился в литературе, но не получил удовлетворительного разрешения.Актуальность таких исследований определяется,в частности,их приложениями в вопросах автоматизации процессов логической дедукции и в вопросах преобразования и оптимизации алгорифмов и машинных программ..■

Це-ль работы - построение логического аппарата, который вводит логические оценки достоверности сундений вида "истина", ''ложь", "неопределенность" в-'математический язык исследователя и применяется для построения и исследования граф-схем и алгоритмических операторов.

Методика. В работе, народу с традиционными методами математической логики и теории алгорифмов,существенную роль играют разработанные автором методы логического представления конструктивных множеств,граф-схем,алгорифмических операторов при помощи неклассического логического аппарата (с использованием вводимых в работе новых логических операций,в частности, односторонней конъюнкции и дизъюнкции).

Научная но визна. В диссертации впервые построена логико-математическая система,вводящая оценки истинности сузде-ний "истина", "ложь", "неопределенность" в математический язык исследователя,в частности,включающая сузздения,выражаемые замкнутыга формулами,недоказуемыми и не опровержимыми ни в каком непротиворечивом расширении системы.Впервые установлены взаимосвязи меящу конструктивной логикой и трехзначной логикой Лукасевича,установлены понятия сильного и слабого равенства -множеств,сильной и слабой разрешимости множеств{установлены теоремы, показывающие естественность употребления этих понятий в

конкретных ситуациях,связанных с исследованием алгорифмов и рл-горифмических операторов. Впервые строятся и исследуются логические представления алгорифмов и алгоритмических операторов средствами многозначных неклассических логик.В одной из работ* автора,отраженных в диссертации, были впервые установлены алгебраические представления граф-схемных алгорифмов и возможности замены операторов перехода операторами цикла в схемах.алгорифмов и программ.

Практическая и теоретическая ценность. Результаты работы, относящиеся к логическим и алгебраичзскилз описаниям и преобразованиям алгорифмов,были'фактически использованы в раде работ в целях исследования возможностей .граф-схемных алгорифмов,а также при построении некоторых практических алгоритмических языков ^;они могут быть использова ны твкж.8 в целях преобразований и оптимизации алгорифмов и прог рада.Результаты,относящиеся к логическим и логико-математическим системам,могут быть использованы для формализации,построения и исследования математических теорий и систем автоматизации процессов логической дедукции,в которых участвуют неопределенные сувдения и.частично определенные предикаты.

¿проб а ц и я. Результаты работы излагались в сообщениях автора на 4-м Всесоюзном математическом съезде в Ленинграде в 1961г.,на Международном конгрессе математиков в Москве в 1966г. в цикле докладов,прочитанных во время летней школы по математической логике и основаниям математики в Обнинске в 1971г.,в сообщениях на 3-й,7-й,8-!'; Всесоюзных конференциях по математической логике (Новосибирск,1974г.;Новосибирск,1984г.;Москва,1986г. в докладах на семинарах по математической логике в ЛОЩ чм.В.А. Стеклова АН СССР,в ВЦ АН СССР.вВЦ АН Арм.ССР.

Публикации. По теме диссертации опубликованы 9 ра-

1 Заславский И.Д. Граф-схемы с памятью.-Труды Мат.инст. им. В. А. Стеклова, 1964, т.72, с.99-192.

^ См.,например: Гаврилов Ы.А..Дввятков В.В..Чичковский А.Б. язык операторных схем параллелных алгоритмов с памятью (язык ОСПАШВ кн.:Абстрактная и структурная теория релейных устройств автоматизация логического синтеза,-Ы.:Наука,1975,с.53-61

от (I) - (9)¡монография (1978г.).статьи (1964г.,1973г.,1975г., 979г.) и сообщения (1965г.,1974г.,1984г.,1986г.).

Объем работы. Диссертация изложена на 296 странных (включая библиографию на II страницах) и состоит из введения I четырех частей,подразделяемых на 24 параграфа.Библиография юдеряит 104 названия ргбот советских и иностранных авторов.

СОДЕРЖАНИЕ РАБОТЫ

Логическая система, вводимая и исследуемая в работе, основа-1а на равноправной трактовке понятий конструктивной истинности I конструктивной ложно'-™ суждений,и,вследствие этого, названа 'симметрической конструктивной логикой".Эта логика рассматривался в работе двояко объзкт исследования и как логическая основа изложения.Предг^то?? исслэдования в работе являются логи-мские и логико-матеш/гкчесниг исчисления (в том числе исчисле-шя симметрической конструктивной логики).алгорифмы и.алгориф-шческие операторы,фун:гц;ш трехзначной логики и их представле-отя средствами симметрической конструктивной логики.В качестве югической основы изле.-зния симметрическая конструктивная логи-са выступает как систем правил умозаключений (определяемая в }4),в соответствии с потерей проводятся доказательства, излага-!мые в работе.

Работа состоит из четырех частей.В первой части (§1-§5) эпределяется симметрическая конструктивная логика,в частности, зводится основное понятие симметрической истинности суждений, 1 также определяется система правил умозакллчений, в рамхах {оторой проводятся дальнейшие рассмотрения.Во второй части (§6--§15) исследуется симметрическое конструктивное исчисление предикатов и его взаимосвязи с предикатными исчислениями класси-?еской логики, традиционной конструктивной логики и трехзначной логики Лукасевича.Шри этом классическое исчисление предикатов понимается обычным образом^;под трехзначной логикой Дука-гевича понимается логическая система, введенная Лукасевичем4

^ Клики С.К. Введение в метаматематику.- И.:йзд-во иностр. яиг.,1957*- 527 с.(с«.§31~§37,§73).

"к 0 се I-у/о*/, 19Ю , , г.^69—"(И; ^ см.такясе Клини С.К.,цит.соч. ,с.298-58».

- посредством трехзначных таблиц истинности;под"традиционной конструктивной логикой" понимается любая из конструктивных семан-ческих систем^"®,согласованных с конструктивным (интуиционистским) исчислением предикатов®.В третьей части (§16-§21) иссле-. дуются симметрические конструктивные арифметические системы и их- взаимосвязи с системами формальной арифметики,основанными на иных упомянутых выше логиках.В четвертой части 1*21-§24) исследуются приложения симметрической конструктивной логики к логи-, ческим описаниям и преобразованиям алгорифмов и алгорифмических операторов;для этого,в частности, вводится и исследуется язык граф-схем с памятью и устанавливаются некоторые логические представления алгорифмов в этом языке. .

В первой части изложение ведется в рамках традиционной конструктивной логики и арифметики.Во второй и третьей части изложение ведется в рамках симметрической конструктивной логико-арифметической системы,определенной в §5.В четвертой части изложение ведется в рамках расширенной симметрической конструктивной логико-арифметической, системы Н5АДоопределяемой в §18.

В §1 работы вводится в рассмотрение логико-арифметический язык с обычными логическими операциями ,1 ,V,3 и с

функциональными символами для всех примитивно-рекурсивных функций; этот язык может рассматриваться как объединение логико-ма-

5 Клики С.К., цит.соч.3, §82. .

с ■

Марков A.A. О логике конструктивной математики.- Вестник МГУ . им. М.В.Ломоносова,1970,сер.I,т.2,с.7-29. 7

Шанин H.A. 0 конструктивном понимании математических суждений.- Труды Мат.Инст. им.В.А.Стеклова,19Ь8,т.52,с.266-311.

® Шанин H.A. Об иерархии способов понимания суждений в конструк тивной математике.- Труды Мат.Инст. ий.В.А.Стеклова,1974,т.129, с. 203-266.'

9 3

Клини С.К.,цит. соч. , с.94. ' . .

тематических языков,определенных в книгах С.К.Клини^ и P.Ji. Гудстейна**.Эквивалентность А~В, слабая импликация AsB, сла-5ая эквивалентность А~В, слабое отрицание ОА,односторонняя конъюнкция А&В, односторонняя дизъюнкция AVВ,сильная конъ-онкция А ¿В, ослабленная дизъюнкция AvB определяются посредством формул, соответственно, (Аoß)Цв =>Д), А = (А = В), (А =

Операции о^и С" над формулами арифметики определяются следу-ощими правилами (§2):

1. Если А - элементарная формула,то = А j 6"~(A)=1A;

2. cr+(Atcß)=:cr-XA)&6'+(e)jG'-(Ag:B)=aJ-(A)ver-(e);

3. <S'+(AvB)-^(A)v6'i(0)j^-(Ave) = 6'-CA)&ö-(:ö)i . 4

4 6-+fА => => fa);

5. C + ("JA) - {^"(A) ;

6. <T(V*A) = Vx6"h(A); ^-(VxA)=ЭхбГ-(А);

7. (ЭхА) = Зх&ЧА);e"(3x А) = V* «Г"CA).

Формула А называется симметрически истинной (соответственно, ложной),если формула 5"+(А) (соответственно,с*"(А)) истинна в традиционном конструктивном смысле. Формулы А и В называются эквивалентными (соответственно,слабо эквивалентными),если формула АЛВ (соответственно, А~В) симметрически истинна.

Определения операций и б" ~сходны с определениями операций и V0, введенных Н.А.Шаниным*^,однако свойства б"~иные, чем у Д0 и ^;можно сказать, что Дри V0 определяют некоторые типы конструктивной истинности и конструктивной ложности в пределах традиционной конструктивной логики,в то время,как на основании и б" вводится логическая система, отличная от традиционной конструктивной логики.Фактически формулы c'^Viб"(bJmo-

[0 Клини С.К.,цит.соч.3, §1б-§18.

^ Гудстейн Р.Л. Рекурсивный математический анализ.-М.:Наука, [970,.- 472 с.¿вступительная статья H.A.Шанина,с.53-56.

[2

Шанин H.A. 0 некоторых логических проблемах арифметики.-Тру-Мат.Инст. им.В.А.Стехлова,1955,т.43,с. 81.

гут рассматриваться как некоторые описания соответственно "области истинности" и "области ложности" предиката, выражаемого формулой А.При такой интерпретации определения<Г+и б" " имеют весьма прозрачный "геометрический" смысл (например, область истинности конъюнкции предикатов есть пересечение их областей истинности; область ложности конъюнкции предикатов есть сумма их областей ложности).Согласно теореме 21.I,устанавливаемой в §21, для любых непересекающихся конструктивных множеств, описываемых формулами А и В традиционной конструктивной арифметики,существует арифметическая формула D ,для которой ) и <5 (2Э эквивалентны.в традиционной конструктивной арифметике соответс! венно А и В,т.е. заданные множества служат для Х> соответствен^ областью истинности и областью ложности.

Правила содержательных умозаключений симметрической конструн тивной логики устанавливаются в.§4;предварительно мы рассмотрим формальные исчисления,вводимые во II и III части.Основные предикатные исчисления симметрической конструктивной логики вводят ся в §6 (секвенциальные исчисления fVS , N$ ,G-S ) и в §7 (формульное исчисление HS ).Опишем исчисления NS и HS .Объекты, выводимость которых рассматривается в A/S ,суть секвенции^ с многофорыульныыи (быть может,пустыми) антецедентами и однофор-мульными или пустыми сукцедентами (по техническим причинам такие секвенции обозначаются посредством A>(oA5o...®Arr»B или A,oAj0...°Ah~* вместо обычных обозначений ...,А„-*В или

Ал,Аг,,..,АП-* );формулы,из которых строятся секвенции,суть предикатные формулы с функциональными символами*^.Исчисление N1 задается следующими схемами аксиом и правилами вывода (в которых А и В суть произвольные предикатные формулы, Гий - произвольные, быть может пустые наборы формул, соединенных знаком I - произвольный терм, х и у - произвольные предметные пере

^ Генцен Г.Исследования логических выводов,- В кн.:Математическая теория логического вывода.-М. :Наука, 1967,с.9-76 (см. также Клини С.К.,цит.соч.^,§77).

^ Мальцев А.И. Алгоритмы и рекурсивные функции.- М.: Наука, 1965.- 392 с. с.284-287.

энные, 0 - пустое слово или формула; [А^гозначает результат одстановки терма Т вместо свободных вхождений переменной х в ормулу А;в правилах вывода 22 и 28 предполагается,что перемен-ая у не входит свободно в Г;в правилах вывода 25 и 27 предполагается,что переменная у не входит свободно ни в Г, ни в Дни 0;в схемах аксиом23,24,26,29 предполагается,что подстановка [А]* допустима в обычном смысле этого определений

. ГоА-> В 1У7В ~>1А Г-* А=> В

I. тВ*(А=В)-*1А ; >. т(А= В)~* А ;

к-Ъ-гк&Ъ ; >. А&В-*В ;

!. ТВ-»Ч(А£В); .

А-»Ау В ;

1.

>. _

Г'АУВ ?. 1 ^kvЪ)-*^k ;

А-»пА ; [. А»1 А-* ;

Г'В'й 0

2. А.(АэВ)-»В ;

4. А-тВ->^А=В) ; 6. 1(А=В)-^1В ; 8. А^В-»А ; 10. пА-*7(А&В) ; 12. 1МА-Д-*0 Г» ТВ'*-» Г" т(к£В)*л ~*9 14. В->А\/В ; Хб. ТА» 1В^1(АУ В) ;

Л ~> 9

3. \/хА-»[А], 5. Г° Т А » Л

7.

Э. Г.

3.

ГоТУ^ А»Л->8 Г» А о л 9

&

Г о Ас

ЛЗхА^П [А^ Гей —90

Г-А»В ° & ■

е

9

î»А«4 ->> 0 5. Г-*А Г»А

18. Т(АИВ)' ;20. 71 А->А ; 22. Г ->А

•ТВ

Г->

24. 26.

1 [А]1

1У хк -ЗхА ;

28. Г—> 7 А

30. 32.

34.

Г-* ТЗ^А

А-»А ; Г —

Г->А

• Г» А» А • Л -

е

Г'Дод-» е

— (сечение).

Г 0

Формула А называется выводимой в ,если в А/_5 выводима секвенция-^-А. Исчисления N5 и СБ (определения которых для краткости здесь не приводятся) могут рассматриваться как ыоди-

*

фикации исчисления J!L5 ;для исчисления С б справедлива теорема об устранении сечений (§15).

Объекты, выводимость которых"рассматривается в исчислении И ~ суть предикатные формулы с функциональными символами.Исчисление Н$ задается единственным правилом вывода

А А°В В

у

ч следующими схемами аксиом (где обозначения А,В,х,Т, [А]т , имеют такой же смысл, как и ранее; С иР - произвольные предикатные формулы; V - произвольныйбыть может,пустой набор кванторов общности по произвольным предметным переменным; в схемах аксиом 15 и 18 предполагается.что переменная х не входит свободно в 1) ;в схемах 14 и 17 предполагается, что подстановка £аДт допустима):

I. 9"(А=(В=>А)) ; 2. £((А= (В=>С))=> (В=> (А=>С))) ;

3. V ((А = В)=>((В=С)=>(А=С))) ;

4. У((А?В)=((7В=7А)='(А='В))) ;

5. ^((А^В)3 (ТВэТА)) ; б. £(А=>ПА) ;

7. у(ПА=А) ; 8. V ((А^В)=>А) ;

9. ^ ((А&В) =>В) ; 10. V ((С^А)'((С='В)='(Со(А<£В))))

II. У(А=(АУВ)) ; 12.'^(В^(А^В)) ;

13. У((А=>С)=>((В=>С)=> ((АУВ)= С))) ;

14. ^(УхА^А^) ; 15. V (Тэ^Ухр) ;

16. ^(Ух(А=>В)^ (3 хА э "3 хВ)) ; 17. 9 3 хА) ;

18. 9"(ЗхРэР) ; 19. \/х((АрВ)э ( УхАз "/хВ)) ;

20. ух((а=?В):=>(3 хАгЗ хВ)).

В §7 устанавливается,что выводимость предикатной формулы в исчислении Н5 эквивалентна её выводимости в .N5 (а также и в исчислениях А/5 и£5 );таким образом, можно говорить о едином понятии предикатной формулы,выводимой в симметрическом конструктивном исчислении предикатов. Система симметрической конструктивной арифметики Н5А, вводимая в §16,может быть определена посредством правила роп-е.пе .схем аксиом исчисления Н5(понимаемых теперь как схемы арифметических формул) и арифметических аксиом,вводимых так же,как аксиомы и схемы 13-21 в формальной системе С.К.Клинике той лишь разницей,

15 Клини С.К.,цит.соч.3,с.77.

о схема аксиом индукции записывается в виде [А] \/хА)) ,во всех аксиомах добавляются кванторы общности ) всем имеющимся свободным переменным,и к аксиомам 18-21,опре-:ляющим примитивно-рекурсивные описания сложения и умножения, >бавляются аксиомы, определяющие примитивно-рекурсивные они-шия всевозможных других примитивно-рекурсивных функций.

В §4 и §5 устанавливается,что всякая формула, выводимая в «.метрической конструктивной арифметике,симметрически истинна этсюда следует,что аналогичное утверждение справедливо и для ормул,выводимых в исчислении Н &). Таким образом, построенные счисления согласуются с понятием симметрической конструктивной стинности арифметических формул.

Возвращаясь теперь к правилам содержательных умозаключений имметрической конструктивной логики, устанавливаемым в §4,и к рифметической системе,определенной в §5,отметим следующее:сужения, рассматриваемые на протяжении всей работы,записываются в 1иде формул определенного выше логико-арифметического языка;пра-шла содержательных умозаключений в §4 строятся в виде правил, юстроенных по образцу правил натурального вывода^,аналогичных фавилам исчисления Д/_5 и относящихся к формулам указанного . югико-арифметического языка;арифметическая система в §5 опре-;еляется как логико-математическая теория,основанная на логических правилах из §4 и на арифметических аксиомах, указанных выше;такая система равносильна описанной выше системе

В §$-§7 второй части,как было сказано ранее,исследуются предикатные исчисления симметрической конструктивной логики;теория этих исчислений,как и все рассмотрения второй и третьей части, строится в рамках симметрической конструктивной арифметики. В §8 и §10 вводятся в форме,приспособленной для дальнейших рассмотрений, предикатные исчисления: классические N К, А/К, С К. Ш. традиционные'конструктивные б-Т и НТ,а также исчисления трехзначной логики Лукасевича N1. , N1- , , ;среди них исчисление

получается из Д/ $ добавлением правила вывода

1бГенцен Г..цит.соч.13, с.17-24.-

Го НА —». .

Г-»А '

исчисление Н I. получается из Н5 добавлением схемы аксиом

у(т=>А),

(применяемые обозначения имеют тот смысл,что и ранее).

Доказывается эквивалентность исчислений Н С, [УЬ , Л'Л , &Ь эквивалентность исчислений НК, {\/К, ЫК, £К и эквивалентность исчислений НТ и С.-Т. Для исчисления СЬ справедлива теорема об устранении сечений (§15).Рассматриваемые предикатные исчисления классической (НК, А/К, ЫК., &К) и традиционной конструктивной (НТ,С ТУ логики отличаются от уже известных формализации этих логик лишь техническими особенностями.В §10 устанавливается полнота пропозициональной части исчисления Н (_> относительно истинностных таблиц трехзначной логики Лукасевича (теорема 10.7); этим подтверждается характеризация исчислений НЬ , N1, , Ы11 а как «счислений,описывающих эту логику. Указанное доказательство полноты, в отличие от аналогичных доказательств для большинства известных исчислений,описывающих логику Лукасевича^'не опирается на функциональную полноту рассматриваемой системы пропозициональных операций (фактически система трехзначных операций V, =>,1 логики Лукасевича функционально неполна);в .отличие от указанных выше исчислений многозначной логики,определения исчислений НЬ. ЫЬ » ^Ь , не апеллируют в явном виде к трехзначности рассматриваемой логики.

В §9 вводятся и исследуются погружающие операции из Н £ в НГ,а также погружающие операции из НТ в Н£ (в §10 устанавливается, что те же операции являются погружающими операциями соответственно из Н Ь вНКиизШвНЬ ;таким образом устанавливается общее соотношение между указанными системами, которое можно выразить следующей формулировкой:симметрическая логика так же соотносится с трехзначной логикой Лукасевича,как традиционная конструктивная логика соотносится с классической логи-

1 В, ТигаиеЬЬ Мапу-уаЫеА 1оа1 с£ —

Атв1егИэт:КоЛк-Ноеб. С*тр.

18 Яо«5$вэи % Эевиепк м тапу-ю^иеЛ

кой).Вследствие разнообразия свойств исследуемых погружающих операций,оказывается целесообразным выделить среди них операции, именуемые операциями вложения (§11). А именно,операция Y из формульного исчисления ^±ъ формульное исчисление ^ называется операцией вложения из ^ в ^^если она удовлетворяет следующим условиям:

1. выводимость формулы А в ^равносильна выводимости V(Л) в (иначе говоря, f есть погружающая операция из в ^ );

2. выводимость формулы А => В в равносильна выводимости формулы f (А) => f (В) в (таким образом, f сохраняет упорядочение формул в соответствии с отношением "А сильнее В",);

3. формулы ¥ (А£В), .^(AvB) , f (А=>В), выражаются через f(A) и V>(B) посредством фиксированных пропозициональных формул;

4. формула f( 1 А) выражается через (А) посредством фиксированной пропозициональной формулы;

5. формулы Ч* ( VxA) и f ( ЗхА) выражаются через f (А) посред ством фиксированных предикатных формул.

Говорим,что исчисление ^ вложимо в ^,если существует операция Ч* .являющаяся операцией вложения из ^ в .Доказывается (теоремыП.1-П.5),что имеют место следующие отношения вло-жимости между исчислениями Н5 ,НТ,НКЩ1) все указанные исчисления влокимы в HS ; (2) исчисление НК вложимо во все указанные исчисления; (3) в остальных случаях вложимость отсутствует . Таким образом,симметрическое конструктивное исчисление предикатов в определенном смысле обладает наилучшими возможностями моделирования остальных указанных предикатных исчислений.

Устанавливаются (§12) соотношения между симметрической конструктивной логикой и системами традиционной конструктивной логики с сильным отрицанием*?-,^. Эти соотношение могут быть сфор-

19 Nèlsonl). Coniiruciißfe Saêsli^.-go«'-'' Symè.Lo^.iJl34}lv.16>p. 1 е-ле.

^ Марков А.А.Конструктивная логика.-Успехи мат. наук. ,1950, т. 5> №3(37),с.187-188.

21 NebonD.Ntgalion and separ^ioa OÎ concepts consW^Ve systems,-In: Cons^ructivii*) in mathematics /Ргос. of -t-hc -Amsterda.m:Norik.Hot,ie. Сотр., 1953 , p. £08-Я15.

Воробьев H.H. Конструктивное исчисление высказываний с сильным отрицанием.-Труды Мат.Инст им.В.А.Стеклова,19б4,т.72, с.195-227.

мулированы следующим образом:из систем конструктивной логики с сильным отрицанием в системы симметрической конструктивной логики действуют такие же погружающие операции,что из систем традиционной конструктивной логики в системы симметрической конструктивной логики;аналогичные взаимосвязи устанавливаются для. обратных погружающих операций; "сильной эквивалентности" формул в конструктивной логике с сильным отрицанием соответствует эквивалентность формул в симметрической конструктивной логике.Системы традиционной конструктивной логики с сильным отрицанием, таким образом,оказываются тесно связанными с системами симметрической конструктивной логики;некоторые формальные системы из указанных работ Д.Нельсона и А.А.Маркова при надлежащем их истолковании и при отождествлении суждений в соответствии с их "сильной" эквивалентностью могли бы выступать в роли систем симметрической конструктивной логики.Отличия систем традиционной конструктивной логики с сильным отрицанием от систем симметрической конструктивной логики заключаются в следующем:(I) понятие "сильной"эквивалентности в работах по традиционной конструктивной логике с "сильным" отрицанием встречается лишь эпизодически и нигде не берется за основу;в соответствии с этим в работах по'традиционной конструктивной логике с "сильным отрицанием" широко используются соотношения традиционной конструктивной логики для логических операций, отличных от "сильного" отрицания,хотя многие такие соотношения неверны при "сильном" понимании эквивалентности суждений (например,эквивалентность между Зх(А<5 В(х)) и А& ЭхВ(х),где А не содержит свободно х) и неверны в симметрической конструктивной логике; £2) системы традиционной конструктивной логики с "сильным" отрицанием не приспособлены для употребления их в языке исследователя (что выражается в отсутствии соответствующих систем натурального .вывода); (3) подход,принятый при построении и исследовании этих систем,не позволяет обнаружить взаимосвязи между конструктивной и трехзначной логикой. Аналогичные черты можно отметить у системы,построенной П.Вудраффом^ на уровне исчисления высказываний^ заключительной фразе работы П.Вудраффа отмечается:

м Р.У. Соп^гис-Ьые Цлгсе^дбасА с.-

•Зоага.-Бут*. 1.03.,4970, р.183-18*.

"Проблема построения конструктивной "лукасевической" трехзначной логики остается открытой".

В §13 устанавливаются законы двойственности между и V , V и 3 в симметрической конструктивной логике.В §14 устанавливаются основные алгебраические соотношения,имеющие место для операций сильной конъюнкции.ослабленной дизъюнкции,односторонней конъюнкции и дизъюнкции.При помощи операции сильной конюнкции устанавливается,что две формы схемы аксиом введения конъюнкции А=> (В=> (А&В)) и (С=>А)= ((С => А) о ((С В) о (С В))),равносильные в классической и традиционной конструктивной логике, оказываются не равносильными в симметрической конструктивной логике. Односторонняя конъюнкгия и односторонняя дизъюнкция не имеют аналогов в классической логике и в традиционной конструктивной логике;эти операции применяются в дальнейших частях работы для логического представления граф-схемных алгорифмов и алгорифыических операторов.

В третьей части работы исследуются системы формальной ариф- . метики.В §16 определяются системы формальной арифметики,соответственно Н$А (симметрическая конструктивная арифметика),НТА (традиционная конструктивная арифметика), НЬА (трехзначная арифметика),НКА (классическая арифметика); они получаются соответственно из систем исчисления предикатов Н5 ,НГ,НЬ,НК посредством ограничения этих исчислений лишь арифметическими формулами и добавлением указанных выше арифметических аксиом.В §17 устанавливается равносильность систем НЬА и ША:всякая арифметическая формула,выводимая в одной из этих систем, выводима и в другой. Таким образом,оказывается несостоятельным кажущийся'естественным метод введения трехзначных логических оценок суждений в арифметику посредством присоединения аксиом арифметики к логическим аксиомам трехзначной логики Лукасевича;система,получаемая таким методом,оказывается равносильной классической арифметике.

В §18 вводятся формальные арифметические системы,основанные на понятиях конструктивной реализуемости.Для каждой арифметической формулы А определяются формулы е_£ А и е_К А ( содержательно истолковываемые следующим образом: "число е содержит алгориф-мическую информацию.подтверждающую симметрическую истинность (или ложность) формулы А").В нижеследующих индуктивных определениях этих формул С,Ь,Я суть примитивно-рекурсивные функции,за-

дающие нумерацию пар натуральных чисел и такие,что всегда

и(С(х,у))=Х , Я С(1(*),Ш)) = 2; иГ

суть примитивно-рекурсивные функции,задающие клиниеву нормальную форцу двуместной частично рекурсивной функции и «универсальной для одноместных частично-рекурсивных функций (а именно, 1Л(х,у)-- У ( Н 2' ; при этом всегда

1. Если А - элементарная формула,то е]< А есть (е=0)$ А; еКГАесть (в=1)#ТА. + с ог 0*/-7е

2. Если А имеет вид В&С,то е^ А есть

ие) — "'«С«)

3. Если А имеет вид ¿V С,то е & А есть

(асе)=0 & [€ V (С I- (с) = 1) & [евТс]^);

е В. А есть [е^вЦСе) & Се^сГЦ^ . '

4. Если А имеет вид В=>С,то е£*"А есть

V, ([еГвЗ€к 2 Зг(т(Ш,х,г) = 0 & к ^п^ & & У*(Сс£-с£ » 3*(т(исо,х(г) = о & [еВЭ!^,», где переменные х и г различны, отличны от е и не входят в А; е ¥Г А есть [са+В_3?(в) & СеЯ'СЗ %(е) ■

5. Если А имеет ввд ~Ш,то е£+А есть е,К"В; ей]"А есть еК^В.

6. Если А имеет вид УхВ.то е£^А есть

V* Зн (г(е,к,-е) = о& Се-В? В3£(г.) ).

где переменная г. отлична от е и не входит в А; е^'А есть

ВЗис'о.йСе) • + + -е у

7. Если А имеет вид ЭхВ.то ей А есть В3ие),(г(е) » е ВГА есть Ух Зг (г (е,х)г) = 0 & [еЕТв^.,),

где переменная 2 не входит в А и отлична от е.

Вводятся схемы аксиом симметрической реализуемости: схема Я , имеющая вид

и схема В. .имеющая вид

V (А~3е(е8»).

Определения е £+А и ей" А аналогичны определениям ^-реализуемости и ^-реализуемости в работе Д.Нельсона^*;схема аксиом Я"1" аналогична схеме аксиом,вводимой в работе Д.Нельсона^для системы традиционной конструктивной арифметики с сильным отрицанием.

В §19 исследуются системы формальной" арифметики,дополнение схемами R и В* ;такие системы обозначаются посредством НSЛ НТА£"\Н SAR* и т.п. Доказывается (теорема 19.I),что из непротиворечивости классической арифметики следует непротиворечивость системы HS AR"*" (идея доказательства аналогична идее установления непротиворечивости системы,рассмотренной в работе Д.Нель-сона^). Все остальные системы указанного вида оказываются противоречивыми. В частности, (теорема 19.4).противоречива система Н SAR* ;этот факт показывает,что отоядествление формулы А и её "конструктивной симметрической алгорифмической расшифровки" Зе(е£+А) не может быть продвинуто слишком далеко и,во всяком случае,не может быть рапространено на условия конструктивной ложности указанных формул.Таким образом,в симметрической конструктивной логике оказывается невозможным полное отождествление формулы и её алгорифмической конструктивной расшифровки (применяемое в ряде работ по конструктивной математике).

В §20 рассматриваются свойства формальной неопределенности формул.Арифметическая формула А называется формально неопределенной в HS AR4" ,если присоединение каздой из формул А и ~1А к системе HSARV в качестве аксиомы приводит к противоречивой системе. Доказывается (теорема 20.1),что существует замкнутая арифметическая формула,формально' неопределенная в Н S AR*" .Таким образом,система Н SAR* оказывается "устойчиво непополнимой":существует замкнутая формула,не выводимая и не опровержимая ни в каком непротиворечивом расширении системы HSAR+ .Явление устойчивой непополнимости,как легко видеть,не может иметь места в формальных арифметических системах,основанных на классической или традиционной конструктивной логике.Доказывается (теорема 20.2),что если "истинность", "ложность", "неопределенность" замкнутых арифметических формул понимать соответственно как доказуемость, опровержимость .неформальную неопределенность формул в системе HSAR+ ,то тогда истинность,ложность и неопределенность формул вида А&В, Av'B, А=В, 1А получается на основании аналогичных характеристик А и В по таблицам трехзначной логики Лука-севича.Поскольку указанные характеристики формул сохраняются при любом непротиворечивом расширении системы Н S А Я* ,мы можем сказать,что среди рассмотренных систем именно HS AR* (а не HLA, как естественно было бы ожидать) является арифметической систе-

мой,позволяющей ввести трехзначные логические оценки истинности суждений в метаязык арифметики.При изложении математического материала части 1У на основе системы HSAfL* вместо аппарата исчисления HS применяются соответствующие правила умозаключений, определенные в §4.

Отметим,что одна из формулировок указанной выше работы Д. Нельсона^ стр.213,строки 2-7 снизу: "если принять непротиворечивость любой из рассмотренных выше арифметических систем,то система S может быть непротиворечиво расширена посредством добавления аксиомы в еда Ан"]А") показывает, что Д.Нельсону были известны некоторые аналоги свойства формальной неопределенности формул (хотя детали рассмотрений и вид формулы А остаются невыясненными, и вся система в целом,насколько можно судить из крат кого изложения,не приспособлена для введения в язык исследователе; Д. Нельсон не указывает взаимосвязей своих понятий с трехзначной логикой).

В четвертой части работы исследуются приложения симметрической конструктивной логики к теории граф-схемных алгорифмов и ал-горифмических операторов.Эти приложения основаны на приятии ал-горифмического симметрического предиката.Симметрический предикат называется алгоритмическим,если области его истинности и ложности алгорифмически перечислимы;каждый такой предикат может быть задан посредством алгорифма .ведающего в случае применимости символ истинности или символ ложности.В §22 вводится язык граф-схем с памятью.Кавдая граф-схема с памятью обладает памятью, состоящей из конечного числа ячеек, и задается ориентированным графом,в вершинах которого располагаются элементы четырех видов: стартеры,остановы,преобразователи и распознаватели, причем количества дуг,исходящих из вершин указанных типов равны,соответст венно,1,0,1,2 (в последнем случае дуги помечаются символами "да" и "нет").Работа алгорифма,задаваемого граф-схемой,состоит в последовательном выполнении предписаний,помещенных в вершинах графа, с последующами переходами по дугам графа из одной вершины в другую.Со стартерами и остановами связываются предписания соответственно начала и завершения работы схемы. С преобразователями связываются предписания следующего вида:применить какой-либо алгорифм к системе объектов,помещенных в некоторых ячейках памяти и -результат его работы (в случае применимости алгорифма) помес-

тить в некоторую ячейку памяти.С распознавателями свярываются-предписания следующего вида .-перейти по дуге, помеченной символами "да" или "нет",в случаях,когда какой-либо алгорифмический предикат выдает соответственно значения "истина" или ложь" исходя из системы объектов,помещенных в некоторых ячейках памяти. В случае неприменимости какого-либо из указанных алгорифмов к соответствующей системе объектов дальнейший ход процесса работы схемы невозможен.Естественным образом определяется алгорифм, реализуемой граф-схемой с памятью (в частности,он может быть и алгорифмическим предикатом).

Понятие.граф-схемы с памятью является видоизменением понятия граф-схемы,введенного Л.А.Калужниным^.оно имеет ряд общих черт также с понятиями,введенными в работах А.П.Ершова ,А.А.Ляпунова26'27, Ю.И.Янова28.

Граф-схемное замыкание данного конструктивного множества алгорифмов определяется (§22) как множество алгорифмов,реализуемых при помощи граф-схем с памятью,построенных на основе алгорифмов из данного множества.Нормальное замыкание данного конт структивного множества алгорифмов определяется (§23) как множество алгорифмов,получаемых исходя из алгорифмов заданного мно жества й некоторых тривиально реализуемых алгорифмов (а именно, тождественного алгорифма, всегда истинного алгорифмического предиката и всегда ложного алгорифмического предиката) посредством операций композиции,разветвления,повторения алгорифмов,а также

Калужнин Л.А. Об алгорифмизации математических задач,- В кн.:Проблемы кибернетики:М.,1959,вып.2, с.51-6?.

^ Ершов А.П.Операторные алгорифмы.I.- В кн.:Проблемы кибернетики. М.,1950,вып.3,с.5-48;11.там же,1962,вып.8.с.211-233:111. там же,1968,вып.20,с.181-200.

Ляпунов A.A.О логических схемах программ.-В кн.:Проблемы ки-бернитики.М.,выпЛ,с.46-74.

27. Ляпунов A.A. К алгебраической трактовке программирования.В кн.-.Проблемы кибернетики.М. ,1962,вып.8,с.235-241.

Янов Ю.И. О логических схемах алгоритмов.-В кн.-.Проблемы кибернетики.М.,1958,вып.I,с.75—187.

операций добавления и отбрасывания переменных.Доказывается (теорема 23.1,теорема 24.1),что граф-схемное и нормальное зашкание любого конструктивного множества алгорифмов равны.Эта теорема, установленная в работе автора .показывает,в частности возможность устранения оператора до Ьо из алгоритмических схем программ в в практических алгорифмических языках (отметим,что возможность устранения оператора с|о ¿о из схем программ в терминах теории программирования показана в работе З.Эшкрофта и 3. ИанньР ). Доказывается, далее,(теорема 23.2,теорема 24.1) равенство граф-схемного замыкания любого конструктивного множества Ы алгорифмических предикатов и множества алгорифмических предикатов, получаемых из предикатов, принадлежащих Ы,посредством операций односторонней конъюнкции,односторонней дизъюнкции,симметрического отрицания,перестановки и отовдествления переменных.добавления и устранения фиктивных переменных.Тем самым устанавливается возможность приложения логического аппарата симметрической конструктивной логики для описания граф-схемных замыканий конструктивных множеств алгорифмов.

В §23 дается определение реализуемости трехзначной логической функции посредством рекурсивного или тюрингова оператора.А именно, говорим, что оператор указанного типа реализует заданную трехзначную функцию,если он преобразует тождественно равные нулю, тождественно равные единице и тождественно неопределенные частич но-рекурсивные . функции (кодирующие логические значения,соответственно, "истина", "ложь", "неопределенность") в соответствии с функциональной зависимостью,определяемой данной функцией.Дока-зывается (теорема 23.3 и 23.4) слабое равенство множества трехзначных логических функций,реализуемых посредством тюринговых (соответственно,рекурсивных) операторов и множества трехзначных логических функций.представимых посредством операции суперпозиции исходя из логических функций-констант и логических функций, соответствующих односторонней конъюнкции,односторонней дкзъюнк-

29Askcroit E.,Manna 2. Tk iransiaiion o$ io" proj«« to „whift" programs.— J*v: ¿onat processing

- Amsid r d a m:Ne>rih-Ho It. Pufci. Сотр. ¡>.

ции и отрицанию (соответственно,коышнкцки.дизъюнкции и отрицанию) .Тем самым устанавливается взаимосвязь меаду алгоритмическими и формульными представлениями трехзначных логических функций. Доказывается (теорема 24.2),что в обоих случаях равенство множеств не имеет места.Тем сашм устанавливаются примеры слабо равных,но не равных конструктивных множеств.Естественность такой характеризации соотношений меаду рассматриваемыми множествами можно подтвердить и некоторыми соображениями на интуитивном уровне.Например,представление трехзначной логической функции при помощи суперпозиции функций & , V , "1 ,И,Л,Н описывает её посредством дискретной схемы с алгорифмически проверяемыми свойствами её функционирования^ то же время,представимость функции посредством рекурсивного оператора является характеристикой её в терминах схем значительно более сложного типа,результаты функционирования которых,вообще говоря, конструктивно не прогнозируются. Поэтому условия конструктивной ложности суждений о наличии таких представлений для данной логической функции не равносильны (а именно,в первом случае проверка их значительно легче, чем во втором).Таким образом,аппарат симметрической конструктивной логики дает возможность непосредственно описывать такие логические особенности конструктивных множеств и их взаимоотношений, которые непосредственно нг поддаются описанию при помощи иных имеющихся логических апт._ атов.

Материал настоящей работы изложен в следующих публикациях автора:

1. Граф-схемы с памятью.-Труды Ыат.Инст. им.В.А.Стеклова, 1954,т.67,с.99-192.

2. Симметрическая конструктивная логика.- В кн.:Международный конгресс математиков,Москва,16-26 августа 1966г.Тезисы кратких научных сообщений,секция I,- М.,1956,с.16.

3. О предикатных и арифметических исчислениях симметрической конструктивной логики.-Докл.АН СССР,1973,т.210,№3,с.517-520.

4. Об операторных реализациях трехзначных логических функций. В кн.:Третья Всесоюзная конференция по математической логике. Тезисы докладов.Новосибирск,1974,с.78.

5. О конструктивной истинности суждений и некоторых нетрадиционных системах конструктивной логики.- В кн.:Труды Вычислительного центра АН Арм.ССР и £ГУ /Математические вопросы ккбер-

нетики и вычислительной техники/ Конструктивная математика. Ереван,АН Арм.ССР,1975,вып.8,с.99-153.

6. Симметрическая конструктивная логика.- Ереван: АН Арм.ССР, 1978,- 281 с.

7. Реализация трехзначных логических функций посредством рекурсивных и тюринговых операторов,- В кн. Исследования по теории алгорифмов и математической логике.М.,ВЦ АН СССР, 1979,с.52-61.

8. О симметрической конструктивной истинности арифметических формул.- В кн.: Седьмая Всесоюзная конференция по математической логике,посвященная 75-летию академика А.И.Мальцева.Тезисы докладов .Новосибирск,1984,с.67.

9. О равенстве конструктивных множеств.- В кн.: Восьмая Всесоюзная конференция по математической логике,посвященная 85-летию академика П.С.Новикова.Тезисы докладов.Москва,1986,с.67.