Конструктивная математика

Акимов О.Е.

3. Логика и математика как два метода познания

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

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

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

Логики и акусматики все свои знания выражали в словесно-символической форме, часто в очень претенциозной, поэтической и религиозной; математики же должны сами конструировать свои представления, т.е. заниматься более рациональным и прозаическим трудом. Понятийный спектр имеет две крайности в виде простого символа и философского принципа. Чистыми символами оперируют обыкновенно мистики. Так, пифагорейцы в качестве символов избрали для себя числа, сторонники каббалы - буквы, но перед первыми лежит всё же реальный мир, а перед вторыми - «священные тексты», поэтому пифагорейцы по степени идеализации мира приближаются к платоникам, а каббалисты занимают исключительно иррациональную позицию, смыкающуюся с позициейбогословов.

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

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

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

Ошибка конструктивиста-математика - это недопустимое расхождение между объектом и его моделью; ошибка формалиста-логика - это противоречие внутри формальной системы, которое никакого отношения к объективной реальности не имеет, так как он оперирует только символами действительного мира. Двигаясь итерационно шаг за шагом, конструктивный математик приближается к своему идеалу совсем не так как математик-формалист или логик. Опираясь напредставления о реальности, он стремится воссоздать, сконструировать соответствующую этой реальности конкретную модель. Эта его частная модель всегда будет более восприимчива к модернизации, ее наглядные детали обладают высокой мобильностью и легко поддаются коррекции. Психика конструктивиста как нельзя лучше приспособлена для подобного рода занятий. Так, Архимед за свою долгую жизнь инженера и теоретика успел построить и проанализировать множество механических и геометрических моделей. Или взять Максвелла, который за свою короткую творческую жизнь поменял три совершенно различных модели электромагнитного взаимодействия.

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

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

Конструктивист уверен в ценности теории самой по себе, без всяких меркантильных, утилитарных и прагматических намерений. Он говорит себе: объективный мир устроен так-то и так-то, вот адекватная модель, отображающая реальные процессы. Формалист критикует конструктивиста за идеализм, оторванность от жизни и бесполезность его теоретических построений. Путем эмпирической и формальной подгонки, он снабжает потребителей интеллектуального продукта неким «описанием» природы или «инструкцией» к ее использованию. Дескриптивной эпистемологией устанавливаются необходимые каузальные связи между причиной и следствием или функциональные зависимости между воздействием и откликом. Формалисты уверены, будто логика (т.е. техника составления правильных цепей рассуждений, сюда же можно включить силлогистику Аристотеля, диалектику Гегеля, а также античную и средневековую диалектику как искусство ведения софистических и схоластических споров) помогает открывать новые истины, что, конечно же, не так. Формально-феноменологические уравнения, таблицы и графики имеют весьма косвенное отношение к физической действительности, хотя они и позволяют сделать быстрый расчет или предсказать наперед ту или иную опытную ситуацию.

Формалисты говорят: «Математика - это символьный язык, служащий для формального описания объекта познания». Конструктивист возразит ему: «Нет, математика это не столько язык познания, сколько сам объект познания». Граф или группа, конечно, могут отображать некие объекты, существующие в реальности, однако эти математические сущности могут обойтись и без физических представителей. Поэтому правильнее говорить о параллелизме между математическим и физическим мирами, когда вправе утверждать о представлении математических структур физическими моделями. Чтобы почувствовать разницу между формальным и конструктивным подходом, нужно отчетливо видеть разницу между математическим и логическим выражением.

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

Логический вывод подчиняется отношению порядка, который выражается словосочетаниями: «если А, то В», «А влечет В», «В, потому что А». Вместо букв А и В мы можем подставить C и D или любые другие буквы, т.е. логика изначально и принципиально имеет дело только с символами реальности, но не с самой объективной реальностью. Она упорядочивает мысли субъекта, но не внешние объекты, и правильность дедуктивного вывода еще не гарантирует истинности знаний о реальном мире, поскольку в буквенной идентификации реальных предметов может быть допущена ошибка.

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

