В библиотеке

Книги2 383
Статьи2 537
Новые поступления0
Весь каталог4 920

Рекомендуем прочитать

Хоффер Э.Истинноверующий
Имя американского мыслителя Эрика Хоффера (1902-1983) все еще остается недостаточно известным нашему читателю. Его первая и, по-видимому, самая значительная из опубликованных им девяти книг - Истинноверующий, - представляет собой размышления о природе массовых движений.

Полезный совет

Если Вам трудно читать текст, вы можете увеличить размер шрифта: Вид - размер шрифта...

Алфавитный каталог
по названию произведения
по фамилии автора
 

АвторНепейвода Н.Н.
НазваниеПрикладная логика
Год издания1996
РазделКниги
Рейтинг0.60 из 10.00
Zip архивскачать (1 503 Кб)
  Поиск по произведению

Глава 16. Интуиционистская логика

Интуиционистская логика — наиболее близкий во многих отношениях к классической член семейства неклассических логик. Более того, она — практически единственная неклассическая логика, являющаяся не просто одним из членов целого семейства, а обладающая уникальными, выделенными свойствами. Если классическая логика имеет почти стандартную и простейшую из возможных семантику в виде таблиц истинности 1 , то интуиционистская логика замечательна тем, что для неё сосуществуют четыре известных разнородных класса семантик для неклассических логик. Поэтому интуиционистская логика может послужить в качестве полигона для семантик неклассических логик, применяемых далее к самым разнообразным системам.

§ 16.1. Создание интуиционистской логики

16.1.1. Брауэр: идея конструктивности

К началу XX века математика столкнулась с кризисом оснований, проявлявшимся как в грубых парадоксах типа противоречий (например, парадокс Рассела в ч. 1, § 1.7), так и в том, что понятия, изначально считавшиеся тождественными, стали заметно расходиться.

Вернемся к парадоксу института математики из § 244 и напомним его логическую суть.

Предложение 16.1.1. Если классическая теория Th неполна и имеются обозначения для всех элементов универса (эти термы будем называть конкретными), и мощность универса не меньше 2, то имеется такая формула А ( х ), что доказано Зх А ( х ), но ни при каком конкретном и не может быть доказано А ( и ).

  • 1 Но вспомните семантику булевых алгебр из первой части.

Доказательство. Пусть G — неразрешимая в Th замкнутая формула. Пусть 0 и 1 — два различных элемента универса, которые имеются по определению. В качестве А ( х ) возьмем

( G & х = 1) V (G & х = 0).

Зх А ( х ) доказывается разбором случаев G и G . Но если бы при каком-
то и было доказано А ( и ), то заодно была бы разрешена и проблема G ,
которая неразрешима по предположению. ?

Мы видим, что парадокс института математики зависит лишь от теоремы Гёделя о неполноте и от логического принципа А\/ А .

В начале XX века теорема Гёделя о неполноте могла лишь присниться в страшном сне, но математики уже заметили, что понятия ‘ существовать ' и ‘ быть построенным ' стали заметно различаться. Появилось понятие чистых теорем существования, в которых нет построения объекта, чье существование доказывается 2 . Козел отпущения, на которого можно было свалить ответственность за чистые теоремы существования, нашелся сравнительно быстро: аксиома выбора3 (§ 32).

Но молодой голландский ученый Л. Э. Я. Брауэр уже в 1908 г. опубликовал на голландском языке статью под вызывающим названием: “ О недостоверности логических принципов”.

Личность самого Брауэра весьма интересна и необычна. Его первая книга имела заголовок “Жизнь, искусство и мистика” и была посвящена философии, на него оказали большое влияние идеи Ницше, Бергсона и Хайдеггера, а также восточная (прежде всего индийская) философия. Впрочем, на Хайдеггера и он сам оказал большое обратное влияние. Упомянутая выше его диссертация также была прежде всего философским трудом.

Идеей диссертации Брауэра было то, что законы классической логики не носят ни априорного, ни абсолютного характера. Они выведены прямым обобщением законов работы с небольшими конечными совокупностями устойчивых во времени объектов. Затем они были незаконно перенесены на оперирование с бесконечно большими совокупностями и стали, соответственно, неадекватны. Эта неадекватность не осознавалась длительное время и в конце концов завела математику в громадный тупик, из которого не выберешься пересмотром отдельных аксиом. Нужно либо полностью отказаться от бесконечных совокупностей объектов, либо перейти к другой логике, либо перестать придавать какой-то содержательный смысл математическим утверждениям, признав их чисто абстрактными, идеальными. Далее, математика полностью игнорирует незавершенность человеческого знания и незавершенность, как говорил Брауэр — становящийся характер многих математических объектов. В частности, действительное число рассматривается как уже существующая бесконечная десятичная дробь, а не как процесс получения все более и более точных приближений.

Любопытно, что в человеческой истории зачастую самые грязные явления называются чистыми!

И на первый взгляд поделом! Она действительно ответственна в классической математике за самые грубые формы чистых теорем существования.

Даже если мы точно определили абстрактный объект, например, число ? , мы все равно не знаем его полностью. Например, вычислив 1010 знаков данного числа, мы можем так и не узнать, есть ли в его десятичном разложении последовательность 30 семерок.

Чтобы преодолеть рассмотренные выше трудности, предлагалось разрушить до основания все здание математики и заново построить его на новых принципах. Но откуда было взять новые принципы, если даже логика была поставлена под сомнение? Брауэр предложил пользоваться новой логикой, которая, как он утверждал, гораздо интуитивно понятнее, чем классическая, и описывает математические утверждения не как абстрактные истину и ложь, а как предложения о возможности выполнить некоторое умственное построение , решить некоторую конструктивную задачу 4 . Математическое доказательство должно дать требуемое построение вместе с его обоснованием. Методы, дающие построения, Брауэр (и не только он) называл эффективными методами.

Брауэр прекрасно понимал, что математическое построение — сущность весьма высокого уровня и для его обоснования недостаточно ссылки на практику, тем более что в те времена точного понятия алгоритма, котороематематически мыслящему человеку соблазнительно взять в качестве формализации расплывчатого понятия вычисления, еще не существовало. Поэтому оставалось ссылаться в качестве первоисточника математики на Идеи, но уже не считая математику прямым воплощением Идей. Поскольку понятий для выражения новых ипостасей Идей, которые осознал Брауэр, в европейской науке еще не было выработано, Брауэр ссылался на интуицию как инструмент их понимания. Поэтому он назвал предлагаемую обновленную логику и математику интуиционистской . Иногда он употреблял и другое название, связанное с центральной ролью конструкций в предлагаемой модификации математики и логики, — конструктивная логика и математика. Исторически в дальнейшем эти два термина разошлись. Названия ‘ интуиционизм ' и ‘ интуиционистская логика ' остались за системами, идущими напрямую от оригинальных брауэровских рассмотрений. ‘ Конструктивизм ' и ‘ конструктивная логика ' стали более общими терминами, характеризующими весь класс математик и логик, ставящих на первое место понятие задачи и конструкции, а не истины и обоснования 5 .

  • 4 Здесь не зря мы добавили прилагательное к задаче. Как говорилось в § 15.3.1, математическая задача отнюдь не обязательно включает построение, вспомните, что значит ее решить?

16.1.2. Интуиционизм и программа Гильберта

Надо сказать, что при всей радикальности исходных принципиальных позиций Брауэр подошел к задаче реформирования логики и математики исключительно осторожно, пытаясь сохранить все, что не противоречит исходным принципам конструктивности.6 Чтобы проделать это максимально квалифицированно, он даже пошел на период стратегического отступления и, продекларировав необходимость замены математики, занялся вначале традиционной (как ее сегодня называют, классической ) математикой. Он получил первоклассные результаты и завоевал настолько большой авторитет, что его ввели в редакцию ведущего в то время в мире математического журнала “ Mathematische Annalen ” (председателем редакционного совета которого был сам Давид Гильберт7). Одна из его теорем вошла в золотой фонд математики:

В советской, а зачастую и в мировой, научной литературе термином ‘ конструктивная математика ' или ‘конструктивное направление в математике' порою называют конкретную ее разновидность, развивавшуюся в 50-е – 70-е гг. в СССР под руководством А. А. Маркова.

Это стало особенно ясно после появления гораздо более радикальных программ, в частности, узкого конструктивизма Н. А. Шанина.

Давид Гильберт считается одним из самых выдающихся математиков, когда-либо живших на Земле. Он получил принципиальные результаты в самых разных разделах математики, в том числе и в логике. Но еще важнее, чем его результаты, была формулировка им 20-ти проблем математики на I международном конгрессе математиков.

Теорема 16.1. (Теорема Брауэра о неподвижной точке) Любое непрерывное отображение n -мерного шара в себя имеет неподвижную точку.

После этого Брауэр начал публиковать серию работ, посвященных пересозданию математики на новой основе, следя за тем, чтобы каждое доказательство давало построение. У него появились и ученики, прежде всего в самой Голландии. Большинство математиков высокомерно игнорировали новое направление, тем более что Брауэр подчеркивал неформализуемость интуиционистской математики и не желал явно выписывать ее аксиомы.

Работы и декларации Брауэра вызвали раздражение у Гильберта, который считал, что Брауэр выплескивает вместе с водой и ребенка8. Но Гильберт не мог игнорировать критики Брауэра и поэтому предложил свою программу спасения классической математики, в которой был ряд важнейших мировоззренческих моментов.

Программа Гильберта

8 Интересно, что основное эмоциональное возражение Гильберта против интуицио
низма высвечивает сразу два методологических корня классической математики.

Отнятьуматематиков законисключенноготретьего всеравно, что запретить астроному пользоваться телескопом или (16.1) боксеру — кулаками.

В самом деле, Брауэр пожелал вывести математику за пределы общей естественнонаучной и прогрессистской концепции европейского рационализма и заодно пересмотреть в ней правила игры, превратив ее из европейского бокса в нечто более похожее на восточные единоборства.

  • 9 В данном пункте Гильберт полностью признал обоснованность критики Брауэра.

Необходимо четко осознать, что подавляющее большинство математических объектов и теорем никаких прообразов в реальном мире не имеют. Реальными являются лишь утверждения типа 2 ? 2 = 4, а число ? и теорема Ферма — уже идеальные объект и высказывание. В принципе идеальные объекты и результаты нужны лишь как промежуточные стадии для получения реальных результатов и в данном смысле не являются необходимыми9.

Тем не менее математика не может существовать без идеальных объектов, поскольку иначе мы не могли бы практически получить многих реальных результатов. Таким образом, идеальные объекты необходимы для эффективности нашего мышления10.

Необходимо обосновать, что в принципе идеальные объектыи утверждения можно устранитьизвыводовреальных утверждений;сложность получившихся преобразований при этом роли не играет, поскольку реально их устранять никто не собирается, но доказательство возможности устранения должно быть проведено как можно более абсолютными средствами, с которыми согласны и классики, и интуиционисты, и по возможности все могущие появиться в будущем диссиденты других толков. Такие средства Гильберт назвал финитными 11.

Для строгого финитного доказательства теорем о преобразовании выводов необходимо полностью уточнить понятие математического языка и логического вывода 12.

После формализации необходимо финитно доказать непротиворечивость и полноту получившейся формальной системы, поскольку это гарантирует пункт 3 13 .

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

Ничего не возразишь! Даже Брауэр заявил, что после такого обоснования он бы снял все возражения против классической математики, лишь бы сами математики классического направления перестали говорить о реальном смысле, кроющемся за идеальными объектами и утверждениями.

  • 12 Таким образом, впервые была поставлена со всей остротой задача формализации классической математики.
  • 13 И после десятилетия попыток в данном направлении, когда Гильберт неоднократно объявлял, что искомые доказательства почти получены,остались лишьнесколько незначительных частных случаев — теорема Гёделяонеполноте! Она произвела впечатление атомной бомбы, полностью уничтожившей программу Гильберта, и все, сконцентрировавшисьнапредложенных Гильбертом средствах,забыли его основную цель—пункт 3. А средства ведь не только что не необходимы, но иногда даже не достаточны для главной цели! Сам Гильберт пытался заметить,даи Гёдель говорил, что опровергнуты лишь конкретные средства достижения цели, но их никто уже не слушал.

Хотя взаимодействие между Брауэром и Гильбертом привело к формулировке Гильбертом весьма разумной программы (более разумной, чем большевистские замашки Брауэра), взаимоотношения между ними сложились достаточно сложные. В редакционном совете журнала Гильберту все время приходилось выслушивать декларации Брауэра о том, что данная работа смысла не имеет, неожиданно для Гильберта завершавшиеся объективной оценкой возможности ее опубликования. Не имея прав вывести Брауэра из редсовета, Гильберт организовал коллективную отставку его членов и не ввел Брауэра в новый состав. Так что тот, кто был более нетерпим в теории, оказался более терпим на практике, и наоборот.

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

Неправильная теория, не натолкнувшаяся на противоречие, не становится от этого более правильной, точно так же, как преступное поведение, не осужденное законом, не становится от этого менее преступным.

16.1.3. Формализация и первые интерпретации

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

Как только появилась формализация интуиционистской логики, почти сразу же была дана и ее первая строгая интерпретация. Она основывалась на идее алгебр Линденбаума-Тарского и, в свою очередь, была подтверждением их силы как математического аппарата. Было сформулировано понятие псевдобулевой алгебры и дана интерпретация интуиционистской логики как логики со значениями в псевдобулевых алгебрах.

Тем не менее само понятие псевдобулевой алгебры могло первоначально рассматриваться как выдуманное ad hoc , специально для того, чтобы проинтерпретировать интуиционистскую логику. Следующим принципиальнымшагомвданномнаправлениистала интерпретацияин- туиционистской логики польскими математиками, где значениями формул являлись открытые подмножества произвольного топологического пространства. Итак, интуиционистская логика оказалась связанной с важнейшими математическими понятиями.

Далее, новые понятия в математической логике стали все чаще создаваться и для классической, и для интуиционистской логики. Г. Ген- цен создал свое исчисление естественного вывода и исчисление секвенций сразу для двух данных логик. Для них же он доказал теорему нормализации. Э. Бет также создал семантические таблицы и для той, и для другой логики, и для интуиционистской — чуть раньше.

16.1.4. Разногласия и новые идеи

Полное единство мнений бывает только на кладбище.
И. Джугашвили (Сталин), 1917 г.

А в самом интуиционизме начались расхождения. Многие были недовольны формализацией отрицания по Гейтингу и начали ее варьировать (минимальная логика, сильное отрицание, безотрицательная математика). Другие начали проявлять недовольство слишком сильными, по их мнению, абстракциями, введенными Брауэром, особенно это течение усилилось после появления точного понятия алгоритма. Третьи... но в учебнике можно и остановиться.

Реакция Брауэра была совершенно неординарной для отца-основателя школы. Вместо обвинений в адрес ревизионистов и уклонистов он спокойно сказал:

Поскольку интуиционисты говорят на неформализованном языке, среди них должны были появиться разногласия. (16.2)

Там, гдеесть единомыслие, нет мысли! Еслибыпобольше выдающихся умов это понимали, и понимали бы еще, насколько апостолы, как правило, профанируют и компрометируют идею!

Принципиальный плюрализм и уважение к чужой точке зрения у Брауэра тем более примечательны, что в жизни он отдал дань традиционной слабости творческих людей, часто позволявших себя соблазнить лозунгами экстремистских групп. Брауэр поддерживал Гитлера до тех пор, пока не столкнулся с гитлеризмом на практике, пока Германия не оккупировала самым подлым и вероломным образом нейтральную Голландию. Брауэр после этого занял патриотическую позицию.

