Понятие о формальных теориях

 

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

Всякая теория выступает как учение о бытии, онтология (греч. ontos – сущее + logos – учение); любая онтология есть теория. Отсюда следует вывод, что именно существует и каким образом, выясняется на основе теорий [40].

Многие сложнейшие логико-философские вопросы, так или иначе, приводят к проблеме существования. Что существует? Почему люди так часто пересматривают свое мнение относительно того, что именно действительно существует.

Лишь на первый взгляд вопрос о существовании кажется чрезвычайно простым: существует, мол, все то, что я вижу и слышу. Как у В. Маяковского: «…существует – и не в зуб ногой…». Увы, наука не сводится к очевидностям, более того, она постоянно лишает их ореола самодостаточности. Солнце кажется нам по своим размерам небольшим, а оно огромное. Из физики известно, что на Солнце происходят ядерные реакции, но знаем мы об этом в первую очередь благодаря не глазам, а теориям.

Онтологические аспекты, так же как и логические, являются одними из основных в науке об искусственном интеллекте [39].

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

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

Всякая теория определяется алфавитом, с помощью которого строится язык, на котором сформулированы выражения (формулы) [32]. Некоторый набор правил позволяет отличить выражение от произвольной последовательности символов. Задаются базисные выражения – аксиомы или постулаты, считающиеся истинными. Способ рассуждения или доказательства позволяет получать, исходя из аксиом, новые выражения.

В XIX в. сформировался такой раздел математики, как основания математики. В этом разделе математики искали ответ на вопрос: как должна быть построена теория, чтобы в ней не было противоречий, каковы должны быть методы доказательства?

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

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

Ранее мы уже говорили о дедукции, о дедуктивных умозаключениях. Кроме дедуктивных, рассматривались и правдоподобные рассуждения с использованием математического аппарата теории вероятности и математической статистики. Дедукция – теоретический метод познания, используется тогда, когда для получения нового знания недостаточно только практики (наблюдений, измерений, экспериментов) [5].

В зависимости от степени использования дедукции различают [15]:

1) Содержательные теории. В них знания представлены почти полностью на содержательном уровне, словесно (вербально). Дедукция практически не используется. Например, теория прибавочной стоимости, теория Дарвина.

2) Формализованные теории. В них дедукция используется частично. Знания частично формализованы и структурированы. Например, школьная арифметика, формальная логика, логика высказываний и логика предикатов. Среди формализованных теорий особо выделяются аксиоматизированные теории. Классический пример – геометрия Эвклида. Принимаются аксиомы, то есть истинные утверждения (положения) теории, а из них выводятся другие, которые считаются истинными. Если взять другие аксиомы – получается другая теория, например, геометрия Лобачевского.

3) Формальные теории. В них дедукция – основной метод. Структурируются не только знания, но и средства их получения. Такова формальная арифметика, разработанная итальянским математиком Дж. Пеано, теория групп и т.д. Среди формальных теорий выделяют теории, содержание которых представлено на специально созданном символическом языке и все заданные допустимые преобразования – это преобразования одних последовательностей символов в другие. Такие теории называют исчислениями. Мы рассмотрим исчисление высказываний и исчисление предикатов. Иногда применяют более широкое понятие – формальная система.

Формальные системы – системы операций над объектами, понимаемыми как последовательности символов, то есть, как слова в фиксированных алфавитах [19].Это знаковая система, создаваемая с использованием процесса образования всех синтаксически правильных символических выражений из букв алфавита системы – языка, то есть слов, формул и процесса вывода потенциально значимых (т.е. истинных) формул [15].

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

Большое значение в формальных системах имеют понятия перечислимости и разрешимости.

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

Говорят, что множество разрешимо, если имеется процедура, которая по любому объекту, дает ответ, принадлежит он этому множеству или нет.

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

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

Формальная система задаётся следующим образом [19]:

1) алфавитом;

2) процедурой получения множества формул или правильно построенных выражений на основе алфавита;

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

4) правилами вывода теории. Правила вывода описывают отношения выводимости на множестве формул.

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

Пусть Gвыводится из множества формул F₁, F₂,…,F_n.

Формула G называется непосредственно выводимой из формул F₁,F₂,…,F_n по правилу R.

или F₁,F₂,…,F_n├^R G.

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

Вывод формулы B из формул А₁,А₂,…,А_n – это последовательность формул F₁,F₂,…,F_m, где F_m=В, а любая F от F₁ до F_m-1 – либо аксиома, либо одна из исходных формул, либо непосредственно выводима из F₁,…,F_m-1 по какому либо правилу вывода, это обозначают так:

A₁,A₂,…,A_n├B.

Здесь A_i – гипотезы, В – вывод: «из A₁,A₂,…,A_n выводимо В». Такие выражения называют секвенциями.

Пишется ├B – выводимо В.

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

Пишется – общезначимо В.

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

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

