Аксоматические теории
Мать и Матика
Если алгебра логики и дает образец логического мышления, то уж очень специфический. Строгие логические рассуждения и близко от такого образца не лежали. Создавать (абсолютно) строгие логические (то есть абсолютно логичные) системы позволяет дедуктивный подход. Не путать с "дедуктивным методом" Шерлока Холмса. У Холмса, или скорее у Конан-Дойля, явно были проблемы с логикой, коль скоро он путал дедукцию с индукцией.
ДЕДУКТИВНЫЙ подход, называемый еще АКСИОМАТИЧЕСКИМ, это подход от общего к частному. От аксиом (постулатов) к теоремам (следствиям). Аксиоматическая теория строго задана, если строго сформулирован (задан) язык теории, ее аксиомы и правила вывода. Стоит хотя бы в одной из этих трех составляющих "дать слабину" и строгой теории как не бывало!
Знаменитая (одна из первых) аксиоматическая теория - геометрия Эвклида худо-бедно обеспечила строгость только в одном компоненте - в постулатах. Но язык, на котором проводятся доказательства в геометрии даже через тысячелетия, как и строгость самих доказательств не выдерживают критики. Это не более чем неоднозначный метафорически-аллегорический язык и правдоподобные рассуждения. Потому-то нередки случаи, когда опровергаются "доказанные" теоремы. Собственно, почти вся математика за исключением сравнительно малюсенького раздела из логики аксиоматических систем покоится (лучше звучит - зиждется) на правдоподобных рассуждениях и порядочности доказывающих.
Так что образцовая безупречно строгая теория задается на языке предикатных формул. Мы здесь зареклись использовать формулы, поэтому остается полагаться на собственную честность.
Аксиомами объявляются некоторые из формул. В жизни мы также объявляем законами (аксиомами) не все фразы, которые можно ввернуть в той или иной ситуации, а лишь некоторые, которые мы решили считать таковыми. Законы (аксиомы) - это вопрос веры, а иногда целесообразности. Они недоказуемы! Если доказуемы, то это уже теоремы! Существование Бога недоказуемо! Иначе это была бы теорема. А из каких, простите, более первичных понятий такую "теорему" выводить прикажете?! Закон всемирного тяготения недоказуем. Мы просто ему поверили, поскольку надоело проводить эксперименты по падению тел в ожидании, когда с ними произойдет что-нибудь оригинальное.
Выводы в теории тоже следует формализовать, поскольку каждому в жизни встречались люди, которые "убедительно" доказывали какую-нибудь чушь. Кстати, самое знаменитое правило вывода в математической логике (modus ponens) удручает своей очевидностью и даже примитивностью. Проиллюстрировать его можно так: пусть в системе есть утверждения "ЕСЛИ хорошая погода, ТО мы гуляем" и "Хорошая погода", тогда в соответствии с modus ponens выводимо утверждение "Мы гуляем".
При всей своей примитивности это правило вывода имеет решающее достоинство. Оно очевидно для всех. Очевиднее не бывает! А если в системе есть еще и утверждение: "ЕСЛИ мы гуляем, ТО обязательно заблудимся", то с учетом ранее выведенного "Мы гуляем" получим "Обязательно заблудимся".
Видите, как далеко можно зайти маленькими очевидными шажками! Существует много и других правил вывода, но все имеют обязательное свойство - очевидность. Эта очевидность позволяет далее использовать эти правила абсолютно формально. То есть результат вычисляется. Такие символьные вычисления называются ИСЧИСЛЕНИЯМИ.
Есть еще один подход к аксиоматике, когда основной упор делается именно на правила вывода. Такие системы (почему-то) называются системами естественного вывода, намекая на то, что в них собраны базовые естественные правила логических рассуждений.
Логики резвились меж собой до тех пор, пока не был сформулирован подход к созданию аксиоматических систем под названием ПРИНЦИП (МЕТОД) РЕЗОЛЮЦИИ. Он очень способствовал продвижению логики в широкие народные массы.
С одной стороны активизировались работы по использованию компьютеров для реализации логического вывода и работы по искусственному интеллекту в частности. А с другой стороны на этой основе был создан язык ПРОЛОГ.
Это совсем другое программирование, нежели традиционное процедурное. Это даже не программирование в обычном смысле слова, коль скоро здесь программист не пишет алгоритм решения задачи. Он описывает логические зависимости "мира", в котором существует задача. На основе описанной логики "мира" система (машина) сама создает алгоритм в процессе поиска решения!
Это только кажется, что аксиоматические системы - это сложно. Любой может напридумать их сколько угодно. Более простым делом вам вряд ли приходилось заниматься. Например, в качестве языка можно объявить любые "слова" из последовательности буквы Я. Букву Я объявим аксиомой. Правило вывода будет удваивать букву Я. То есть сходу придумана теория, в которой выводимы любые последовательности (слова), состоящие из буквы Я.
Я ЯЯ ЯЯЯ ... ЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯЯ ...
И все бы хорошо, только такая строго заданная теория мало что дает создателю, кроме радости созидания. Поэтому встает вопрос целесообразности, смысла. Той самой семантики. Здесь логики заняли очень интересную позицию.
Коль скоро логика не интересуется смыслом высказываний, а лишь их истинностью, то истинность и объявили смыслом высказываний. Вдумайтесь, смысл высказывания, например, "Газ при нагревании расширяется" не в том, что это отражение физического закона, а в том что оно истинно. Следовательно, точно такой же смысл имеет высказывание "Никита Михалков - кинорежиссер". То есть его смысл в том, что оно тоже истинное.
Дальше - больше. Язык предикатов - это существенное расширение языка высказываний и обычным образом перебрать все случаи даже в простейшей ситуации вроде "Икс любит кашу" не всегда возможно. Тем более что речь может идти и о бесконечностях. Для решения проблем семантики в этом случае прибегают к теории моделей. Но это теория также в конечном итоге упирается в "смысл" типа истинно-ложно.
Возвращаясь к аксиоматическим теориям, следует сказать, что в математике "практический смысл" имеют лишь такие теории, в которых можно выводить только истинные формулы. И нельзя ложные. Одна ложная формула "уничтожает без остатка" любую аксиоматическую теорию.
Наша теория, созданная из буквы Я, не привязана к понятию истинности. Поэтому она бессмысленна, как бессистемная перестановка детских кубиков.
С кубиками все ясно. Но проблемы аксиоматических теорий на этом не исчерпываются. Пожалуй, самым фундаментальным открытием в этой сфере следует считать доказанную Геделем ТЕОРЕМУ О НЕПОЛНОТЕ. Оказывается, в сколько-нибудь сложной аксиоматической системе (посложнее, чем кубики, но достаточно даже арифметики) существуют формулы, которые нельзя ни доказать, ни опровергнуть. Может в этом причина, что не все школьные задачки имеют решения?! Так что создавая свои аксиоматические теории, помните, что они должны обладать какими-то полезными свойствами. А такие теории создавать уже не так-то просто. Хотя создать свою собственную математику может каждый! Известно высказывание одного крупного математика: "Преимущество аксиоматизации - это преимущество воровства перед честным трудом".
А.Е.Соловьев, soloviev.nevod.ru, 2001 год