Логика очень ревниво относится к формированию понятий, можно сказать, что она только этим и занята. Она может давать себе высокопарные определения: «наука о доказательствах» или «наука о правильных умозаключениях», но большая часть ее всегда приходилась на долгие и нудные суждения об именах, значениях, определениях и классификациях огромного количества слов, почерпнутых из жизни или различных отраслей знаний, вроде религии, морали и права. Логика со времен Зенона Элейского стремилась включить в качестве частностей арифметические и геометрические объекты, но последние этой близости настойчиво сопротивлялись. По апории Зенона «Ахилл и черепаха» противостояние между математикой и логикой особенно заметно. Еще большие претензии логика распространяла на естествознание. Завладев биологической классификацией и описанием животных и растительных форм, она возомнила, что это и есть настоящая наука. Но конструктивные представления не совместимы с составлением классификаций детерминированных сознанием форм; систематизация знаний - это самая первая форма естествознания, которая больше сковывает, чем способствует его развитию. Классификация предполагает описание по родам и видам, но посмотрите, например, на астрономию, какая здесь может быть подчиненность? Ее нет, по крайней мере, в той форме, в какой подчиненность существует в логике.

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

7. СОВРЕМЕННАЯ ЛОГИКА И ДРУГИЕ НАУКИ

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

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

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

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

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

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

Другой формой объединения математики и логики в одну науку было объявление математической, или современной, логики одним из разделов современной математики. Многие математики и сейчас ещё считают главной - если не единственной - задачей математической логики уточнение понятия математического доказательства.

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

Современная логика тесно связана также с кибернетикой - наукой о закономерностях управления процессами и системами в любых областях: в технике, в живых организмах, в обществе. Основоположник кибернетики, американский математик Н.Винер не без оснований подчёркивал, что само возникновение кибернетики было бы немыслимо без математической логики. Автоматика и электронно-вычислительная техника, применяемые в кибернетике, были бы невозможны без использования алгебры логики - этого возникшего первым раздела современной логики. В управляющих системах, применяемых в кибернетике, значительное место занимают релейно-контактные схемы, моделирующие логические операции. Описание таких операций, даваемое логикой, способствует детальному анализу логического строения мысли и открывает поразительные перспективы автоматизации логических процессов.

Помимо кибернетики современная логика находит широкие приложения и во многих других областях науки и техники.

Логика предикатов

Понятие ``предикат'' обобщает понятие ``высказывание''. Неформально говоря, предикат - это высказывание, в которое можно подставлять аргументы. Если аргумент один - то предикат выражает свойство аргумента, если больше - то отношение между аргументами.

Пример предикатов. Возьмём высказывания: ``Сократ - человек'', ``Платон - человек''. Оба эти высказывания выражают свойство ``быть человеком''. Таким образом, мы можем рассматривать предикат ``быть человеком'' и говорить, что он выполняется для Сократа и Платона.

Возьмём высказывание: ``расстояние от Иркутска до Москвы 5 тысяч километров''. Вместо него мы можем записать предикат ``расстояние'' (означающий, что первый и второй аргумент этого предиката находятся на расстоянии, равном третьему аргументу) для аргументов ``Иркутск'', ``Москва'' и ``5 тысяч километров''.

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

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

Это рассуждение на языке логики высказываний можно записать тремя отдельными высказываниями. Однако никакой связи между ними установить не удастся. На языке логики предикатов эти предложения можно выразить с помощью двух предикатов: ``быть человеком'' и ``быть смертным''. Первое предложение устанавливает связь между этими предикатами.

Перейдём теперь к формальному изложению логики предикатов.

Язык логики предикатов

``Предикатные формулы'' обобщают понятие пропозициональной формулы, определённое в части 2.

Предикатная сигнатура - это множество символов двух типов - объектные константы и предикатные константы - с неотрицательным целым числом, называемымарностью, назначенным каждой предикатной константе. Предикатную константу мы будем называть пропозициональной, если её арность равна 0. Пропозициональные константы являются аналогом атомов в логике высказываний. Предикатная константа унарна, если её арность равна 1, и бинарна, если её арность равна 2. Например, мы можем определить предикатную сигнатуру

{ a, P, Q }

(4)

объявляя a объектной константой, P - унарной предикатной константой, и Q - бинарной предикатной константой.

Возьмём предикатную сигнатуру , которая включает по крайней мере одну предикатную константу и не включает ни одного из следующих символов:

• объектные переменные x, y, z, x1, y1, z1, x2, y2, z2, ...,

• пропозициональные связки,

• квантор всеобщности и квантор существования ,