Рассматриваются два основных типа доказательств:

1) доказательство по Гильберту – когда «много аксиом и мало правил вывода»;

2) доказательство по Генцену – когда «мало аксиом (всего одна: А®А) и много правил вывода».

В формальной теории существует два типа высказываний:

1) Высказывание самой теории – это теоремы.

2) Высказывание о теории – это свойства, которые формулируются на языке внешнем, по отношению к теории (метаязыке). Такие высказывания называются метатеоремы.

К формальным теориям предъявляют следующие требования:

· непротиворечивость, т.е. невозможность (├B)Ù(├ );

· минимальность, т.е. минимальность средств задания системы (1,2,3,4);

· адекватность: (├B)Þ(¿B), т.е., если В выводимо, то общезначимо, где Þ метасимвол «влечет», «выводится»;

· полнота: (¿B)Þ(├B), т.е., если В общезначимо, то выводимо.

Исчисление высказываний

 

Исчисление высказываний является простым примером формальной аксиоматической теории [19]. Порождение тождественно-истинных высказываний и является основной задачей исчисления высказываний.

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

1. Алфавит исчисления высказываний состоит из:

а) высказывательных переменных, которые будем обозначать прописными буквами X,Y,…,Z;

б) символов логических операций, из которых выберем импликацию ® и инверсию ¯ (можно показать, что такая система соответствующих логических функций является функционально полной);

в) скобок (,).

2. Формулы исчисления высказываний:

а) все переменные – формулы;

б) если А и В – формулы, то () и (А®В) тоже формулы.

Пример. Пусть А,В,С – формулы.

Тогда: (С®(А®В)), ((()®В)®()) – тоже формулы.

Для сокращения записи опустим в формуле внешние скобки и те пары скобок, которые относятся к инверсии:

С®(А®В), ( ®В)® .

3. Аксиомы исчисления высказываний.

Аксиомы должны обеспечивать порождение всех тождественно истинных высказываний.

Рассмотрим одну из возможных систем аксиом, содержащую всего три аксиомы.

А1. А®(В®А);

А2. (А®(В®С))®((А®В)®(А®С));

А3. ( ® )®(( ®А)®В).

По сути А1-А3 – схемы аксиом, поскольку они порождают бесконечное множество формул, учитывая правило подстановки.

4. Правила вывода.

1) Правило подстановки.

Если Х – выводимая формула, содержащая букву А (обозначим Х(А)), то выводима и формула Х(В), получающаяся из Х заменой всех вхождений А на произвольную формулу:

;

2) Правило заключения.

Это правило называют Modus Ponens или сокращенно m.p:

.

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

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

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

Проиллюстрируем вывод формулы исключенного третьего АÚ или А®А, т.е. докажем А├А для любой формулы А.

1. Возьмем аксиому А2 и подставим формулу А®А вместо В и формулу А вместо С, в соответствии с правилом подстановки:

Получим:

(А®((А®А)®А))®((А®(А®А))®(А®А)).

2. Подставим в А1(А®А) вместо В:

Получим:

А®((А®А)®А).

3. Обратим внимание, что это выражение является левой частью импликации, полученной после первого шага, то есть по правилу m.p:

,

получаем ((А®(А®А))®(А®А)), т.е. выражение под чертой.

4. Подставим теперь в А1 формулу А вместо В:

получим А®(А®А).

5. Обратим внимание, что это выражение также является левой частью выражения, полученного в результате третьего шага, то есть по правилу m.p:

,

получаем ├А®А,что и требовалось доказать. Поскольку вывод формулы был получен из аксиом А1-А2, то ¿(А®А), т.е. формула (А®А) общезначима.

Аналогично могут быть выведены другие тождества логики высказываний.

Более строго, в исчислении высказываний [19]:

1) всякая выводимая (из пустой системы гипотез) формула исчисления высказываний тождественно истинна;

2) если формула А исчисления высказываний является тождественно истинной, то она выводима.

Формальную аксиоматическую теорию называют непротиворечивой, если не существует формулы А такой, что одновременно выводимы А и .

В математической логике доказывается, что исчисление высказываний непротиворечиво.

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

Исчисление высказываний полно.

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

 

В логике предикатов, в отличие от логики высказываний, нет эффективного способа распознавания общезначимости формул. Поэтому аксиоматический метод становится главным [19, 26].

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

Аксиомы исчисления предикатов: в качестве трех первых берутся, например, аксиомы исчисления высказываний:

А1. А®(В®А);

А2. (А®(В®С))®((А®В)®(А®С));

Добавляются «собственные» аксиомы:

А4. "x_iA(x_i)®A(x_j), где формула A(x_i) не содержит переменной x_j.

А5. A(x_i)®$x_jA(x_j), где формула A(x_i) не содержит переменной x_j.

Как и ранее А1-А5 – тождественно истинные (общезначимые) формулы.

