Введение в формальные системы

Раздел 4. Математическая логика и формальные системы.

Введение в формальные системы

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

Если предложить читателю упорядочить объекты 53, 109, 3, то, скорее всего, он без всяких дополнительных вопросов расположит их в порядке 3, 53,109. Иначе говоря, этой задаче будет дана обычная арифметическая интерпретация: последова­тельности цифр рассматриваются как изображение чисел в обычной десятичной системе, упорядочение этих последовательностей есть расположение изображаемых ими чисел по возрастанию, а правило сравнения таких изображений чисел известно настолько хорошо, что обычно о них никто не задумывается.

В действительности такое упорядочение не очевидно. Возможность неоднозначного извлечения задач из текста ограничений означает, что текст не содержит формального определения задачи. Для такого определения необходимо четко опи­сать класс объектов, для которых задача решается и явно ввести для них понятие упорядочения, описав его как систему локальных операций над символами, из ко­торых эти объекты состоят.

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

Сходные соображения по поводу того, что такое точное описание можно проследить на примере понятий “алгоритм”, “данные” и т.п. В определенном смысле проблему точного описания некоторого множества можно рассматривать, как проблему построения алгоритма, перечисляющего или порождающего это множество.

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

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

4.2. Принципы построения формальных теорий.

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

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

В математике с античных времен существовал образец систематического построения теории - геометрия Евклида, в которой все исходные предпосылки сформулированы явно, в виде аксиом, а теоремы выводятся из этих аксиом с помощью цепочек логических рассуждений, называемых доказательствами. Однако до середины 19 века математические теории, как правило, не считали нужным явно выделять действительно все исходные принципы. Критерии же строго доказательства и очевидности утверждений в математике в разные времена были различны и также явно не формулировались. Время от времени это приводило к необходимости пересмотра основ той или иной теории. Известно, например, что основания дифференциального и интегрального исчислений, разработанных в 18 - м веке Ньютоном и Лейбницем, в 19 веке подверглись серьезному пересмотру; математический анализ в его современном виде опирается на работы Коши, Больцано, Вейерштрасса по теории пределов. В конце 19 века такой пересмотр затронул общие принципы организации математических теорий

Это привело к созданию новой отрасли математики – оснований математики, предметом которой стало как раз построение математических теорий и утвержде­ний и которая поставила своей целью ответить на вопросы типа: “как должна быть построена теорема, чтобы в ней не возникало противоречий?”, “какими свой­ствами должны обладать методы доказательств, чтобы считаться достаточно стро­гими?”.

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

Более конкретно формальная теория (или исчисление) строится следующим обра­зом:

1. Определяется множество формул или правильно построенных выра­жений, которые образуют язык теории. Это множество задаётся конструк­тивными средствами (как правило, индуктивным определением). Данное множество перечислимо и часто разрешимо.