• скобки и запятая.

Алфавит логики предикатов состоит из элементов из и четырёх групп дополнительных символов, указанных выше. Строка - это конечная последовательность символов из этого алфавита.

Терм - это объектная константа или объектная переменная. Строка называется атомарной формулой, если она является пропозициональной константой или имеет вид R(t1, ..., t_n), где R - предикатная константа арности n (n > 0) и t1, ... , t_n - термы. Например, если мы рассматриваем сигнатуру (4), то P(a) и Q(a, x) - атомарные формулы.

Множество X строк замкнуто относительно правил построения (для логики предикатов), если

• каждая атомарная формула принадлежит X,

• для любой строки F если F принадлежит X, то ¬F тоже принадлежит,

• для любых строк F, G и любой бинарной связки , если F и G принадлежат X, то также принадлежит (F G),

• для любого квантора K, любой переменной v и любой строки F если F принадлежит X, то также принадлежит Kv F.

Строка F является (предикатной) формулой, если F принадлежит всем множествам, которые замкнуты относительно правил построения.

Например, если рассматриваемая сигнатура есть (4), тогда

(¬P (a) x(P (x) & Q(x, y)))

- формула.

3.1 Является ли x формулой?

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

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

• каждая атомарная формула обладает этим свойством,

• для любой формулы F, обладающей этим свойством, ¬F также обладает этим свойством,

• для любых формул F, G, обладающих этим свойством, и любой бинарной связки , (F G) также обладает этим свойством,

• для любого квантора K, любой переменной v и любой формулы F, обладающей этим свойством, Kv F также обладает этим свойством.

Тогда это свойство выполняется для всех формул.

3.2 Если формула содержит квантор, тогда она содержит переменную. Верно или нет ?

3.3 Если формула содержит квантор, тогда она содержит скобки. Верно или нет ?

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

v1 ··· v_n (n 0)

будем писать как v1 ··· v_n, и подобным образом для квантора существования.

Свободные и связанные переменные

Множество свободных переменных^* формулы F определяется рекурсивно, следующим образом:

Определение 22 (Свободные переменные).

• Все переменные, входящие в атомарную формулу, являются свободными переменными этой формулы,

• свободные переменные формулы F являются свободными переменными формулы ¬F,

• переменные, являющиеся свободными для хотя бы одной из формул F или G, являются свободными переменными формулы (F G),

• все свободные переменные формулы F кроме v являются свободными переменными формулы Kv F.

Определение 23 (Замкнутая формула). Формула без свободных переменных называется замкнутой формулой, или предложением.

Определение 24 (Связаная переменная). Переменная v связана в формуле F, если F содержит вхождение Kv, где K - квантор.

3.4 Найдите свободные переменные и связанные переменные формулы

y P(x, y) & ¬ x P (x, x)

Представление предложений русского языка предикатными формулами

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

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

• a представляет число 10,

• P(x) выражает условие ``x является простым числом'',

• Q(x, y) выражает условие ``x меньше чем y''.

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

3.5 Все простые числа больше чем x.

Ответ: y(P (y) Q(x, y)).

3.6 Существует простое число, которое меньше чем 10.

3.7 x равно 2. см. Указания

3.8 x равно 11. см. Указания

3.9 Существует бесконечно много простых чисел.

Подстановка

Определение 25 (Подстановка терма). Пусть F - формула и v - переменная. Результат подстановки терма t вместо v в F - формула, определённая рекурсивно следующим образом:

• результат подстановки t вместо v в атомарную формулу F получается из F одновременной заменой всех вхождений v на t,

• если результат подстановки t вместо v в F есть F' тогда результат подстановки t вместо v в ¬F есть ¬F',

• если результат подстановки t вместо v в F и G есть F' и G' тогда результат подстановки t вместо v в (F G) есть (F' G'),

• если результат подстановки t вместо v в F есть F' и w - переменная, отличающаяся от v, тогда результат подстановки t вместо v в Kw F есть Kw F',

• результат подстановки t вместо v в Kv F есть Kv F.

3.10 Найдите результат подстановки константы a вместо x в формулу из задачи 3.4.

Когда мы намереваемся рассмотреть подстановки вместо переменной v в некоторую формулу, удобно обозначать эту формулу выражением F(v), и обозначать результат подстановки терма t вместо v в этой формуле через F(t) .