После войны Брауэр опубликовал серию работ, в которых как будто задался целью показать, что он не хуже других умеет создавать альтернативы. Он ввел в математику последовательности, зависящие от развития самого математического знания (и тем самым в дальнейшем, через своего ученика Бета, дал начало новой теории моделей, ныне популярных под именем моделей Крипке). Он показал принципиально новые возможности интуиционистской математики, в частности, возможность формализации и позитивного использования незнания . Он дал новый подход к известному со времен Зенона Элейского 14 концептуальному противоречию в математической модели пространства: существуют точки и вместе с тем пространство бесконечно делимо, — он показал, что точки вводить необязательно.

  • 14 Зенон Элейский — греческий мудрец, живший, по традиционной хронологии, в VI веке до н. э. и прославившийся своими апориями : парадоксами пространства и времени. В частности, бесконечную делимость пространства ставит под сомнение апория Ахиллес и черепаха .

Докажем, что быстроногий Ахиллес никогда не догонит черепаху. В самом деле, пока Ахиллес добежит до того места, где была черепаха, та проползет еще немного, пока он доберется до нового ее положения, она продвинется еще дальше, и так до бесконечности. (16.3)

Существование точек ставит под сомнение апория Стрела :

Если стрела находится в любой данный момент в одной и той же точке, то она не движется, а если она не находится в некоторый момент ни в одной точке, то где же она? (16.4)

16.1.5. Период после Брауэра

Начинаяс 1954г. Брауэр большене публиковал научных работ. Но целое направление ужебыло созданоипродолжалоинтенсивно развиваться.В это время расцвел, в частности, советский конструктивизм, основателем которого был А. А. Марков 15 .

Советский конструктивизм, в отличие от интуиционизма, с самого начала взял курс на точное понятие алгоритма, которое уже сформировалось к началу 50-х годов. Первым применил точное понятие алгоритма для построения семантики интуционистских теорий американский ученый С. К. Клини в 1940–1945 гг.16 Он дал понятие реализуемости , которое мо ет рассматриваться как подстановка конкретного понятия алгоритма в общую схему Колмогорова. Но, тем не менее, именно понятие реализуемости стало первой точной реализацией неформальной схемы, предложенной Колмогоровым. Затем (уже в 50-х гг.) Клини показал, что такую подстановку можно осуществлять разными, расходящимися между собой, способами.

15 Андрей Андреевич Марков —выдающийся русский математик.Онсын знаменитого математика А. А. Маркова, и, отталкиваясь от отца, не пожелал заканчивать математический факультет, и некоторое время работал инженером. Но затем он вернулся в математику. Работы, принесшие ему славу, были сделаны во многих областях, но в первую очередь в топологии и в алгебре, где предельно неконструктивные доказательства были скорее правилом, чем исключением. В дальнейшем он, возможно, под влиянием прикладных работ в области кодирования и декодирования (вспомним, что и Тьюринг этим занимался), перешел к конструктивной точке зрения и в некоторых отношениях стал более радикален, чем Брауэр. Это было связано и с более физическим и материалистическим мировоззрением А. А. Маркова, искавшего твердых оснований. Подходящим и надежным основанием стало точное понятие алгоритма, и А. А. Марков перестроил конструктивный взгляд таким образом, что везде были лишь алгоритмы и данные для них. В дальнейшем А. А. Марков стал пытаться обосновать саму интуиционистскую логику через теорию алгоритмов. Он столь же бескомпромиссно, как и Брауэр, отстаивал свои убеждения и столь же был терпим на практике к людям с другой точкой зрения. Порою он заявлял следующим образом:

Я этого не понимаю, но этим надо заниматься! (16.5)

Необходимо помнить, что в его устах “не понимаю” означало невозможность проинтерпретировать нечто со строго конструктивной точки зрения.

  • 16 С. К. Клини — выдающийся американский логик. Его фамилия читается так необычно, поскольку она сохранила остатки фризского чтения (фризы — маленький народ на островах Северного моря). Курсовой работой Клини было построение алгоритма для вычисления разности натуральных чисел (в те времена теория алгоритмов лишь начинала развиваться). Затем он дал множество красивых интерпретаций неклассических теорий, написал фундаментальную книгу по математической логике [35]. Он — один из основателей теории нейронных сетей.

Н. А. Шанин17 построил алгоритм конструктивной расшифровки, аналогичный сколемизации в классической логике. Этот алгоритм выносил конструктивную задачу наружу, а проблему обоснования решения ставил таким образом, чтобы для ее доказательства можно было пользоваться классической логикой. Это еще сильнее прояснило связь классической и конструктивной логики.

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

Пожалуй, конец этого этапа знаменуется несколькими событиями. Во-первых, наконец-то с помощью предложенной Д. Правитцем нормализации выводов и реализуемости по Клини было строго доказано, что во многих сильных теориях, базирующихся на интуиционистской логике, доказательство и на самом деле дает построение. Далее, были выделены важные классы формул, где классическая и конструктивная доказуемость совпадают (в частности, хорновские формулы, давшие начало языку Пролог).Былипредложенынесколькосемантикисамой интуиционистской логики, и базирующихся на ней теорий, с помощью которых стало возможным точно исследовать вопросы о совместимости различных интуиционистских принципов и классы построений,к которым они ведут. И, наконец, Э. Бишоп (США) предложил концепцию конструктивной математики, ориентированную на соединение достоинств интуиционистского и конструктивного в советском смысле подходов. Идея была следующей: пользоваться лишь алгоритмами, но явно этого не говорить, и применять преимущества формализации намеренного незнания, показанные Брауэром. В дальнейшем мы это рассмотрим подробнее.

  • 17 Н. А. Шанин — ученик А. А. Маркова. Он начинал с работы в самых абстрактных теоретико-множественных областях математики, в частности, в топологии. Именно по топологии он защитил докторскую диссертацию. Затем он всей душой воспринял конструктивную математику и начал, по примеру Брауэра, заявлять всем, что их работы никакого смысла не имеют. Ему возразили, что никакого смысла тогда не имеет и его диссертация, и он обратился в Высшую аттестационную комиссию с письмом, в котором просил лишить его степени доктора наук, поскольку его диссертация выполнена в области, не имеющей никакого смысла. Ему ответили, что поположению такая причина лишения степени не предусмотрена.

Н. А. Шанин — гораздо более крайний конструктивист, чем А. А. Марков, но и у него убежденность и научный экстремизм никогда не вырождались в личную нетерпимость по отношению к людям, придерживающимся других точек зрения (но тем, кто считались конструктивистами, порой приходилось несладко за уклонения).

16.1.6. Вторая героическая эпоха: математические результаты и попытки приложений

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

Провозвестниками приложений конструктивной логики к программированию явились работы Х. Б. Карри и Р. Л. Констейбла. Карри заметил, что доказательства в импликативном фрагменте гильбертовской формулировки логики высказываний в точности соответствуют типизируемым термам в комбинаторной логике. Констейбл заметил, что, поскольку конструктивное доказательство обязательно включает построение, оно может использоваться для автоматизированного синтеза программ. Оба этих наблюдения в дальнейшем были развиты многими способами и скрещены между собой.

§ 16.2. Интерпретация Колмогорова

Поскольку логические формулы понимаются в интуиционистской логике (и в других конструктивных логиках) как задачи, естественно построить интерпретацию, которая оперировала бы не с их истинностными значениями, а с решениями этих задач. Такую интерпретацию построил А. Н. Колмогоров в 1925 г. (более развитый вариант — 1932 г.). Надо заметить, что при этом Колмогоров следовал брауэровскому описанию смысла логических связок при конструктивном понимании, а его интерпретацию сразу же развил и уточнил ученик Брауэра А. Гейтинг. Поэтому на Западе данная интерпретация часто называется ВКН-интерпрета- цией. Мы предпочитаем традиционный русский термин.

