4. Формальное уточнение понятий алгоритма и вычислимой функции.
5. Арифметизация и погружение в формальную теорию таких важных понятий метаматематики, как доказуемость, непротиворечивость и др., что позволило решать многие метаматематические проблемы математическими средствами.
Перечисленные достижения потребовали осознания и уточнения многих важных математических и метаматематических понятий таких, как язык, синтаксис и семантика математических теорий и др. Всё это позволило взглянуть на проблему оснований математики с новых позиций по сравнению с предшествующими временами. Чтобы судить о надежности такого фундамента, необходимо более подробно рассмотреть основные понятия.
4.1 Язык
В естественных языках синтаксис и семантика находятся в неразрывном единстве, что и образует собственно язык. В математике оказалось удобным под формальным языком понимать только его синтаксическую часть, в то время как семантика может варьироваться в зависимости от предметной области, круга задач и других условий. Говоря о языке математики, мы будем иметь в виду формальный язык, используемый в математических теориях, и в частности, в математической логике. Некоторые авторы называют языком часть алфавита, именуемую обычно в нашей литературе сигнатурой, которая представляет собой множество предикатных и функциональных символов. Однако, как правило термин “язык” используется в приводимом здесь смысле.
Если задан какой-либо алфавит, т.е. конечное или бесконечное множество букв, то всякая конечная цепочка букв этого алфавита называется словом в этом алфавите. (Формальным) языком в данном алфавите называется произвольное множество слов. Однако фактически в математике рассматриваются не произвольные языки, а полученные с помощью формальных (дедуктивных, аксиоматических или аксиоматизированных) систем (исчислений). Формальная система задаётся алфавитом, множеством исходных слов - аксиом и множеством правил вывода, которые из определённых слов - посылок порождают слово, называемое заключением. Таким образом, каждая формальная система определяет язык - множество всех слов, которые можно породить применением правил вывода к аксиомам и ранее порождённым словам (ср.п. 4.3). Содержательный смысл этого понятия в том, что формальный язык - это точно описанная синтаксическая компонента языка в обычном понимании. Следует заметить, что основной целью построения формальных систем является достижение максимальной объективности (т.е. независимости от субъективного восприятия) математических понятий, что получается благодаря использованию таких процессов построения математических объектов (понятий), которые могут быть осуществлены автоматически.
Основным языком современной математики считается так называемый язык предикатов Предикат (отношение, свойство) - функция (от п аргументов, п?0) на предметной области, принимающая два значения: «истина» и «ложь», которые обычно обозначаются буквами 1 и 0., алфавит которого обычно содержит символы предметных переменных и констант, предикатов и функций, логических операций, включая кванторы, а также вспомогательные символы, например, скобки, запятые и т.п. Язык предикатов, в котором допускаются кванторы только по предметным переменным, называется языком первой ступени или первого порядка. Если же кроме этого допускаются кванторы по предикатным и (или) функциональным переменным, то соответствующий язык называется языком второй ступени. Такую классификацию можно продолжить.
4.2 Формальная теория
Для определения формальной теории в каком-либо алфавите определяют обычно два (но может быть одно или больше двух) подмножества слов формального языка. Слова одного из них, называемые термами, интерпретируются как имена объектов предметной области и функций на ней, слова другого, называемые формулами, предложениями, высказываниями, играют роль утверждений о свойствах объектов (и предикатов - для языков второй и выше ступеней). Собственно формальной теорией называется множество формул, причем оно должно быть замкнуто относительно логических правил вывода (см.п.4.3 и 4.5). Обычно рассматриваются аксиоматические (или - аксиоматизированные) теории, т.е. являющиеся формальными исчислениями. Теория называется рекурсивно аксиоматизируемой, если она может быть определена как формальное исчисление с рекурсивным (разрешимым) множеством аксиом. В общем случае теория может быть задана любым другим способом, в том числе - с помощью семантики. При этом она может быть не только не разрешимой, но и не рекурсивно перечислимой (а потому и не рекурсивно аксиоматизируемой, поскольку всякая рекурсивно аксиоматизируемая теория рекурсивно перечислима).
Множество называется разрешимым, если существует единый способ, позволяющий относительно любого объекта определить, принадлежит он этому множеству, или нет. Формальным уточнением этого понятия является понятие рекурсивного множества - такого множества, для которого существует (формальный) алгоритм, разрешающий это множество, т.е. дающий для любого объекта ответ, принадлежит он этому множеству или не принадлежит. Согласно тезису Чёрча термины «разрешимое» и «рекурсивное» можно рассматривать как синонимы. Множество называется (рекурсивно-)перечислимым, если существует алгоритм, порождающий это множество, т.е. такой алгоритм, который последовательно выдаёт элементы данного множества (быть может с повторениями) и только их. Предполагается, что любой элемент множества рано или поздно будет получен. Очевидно, что всякое разрешимое множество перечислимо. Обратное неверно, поскольку можно привести примеры перечислимых, но не разрешимых множеств.
Теории, использующие язык предикатов первой (второй) ступени, называются теориями первой (второй) ступени. В некоторых случаях используются промежуточные языки, выходящие за рамки первой ступени, но не обладающие всеми возможностями языка второй ступени.
4.3 Доказательство
Если задано подмножество слов формального языка, называемых аксиомами, а также - правила вывода, каждое из которых представляет собой совокупность конечного множества слов, называемых посылками и одного слова, которое называется заключением, то доказательством или выводом в такой системе называется конечная последовательность слов, каждое из которых является либо аксиомой, либо заключением правила вывода, посылками которого являются некоторые слова из предшествующих данному слову в этой последовательности. Это общее понятие доказательства относится к любой формальной теории и в каждом конкретном случае является математическим объектом.
Для всякой рекурсивно аксиоматизированной теории множество доказательств разрешимо, т.е. существует эффективный формальный способ отличить доказательство от цепочки слов, не являющейся таковым. Это означает, что для таких теорий правильность доказательства всегда может быть эффективно проверена, и следовательно, гарантирована.
4.4 Интерпретация и модель
При содержательном построении теории слова её языка (термы, формулы и пр.) с самого начала обладают определенным значением (или смыслом), соответствующим семантике языка. Формальные же языки и теории, хотя и строятся в расчёте на какую-либо конкретную семантику, тем не менее, как чисто синтаксические объекты, нуждаются в специальном приписывании им подходящей семантики или интерпретации, которая словам языка присваивает определенные значения. Например, если алфавит теории содержит предикатные и функциональные символы, то всякая интерпретация должна присвоить им, соответственно, конкретные предикаты и функции на предметной области, принадлежащей данной интерпретации. Поскольку формулы интерпретируются как предложения (утверждения), то каждая интерпретация порождает свою логическую оценку формул (предложений) в языке теории. Для классической логики эта оценка двузначна и придаёт каждому предложению одно из двух значений - “истина” или “ложь”. Интерпретация, в которой все предложения теории истинны (т.е. имеют оценку “истина”) называется моделью Очень часто термин «модель» употребляется как синоним интерпретации, однако удобнее различать эти понятия. Более точное определение понятия модели использует сопоставление двух теорий (не обязательно формальных). Заметим, что модель может быть более формализованной, чем исходная теория, как это имеет место при построении математических моделей для естественнонаучных теорий. этой теории.
4.5 Логика
Всякая формальная теория должна содержать формальную логику, т.е. логические аксиомы и правила вывода, благодаря которым становится возможным рассматривать формальные доказательства в теории как экспликаты содержательных математических доказательств. Несмотря на то, что в реальной жизни и в некоторых содержательных теориях существуют не только истинные и ложные предложения (высказывания), но также - неопределённые, бессмысленные, модальные и т.п., математика всегда может обойтись только двузначной логикой, т.е. такой логикой, в которой каждое замкнутое предложение либо истинно, либо ложно. Надо сказать, что в 20-м веке широко изучались всевозможные многозначные логики (в основном - логики высказываний), однако они фактически являются математическим, а не логическим аппаратом, для самой же математики достаточно двузначной логики.
Понятие логической истины достаточно определенно сформулировал Лейбниц. Он назвал предложение логически истинным, если оно истинно во всех “мирах”, т.е. во всех интерпретациях. Именно такое понимание логики проводит чёткую границу между логическими и фактическими истинами, что необходимо для построения формальных теорий, и в частности, самой логики. Многовековой процесс построения логики привёл в ХХ веке к созданию современной математической логики, получившей название классической логики.
Основной логикой для построения математических теорий является классическая логика предикатов первой ступени (т.е. все предложения и правила вывода этой логики должны формулироваться в языке предикатов первой ступени). В силу самой конструкции её языка, класс всех её интерпретаций исчерпывается алгебраическими системами ([Мал], [МЭ]). В соответствии с лейбницевским понятием логики, её предложения должны быть истинными “во всех мирах”, т.е. во всех конкретных алгебраических системах в том же языке. Очень важным достоинством логики предикатов первой ступени является её семантическая полнота и непротиворечивость (см.п.4.6) в том смысле, что в ней доказуемы (ей принадлежат) все общезначимые, т.е. истинные во всех интерпретациях, предложения и только они, что собственно и отличает логику от других теорий (для прикладных теорий рассматиривается либо синтаксическая полнота, Теория называется синтаксически полной, если для всякого замкнутого предложения в языке этой теории доказуемо либо оно, либо его отрицание. либо полнота относительно каких-либо специальных семантик). Значение полной формальной логики для математики невозможно переоценить. Во-первых, понятие доказательства в любой формальной теории приобретает объективный характер, можно даже сказать, что формальное доказательство абсолютно, поскольку для любой рекурсивно аксиоматизированной теории и любой конечной цепочки формул существует эффективная процедура формальной, и следовательно, объективной проверки, является ли данная цепочка доказательством, или не является. Во-вторых, наличие формального доказательства (логического вывода) какого-либо предложения в непротиворечивой теории Т означает, что это предложение будет истинным в любой модели теории Т. Благодаря таким замечательным свойствам, логика предикатов первой ступени в настоящее время широко применяется во всей математике, несмотря на некоторую ограниченность её языка. Более широкая логика второй ступени применяется обычно с некоторыми ограничениями из опасения противоречий.
Несколько слов о языке логики. В основе языка совремённой математической логики лежат общие понятия предиката или отношения и, как частный случай его, - функции. Этот, на первый взгляд, бедный язык оказался достаточным для построения любых математических теорий. Тем не менее, вскоре после появления классической математической логики стали создаваться логики в языках, расширенных различными дополнительными операторами - модальными, временными, деонтическими и т.п. с общей тенденцией приблизить язык логики к естественному языку. Однако, если иметь в виду основной смысл логики как истинности во всех мыслимых мирах, то подобные расширения нельзя считать чистой логикой, поскольку такие понятия, как необходимость, возможность, долженствование, время и т.п. не присущи всем возможным мирам. Поэтому упомянутые расширения логики фактически являются не логиками, а прикладными логико-математическими теориями. В связи с этим возникает вопрос о возможности построения чистой логики в более широких языках, чем язык предикатов.
4.6 Непротиворечивость
Теория считается непротиворечивой, если она не содержит наряду с каким-либо предложением также и его отрицание. Для теорий с классической логикой это равносильно тому, что не всякое предложение принадлежит этой теории. Для теорий в достаточно широком языке утверждение о непротиворечивости теории может быть сформулировано на этом же языке. Поэтому можно пытаться доказывать непротиворечивость теории в ней самой. Однако ясно, что такое доказательство, если даже оно будет получено, не означает действительной непротиворечивости теории, поскольку в противоречивой теории всегда доказуема её непротиворечивость. Идея Гильберта не подчинена этому явлению, поскольку он предлагал строить доказательство непротиворечивости сильно ограниченными средствами, которые он называл финитными. По его замыслу такие средства должны гарантировать от проникновения в доказательство противоречий. Однако отрицательные теоремы Гёделя исключают эту возможность для таких основополагающих теорий, как арифметика или теория множеств.
Так называемые «отрицательные» Теоремы Гёделя (в усиленном Россером варианте) утверждают, что если формальная арифметика первого порядка непротиворечива, то она неполна и даже принципиально непополнима в том смысле, что в любом непротиворечивом рекурсивно аксиоматизируемом расширении арифметики существует неразрешимая замкнутая формула, т.е. недоказуемая формула, отрицание которой также недоказуемо (первая теорема Гёделя). Поскольку каждая замкнутая формула в интерпретации либо истинна, либо ложна, то это означает, что существует истинная арифметическая формула, не доказуемая в формальной арифметике. Вторая теорема утверждает, что при том же условии непротиворечивости в арифметике недоказуема формула, утверждающая непротиворечивость арифметики.