Металогика

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

Начала металогической проблематики отмечаются уже в античной философской мысли, в частности в «Аналитиках» Аристотеля (Ἀναλυτικὰ πρότερα, Ἀναλυτικὰ ὕστερα, 350-е годы до Новой эры), который пытался обосновать синтаксическими методами полноту своей силлогистики. Однако в качестве самостоятельного направления металогика стала активно развиваться в связи с построением разнообразных логических систем и их использованием в обосновании математики (в метаматематике).

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

Разделами металогики являются:

1. Логический синтаксис, в рамках которого изучаются [только] принципы построения логических исчислений и отношения между логическими выражениями (см. Синтактика).
2. Логическая семантика, в рамках которой изучаются отношения между логическими выражениями и объектами, обозначаемыми данными выражениями (см. Семантика).
3. Логическая прагматика, в рамках которой изучаются отношения между логическими выражениями, объектами, к которым относятся данные выражения, и их интерпретации, а также принципы формализации аспектов логического языка (см. Прагматика).

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

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

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

Другой важной парой понятий металогики являются понятия синтаксической и семантической полноты.

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

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

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

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

Ещё одним важным свойством логических теорий является свойство их разрешимости (см. Проблема разрешимости). Теория считается разрешимой, если существует некоторая алгоритмическая процедура, которая даёт ответ на вопрос, является некоторое утверждение теоремой теории или нет. Свойством разрешимости обладает классическое исчисление высказываний. В качестве разрешающей процедуры здесь применяется процедура построения таблиц истинности. Свойством разрешимости обладают и некоторые простые математические теории. Однако, как доказал А. Чёрч, уже классическое первопорядковое исчисление предикатов не является разрешимой теорией. Следует отметить ещё один важный ограничительный результат металогики, полученный А. Тарским. Для достаточно широкого класса теорий, в том числе логических, им была доказана метатеорема о неопределимости предиката «истина» логическими средствами, формализуемыми в данных теориях. Этот результат аналогичен результату К. Гёделя о недоказуемости утверждения о непротиворечивости формальной арифметики теми средствами, которые формализуются этой теорией. Ещё одним часто проверяемым свойством логических теорий является свойство независимости друг от друга их дедуктивных принципов. Значение этих исследований в металогике можно уяснить из аналогии с проверкой независимости пятого постулата в геометрии Евклида. Известно что, эти исследования привели к созданию неевклидовых геометрий. В общем случае построение доказательств является творческим процессом. Однако в последнее время в связи с исследованиями в области искусственного интеллекта в металогике возникла насущная задача доказательства метатеорем о нормализации выводов, устранимости особого правила — сечения — в секвенциальных исчислениях, алгоритмизации на этой основе процессов доказательств в различных логических системах и построения компьютерных реализаций этих алгоритмов для осуществления автоматического поиска теорем. В настоящее время построены весьма разнообразные и достаточно мощные компьютерные реализации алгоритмов автоматического поиска доказательств теорем.

Так как теории представляют собой классы предложений, над ними можно производить все операции, которые производятся и над множествами. Единственное условие состоит в том, что результатом этих операций должна быть опять теория. Так, например, пересечение двух теорий T₁ и T₂ всегда является теорией. Однако в общем случае объединение двух теорий T₁ и T₂ не обязательно является теорией. Тем не менее, Сn (T₁ и T₂) всегда есть теория, где Сn — операция замыкания относительно выводимости. Можно особым образом ввести и другие теоретико-множественные операции над теориями. А. Тарским было показано, что класс всех теорий, сформулированных на одном и том же языке на базе классической логики, образует брауэрову алгебру. С другой стороны, если ограничиться рассмотрением только конечно-аксиоматизируемых теорий, то класс всех таких теорий образует булеву алгебру.

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

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