Формальные системы.Исчисление предикатов

1. Формальные системы

 

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

Если предложить читателю упорядочить объекты 53, 109, 3, то, скорее всего, он без всяких дополнительных вопросов расположит их в порядке 3, 53, 109. Иначе говоря, этой задаче будет дана обычная арифметическая интерпретация: последовательности цифр рассматриваются как изображения чисел в десятичной системе, упорядочение этих последовательностей есть расположение изображаемых ими чисел по возрастанию, а правила сравнения таких изображений чисел известны настолько хорошо, что обычно о них никто не задумывается. В действительности же такое истолкование задачи, вообще говоря, не вытекает из текста «упорядочить объекты 53, 109, 3»; его можно понимать как задачу лексико-графического упорядочения (что приведет к результату 109, 3, 53), как задачу распределения бегунов с номерами 53, 109, 3 по дорожкам (решение которой зависит от процедуры распределения и заведомо не связано с числовой интерпретацией объектов) и т. д. Возможность неоднозначного извлечения задач из текста означает, что этот текст не содержит формального определения задачи. Для такого определения нужно четко описать класс объектов, для которых задача решается, и явно ввести для них понятие упорядочения, описав его как систему локальных операций над символами, из которых эти объекты состоят.

По существу при таком  понимании «формальное описание» задачи означает ее точное, явное описание — все, что существенно для решения задачи, выписано явно. Поэтому уточнение задачи принято называть ее формализацией.

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

Индуктивное определение  формулы — простой пример описания перечислимого множества, в котором  использованы все существенные составные части понятия «алгоритм», кроме одного — детерминированности. Отбрасывая несущественный здесь порядок перечисления элементов множества, мы выигрываем в компактности описания, которое при этом не становится менее точным. Такое описание, не являюсь алгоритмом, представляет собой формальную систему, Однозначно описывающую множество формул.

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

2. Формальные теории (логические исчисления)

 

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

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

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

Каким образом теория получает свои теоремы?

В математике с античных времен существовал образец систематического построения теории — геометрия Евклида, в которой все исходные предпосылки сформулированы явно, в виде аксиом, а теоремы выводятся из этих аксиом с помощью цепочек логических рассуждений, называемых доказательствами. Однако до середины XIX в. математические теории, как правило, не считали нужным явно выделять действительно все исходные принципы; критерии же строгости доказательств и очевидности утверждений в математике в разные времена были различны и также явно не формулировались. Время от времени это приводило к необходимости пересмотра основ той или иной теории. Известно, например, что основания дифференциального и интегрального исчислений, разработанных в XVIII в. Ньютоном и Лейбницем, в XIX в. подверглись серьезному пересмотру; математический анализ в его современном виде опирается на работы Коши, Больцано, Вейерштрасса по теории пределов. В конце XIX в. такой пересмотр затронул общие принципы организации математических теорий. Это привело к созданию новой отрасли математики — оснований математики, предметом которой стало как раз строение математических утверждений и теорий и которая поставила своей целью ответить на вопросы типа: «как должна быть построена теория, чтобы в ней не возникало противоречий?», «какими свойствами должны обладать методы доказательств, чтобы считаться достаточно строгими?» и т. д. Одной из фундаментальных идей, на которые опираются исследования по основаниям математики, является идея формализации теорий, т, е. последовательного проведения аксиоматического метода построения теорий. При этом не допускается пользоваться какими-либо предположениями об объектах теории, кроме тех, которые выражены явно в виде аксиом; аксиомы рассматриваются как формальные последователь* ности символов( выражения), а методы доказательств — как методы получения одних выражений из других с помощью операций над символами. Такой подход гарантирует четкость исходных утверждений и однозначность выводов, однако может создаться впечатление, что осмысленность и истинность в формализованной теории не играют никакой роли. Внешне это так; однако в действительности и аксиомы, и правила вывода стремятся выбирать таким образом, чтобы построенной с их помощью формальной теории можно было придать содержательный смысл.

Формальная система определена, если:

1. Задан конечный алфавит (конечное множество символов).
2. Определена процедура построения формул (или слов) формальной системы.
3. Выделено некоторое множество формул, называемых аксиомами.

   4.      Задано конечное множество правил вывода. которые позволяют получать из некоторого конечного множества формул другое множество формул. Эти правила могут быть представлены в виде  

U₁ и U₂ и ... U_p→W₁ и W₂ и ... W_n,

Где U_i и W_i — формулы формальной системы, а стрелка → читается как “влечет” или “следует”.

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

Формальное доказательство (или просто доказательство) определяется как конечная последовательность формул M₁, M₂,…, M_r такая, что каждая формула Mi либо является аксиомой, либо при помощи одного из правил вывода выводима из предшествующих ей формул М_j, где j< i.

Формула t называется теоремой, если существует доказательство, в котором она является последней, т. е. М_r≡t. В частности, всякая аксиома является теоремой. Если t есть теорема, то этот факт кратко обозначается так: Hi

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

