Понятие доказуемости можно обобщить следующим образом. Возьмем некоторую совокупность формул (утверждений) Г, называемых посылками. Говорят, что формула 6 выводима из посылок Г, если существует конечная последовательность формул вида 6₂, , 6_П = 6, которая также заканчивается формулой 6, и каждый ее член является доказуемой формулой или одной из формул-посылок или выводится по правилу отделения из предыдущих членов этой последовательности. Доказуемые формулы называются теоремами данного исчисления.

Исчисление предикатов

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

В исчислении высказываний предложения интересовали нас лишь с точки зрения истинности или ложности без учета внутренней структуры самого предложения. Однако мы часто пользуемся в математике такими предложениями, которые не являются высказываниями. Например, предложение «х меньше у» не является высказыванием и потому не рассматривается в исчислении высказываний. Данное предложение будет высказыванием при условии, если указать, какие конкретно числа х, у имеются в виду. Полагая х = 2, у = 3 или х = 5, у = 4, мы получим предложения соответственно «2 меньше 3», «5 меньше 4», которые будут уже высказываниями. Можно сказать, что предложение «х меньше у» является неопределенным высказыванием и зависит от двух предметных переменных. Это предложение не является высказыванием, но становится таковым при каждом конкретном наборе значений указанных переменных. В этом случае говорят, что «х <Z у» является предикатом от переменных х, у (двухместным предикатом). Аналогично, предложения «х — простое число», «х у», «г = = х + у» не являются высказываниями и представляют собой соответственно одноместный, двухместный и трехместный предикаты, определенные, скажем, на множестве натуральных чисел.

Рассмотрим еще предложение «х — четное число». Оно также не является высказыванием, однако при подстановке вместо х конкретного натурального числа, будем получать каждый раз определенное высказывание. До подстановки конкретных значений данное предложение, можно сказать, 56

выражало неопределенное высказывание (предикат). После этих примеров дадим определение понятия предиката.

Предикатами (неопределенными высказываниями, высказывательными формами) называются функции

<Р (х), f (х, у), ,

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

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

Предикаты так же, как и высказывания, допускают операции конъюнкции или умножения (Д), дизъюнкции или сложения (\/), отрицания (—) и импликации (->).

Таким образом, с указанными выше переменными и операциями исчисления высказываний в исчислении предикатов вводятся дополнительно предметные и предикатные переменные х, у, г соответственно Р ( ), Q (,), R (,) и еще две следующие операции. Квантор общности (ух) для предиката Р (х) означает высказывание (ух)Р(х) «для каждого х предикат Р (х) принимает значение И». Квантор существования (gx) для предиката Р (х) означает высказывание (jx)P (х) «существует х такой, что предикат Р (х) принимает значение И».

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

При построении исчисления предикатов вводятся три рода переменных:

А)  предметные переменные х, у, г,

Значение этих переменных принадлежат полю D (или нескольким полям);

Б) переменные высказывания А, В, С, , X, У, Z.

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

В)  предикатные переменные Р ( ), Q (,), /?(,,),

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

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

2. Переменный предикат есть формула.

3. Если а, р формулы, то

a V 0, a A 0, a -> 0, a являются формулами.

4. Если a (x) формула, содержащая переменную х, то (yx)a (х), (jx)a (х) — также формулы.

5.  Никаких других формул не существует.

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

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

12.  (_Vx)P (X) Р (£/), 13. Р (у) -> (₇х)Р (х).

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

1. Правило отделения. Если а, а -> 0 — истинные формулы, то 0 — истинная формула.

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

Мы не даем здесь сводку всех правил подстановки и обращаем внимание лишь на идею их применения; правил введения кванторов совершенно не касаемся. Понятия теоремы и вывода переносятся и в исчисление предикатов.

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

Символические исчисления, математические структуры как формальные системы

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

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

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

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

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

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

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

В эквивалентных исчислениях базисные формулы будут, вообще говоря, различными.

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

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

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

Ниже приводится аксиоматика Цермело — Френкеля, в которой основными понятиями являются понятия «множества» и «содержит». Предположим, что нам даны два множества г/, z, и если любой элемент первого множества является элементом второго, то у называется подмножеством множества г (у включается в г). Затем вводится понятие собственного подмножества (если у включается в г и множество г содержит некоторый элемент, а множество у его не содержит, то у называется собственным подмножеством множества г).

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

Аксиомы теории множеств

1. Равные множества содержатся в одних и тех же множествах.

2. Если хну являются множествами, то неупорядоченная пара (х, у) является множеством.

3. Если х является множеством множеств, то совокупность элементов последних является множеством. (Полученное множество называется множеством — суммой.)

4. Совокупность всех подмножеств данного множества является множеством.

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

6. Если х есть множество непустых множеств, попарно не содержащие общих элементов, то его множество-сумма содержит по крайней мере одно подмножество, которое содержит в точности один общий элемент с каждым членом множества (аксиома выбора).

7. Существует множество, которое содержит в качестве своего элемента пустое множество и которое вместе с любым своим элементом х включает множество {х}.

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

9. Всякое непустое множество х содержит такой элемент у, что х и у не имеют общих элементов.

Аксиомами 1—9 исчерпывается аксиоматика Цермело — Френкеля теории множеств.

Исключительная роль в теории множеств принадлежит аксиоме 6, называемой также аксиомой выбора. Эта аксиома впервые была сформулирована Цермело и, подобно пятому постулату Евклида, вызвала появление большого количества статей.

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

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

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

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

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

Присоединяя к аксиомам 1—13 исчисления предикатов (с равенством) выписанные аксиомы 1—9 теории множеств,

мы получим систему аксиом формализованной теории множеств.

Более того, если к аксиомам 1—13 и 1—9 формализованной теории множеств мы присоединим аксиомы некоторой математической дисциплины, выраженные в терминах теории множеств, то получим аксиоматику рода структур соответствующих формализованных теорий.

Например, присоединяя к аксиомам 1—13 исчисления предикатов с равенством и аксиомам 1—9 теории множеств аксиомы А. Н. Колмогорова, мы получим аксиоматику рода структур евклидовой геометрии. Она содержит всего 13 аксиом исчисления предикатов (без аксиом равенства), 9 аксиом теории множеств, 12 аксиом школьной аксиоматики. Ясно, что понятия алфавита, формулы и истинной формулы должны быть уточнены. Соответствующим образом уточняются и правила вывода. Излагать уточнения и приводить доказательства теорем формализованной геометрии здесь мы не будем.

Формализованная теория, в которой кванторы общности и существования не берутся от предикатов, называется элементарной теорией.

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

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

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

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

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

Элементарная пеановская арифметика некатегорична и дедуктивно неполна.

Положение с евклидовой геометрией таково: доказывается, что аксиоматика обычной евклидовой геометрии (например, гильбертовская) категорична; определяемая ею теория неэлементарна.

Элементарная же евклидова геометрия с аксиомой (элементарной) непрерывности Тарского некатегорична, но дедуктивно полна (теорема Тарского — Швабхойзера). Вообще элементарные бесконечные структуры не являются категоричными (теорема Левенгейма — Сколе- ма — Тарского).

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

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

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

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

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

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