Как Вы помните, в теории вычислимости было установлено, что не всюду определенность (частичность) является необходимым свойством алгоритмически определяемых функций. Поэтому мы будем работать с не всюду определенными функциями и в наших интерпретациях18. Поэтому введем терминологическое различие. Оператор всюду определен для данных соответствующего типа, а функционал либо отображение — не обязательно. Если / — отображение, то !/( ?) означает, что значение / ( ? ) существует (т. е. что / ( ? ) определено).

Определение 16.2.1. (Колмогоровская интерпретация) Пусть ©А — множество решений А , и а © А означает, что a — решение А , т. е. что a € (г) А Пусть U — наш универс рассмотрения. Оператор, преобразующий А в © А , называется слабо колмогоровской интерпретацией, если выполнены следующие условия (пункты, помеченные * , нужны лишь для логики предикатов):

1. Есть оператор join и отображения рг ь рг 2 , такие, что:

Va , Ь ( а © А & 6 © В D join ( a , Ь ) (?) ( А & В )), yc ( c © ASzBZ ) Ipi ^ ( с ) & pi ^ ( с ) (?) А & ! рг 2 ( с ) & рг 2 ( с ) (?) В ).

* Для квантора 3 :

w ( с (?) Зж А ( ж ) D \

VC . ч ГГ01 С N С I \ Г~\ М I \\ ¦

!рг 1 (с) & рг 1 (с) € (7 &' Pr 2 l C J MPr 2 l C J ( I ) ^-( Prl ( C JJ

2. Есть операторы m ± , in 2 и отображение case , такие, что

Va (a(r)iD ini (a) (?) A V B), V6 (b (?) -B z> Шг ( Ь ) (?) A V B), Vc (c (?) (A V B) Z> (!case(l, c) & case(l, c) (?) A ) V (! case (2, c ) & case (2, c ) (?) B )).

  • 18 Во времена Колмогорова это еще не было ясно, и поэтому он не делал оговорки о частичности функций.

3. Есть отображение ev , такое, что

V a (a © А & /(f) ( А => . В ) z> !ev(/, a) & ev(/, a) (f) - В ).

* Для квантора V :

/ (f) Vr А ( ж ) z> V a (aG U d !ev(/, a) & ev(/, a) (f) ^4(a))

4. Если нет таких a , что a © А, то 0 ® A .

Если главные импликации D повсюду заменить на =, то интерпретация называется строго колмогоровской или просто колмогоровской.

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

Это определение отличается от оригинального в нескольких отношениях. Во-первых, у Колмогорова не было явно указанных отображений и операторов, а прямо говорилось, что множество ( f ) А & В — прямое произведение ©Ах ©В, множество © А V В — прямая сумма © А ф © В. Пункт, соответствующий © А => В, был определен только частично. Было сказано, что элементами © А => В являются эффективные преобразования © А в © В, но само понятие эффективного преобразования оставалось неопределенным.

Таким образом, в сущности интерпретация Колмогорова была мета- интерпретацией, общим методом построения целого множества интерпретаций. Наше определение еще сильнее подчеркивает этот аспект и ее взаимосвязи с категорными конструкциями. Посмотрите на операторы и отображения, определявшиеся в пунктах 1 и 2. Они наводят на воспоминание об определяющих диаграммах для прямого произведения и прямой суммы (ч. I , диаграммы 5.9, 5.10).

Посмотрим, что гарантирует наше слабое определение.

Предложение 16.2.1. Выполнены следующие соотношения:

  1. Если ! © А и ! © В, то ! © А & В.
  2. Если ! © А & В, то ! © А и ! © В.
  3. Если ! © А и ! © А =5- В, то ! © В.
  4. Если ! © А или ! © В, то ! © А V В.
  5. Не могут быть одновременно ! (?) А и ! (?) А
  6. Если ! (?) \/ж - А ( ж ) , то ! (?) А ( и ) для любого и ? U .
  7. Если ! (?) Зж - А ( ж ) , то ! (?) А ( и ) для некоторого и ? U .
  8. Если ! (?) Л ( и ) для некоторого и ? U , то ! (?) Зж - А ( ж ) .

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

Интерпретация Колмогорова служит и сильным косвенным, полуформальным, методом анализа конструктивных утверждений. Прежде всего рассмотрим сильный закон исключенного третьего и закон двойного отрицания, критиковавшиеся Брауэром в его диссертации.

Пример 16.2.1. Реализуемость АУ А означает возможность либо построения реализации А , либо установления, что такой реализации не существует. А именно, для каждого А имеется элемент, из которого с помощью операции case можно получить либо реализацию А , либо реализацию А . Если этот закон принят как общий, то такая проверка должна делаться допустимыми у нас средствами. Значит, если мы интересуемся вычислимостью, то закон исключенного третьего может приниматься лишь в случае, если наш язык настолько ограничен, что все выразимые в нем свойства разрешимы.

Пример 16.2.2. Доказано, что элементарная теория действительных чисел и элементарная геометрия полны. В качестве примера приведем формулировку аксиом элементарной теории действительных чисел.

Сигнатура состоит из отношений > и =, операций сложения, умножения и вычитания и трехместного предиката, выражающего деление Div ( x , у , z ), истинного, когда х / у = z .

Аксиомы делятся на три группы. Первая — стандартные аксиомы поля, которые, в частности, позволяют определить константы 0 как х—х и 1 как х / х для произвольного х ф 0 .

Вторая — аксиомы линейно упорядоченного поля.

Ух , у , z ( x > y $ zy > z => x > z ) Ух , у , z ( y < z => х + у < х + z )
Ух , у , z ( y < z & x >0=^ x - y < x - z ) Ух < ( х > х )

0 < 1 Ух , у ( х = у х < у V х > у )

(16.6)

Третья группа состоит из единственной схемы аксиом, утверждающей существование корня для любого многочлена нечетной степени .

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

Что означает реализуемость A ? A без ограничений на язык? Значит, мы можем решить любую задачу! Значит, теорема Гёделя о неполноте просто не может быть выполнена! Итак, закон исключенного третьего сконструктивной точки зрения вполне заслуживает названия принцип всезнания и выглядит совершенно нереалистичным 19 .

  • 19 Анекдотично, но показательно для стиля мышления большинства математиков следующее. Теоремы Гёделя во времена Брауэра сначала не было, а затем он принципиально не желал пользоваться данным результатом для обоснования своих конструкций, поскольку не считал, что теорема имеет отношение к сущности классической математики (в этом отношении он был прав, поскольку теорема Гёделя имеет отношение к сущности любой достаточно богатой формализации любой математики ). Поэтому он аргументировал неприемлемость, скажем, сильного закона исключенного третьего следующим образом.

Мы не знаем, есть ли в десятичном разложении числа ? последовательность цифр 0123456789. Поэтому, если через A обозначить утверждение

В десятичном разложении ? есть последовательность цифр (16.7) 0123456789 , то мы не можем утверждать ни A , ни A , и поэтому A ? A нельзя считать истинным.

Брауэр не мог вообразить себе ни мощности и общедоступности современных компьютеров, ни тупости многих их использований. Некто совершенно точно вычислил, что эта последовательность встречается в числе ? и объявил о решении проблемы, давно поставленной интуиционистами!

А чем же провинился принцип двойного отрицания? Тут вопрос несколько тоньше. Рассмотрим формулу А Когда она реализуема и каковы ее реализации?

Реализацией ее является стандартный элемент 0, а реализуема она, когда нет реализаций у А Расшифровываем последнее условие и получаем интересное соотношение:

А реализуема тогда и только тогда, когда реализуема А но реализацией ее является заранее (16.8) известный элемент 0 .

Что теперь означало бы принятие закона А => А! Тогда был бы общий метод преобразовывать любую решаемую проблему в ее решение, т. е. общий решатель задач 20 . Итак, закон снятия двойного отрицания с конструктивной точки зрения означает существование общего решателя задач, и естественно, что, приняв сильный закон исключенного третьего, мы должны принять и закон двойного отрицания, и наоборот.

Пример 16.2.3. Рассмотрим вопрос, может ли интуиционистская теория противоречить классической? Пусть А{х) — неразрешимое свойство, а наши эффективные методы — алгоритмические. Тогда нет такого функционала ip , который реализует Ух ( А ( х ) V А ( х )), и, значит, по определению реализумости, мы должны считать обоснованным Ух ( А ( х ) V А ( х ))

Пример 16.2.4. Рассмотрим совершенно неформальный пример, темне менее достаточно убедительно показывающий, что нельзя механически получать Эх А ( х ) из Ух А ( х ).

Пусть реализовать { х ) означает соблазнить девушку х. Тогда реализовать Ух А{х) — это найти общий метод соблазнения любой девушки. Вполне реалистична ситуация, когда такого метода нет, и, тем не менее, любую девушку в принципе можно соблазнить, подойдя к этому творчески.

Неформальные ответы на многие вопросы требуют исследования более тонкой структуры колмогоровской интерпретации.

  • 20 Общий решатель задач — такой же нонсенс, как вечный двигатель, но тем не менее традиционно являлся одной из целей классического искусственного интеллекта. Некоторые программы даже так назывались.

Пример 16.2.5. Рассмотрим следующий вопрос:

Каков конструктивный смысл формулы А => А и в каких случаях она может быть конструктивно (16.9) неверна?

Ее реализацией является тождественная функция, и, соответственно, формальный закон тождества неформально означает возможность бездействия, наличие преобразований, которые ничего не изменяют. Таким образом, чтобы не было А => А, необходимо не иметь и тождественных функционалов. В частности, для этого достаточно учесть, что есть время, которое необратимо расходуется даже при бездействии.

Пример 16.2.6. Чуть-чуть видоизменим предыдущую импликацию. А => А & А уже требует удвоения реализации А. А если на реализацию тратятся ресурсы, то вполне их может не хватить на два экземпляра такой реализации. Конечно, примером такого ресурса опять-таки может служить время, но здесь достаточно и денег, которые могут не расходоваться при бездействии, но расходоваться при действиях.

Упражнения к § 16.2

Пусть реализации конъюнкции, дизъюнкции и существования — прямые суммы и прямые произведения.

Что получится, если в качестве реализаций А => В будут рассматриваться все классические теоретико-множественные функции / : (г) А —> (г) В! А если еще обобщим и будем рассматривать все отношения?

А если теперь будем рассматривать лишь постоянные функции?

Рассмотрим формулу

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

Студент Классиков следующим образом обосновал ее конструктивную приемлемость.

Пусть некоторый функционал ip решает задачу А => В V С. Тогда ip по решению А вычисляет, какой из членов дизъюнкции решается, и дает его решение. Но реализация отрицания известна заранее — 0. Так подставим Ов^и получим, какой из членов дизънкции в заклчении реается, а у его реение нетрудно получить опять-таки из tp !

Можете ли Вы что-либо возразить, и если да, то что? Если возражаете, то что разумного в рассуждениях Классикова?

16.2.4. Почему мы не включили в число аксиом действительных чисел
плотность порядка

Ух,у(х < у => 3 z ( x < z & z < у ))? (16.10)

Напишите одну аксиому, выражающую наличие корня у любого многочлена третьей степени.

Мы позаботились о существовании корней у многочленов нечетной степени. А как доказать существование у2?

§ 16.3. Формализация Гейтинга

Как уже говорилось, первую формализацию интуиционистской логики дал ученик Брауэра А. Гейтинг. Первоначально сам Брауэр не рассматривал эту формализацию как нечто устойчивое, настаивая на неформализуемости не только интуиционистской математики (в чем он был прав), но и самой логики (в чем он тоже был прав, если рассматривать целый класс конструктивных логик). Но попытки видоизменить конструкцию Гейтинга приводили к гораздо менее красивым системам, а его формализация постепенно обрастала точными интерпретациями и красивыми теоремами. В результате сейчас интуиционистскую логику отождествляют с формализаций Гейтинга.

Формализацию Гейтинга проще всего описать как результат замены в исчислении естественного вывода для классической логики правила двойного отрицания на правило из лжи следует все что угодно ( exfalso quodlibet ).

A А

---- (16.11)

Поскольку ex / also quodlibet допустимо в классической логике, любое логическое доказательство в системе Гейтинга одновременно является классическим доказательством 21 . Так что имеется возможность, не будучи интуиционистом, анализировать конкретные доказательства и при прочих равных условиях проводить их интуиционистскими средствами. Доказательство закона исключенного третьего А V А ( 11.2 ) использовало закон двойного отрицания. В интуиционистской логике от данного вывода остается почти все, кроме конца, и доказывается

Доказательство формулы А & ЗхВ(х) =>• Зх(А & В ( х )) может быть проведено интуиционистскими средствами, а Ух(А V В ( х )) => • А V Ух В ( х ) — нет.

В самом деле, рассмотрим два этих доказательства.

* А & Зх В ( х )

А ЗхВ(х) В ( С 1 )

А & B ( ci )

Зх(А & В ( х )) А & Зх В ( х ) => • Зх(А & В ( х ))

Второе доказательство:

(16.12)

* Ух(А V В ( х ))

* А * А

* z произвольное

| А V Ух В ( х )

A V B(z) B(z)

A xB(x)

УхВ(х) АУУхВ(х)

(16.13)

Ух(А V В(х)) ^ А\/ УхВ(х)

В данном доказательстве используются и закон исключенного третьего, и правило exfalso quodlibet (когда из А и А V B ( z ) следует B ( z )).

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

  • 21 Тем не менее в конкретных теориях, основанных на гейтинговской формализации интуиционистской логики, вполне могут быть результаты, противоречащие классической логике. См. далее.

Отметим, что свойство замены эквивалентных сохраняется и для интуиционистской логики (все формулы, на которых оно базируется, доказываются интуиционистски).

Упражнения к § 16.3

Попытайтесь доказать интуиционистски:

А & ( В V С ) => ( А & В ) V ( А & С).

А V ( В & С ) => ( А V - В ) & ( А V С).

( А & В ) V ( А & С ) =^ А & ( В V С).

( А V - В ) & ( Л V С ) => Л V ( В & С).

А => А .

А V -В =>• ( А => В).

( А => В ) => А V .

§ 16.4. Первые математические модели интуиционистской логики

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

Прежде всего, поскольку отношение Ь А => В транзитивно, рефлексивно и почти антисимметрично, оно является отношением частичного порядка на элементах алгебры Линденбаума-Тарского. Далее, & и V являются нижней и верхней гранями двух элементов согласно данному отношению. Для обоснования этого достаточно доказать (для &; для V аналогично):

А & В =>• А , А & В =>• В ,

( П А\ ( п п\ ( П ли п\ (16.14)

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

Рассмотрим характеристическое свойство импликации. Если А и А => В , то В . Для корректности вывода при оценках формул элементами частично-упорядоченного множества необходимо, чтобы ни один шаг вывода не понижал оценки формул. Поэтому приходим к характеристическому свойству импликации:

а П ( a D Ь ) =4 Ь . (16.15)

А для того, чтобы обеспечить (хотя бы косвенно) свойства, связанные с правилом дедукции, нужно, чтобы импликация была максимальным элементом, для которого выполнено такое свойство. И тогда а =4 Ь 43- ( a D 6 ) = 1.

Теперь рассмотрим частный случай, когда Ъ = 0. В этом случае импликация a D 0 несовместима с а : а П ( a D 0) = 0, и, более того, является максимальным из элементов, несовместимых с а . Поэтому a D 0 естественно называть псевдодополнением а , и по аналогии в алгебре ( a D 6 ) называют относительным псевдодополнением а относительно Ъ .

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

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

Предложение 16.4.1. Каждая интуиционистская теория имеет точную гейтинговозначную модель.

Доказательство. Такой моделью является алгебра Линденбаума-Тар-
ского рассматриваемой теории. ?

Первоначально понятие псевдобулевых алгебр могло показаться специально придуманным для интуиционистской логики и поэтому не очень интересным. Но уже в 30-х гг. Тарский и Куратовский показали, что решетки открытых множеств топологического пространства являются псевдобулевыми алгебрами и поэтому в качестве логических значений формул интуиционистской логики можно брать открытые множества некоторого пространства (скажем, отрезка действительных чисел [0, 1]).

Формула считается истинной, если ее значением является все пространство, ложной — если ее значение есть 0 .

Значением А нельзя брать дополнение значения А , поскольку дополнение открытого множества замкнуто и, соответственно, почти никогда не является открытым. Но можно взять внутренность дополнения A : Int А . Одна из эквивалентных формулировок определения внутренности множества — наибольшее открытое подмножество, в нем содержащееся, что в точности соответствует псевдодополнению.

Соотвественно, значение импликации определяется «почти» как в булевой алгебре: ( A D В ) = Int ( ВГ \ А). Еще одно место, где приходится брать внутренность, — значение всеобщности, поскольку пересечение бесконечного семейства открытых множеств не всегда открыто.

Упражнения к § 16.4

Покажите, что в определении псевдобулевой алгебры дистрибутивность выводится из существования и единственности относительного псевдодополнения.

Постройте топологическую модель, на которой опровергаются следующие формулы:

A V А;

А => А ;

А V А ;

А V (А => А).

Наглядней данные модели получатся, если в качестве пространства взять единичный круг, а не отрезок.

§ 16.5. Модели крипке

Следующий класс моделей интуиционистской логики связан с давней проблемой, наиболее остро прозвучавшей в знаменитом вопросе Авер- роэса. Если даже Бог может подчиняться законам логики, значит, она описывает не только наш мир, но и другие возможные миры. Поэтому возникает идея рассмотреть модели, основанные на множестве миров.

Еще Брауэр заметил, что содержательно интуиционистская логика предполагает накопление знаний, а не их видоизменение, и это замечание было положено в основу моделей возможных миров, обычно называемых моделями Крипке 22 .

Определение 16.5.1. Модель Крипке Я для сигнатуры a — алгебраическая система некоторой одноосновной сигнатуры w , называемой сигнатурой отношений на мирах, элементами универса которой UK (часто обозначаемого WK или просто W ) служат алгебраические системы сигнатуры а. Элементы универса называются (возможными) мирами. Уни- верс мирар W обозначается U p .

Для случая интуиционистской логики рассматривается конкретный вид моделей Крипке — интуиционистские модели Крипке. Сигнатура отношений w состоит из одного двуместного отношения =<;. Оно является отношением частичного порядка. Миры согласованы с данным отношением следующим образом:

р Ц. q => Up С Uq,

p4q&U p \ = P(ai,...,a n ) => U q \ = P(ai,... ,a n ).

Таким образом, при подъеме по мирам универсы могу лишь расширяться, и истинность элементарных формул не может перети в ложность. Вспоминая определение из гл. 1, получаем, что при р =4 q q является надструктурой р.

Истинность в модели Крипке интуиционистской логики определяется следующим образом.

Определение 16.5.2. Индуктивно определяем отношение р |= А, где

р — мир, А — формула.

1. р |= Р(а±, ..., а п ) означает истинность Р(а±, ..., а п ) в классической алгебраической системе р23.

История создания данного понятия, как всегда, более сложная. Этот класс моделей неявно содержался еще в алгебраических моделях (см. замечание ниже). Явно он был использован П. Дж. Коэном для доказательства независимости аксиомы выбора и континуум-гипотезы от стандартной теории множеств. С. Крипке первым показал применимость данной конструкции к широкому классу логик и ее гибкость.

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

р |= А & В означает, что р |= А ир |= В.

р |= А V В означает, что р |= А илир |= В .

р\= А=? В означает, что для всех миров q , таких, что р =4 Q , если q |= А, то q \= В.

р |= А означает, что для всех миров q , таких, что р =4 Q , неверно, что q |= А.

р |= Зх А{х) означает, что найдется такое a U p , чтор |= А{а).

р |= Ух А ( х ) означает, что для всех миров q , таких, что р =4 q , и для всех a ( z U q q \ = A ( a ).

Пример 16.5.1. Рассмотрим следующую модель Крипке.

• А

(16.16)

В ней не истинно А V А, поскольку в начальной точке у нас не известно ни то, ни другое (нет А, но нельзя утверждать иА, поскольку выше А может появиться).

Пример 16.5.2. Покажем, что интуиционистская логика не задается никакой конечной системой истинностных значений. В самом деле, если бы это было так, то имелось бы не более п логических значений формул, и, значит, в любой интерпретации в любой совокупности из п + 1 формулы две обязательно были бы эквивалентны24. Значит, была бы тождественно истинна формула разности разных формул. Но следующая модель Крипке опровергает дан - ную дизъюнкцию, поскольку ни одна из эквивалентностей не истинна в нижней точке :

( А \ <^> А 2) V V ( A n <^> A n + i ),

  • 24 Здесь мы принимаем естественную гипотезу, что эквивалентность означает совпадение истинностных значений.

И, наконец, рассмотрим пример модели Крипке для логики предикатов.

Пример 16.5.3.

|0,1, 2|- A(0), A(l)

L \ ' (16.18)

{0,1} • A (0)

t

{0} ¦

В данной модели в любом из миров есть такое п, что не истинно А{п) V А ( п ). Значит ни в каком из миров не истинно Ух(А(х) V А ( х )). А тогда, по определению истинности отрицания, в любой ее точке истинно

Ух ( А ( х ) V А ( х )).

(16.19)

Итак, с интуиционистской логикой могут быть совместимы и формулы, противоречащие классической.

Упражнения к § 16.5

Постройте модель, в которой УхА ( х ), но не выполнено, что Эх А ( х ).

Постройте модель, где опровергается ( А => • В ) V ( В => • А). Может ли такая модель не иметь ветвлений?

§ 16.6. Семантические таблицы для интуиционистской логики

Как уже говорилось, конструкция семантических таблиц переносится на неклассические логики. Здесь мы рассмотрим ее для интуиционистской логики.

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

Определение 16.6.1. Интуиционистская спецификация — фигура а? , где S — спецификация истинностного значения |= или = \ , а a — интуиционистский префикс, описывающий множество миров, в которых должно иметь место данное значение формулы.

Интуиционистский префикс — кортеж, членами которого являются натуральные числа и символы * .

Если префикс не содержит , то он описывает единственный мир, именем которого служит данный кортеж.

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

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

Два префикса совместимы, если их множества миров пересекаются.

Исходная формула помечается как [ ] =| А .

Перепишем все правила классических семантических таблиц, указывая, как видоизменяются префиксы.

Индексы видоизменяются лишь в правилах =| =?-, =\ , =| V . Появившиеся в них формулы будут отвергаться либо утверждаться не в мире а, в котором отвергалась исходная формула, а в новом мире вида а * [ и ] , непосредственно следующем за ним. и в каждом из таких правил выбирается новым. Противоречием считается лишь такая пара формул а |= А, [3 =\ А, в которой а и [3 совместимы.

Заметим, что формула, которая стала истинной, не может в дальнейшем оказаться ложной, поскольку все правила, вводящие |= А, помещают звездочку в конец кортежа.

Пример 16.6.1. Рассмотрим семантическую таблицу для закона исключенного третьего.

[ ] =| А V А
[] =\ А [} А (16.21)

[1, к ]\= А

Противоречия нет, потому что А отвергается на более раннем уровне, чем утверждается. Из данной таблицы получается следующая модель Крипке:

Слева модель Крипке записана со всей информацией, которую можно извлечь из семантической таблицы,асправа—так, как это принято делать, оставив лишь минимальную информацию, полностью ее определяющую25 .

Заметим, что у нас получилась несколько другая модель, чем(16.21), чуть проще, но чуть менее наглядная. Действительно, А нет сейчас, А , правда, тоже нет, но никогда и не будет. Так что на самом деле в данной модели истинно А , но опровергается А , и она более сильна, чем нужно для опровержения А V А .

Пример 16.6.2. Рассмотрим теперь следующую семантическую таблицу-

[] = \ А => А

[1, *| 1= [1] = А

oi — I л (16.23)

[1>A

[1,2] |= -

Получившаяся модель отличается от (16.22) добавлением совершенно избыточного промежуточного мира:

(16.24)


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

Если на данном уровне отвергаемая формула, требующая подъема на новый уровень, единственна, то новый уровень можно не вводить.

  • 25 Заметим, что в моделях Крипке интуиционистской логики (да зачастую и других логик) не принято выписывать отвергаемые в данной точке утверждения, поскольку формально достаточно принять положение о том, что все не истинное отвергается. Но семантическая таблица ставит отвержение лишь там, где истинность данной формулы недопустима для опровержения цели. Поэтому на самом деле мы теряем часть информации, особенно ценную для преобразования моделей.

Строгое обоснование данного сокращающего правила следует ниже .

Рассмотрим теперь семантическую таблицу для достаточно сложной формулы (формулы Крипке ).

[] =| (((( А => • В ) => • А ) => • А ) => • В ) => • В

М 1 = (((-^ ^ -^* ) =^ ^4 ) =^ ^4 ) =^ - В

[] =| 5

[ к ] |= В

М Н (( -^ ^ - В ) ^ -*4 ) ^ -^

(16.25)

[ • ,1,*] |= ( А => Б ) => А [*,1]=| А

[ к , 1] |= А

[*, 1, - к ] =\ А =?¦ В [*,1,*,2]=\ В

[ к , 1, *, 2, - к ] |= А

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

[ ] =| Ух ( А ( х ) V А { х ))

[ к ] |= Ух ( А ( х ) V ( х ))

[- к ] = х ( А ( х ) V A { x ))

[ • ,1] Н ^( со ) V A ( co )

[*, 1] =| А ( со )

[ к , 1] =| - А ( со )

[ • ,1,2,*] |= А ( с 0 )

[*, 1, 2] =| А ( с \) V A ( ci )

(16.26)

Таким образом, в интуиционистской логике правило =| V тоже может оказаться многократно применяемым. Если префикс данного правила содержит * , то в каждом совместимом с данным префиксом мире должна порождаться новая константа, если только применение правила не стало избыточным.

Упражнения к § 16.6

16.6.1. Разработайте быстрый алгоритм для проверки совместимость префиксов.

26 Замечание для профессионалов. Данная формула была изобретена С. Крипке для иллюстрации того, что в интуиционистском выводе и в интуиционистских таблицах нужно, в отличие от классических, иногда по два раза разбивать одну и ту же пропозициональную формулу. У нас оказалось достаточно одного раза из-за механизма отождествлений префиксов.

( А => • В V С ) => • ( А => • .В) V ( А => С).

( Л \/Л ).

( А & - В) =>• А V В.

Ух(А(х) V А ( х ))

§ 16.7. Полнота семантических таблиц

Как было замечено при доказательстве теоремы полноты классической логики, полнота и корректность — первое, что необходимо доказывать для нового формализма.

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

Начнем с обоснования сокращающих правил, специфических для интуиционистской логики.

Предложение 16.7.1. Если на данном уровне в секвенции имеетсялишь единственная формула: отвергаемая формула, требующая подъема на новый уровень, то новый уровень можно не вводить.

Доказательство. Пусть на уровне а = а\ * [ г ] у нас имеется лишь формула а =\ А. Тогда, поскольку после разбиения формулы а =\ А на уровне а больше не останется формул, формулы, специфицированные на уровне а, в дальнейшем появиться не могут. ?

Предложение 16.7.2. Одну и ту же формулу достаточно на одном и том же пути префиксов разбивать не более одного раза (многократно используемую — не более одного раза по каждой константе).

Доказательство. Необходимость многократного разбиения может возникнуть лишь для правил |= => и |= . Здесь возникают отвергаемые формулы, которые автоматически не могут быть перенесены на следующие уровни. Детально разберем варианты, возникающие в |==>.

Если разбивается формула [ а , * ] |= А => В , то в подтаблицах появляются формулы [ а , - к ] |= В и [ а ,*] =| А . Первая из них сохраняется при переходе вверх по таблице, вторая не сохранялась бы, если бы не было звездочки. Таким образом, при повторном разбиении такой же формулы на более высоком уровне мы получаем такие же формулы с более узкими спецификациями, которые являются избыточными. ?

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

§ 16.8. Фундаментальные результаты теории доказательств

Интуиционистская логика — одна из немногих логических систем, на которые переносятся все главные результаты теории доказательств для классической логики.

Система естественного вывода для интуиционистской логики образуется из классической системы заменой правила доказательства от противного на правило ex falso quodlibet :

А А

В Первым нетривиальным результатом теории доказательств для интуи- ционисткой логики был следующий.

Предложение 16.8.1. (Теорема Гливенко) Классическая логика изоморфно погружается в интуиционистскую.

Доказательство. Построим следующее погружение классческой логики в интуциционистскую:

G ( A ) = А ( А элементарна)

G(A & ) = G(A) & G(B)

G( j4 V В ) = (G(A) & G(B))

G(A => В ) = G(A) => G(B)

G(vA) = xG(A) G(3xA) = VxG(A)

Итак, систематически устраняются дизъюнкция и существование.
Остальные связки остаются без изменения.

Этот результатпроизвел шокирующее впечатление. Ослабив одну из логических аксиом,мы получилинасамом деле более сильную систему, включающую классическую логику как подсистему. Но, надеюсь, Вы уже привыкли к тому, что самоограничение и отказ от лишнего слишком часто на самом деле означает получение дополнительных возможностей.

Теоремы устранения сечений и нормализуемости доказываются почти одинаково для классической и инутционистской логики (на самом деле они и впервые были установлены для них одновременно). В правилах нормализации заменяется лишь правило, связанное с отрицанием, когда вслед за введением отрицания идет его удаление.

При переносе на интуиционистскую логику теоремы Крейга об интерполяции опять пользуемся семантическойтаблицей.А изтеоремы Крей- га следует теорема Бета об определимости.

§ 16.9. Реализуемости и вариации интуиционистских принципов

Рекурсивная реализуемость Клини может рассматриваться как непосредственная конкретизация колмогоровской интерпретации следующим образом:

Все функции — алгоритмы.

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

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

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

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

Определение 16.9.1. Каждой формуле А сопоставляется множество натуральных чисел (?) А (множество ее рекурсивных реализаций).

п G (?) А читается « п рекурсивно реализует А » (или просто «реализует», если данный конкретный вариант реализуемости однозначно определяется контекстом) и обозначается сокращенно п (?) А .

1. (?) (t = и ) =

{ 0 } Значения равны; 0 Значения различны.

п (?) А & В - фф - Зп \, иг ( и = [ п \, пг ] & n \ (?) А & иг (?) В) .

п ( г ) i VB < s Зп 1, пг ( и = [ и 1, пг ] & ( их = 0 => • иг (?) А ) & (ni т ^ 0 => • Иг (?) - В ))-

и (?) ( А => • В ) - ФФ - Ут ( т (?) А => ! U ( n , m ) & U ( n , m ) (?) - В) .

5. (?) А

(r) A = $; 0 , © A ^ Й .

и (?) Vx A(x) - ФФ - Vm(!U(n, m) & U(n, m) (?) A(m)) .

и (?) Эх A ( x ) ФФ - 3 m , m ( n = [ ni , m ] & щ (?) A(m)) .

В этих пунктах считаются фиксированными некоторое кодирование кортежей натуральных чисел натуральными числами и некоторая универсальная рекурсивная функция U ( ж , у ) .

Предложение 16.9.1. Любая теорема интуиционистской арифметики рекурсивно реализуема.

Доказательство. Единственный нетривиальный пункт — реализу
емость индукции. Но здесь реализация заключения строится примитив
ной рекурсией по реализациям посылок.

Замечание

Не обольщайтесь, что построение, извлеченное из арифметического доказательства, примитивно-рекурсивно. Примитивно-рекурсивно строится программа функции.

Сразу же после того, как появилась первая точная интерпретация реализуемости, стали появляться результаты, показывающие, что реализуемость отличается от логической выводимости.

Пример 16.9.1. Абсолютная формула — такая, которая понимается одинаково в классической и конструктивной математике. Например, таковы формулы Ух f ( x ) = О , где / — примитивно-рекурсивания функция. Среди таких формул есть как выражающие разрешимые свойства, так и выражающие неразрешимые свойства.

Рассмотрим абсолютную неразрешимую формулу А{х). Тогда, если бы формула Ух ( А ( х ) V А ( х )) была реализуема, то имелась бы рекурсивная функция, которая по числу п выдавала бы пару, первый элемент которой является дискриминатором случая, а второй — реализацией соответствующей формулы. Взяв первую компоненту результата, мы смогли бы построить рекурсивную характеристическую функцию неразрешимого множества27. Значит, у рассматриваемой формулы нет реализации, и, по определению, тогда реализуема

Ух ( А ( х ) УА ( х )). (16.28)

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

Следующий принцип впервые явно сформулировал А. А. Марков. Мы уже формулировали его содержательно на стр. 345.

Формальный принцип Маркова: ... . _.

Ух(А(х) V А ( х )) к ЗхА ( х ) => ЗхА(х) v '

Еще один формальный принцип был сформулирован независимо С. К. Клини и Н. А. Шаниным, но по заслугам носит другое имя.

Формальный тезис Черча:
\/ж( А{х) => ЗуВ(х,у)) (16.30)

=>¦ ЗеУх ( ( х ) => • ! / е ( ж ) & В ( х , / е ( ж )))

  • 27 Данная конструкция переносится практически на любое точное понятие реализуемости, изменяется лишь понятие абсолютной и неразрешимой формулы.

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

Заметим, что принцип Маркова является классически истинной формулой, атезис Черча противоречит классической логике. Исходя из него, доказывается формула ( 16.28 ).

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

Принцип IP :

w ( A t \ и ( \\ V / з ( л ( \ и ( \\ (16.31)

Этот принцип еще сильнее унижает отрицание: оно не может хоть чем-то помочь при нахождении объектов. Он имеет и свое пропозициональное выражение, називаемое принципом Медведева:

(- i ^ BVC )^(- i ^ B ) V (- A ^ C ) (16.32)

Рассмотренные два одинаково красивых, но несовместимых между собой случая были лишь началом в построении целой совокупности различных понятий реализуемости.

§ 16.10. Интуиционистская логика и категории

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

Из интерпретации Колмогорова сразуже видно, что конъюнкции соответствует прямое произведение реализаций, а дизъюнкции — их прямая сумма. Простейшая категорная конструкция, превращающая мор- физмы в объекты, так называемая категория морфизмов. Ее объектами являются морфизмы, а морфизмом между / и д считается коммутативная диаграмма

Но такое определение, с одной стороны, не обеспечивает достаточного богатства операций над морфизмами и, с другой стороны, выводит нас за пределы исходой категории 28 . Поэтому в определении семантики интуиционистской логики используется гораздо более сильная категорная конструкция — экспоненциал.

Определение 16.10.1. Объект Ъ а называется экспоненциалом объектов а иЬ, если есть морфизм означивания ev : Ъ а х а —> Ъ, такой, что для любого объекта с и любого g : с х a —)¦ Ъ имеет место коммутативная диаграмма

Таким образом, морфизм ev играет роль функционала означивания, он получает в качестве первого аргумента код функции, а в качестве второго — аргумент, к которому функция применяется, и выдает значение функции на данном аргументе29 g можно рассматривать как функцию от двух аргументов д(со,ао) Ь. По преобразованию Карри, функцию от двух аргументов можно заменть на функционал ( д —> ( а —> 6)), который и обозначается на диаграмме д. Поскольку стрелка пунктирная, такой д находится единственным образом.

Итак, экспоненциал дает возможность определять преобразование Карри или, что эквивалентно, функционал частичной параметризации.

Что гораздо важнее, поскольку пойти на сознательное ограничение класса операций в некоторых случаях даже целесообразно.

Естественно, все это верно лишь если морфизмы есть функции либо программы, но аналогия работает и в других случаях.

При частичной параметризации мы подставляем в функцию многих аргументов значения некоторых из них и получаем остаточную функцию, которая готова принять оставшиеся неизвестными аргументы.

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

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

Подробнее можно посмотреть данную конструкцию и ее применения в книге [12].

Упражнения к § 16.10

§ 16.11. О формализации незнания

Для тех, кто к совершенству путь прошел,

Неведение знанием бывает.

А знанье, что невежда приобрел,

В невежестве его изобличает.

(Руми. [23, стр. 212])

Рассмотрим принципиально новые возможности, предоставляемые интуиционизмом в области формализации. Творческая последовательность.

если в году n не доказана формула A ,

если она доказана.

16.10.1. Вглядимся в диаграмму для экспоненты, конкретизированную для категории частичного порядка. Чем окажется в данном случае экспонента? Нет ли аналогий с псевдобулевыми алгебрами?

Видно, что творческая последовательность идейно совпадает с моделью Крипке интуиционистской логики. В моделях Крипке формула может некоторое время оставаться неразрешенной, а затем при движении вверх по дереву возможных миров стать истинной. Если же она никогда не станет истинной, она по определению считается ложной. Принцип, формально выражающий наличие творческих последовательностей, носит называние схемы Крипке, хотя Крипке лишь вторым написал его формальное выражение. В доказательствах его использовал уже Брауэр, а под другим названием — конструкций — изоморфный принцип использовал и формально выразил Крайзел:

Ух За(А(х) 43- Зпа(п) = 1). (16.34)

Беззаконные последовательности. Вводится новый тип последовательностей, обладающий следующим свойством:

Уа ( А ( а ) => ЗпУ /( Ут ( т < п => а ( т ) = /( m )) => A ( f ))),

т. е. все, что мы о них знаем, мы знаем из уже полученной информации. Здесь / — произвольная последовательность. Брауэр приводил в качестве примера последовательности, естественно формализуемой как беззаконная, последовательность результатов измерений, воспринимаемых из физического источника, природа которого неизвестна.

Из определения беззаконности следует, что никакая беззаконная последовательность не равна тождественно нулю, то есть

Va Vna ( n ) = 0. (16.35)

В самом деле, возьмем произвольную беззаконную последовательность а. Если бы она была тождественно равна нулю, то это мы узнали бы из конечного числа ее членов, но тогда было бы такое конечное число и членов, что любая последовательность, первые и членов которой были бы равны нулю, была бы тождественно равна нулю, что абсурдно.

Нельзя ввести вместо переменной по беззаконным последовательностям предикат “быть беззаконной”, поскольку его отрицание устанавливалось бы, исходя из конечного числа значений последовательности. Так что не всегда тип данных можно заменить новым предикатом.

Трулстра (Голландия, 1968) доказал, что композиции алгоритмов и беззаконных последовательностей образуют модель интуиционизма, в которой можно промоделировать творческие последовательности.

Беззаконные последовательности явились первым примером позитивного использования незнания в точных науках. Возможность сформулировать незнание в виде логической формулы — еще одно достижение интуиционизма.

СодержаниеДальше

наверх страницынаверх страницы на верх страницы









Заказать работу

© Библиотека учебной и научной литературы, 2012-2016 Рейтинг@Mail.ru Яндекс цитирования