3.11 Если v не является свободной переменной F(v), тогда F(t) равно F(v).

Пусть F(x) обозначает формулу

y (P(y) Q(x, y)),

предложенную выше как перевод условия ``все простые числа больше чем x'' (задача 3.5). Формула вида F(t), где t - терм, обыкновенно выражает то же условие применённое к значению t. Например, F(a) есть y (P(y) Q(a, y)), что значит ``все простые числа больше чем 10'', F(z2) есть y (P(y) Q(z2, y)), что значит ``все простые числа больше чем z2''. Существует, однако, одно исключение. Формула F(y), то есть, y (P(y) Q(y, y)), выражает (неправильное) утверждение ``каждое простое число меньше чем оно само''. Проблема с этой подстановкой в том, что, когда мы подставляем переменную y вместо x в F(x), y ``захватывается'' квантором. Чтобы выразить утверждение ``все простые числа больше чем y'' предикатной формулой, мы будем использовать связанную переменную отличную от y и писать, например,

z(P (z) Q(y, z))

Чтобы различать ``плохие'' подстановки, как в последнем примере, от ``хороших'', мы определим, когда терм t является подстановочным для переменной v в формуле F.^*

• Если F - атомарная, тогда t является подстановочным для переменной v в F,

• t является подстановочным для переменной v в ¬F тогда и только тогда, когда t является подстановочным для v в F,

• t является подстановочным для v в (F G) тогда и только тогда, когда t является подстановочным для v и в F и в G,

• t является подстановочным для v в Kw F тогда и только тогда, когда

  1. t не содержит w и является подстановочным для v в F, или

  2. v не является свободной переменной формулы Kw F.

3.12 Терм, не содержащий ни одной связанной переменной формулы F, является подстановочным в F для любой переменной.

Определение 26 (Универсальное замыкание). Универсальное замыкание формулы F - это предложение

v1 ··· v_n F,

где v1, ... , v_n - все свободные переменные F.

Семантика

Выполнимость

Логическое следование

Выводы в логике предикатов

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

Правила для кванторов всеобщности

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

3.19 (P(a) & x (P(x) Q(x))) Q(a).

3.20 xy P(x, y) x P (x, x).

Правила для кванторов существования

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

3.21 (P(a) P(b)) x P(x).

3.22 ¬ x P(x) x ¬P(x).

Корректность и полнота логики предикатов

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

Теорема корректности. Если существует вывод замкнутой формулы F из множества формул , тогда влечёт F.

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

Полнота логики предикатов для случая счётного и для другого множества правил вывода была доказана Куртом Гёделем в 1930 году.

Функциональные символы и равенство: синтаксис

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

Наше наиболее общее понятие сигнатуры определяется следующим образом.

Определение 28 (Сигнатура,константы). Сигнатура - это множество символов двух типов - функциональных констант и предикатных констант - с неотрицательным целым числом, называемым арностью, связанным с каждым символом. Объектная константа - это функциональная константа арности 0. Функциональная константа унарна, если её арность равна 1, и бинарна, если её арность равна 2. Пропозициональная константы, так же как унарные и бинарные предикатные константы, определены как выше.

Определение 29 (Терм). Возьмём сигнатуру , не включающую ни дополнительных символов, указанных в начале данной части, ни знака равенства. Множество X строк замкнуто относительно правил построения термов, если

• каждая объектная константа принадлежит X,

• каждая объектная переменная принадлежит X,

• для каждой функциональной константы h арности n (n > 0) и любой строки t1, ... , t_n, если t1, ... , t_n принадлежит X, тогда также принадлежит h(t1, ... , t_n).

Строка является термом, если она принадлежит все множествам, которые замкнуты относительно правил построения.^*

3.23 Каждый терм содержит объектную константу или объектную переменную. Верно или нет ?

В логике первого порядка существуют три типа атомарных формул:

• пропозициональные константы,

• строки вида R(t1, ... , t_n) где R - предикатная константа арности n (n > 0) и t1, ..., t_n - термы,

• строки вида (t1 = t2), где t1, t2 - термы.

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

Для любых термов t1 и t2, t1 t2 обозначает формулу ¬(t1 = t2).

Функциональные символы и равенство: семантика

Выводы в логике первого порядка

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