Действительно, А1-А3 тождественно истинны (метадоказательство мы приводили выше). А4: "x_iA(x_i)®A(x_j) – замкнутая формула и ее частный случай "x_iA(x_i)®A(x_i) при подстановке {(x_i,x_j)}, что тождественно истинно.

А5: A(x_i)®$x_jA(x_j) может быть представлена в виде = , где а – функция Сколема. Частный случай этой формулы тождественно истинен: .

Правила вывода.

1. Правило m.p: . Нами уже использовалось и доказывалось.

2. Правило связывания квантором общности:

,

где формула В не содержит переменной x_i. Воспользуемся «метадоказательством»: соответствующее множество дизъюнктов невыполнимо (а – функция Сколема).

3. Правило связывания квантором существования:

,

где формула В не содержит переменной x_i.

Метадоказательство: множество дизъюнктов также невыполнимо.

4. Правило переименования связанной переменной.

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

Докажем общезначимость формулы, описывающей правило перестановки разноименных кванторов [24]:

$x"yP(x,y)®"y$xP(x,y).

1. "yP(x,y)®P(x,z) – по аксиоме 4.

2. P(x,z)®$wP(w,z) – по аксиоме 5.

3. ¿(А®В,В®С)®(А®С) – цепное заключение, которое доказывалось в логике высказываний:

;

4. "yP(x,y)®$wP(w,z), где 3 применено к 1 и к 2.

5. $x"yP(x,y)®$wP(w,z) – по правилу вывода 3 из 4 – связывание квантором существования.

6. $x"yP(x,y)®"z$wP(w,z) – правило вывода 2 из 5 – связывание квантором общности.

7. $x"yP(x,y)®"y$wP(w,y) – правило вывода 4 из 6: переименование z в y.

8. $x"yP(x,y)®"y$xP(x,y) – правило вывода 4 из 7: переименование w в x.

Поскольку в качестве исходных формул использованы только аксиомы, то ¿[$x"yP(x,y)®"y$xP(x,y)].

 

Система натурного вывода

 

Система натурного вывода – это доказательство в смысле Генцена. Название «натурный» или «естественный» говорит о том, что такой тип рассуждений близок к человеческому (естественному) [32]. Правила вывода в этой формальной системе делятся на правила введения и правила исключения логических операций.

Рассмотрим основные правила введения (В):

1) введение конъюнкции: (ВÙ) , здесь Н – некоторое множество формул (гипотез); Þ – метасимвол «влечет», «выводится». Читается так: «Если из Н выводится А и из Н выводится В, то из Н выводится конъюнкция А,В»;

2) введение дизъюнкции: (ВÚ) , ;

3) введение импликации: (В®) ;

4) введение инверсии: (В¯) .

Рассмотрим основные правила исключения (И):

5) исключение конъюнкции: (ИÙ) , ;

6) исключение дизъюнкции: (ИÚ) ;

7) исключение импликации: (И®) ;

8) исключение инверсии: (И¯) .

Кроме того, необходимы еще так называемые базисные правила:

(Б1): ; (Б2): .

Первое базисное правило (Б1) означает, что всякий вывод, заключение которого совпадает с одной из гипотез (А) общезначим, то есть так как над чертой нет гипотез (пустое множество гипотез).

Второе базисное правило (Б2) означает, что добавление гипотезы (В) к множеству гипотез не изменяет выводимости.

Рассмотрим пример [32].

Пусть имеется множество формул Н:

{F,F®(PÚQ),P®C,Q®C}=H.

Докажем, что из этого множества выводится формула С.

1) [Н,F®(PÚQ)]Þ[F®(PÚQ)]]: правило Б1 – гипотеза [F®(PÚQ)] выводима;

2) НÞ[F®(PÚQ)]: объединение Н и F®(PÚQ)] это Н;

3) Н,FÞ(PÚQ)]: в соответствии с 2) и правилом исключения импликации (И®): консеквент импликации выводи́м;

4) НÞ(PÚQ): объединение Н и F – это Н: т.к. из F выводится (PÚQ), то и из H тоже выводится (PÚQ);

5) (Н,P®C)Þ(Р®C): правило Б1 – гипотеза (Р®C): выводима;

6) НÞ(Р®C): объединение Н и (Р®C) это Н;

7) Н,РÞC: в соответствии с 6) и правилом исключения импликации (И®): консеквент импликации выводи́м;

8) (Н,Q®C)Þ(Q®C): правило Б1 – гипотеза (Q®C): выводима;

9) НÞ(Q®C): объединение Н и (Q®C) это Н;

10) Н,QÞC: в соответствии с 9) и правилом исключения импликации (И®): консеквент импликации выводи́м;

11) НÞC: в соответствии с 4), 7), 10) и правилом исключения дизъюнкции (ИÚ). Таким образом, мы доказали правило «разбора случаев».