{теоремы}  {формулы} {цепочки символов  из алфавита}

включение множеств является строгим.

Различают два типа правил вывода: 1) правила, применяемые к формулам, рассматриваемым как единое целое (в этом случае их называют продукциями, правилами продукций или продукционными правилами); 2) правила, которые могут применяться к любой отдельной части формулы, причем сами эти части являются формулами, входящими в формальную систему. В этом случае говорят о правилах переписывания. Так, в обычной математике следующее правило вывода:

х < у и у < z влечет х < z

применяется к формуле как к  целому (в данном случае к предложению математического анализа) — это продукция (с двумя антецедентами, или посылками). Слово ^uвлечет” для краткости при использовании продукции часто заменяется стрелкой →. В отличие от предыдущего правило х — х О имеет смысл при любом виде входящего в него в качестве подвыражения х. Оно является правилом переписывания, и в этом случае для обозначения слова “влечет” используется специальная стрелка

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

При изучении формальных теорий мы имеем дело с двумя типами высказываний: во-первых, с высказываниями самой теории (теоремами), которые рассматриваются как чисто формальные объекты, определенные ранее, а во-вторых, с высказываниями о теории (о свойствах ее теорем, доказательств и т.д.), которые формулируются на языке, внешнем по отношению к теории, — метаязыке и называются метатеоремами. Различие между теоремами и метатеоремами не всегда будет проводиться явно, но его обязательно надо иметь в виду.

 

3. Основы логики предикатов первого порядка

 

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

В связи с этим возникает  необходимость в расширении логики высказываний, в построении такой логической системы, средствами которой можно было бы исследовать структуру высказываний. Такой логической системой является логика предикатов (лат. praedicatum - заявленное, упомянутое, сказанное).

Логика предикатов расчленяет высказывание на объект (подлежащее) и  предикат (сказуемое). Объект - это то, о чем что-то утверждается в высказывании; предикат - это то, что утверждается об объекте.

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

С помощью логических связок (и скобок) предикаты могут объединяться в разнообразные логические формулы - предикатные формулы. Исследование предикатных формул и способов установления их истинности является основным предметом логики предикатов. Логика предикатов вместе с входящей в нее логикой высказываний является основой логического языка математики. С ее помощью удается формализовать и точно исследовать основные методы построения математических теорий. Логика предикатов является важным средством построения развитых логических языков и формальных систем (формальных теорий). 
      Логика предикатов, как и логика высказываний, может быть построена в виде алгебры логики предикатов и исчисления предикатов. Здесь, как и в случае логики высказываний, для знакомства с основными понятиями логики предикатов воспользуемся языком алгебры, а не исчислений. Такой выбор обусловлен рядом причин: 
 
• Исследование предикатных формул алгебры логики, выполнение их преобразований значительно проще, чем в исчислении предикатов. 
 
• Ограничения в использовании аппарата алгебры обусловлены тем, что предметные области (множества, на которых определены предметные переменные предикатов) теоретически могут быть и бесконечными. В таких случаях стандартный метод проверки истинности предикатов и формул в целом, требующий подстановки всех возможных значений предметных переменных, не может быть осуществлен в строгом смысле (точнее, процедура вычисления истинности может быть бесконечной и не дать ответа за конечное время). Однако в практических ситуациях при описании реальных систем, процессов, явлений в качестве предметных областей, как правило, используются конечные множества. Поэтому проблема бесконечности в значительной степени теряет свою актуальность.

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

Например, в высказывании «7 - простое число», «7» - объект, «простое число» - предикат. Это высказывание утверждает, что «7» обладает свойством  «быть простым числом». Если в  рассмотренном примере заменить конкретное число 7 переменной X из множества  натуральных чисел, то получим выражение  «X - простое число». При одних  значениях X (например, 13 или 17) это выражение  истинно, при других (например, 10 или 18) - ложно. Из примера видно, что выражение  «X - простое число» определяет логическую функцию одной переменной X, определенную на множестве натуральных чисел  и принимающую значения из множества {истина, ложь}. Данная функция в виде предиката может быть записана как простое число(X).

Аналогичным образом можно  определить логическую функцию нескольких переменных предикат(X, Y, Z, ...), которая  при одних сочетаниях переменных будет истинна, а при других - ложна. Такую функцию называют n - местным предикатом. Множество всех сочетаний переменных, при которых предикат принимает значение «истина», называется множеством истинности предиката.

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

 

4.Синтаксис логики предикатов первого порядка

 

 

 Синтаксис логики предикатов первого порядка:

- логические константы  – истина (И, TRUE, T,1) и ложь (Л, FALSE, F,0);

- символы констант –  символьные выражения, начинающиеся  со строчной буквы (например, cat, blue);

- символы переменных –  символьные выражения, начинающиеся  с прописной буквы или знака  подчеркивания (например, X, Сat, _blue);

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