Новые аксиомы выражают рефлексивность равенства и имеют вид |- t = t , где t - произвольный терм. Новые правила вывода - правила замены:

где t1 и t2 свободные для v в F(v).^*

Для каждой из следующих формул найдите вывод из пустого множества посылок.

3.27 x = y f(x, y) = f(y, x).

см. Решение

3.28 x y (y = f(x)).

3.29 y (x = y & y = z) x = z.

3.30 x (x = a & P (x)) P (a).

Теории первого порядка

Теория первого порядка сигнатуры определяется с помощью аксиом. Интерпретация, при которой истинны все аксиомы теории первого порядка , называется моделью . Если теория первого порядка выполнима, мы также говорим что она непротиворечива. Логические следствия теории первого порядка называется её теоремами. Доказательство предложения F в теории первого порядка есть вывод F из подмножества аксиом из .

Теоремы корректности и полноты выполняются для логик предикатов с функциональными символами и равенством и могут быть сформулированы в рамках теорий первого порядка следующим образом. В соответствие с теоремой корректности, если существует доказательство предложения F в теории первого порядка , тогда F является теоремой . В соответствие с теоремой полноты Гёделя, обратное также верно: для любой теоремы F теории первого порядка , существует доказательство F в .

Однако, добавление правил вывода для кванторов второго порядка ведёт к формальной системе которая корректна, но не полна.

Пример: Теория линейного порядка

Арифметика первого порядка

Мы будем упрощать запись формул сигнатуры арифметики первого порядка (6) введением следующего обозначения: a будет записываться как 0, s(t) как t' , f(t1, t2) как t1+t2, иg(t1, t2) как t1 · t2. Аксиомы арифметики первого порядка являются универсальным замыканием следующих формул:

1. x' 0.

2. x'= y' x = y.

3. (F(0) & v (F(v) F(v'))) v F(v) для любой формулы F(v).

4. x + 0 = x.

5. x + y'= (x + y)'.

6. x · 0 = 0.

7. x · y'= x · y + x.

^*

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

В следующих формулах 1 обозначает терм 0', 2 - 0'', и 4 - 0''''. Через t1 t2 мы обозначаем формулу v(t2 = t1 + v), где v - первая объектная переменная, которая не встречается вt1, t2.

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

3.34 2 4.

3.35 x' x.

3.36 x'= x + 1.

3.37 x x.

Нестандартные модели арифметики

Термы 0, 0', 0'', ... называются цифрами. Модель M арифметики первого порядка стандартна, если для каждого |M| существует цифра t такая, что t^M = .

3.38 Модель арифметики первого порядка (7) стандартна.

В соответствие с задачей 3.40, существуют модели арифметики первого порядка, которые не обладают этим свойством. Чтобы доказать существование такой модели, полезно рассмотреть следующую теорию первого порядка . Сигнатура получается из сигнатуры арифметики первого порядка добавлением буквы b в качестве новой объектной константы. Множество аксиом получается из множества аксиом арифметики первого порядка добавлением формул b 0, b 0', b 0'', ... в качестве новых аксиом.

3.39 непротиворечива.

3.40 Арифметика первого порядка имеет нестандартную модель.

Существование нестандартных моделей арифметики следует из теоремы Сколема (1920), который обобщил раннюю работу Леопольда Лёвенхейма (1915). Возможность таких моделей резко контрастирует с результатом задачи 1.41. Разница связана с тем, что язык арифметики первого порядка является слишком ограниченным для выражения аксиомы индукции. ``Арифметика второго порядка'', в которой схема индукции заменяется по аксиоме (8), не имеет нестандартных моделей.

Теорема неполноты Гёделя

Пусть M - нестандартная модель арифметики первого порядка. Может случится что M ``не отличима'' от модели (7) в том смысле, что для любой замкнутой формулы F арифметики первого порядка F истинно при M тогда и только тогда, когда F истинно при (7). Но некоторые нестандартные модели не обладают этим свойством: может существовать предложение F такое, что при M предложение F истинно, а при (7) ¬F истинно. Так как и M и интерпретация (7) являются моделями арифметики первого порядка, значит ни F, ни¬F не являются теоремами, а это означает, что арифметика первого порядка неполна. Этот факт, известный как теорема неполноты Гёделя, был доказан Куртом Гёделем в 1931 году.

Недоказуемые теоремы для диофантовых уравнений